nLab locale of real numbers

The locale of real numbers

The locale of real numbers

Summary

This page gives an elementary description of the locale of real numbers, that is the localic real line. The development is manifestly constructive and even predicative over the natural numbers (although we are somewhat careless with the language and do not always point out when a set may predicatively be a proper class). Ideally, we will show that our construction satisfies the seven ‘headline properties’ of the real line described by Bauer & Taylor (although so far we cover only the Heine–Borel theorem).

The exposition here is pretty much my own work, although of course the basic ideas are well known to many. In particular, the technical zigzag lemma is mine (but it is not a very deep result!).

Idea

To describe the locale of the real numbers, we need first of all to describe what an open in the real line is. The key insight is that an open set is determined by the open intervals of rational numbers that it contains. This is analogous to the key insight of Richard Dedekind's definition of real number: that a point in the real line is determined by which open intervals of rational numbers that it belongs to. (Once you're talking about rational numbers, things are manageable.)

Opens

An open in the real line is a binary relation {\sim} on the rational numbers that satisfies the four properties listed below. Intuitively, we have aba \sim b iff the open interval (a,b)(a,b) is contained in the corresponding open set.

  1. If aba \geq b, then aba \sim b.
  2. If abcda \geq b \sim c \geq d, then ada \sim d.
  3. If ab>cda \sim b \gt c \sim d, then ada \sim d.
  4. If bcb \sim c whenever a<ba \lt b and c<dc \lt d, then ada \sim d.

If we suggestively formally write (a,b)U (a, b) \subseteq U_\sim for aba \sim b, and (a,b)(c,d)(a, b) \subseteq (c, d) for cac \leq a and bdb \leq d, then these say

  1. If aba \geq b, then (a,b)U (a, b) \subseteq U_\sim.
  2. If (a,d)(b,c)(a, d) \subseteq (b, c) and (b,c)U (b, c) \subseteq U_\sim, then (a,d)U (a, d) \subseteq U_\sim.
  3. If c<bc \lt b and (a,b),(c,d)U (a, b), (c, d) \subseteq U_\sim, then (a,d)U (a, d) \subseteq U_\sim.
  4. If (b,c)U (b, c) \subseteq U_\sim for all (b,c)(a,d)(b, c) \subsetneq (a, d), then (a,d)U (a, d) \subseteq U_\sim.

Property (1) is motivated because (a,b)(a,b) is empty whenever aba \geq b. Property (2) is motivated because inclusion is transitive. Property (3) is motivated because if c<bc \lt b, then (a,d)=(a,b)(c,d)(a, d) = (a, b) \cup (c, d). Property (4) is motivated because (b,c)(a,d)(b,c)=(a,d)\bigcup_{(b, c) \subsetneq (a, d)} (b, c) = (a, d).

The really interesting property is property (3). It in fact generalises as follows:

  • If
    (1)a 1b 1>a 2b 2>>a nb n, a_1 \sim b_1 \gt a_2 \sim b_2 \gt \cdots \gt a_n \sim b_n ,

    then a 1b na_1 \sim b_n.

We call the combined hypothesis of this property a zigzag; each hypothesis a ib ia_i \sim b_i is a zig, and each hypothesis b i>a i +b_i \gt a_{i^+} is a zag. To indicate the length of a zigzag, we will count the zigs; the zigzag (1) has nn zigs (and n1n - 1 zags). A typical nondegenerate zigzag with 33 zigs is shown below; it consists of 33 overlapping open intervals, each of which belongs to a given open set; we are motivated to conclude that the entire interval from a 1a_1 to b 3b_3 belongs to that open set.

Layer 1 a 1 a 2 b 1 a 3 b 2 b 3 a_1\qquad a_2\longleftarrow\; b_1\qquad a_3\longleftarrow\; b_2\qquad b_3 ~ ~ ~ ~ ~ ~
category: svg

