Point-free Construction of Real Exponentiation

MaRDI QIDQ6364292arXivFDO

Authors Ming Ho Ng, Steven Vickers

Publication date 31 March 2021

Published in arXiv

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

arXiv classification

math.CT

Abstract: We define a point-free construction of real exponentiation and logarithms, i.e. we construct the maps

e x p c o l o n (0, i n f t y) i m e s m a t h b b R i g h t a r r o w! (0, i n f t y),, (x, z e t a) m a p s t o x^{z} e t a

and

l o g c o l o n (1, i n f t y) i m e s (0, i n f t y) i g h t a r r o w m a t h b b R,, (b, y) m a p s t o l o g_{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

m a t h b b 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

m a t h b b Q

, which will provide a geometric perspective into the subtle relationship between

m a t h b b R

and

m a t h b b Q_{p}

, a question of longstanding number-theoretic interest.

This page was built for publication: Point-free Construction of Real Exponentiation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6364292)