POINT-FREE CONSTRUCTION OF REAL EXPONENTIATION.

We define a point-free construction of real exponentiation and logarithms, i.e. we construct the maps exp: (0, ∞) × R →(0, ∞), (x, ζ) 7→ x ^ζ and log: (1, ∞) × (0, ∞) → R, (b, y) 7→ log_b (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_p, a question of longstanding number-theoretic interest. [ABSTRACT FROM AUTHOR]