Back to Search
Start Over
POINT-FREE CONSTRUCTION OF REAL EXPONENTIATION.
- Source :
- Logical Methods in Computer Science (LMCS); 2022, Vol. 18 Issue 3, p1-32, 32p
- Publication Year :
- 2022
-
Abstract
- We define a point-free construction of real exponentiation and logarithms, i.e. we construct the maps exp: (0, ∞) × R →(0, ∞), (x, ζ) 7→ x<superscript> ζ</superscript> and log: (1, ∞) × (0, ∞) → R, (b, y) 7→ log<subscript>b</subscript> (y), and we develop familiar algebraic rules for them. The point-free approach is constructive, and defines the points of a space as models of a geometric theory, rather than as elements of a set — in particular, this allows geometric constructions to be applied to points living in toposes other than Set. Our geometric development includes new lifting and gluing techniques in point-free topology, which highlight how properties of Q determine properties of real exponentiation. This work is motivated by our broader research programme of developing a version of adelic geometry via topos theory. In particular, we wish to construct the classifying topos of places of Q, which will provide a geometric perspective into the subtle relationship between R and Q<subscript>p</subscript>, a question of longstanding number-theoretic interest. [ABSTRACT FROM AUTHOR]
- Subjects :
- EXPONENTIATION
GEOMETRICAL constructions
GEOMETRIC modeling
MODEL theory
Subjects
Details
- Language :
- English
- ISSN :
- 18605974
- Volume :
- 18
- Issue :
- 3
- Database :
- Complementary Index
- Journal :
- Logical Methods in Computer Science (LMCS)
- Publication Type :
- Academic Journal
- Accession number :
- 159984373
- Full Text :
- https://doi.org/10.46298/LMCS-18(3:15)2022