Ming Ng ; Steven Vickers - Point-free Construction of Real Exponentiation

lmcs:7325 - Logical Methods in Computer Science, August 2, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:15)2022
Point-free Construction of Real ExponentiationArticle

Authors: Ming Ng ; Steven Vickers

    We define a point-free construction of real exponentiation and logarithms, i.e.\ we construct the maps exp:(0,)×R(0,),(x,ζ)xζ and log:(1,)×(0,)R,(b,y)logb(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 Qp, a question of longstanding number-theoretic interest.


    Volume: Volume 18, Issue 3
    Published on: August 2, 2022
    Accepted on: May 13, 2022
    Submitted on: April 5, 2021
    Keywords: Mathematics - Category Theory,26E40, 18F10, 18F40

    Consultation statistics

    This page has been seen 2646 times.
    This article's PDF has been downloaded 651 times.