Thus the zigzag property for n=2n = 2 is property (3), the zigzag property for n=1n = 1 is trivial (if aba \sim b, then aba \sim b), and the zigzag property for n>2n \gt 2 may be proved by induction. (There is also a sense in which the zigzag property for n=0n = 0 is property (1), but I haven't quite got my head around that. It would be awesome if the zigzag property for n=n = \infty could be interepreted as property (4), but that seems unlikely so far.)

If GG is an open in the real line, then we write (a,b)G(a,b) \subseteq G to mean that aa is related to bb through GG and say that GG contains the interval from aa to bb.

The zigzag lemma

We will often have occasion to consider a zigzag as in (1), but where the various zigs are taken relative to different opens. Nevertheless, we will usually want to say something about the relationship of a 1a_1 to b nb_n, and it will often be convenient to assume, for all ii, that a 1a ia_1 \leq a_i and b ib nb_i \leq b_n. We may do so without loss of generality as follows: consider the smallest value of ii such that b ib nb_i \geq b_n, truncate the zigzag so that it now has only ii zigs, and change the new endpoint b ib_i to the old endpoint b nb_n. The final zig (a i,b i)G i(a_i,b_i) \subseteq G_i becomes (a i,b n)G i(a_i,b_n) \subseteq G_i, which will hold by property (2) since b ib nb_i \geq b_n. Now consider the largest value of jij \leq i such that a 1a ja_1 \geq a_j, and truncate similarly on the other side. We now have a zigzag with ij+1i - j + 1 zigs that never falls below a 1a_1 on a zag nor rises above b nb_n on a zig.

To be precise:

Zigzag lemma

Given a collection 𝒞\mathcal{C} of opens and a zigzag in which each zig holds relative to some open in 𝒞\mathcal{C}, there exists a zigzag (1) in which each zig holds relative to some open in 𝒞\mathcal{C}, a 1a ia_1 \leq a_i for each ii, and b ib nb_i \leq b_n for each ii.

(Since each b i>a i +b_i \gt a_{i^+}, it follows further that a i<b na_i \lt b_n for each i>1i \gt 1 and a 1<b ia_1 \lt b_i for each i<ni \lt n, although this corollary doesn't seem to be particularly useful.)

At the moment, this lemma is used only in the proof of the infinite distributivity law.

The frame of opens

The opens form a sub-poset of the power set 𝒫(×)\mathcal{P}(\mathbb{Q} \times \mathbb{Q}). This poset is in fact a frame, as we will now show. (It is not a subframe of the power set, since the joins are different. It is a sub-inflattice of the power set, although this seems to be a red herring at least for infinitary meets, since those are not part of the frame structure that we need.)

The top open, denoted \mathbb{R}, is the binary relation which is always true. Given two opens GG and HH, their meet in the poset of opens, denoted GHG \cap H, is simply their conjunction, that is their intersection as subsets of ×\mathbb{Q} \times \mathbb{Q}. (In fact, given any collection of opens, their meet is their conjunction.) It is straightforward to check that \mathbb{R} and GHG \cap H are opens and to prove that these are the desired meets. Intuitively, this all works because an open interval will be contained in the intersection of a family of open sets if and only if it is contained in each individual open set.

The bottom open, denoted \empty, is the binary relation \geq. That is, (a,b)(a,b) \subseteq \empty iff aba \geq b. It is easy to check that this is an open; it precedes every open by property (1). Intuitively, this corresponds to the empty subset of the real line; (a,b)(a,b) is empty if and only if aba \geq b. However, note that \empty is not the empty subset of ×\mathbb{Q} \times \mathbb{Q}; the notation follows our topological intuition rather than the algebra of relations.

Given two opens GG and HH, their join in the poset of opens, denoted GHG \cup H, is defined as follows: (a,b)GH(a,b) \subseteq G \cup H if and only if there exists a zigzag (1) with a=a 1a = a_1 and b=b nb = b_n in which each zig is of the form (a i,b i)G(a_i,b_i) \subseteq G or (a i,b i)H(a_i,b_i) \subseteq H. It is immediate that this is an open in which GG and HH are both contained. Conversely, any open in which GG and HH are contained must contain this open GHG \cup H, by property (3).

More generally, given any family (G k) k(G_k)_k of opens, their join in the poset of opens, denoted kG k\bigcup_k G_k, is defined as follows: (a,b) kG k(a,b) \subseteq \bigcup_k G_k if and only if aba \geq b or there exists a zigzag (1) with a=a 1a = a_1 and b=b nb = b_n in which each zig is of the form (a i,b i)G k(a_i,b_i) \subseteq G_k for some kk. (We can leave out the aba \geq b clause if the family is inhabited.) The same argument applies as before. Note that each individual zigzag has finitely many zigs, and therefore involves finitely many of the opens G kG_k, even when taking the join of an infinite family.

Finally, we must check the distributive law G kH k k(GH k)G \cap \bigcup_k H_k \subseteq \bigcup_k (G \cap H_k). That is, if aba \sim b directly through GG and aba \sim b through a zigzag of HHs (or aba \geq b), then we need that aba \sim b through a zigzag in which each zig is related both through GG and through some HH (or aba \geq b). To prove this (ignoring the trivial case where aba \geq b), start with the zigzag of HHs, and apply the zigzag lemma to get a zigzag of HHs in which each zig involves values bounded by aa and bb. Then these zigs hold for GG as well, by property (2). Therefore, we may interpret each zig using GH kG \cap H_k for some kk, proving the desired result.

This frame of opens, interpreted as a locale, is the locale of real numbers. As usual, we denote this locale with the same symbol as the top element of its frame, in this case \mathbb{R}. (Of course, the true etymology of the symbols runs in the other order.)

Open intervals as opens

Given rational numbers aa and bb, the open interval (a,b)(a,b) may itself be interpreted as an open in the real line, also denoted (a,b)(a,b), as follows: let (c,d)(a,b)(c,d) \subseteq (a,b) hold if every rational number strictly between cc and dd (in that order) is also strictly between aa and bb (in that order). In other words, we interpret ‘{\subseteq}’ literally as comparing subsets of \mathbb{Q}. It is straightforward to check that this condition does indeed define an open. There is now a third way to interpret ‘(c,d)(a,b)(c,d) \subseteq (a,b)’; interpreting both intervals as opens in the real line, this states that the first is contained in the second. But again, it is easy to check that this is equivalent; (c,d)(a,b)(c,d) \subseteq (a,b) (in the set-theoretic sense) if and only if (e,f)(a,b)(e,f) \subseteq (a,b) whenever (e,f)(c,d)(e,f) \subseteq (c,d). Notice that (a,b)=(a,b) = \empty whenever aba \geq b.

We can actually generalise this somewhat. Given any set LL of rational numbers and any set UU of rational numbers, we may define the open (infU,supL)(\inf U, \sup L) as follows: let (a,b)(infU,supL)(a,b) \subseteq (\inf U, \sup L) hold if every rational number strictly between aa and bb (in that order) is greater than some element of UU and less than some element of LL. If the infimum of UU and the supremum of LL exist in the usual sense as rational numbers, then this agrees with the previous paragraph. If instead UU or LL is the set of all rational numbers, then we write -\infty for infU\inf U or \infty for supL\sup L. In general, we may interpret infU\inf U as an extended upper real and supL\sup L as an extended lower real. Classically, every extended upper or lower real is either a real number, -\infty, or \infty; only the converse holds constructively. Notice that (,)=(-\infty,\infty) = \mathbb{R}.

Since we will refer to them below, we will state for the record the complete definitions of (,a)(-\infty,a) and (a,)(a,\infty) for a rational number aa. We have (b,c)(,a)(b,c) \subseteq (-\infty,a) iff every rational number strictly between bb and cc is less than aa, that is iff bcb \geq c or cac \leq a. Similarly, we have (b,c)(a,)(b,c) \subseteq (a,\infty) iff every rational number strictly between bb and cc is greater than aa, that is iff bcb \geq c or bab \geq a. A fortiori, (b,c)(,0)(b,c) \subseteq (-\infty,0) if c=0c = 0, and (b,c)(1,)(b,c) \subseteq (1, \infty) if b=1b = 1.

Open sets, closed sets, and points

We think of each open as defining an open subset of the real line, but we can equally well think of it as defining a closed subset. The difference between these perspectives is reflected in complementary criteria for when a real number belongs to the set. So to make sense of this, we must identify the points of the real line.

Recall that a real number may be defined as a pair (L,U)(L,U) of inhabited subsets of \mathbb{Q} satisfying the following properties:

  1. If aLa \in L, then a<ba \lt b for some bLb \in L.
  2. If bUb \in U, then a<ba \lt b for some aUa \in U.
  3. If aLa \in L and bUb \in U, then a<ba \lt b.
  4. If a<ba \lt b, then aLa \in L or bUb \in U.

We define a point of the real line to be a real number in this sense. Given such a point x=(L,U)x = (L,U) and a rational number aa, we write a<xa \lt x to mean that aLa \in L and a>xa \gt x to mean that aUa \in U. If we wish to refer to LL and UU directly, we may call LL the lower set of xx and UU the upper set.

Given a point xx and an open GG, we say that xx belongs to GG, written xGx \in G, if (a,b)G(a,b) \subseteq G for some a<xa \lt x and b>xb \gt x; that is, GG contains an interval from some element of the lower set to some element of the upper set of xx. We have xx \in \mathbb{R} since its lower and upper sets are inhabited. If xGx \in G and xHx \in H, with (a,b)G(a,b) \subseteq G and (c,d)H(c,d) \subseteq H, then (max(a,c),min(b,d))GH\big(\max(a,c), \min(b,d)\big) \subseteq G \cap H, so xGHx \in G \cap H; note that this argument fails for infinitary intersections. (The converse, that xGx \in G and xHx \in H if xGHx \in G \cap H, is immediate.) Dually, suppose that x kG kx \in \bigcup_k G_k, as shown by some zigzag (since aba \geq b is impossible when a<xa \lt x and b>xb \gt x, by 3). Applying condition (4) of the definition of real number to each zag, we have a i +<xa_{i^+} \lt x or b i>xb_i \gt x, for each i<ni \lt n. Checking all 2 n12^{n-1} possibilities, and knowing that a 1<xa_1 \lt x and b n>xb_n \gt x in any case, we must have a i<xa_i \lt x and b i>xb_i \gt x for some ii. Then we have xG kx \in G_k for some kk, whichever corresponds to the iith zig. (The converse, that x kG kx \in \bigcup_k G_k if xG kx \in G_k for some kk, is immediate.)

Therefore, each point defines a completely prime filter on the frame of all opens, which is the definition of a point in general locale theory. Conversely, given such a completely prime filter PP, let LL be the set of all rational numbers aa such that the open interval (a,)(a, \infty) (when interpreted as an open in the real line as defined above) is in PP, and symmetrically let UU be the set of all aa such that (,a)P(-\infty, a) \in P.

Given a point xx and an open GG, we say that xx co-belongs to GG, written xGx \notin G, if we never have a<xa \lt x, b>xb \gt x, and (a,b)G(a,b) \subseteq G, which is precisely the negation of the property that xGx \in G. We think of this condition as defining a closed set to which xx does belong. Notice that x kG kx \notin \bigcup_k G_k if and only if xG kx \notin G_k for each kk, giving the desired behaviour for an arbitrary intersection of closed sets (which corresponds to union of open sets under de Morgan duality). We also have that xx \notin \mathbb{R} always fails, and xGHx \notin G \cap H if xGx \notin G or xHx \notin H. To prove that xGx \notin G or xHx \notin H whenever xGHx \notin G \cap H, however, we must use excluded middle; constructively, closed sets don't behave well under union.

A related question is whether we can reconstruct GG from the set of points which belong to it. This should be equivalent to the fan theorem, which is classically true and also accepted by Brouwer's school of intuitionism, but refuted in the Russian school in which all real numbers are assumed to be computable. (I should check this.) Arguably, the real lesson of these logical technicalities is that we should remember that opens, not points, are the fundamental concept in a locale.

The Heine–Borel theorem

The classical Heine–Borel theorem, as a statement about sets of real numbers, may fail constructively; this is related to the comments above about the fan theorem. But the beauty of the localic approach is that Heine–Borel necessarily holds when interpreted as a statement about opens in the locale of real numbers. To state the theorem, we must define what it means for a collection of opens to cover the unit interval. We will give an ad-hoc definition, but this may also be derived from the general theory of closed sublocales which allows us to interpret the unit interval as a compact locale in its own right.

Definition

An open cover of the unit interval is a collection 𝒞\mathcal{C} of opens in the real line such that \mathbb{R} is the join of (,0)(-\infty,0), (1,)(1,\infty), and the elements of 𝒞\mathcal{C}.

Theorem

(Heine–Borel)

Every open cover of the unit interval has a finite subcover.

Proof

The proof is almost embarrassingly simple. The key point is that the construction of joins in terms of zigzags involves only finite zigzags, even for an infinitary join.

Let JJ be the join of (,0)(-\infty,0), (1,)(1,\infty), and the elements of 𝒞\mathcal{C}. If this equals \mathbb{R}, then in particular (1,2)J(-1,2) \subseteq J, a fact which is given by some zigzag ζ\zeta. This zigzag involves only finitely many of the elements of 𝒞\mathcal{C}; let 𝒟\mathcal{D} be the collection of these, and let KK be the join of (,0)(-\infty,0), (1,)(1,\infty), and 𝒟\mathcal{D}. Now if (a,b)(a,b) is any pair of rational numbers, we construct a zigzag showing that (a,b)K(a,b) \subseteq K as follows: the zig (a,0)(,0)(a,0) \subseteq (-\infty,0), the zag 0>10 \gt -1, the zigzag ζ\zeta from 1-1 to 22, the zag 2>12 \gt 1, and the zig (1,b)(1,)(1,b) \subseteq (1,\infty). This is always a valid zigzag, so K=K = \mathbb{R}. Therefore, the finite collection 𝒟\mathcal{D} covers the unit interval.

This proof generalises immediately to any closed interval [a,b][a,b], for aa any upper real and bb any lower real. But note that we do not say ‘extended’ here; we need to find some rational number (analogous to 1-1 in the proof above) smaller than aa and some rational number (analogous to 22 above) larger than bb. So the Heine–Borel theorem applies only to bounded closed intervals.

 As a classifying locale

The locale of real numbers is the classifying locale of the geometric theory of Dedekind real numbers.

 Defining functions in the locale of real numbers

There are two general ways to define functions on the locale of real numbers, via the rational numbers and via the Dedekind real numbers.

Using the rational numbers

The first approach uses existing functions already defined on the rational numbers \mathbb{Q}. Suppose that one has a locally uniformly continuous function f:f:\mathbb{Q} \to \mathbb{Q}. Then one could extend ff to a continuous map f:f':\mathbb{R} \to \mathbb{R} on the locale of real numbers.

Using the Dedekind real numbers.

The other approach is via using existing functions defined on the Dedekind real numbers \mathbb{R}. In particular, given any well-defined continuous function xf(x)x \mapsto f(x) on the Dedekind real numbers, and a geometric morphism F:SetSh( D)F:\mathrm{Set} \to \mathrm{Sh}(\mathbb{R}_D) from Set to the sheaf topos Sh( D)\mathrm{Sh}(\mathbb{R}_D), if for all Dedekind real numbers x Dx \in \mathbb{R}_D, f(F *(x))=F *(f(x))f(F^*(x)) = F^*(f(x)), then the function xf(x)x \mapsto f(x) lifts to a function xf(x)x \mapsto f'(x) on the locale of real numbers.

This allows us to first define real-valued functions normally on the set of Dedekind real numbers, and then lift them up to a real-valued function on the locale of real numbers, thus allowing us to define functions such as the exponential function, the sine, and the cosine which can’t be directly defined using functions on the rational numbers.

Arithmetic

Significantly, since the field operations on the discrete locale of rational numbers are all locally uniformly continuous on the \mathbb{Q}, and the field operations are well-defined and continuous on the Dedekind real numbers D\mathbb{R}_D, the field operations in both cases lift up to a field structure on the locale of real numbers, allowing one to do basic arithmetic on \mathbb{R}.

 References

The locale of real numbers as the classifying locale of the geometric theory of two-sided Dedekind cuts is described in section 2.2 of:

An (impredicative) construction of the locale of real numbers can be found in section 5.3 of:

  • Graham Manuell, Uniform locales and their constructive aspects, (arXiv:2106.00678)

On lifting functions from the Dedekind real numbers to the locale of real numbers, see:

Last revised on November 17, 2022 at 23:21:33. See the history of this page for a list of all contributions to it.