The field structure on the locale of real numbers

Question

It is well known how to derive the field operations from the construction of the real numbers as the Dedekind completion of the rational numbers and as the Cauchy completion of the rational numbers; see section 11.2.1 and 11.3.3 of this textbook for an explicit definition of real numbers as a Dedekind completion or Cauchy completion. However, in constructive mathematics, none of the above definitions of the real numbers behave well, as many theorems in classical mathematics fail, such as the Heine-Borel theorem and the fundamental theorem of algebra.

Instead, one has to use the locale of real numbers, defined as the localic completion of the rational numbers. A locale $A$ is a frame $\mathcal{O}(A)$ whose elements are regarded as "opens"; a frame is a partially ordered set with finitary meets and infinitary joins where meets distribute over all joins, and a continuous function between two locales $f:A \to B$ is a frame homomorphism $f^*:\mathcal{O}(B) \to \mathcal{O}(A)$, a function which preserves the frame structure.

Now let $\mathbb{R}$ be the symbol denoting the locale of real numbers. There is a function $B:\mathbb{Q} \times \mathbb{Q}^+ \to \mathcal{O}(\mathbb{R})$ to the frame of opens of the locale of real numbers, with the weak and strict orders defined as

• $B(x,\delta)\le B(y,\epsilon)$ if $\vert y - x \vert + \delta \le \epsilon$
• $B(x,\delta)\lt B(y,\epsilon)$ if $\vert y - x \vert + \delta \lt \epsilon$

respectively for $x, y \in \mathbb{Q}$ and $d, e \in \mathbb{Q}^+$.

The localic completion of the rational numbers is the locale presented by the following generators and constructors

1. If $\vert y - x \vert + \delta \le \epsilon$ then $B(x,\delta)\le B(y,\epsilon)$
2. $\top = \bigvee_{x\in \mathbb{Q}} B(x,\epsilon)$ for any $\epsilon$
3. $B(x,\delta)\cap B(y,\epsilon) = \bigvee \{ B(z,\eta) \mid B(z,\eta) \le B(x,\delta) \, \text{and} \, B(z,\eta) \le B(y,\epsilon) \}$
4. $B(x,\delta) = \bigvee \{ B(y,\epsilon) \mid B(y,\epsilon) \lt B(x,\delta) \}$

However, I wasn't able to find anything on how the field operations are explicitly derived from the construction of the locale of real numbers, as most of the literature I looked at either focused solely on the topological properties of the locale of real numbers such as local compactness, or is about locale theory more generally. The fact that one is able to talk about the fundamental theorem of algebra and Jordan's theorem in the locale of real numbers imply that the field operations are well-defined on the locale of real numbers. How would one go about explicitly defining the field operations on the locale of real numbers?

Answer 1

There are several (equivalent) way to go about it:

You can start form the fields operation on $\mathbb{Q}$ and use that they are "locally uniformly continuous" to extend them by continuity to the localic completion (for the inverse map, you'll have to stay away of $0$ of course).

Regarding the existence of such continuous extention: I don't remember the literature on constructive localic completion very well (I haven't worked on that topic in almost 10 years). You can look at this paper of mine where I do it for maps satisfying $d(f(x),f(y)) \leqslant d(x,y)$ (see sections 3.3, 3.4 and 3.6), which isn't quite what you need but should be enough given that you can restrict to a ball and replace the distance function by a multiple of it to arrive at something that satisfies this condition. But I'm sure there are more appropriate references available. (I'll see if I can remember something)

Alternatively, you can use the fact that these operations are well defined on Dedekind real numbers constructively and the methods explained here allow you to turn these into maps between the corresponding locales (using the fact that these constructions are geometric and the Yoneda lemma).

Here again, to talk about inverse you have to restrict to Dedekind real that are $>0$ or $< 0$ which in terms of classifying locales corresponds to the open subspace $\mathbb{R} - \{0\}$

Answer 2

In constructive mathematics its common to use formal topologies rather than locales, so you might have more luck searching the literature for "formal topology" rather than "locale." You can think of formal topologies as "set presented" versions of locales that are better behaved in predicative settings where we might not have power sets.

There is some analysis for the formal reals in Negri & Soravia, The continuum as a formal space. I'm not sure if that's what you're looking for, but they define the field operations as continuous functions on the points of the formal topology, so the same reasoning should define operations on the points of the locale you gave.

Answer 3

Richard Dedekind's original paper does not include a construction of multiplication.

In The Dedekind Reals in Abstract Stone Duality, Andrej Bauer and I go into considerable detail about all of the topological and arithmetical aspects of the construction.

We introduce Dedekind cuts as the limiting case of intervals (or, conversely, intervals as generalised cuts) and even consider back-to-front intervals.

In particular, multiplication is introduced in this most general form (due to Edgar Kaucher). Since this is possibly rather confusing, you may prefer to read the version without it.

The actual construction of the real number object in ASD in this paper uses the clunky original technology of the subject. However, I am developing a new one that is much easier to use, given by axiomatising the inclusion of compact subsets in open ones. This can also be used in Locale Theory and Formal Topology.

Unconnected with this is John Conway's construction of multiplication for his number system in On Numbers and Games. This was adopted by Peter Johnstone in his first book Topos Theory, which appeared in the same series as Conway's.