Point-free Construction of Positive Real Exponentiation
Date:
Talk at CCC 2020: Continuity, Computability, Constructivity. Slides available here.
Abstract: There are two questions that any mathematician interested (and invested) in the importance of constructive mathematics ought to consider: 1) Given that there are many different flavours of constructive mathematics, what are the advantages of one particular “school” of constructive mathematics over another? 2) To what extent does probing constructivist issues in “classical” mathematics result in mathematical payoffs that have significance beyond the realm of constructivist mathematics?
Both questions will inform the content of this talk, which will be divided into three main sections. In the first section, we introduce the idea of point-free mathematics, and illustrate some of its attractive features from a constructive point of view, along with its connections with topos theory. In the second section, we report on some recent results regarding a point-free construction of positive real exponentiation of the Dedekind reals. In particular, this construction highlights the importance of the order relation on Q in determining many well-known properties of the Dedekind reals, as well as the use of specific gluing techniques in order to justify various forms of case-splitting. In the third section, we motivate our interest in this construction by introducing our broader research programme of developing a version of adelic geometry via topos theory. In particular, we are interested in using the machinery of classifying toposes to engage with Hasse Local-Global problems in number theory, and we explain how the geometric construction of positive real exponentiation is a crucial step towards realising this goal. All this is joint work with Steve Vickers.