Point-free Construction of Real Exponentiation

Abstract

We define a point-free construction of real exponentiation and logarithms, i.e.\ we construct the maps $\exp :(0,\infty )\times \mathbb{R}\to (0,\infty ),(x,\zeta )\mapsto x^{\zeta }$ and $\log :(1,\infty )\times (0,\infty )\to \mathbb{R},(b,y)\mapsto {\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 $\mathbb{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 $\mathbb{Q}$, which will provide a geometric perspective into the subtle relationship between $\mathbb{R}$ and ${\mathbb{Q}}_p$, a question of longstanding number-theoretic interest.

References in corpus (2)

• Arithmetic universes and classifying toposes
• Generalized point-free spaces, pointwise