nLab locale of real numbers

The locale of real numbers

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

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 Toby Bartels's own work, although of course the basic ideas are well known to many. In particular, the Zigzag Lemma is Bartels's as far as they know (but it's not very deep, just bookkeeping). The version of Cousin's Theorem? that appears here may also be original.

Idea

To describe the locale of the real numbers, we need first of all to describe what an open (in the axiomatic sense, equivalent to an open sublocale) in the real line is. The key insight is that an open subspace 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 one is 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.

In practice, rather than using relation-like symbols for opens, we mimic the set-theoretic notation and terminology from point-set topology. So 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 and that this interval is contained in GG.

In this notation, and writing (a,b)(c,d)(a, b) \subseteq (c, d) for cac \leq a and bdb \leq d, and (a,b)(c,d)(a, b) \Subset (c, d) for c<ac \lt a and b<db \lt d, these requirements say:

  1. If aba \geq b, then (a,b)G(a, b) \subseteq G.

  2. If (a,d)(b,c)(a, d) \subseteq (b, c) and (b,c)G(b, c) \subseteq G, then (a,d)G(a, d) \subseteq G.

  3. If c<bc \lt b and (a,b),(c,d)G(a, b), (c, d) \subseteq G, then (a,d)G(a, d) \subseteq G.

  4. If (b,c)G(b, c) \subseteq G for all (b,c)(a,d)(b, c) \Subset (a, d), then (a,d)G(a, d) \subseteq G.

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) \Subset (a, d)} (b, c) = (a, d).

The really interesting property is property (3). It immediately generalizes as follows:

  • If
    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 above 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.

We can incorporate property (2) into this by saying:

  • If
    aa 1b 1>a 2b 2>>a nb nb, a \geq a_1 \sim b_1 \gt a_2 \sim b_2 \gt \cdots \gt a_n \sim b_n \geq b ,

    then aba \sim b.

Then you can think of property (1) as the zigzag property for n=0n = 0. Alternatively, we can incorporate property (4) by saying:

  • If, whenever a<a 1a \lt a_1 and b n<bb_n \lt b, there is a zigzag
    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 aba \sim b.

Or by making both modifications, we can stuff the entire definition into a single statement.

The Zigzag Lemma

A zigzag may not look like the picture above; instead of an orderly progression, the zigs and zags may be wild swings that are undone by other zags and zigs. It is sometimes convenient to replace a zigzag by a more orderly one. Of course, this is easy if all of the zigs belong to a single open, since (by property (3) of the definition of an open), the whole zigzag can be replaced by a single zig. But we'll also want to consider zigzags where the zigs are taken from different opens. The following definitions make precise what kind of zigzag we'll want, and then there will be a lemma that we can indeed have this.

Definitions

Given rational numbers aa and bb and a positive natural number nn, a 2n2n-tuple (a 1,b 1,,a n,b n)(a_1,b_1,\ldots,a_n,b_n) of rational numbers forms a zigzag of length nn from aa to bb if we have:

  • a=a 1a = a_1, b=b nb = b_n, and
  • b i>a i+b_i \gt a_{i+} for i=1,,n1i = 1, \ldots, n - 1.

A zigzag of positive length is orderly if we additionally have:

  • a i<a i+a_i \lt a_{i+} for i=1,,n1i = 1, \ldots, n - 1,
  • a i<b ia_i \lt b_i for i=1,,ni = 1, \ldots, n, and
  • b i<b i+b_i \lt b_{i+} for i=1,,n1i = 1, \ldots, n - 1.

As a technicality, if aba \geq b, then we also count the empty 00-tuple as an orderly zigzag of length 00 from aa to bb. (Notice that no zigzag of positive length can be orderly from aa to bb when aba \geq b.)

Given additionally a collection 𝒰\mathcal{U} of opens, a zigzag (orderly or not) has zigs from 𝒰\mathcal{U} if every pair (a i,b i)(a_i,b_i) is contained in at least one member of 𝒰\mathcal{U}.

Now we can replace any zigzag with an orderly zigzag with zigs from the same opens:

Lemma

(Zigzag Lemma)

Given rational numbers aa and bb, a natural number nn, a collection 𝒰\mathcal{U} of opens, and a zigzag from aa to bb of length nn with zigs from 𝒰\mathcal{U}, there exists an orderly zigzag from aa to bb of length at most nn with zigs from 𝒰\mathcal{U}.

Proof

If aba \geq b, then we use a zigzag of length 00. Otherwise, we assume that a<ba \lt b and prove the lemma by induction on nn. If n=1n = 1, then the original zigzag is orderly since a<ba \lt b.

Now assume (as an inductive hypothesis) that the lemma holds for zigzags of length kk for some k1k \geq 1. A zigzag of length k+k+ consists of a zig (a,b 1)(a,b_1) from some open in 𝒰\mathcal{U}, a zag b 1>a 2b_1 \gt a_2, and a zigzag of length kk from a 2a_2 to bb with zigs from 𝒰\mathcal{U}. Using the inductive hypothesis, replace the zigzag of length kk with an orderly zigzag of length lkl \leq k from a 2a_2 to b=b l+b = b_{l+} with zigs from 𝒰\mathcal{U}. We now have a zigzag of length l+k+l+ \leq k+ from aa to bb with zigs from 𝒰\mathcal{U}.

If a<a 2a \lt a_2 and b 1<b 2b_1 \lt b_2, then also a<a 2<b 1a \lt a_2 \lt b_1, so this zigzag of length l+l+ from aa to bb is orderly.

Next suppose that a<a 2a \lt a_2 but b 1b 2b_1 \geq b_2. In this case, consider the largest value of i2i \geq 2 such that b 1b ib_1 \geq b_i; if i=l+i = l+, then we can use the orderly zigzag of length 11 from aa to bb, which is contained in the same open as (a,b 1)(a,b_1) was, since b 1b i=bb_1 \geq b_i = b. If ili \leq l instead, then take the orderly zigzag from a i+a_{i+} to bb, and precede it with the zig (a,b i)(a,b_i), to get a zigzag of length li+2kl - i + 2 \leq k from aa to bb. This zigzag is orderly, because a<a 2<a i+a \lt a_2 \lt a_{i+}, and its zigs are from 𝒰\mathcal{U} since (a,b i)(a,b_i) is contained in the same open as (a,b 1)(a,b_1) was (since b 1b ib_1 \geq b_i). So either way, we have an orderly zigzag of length at most kk from aa to bb with zigs from 𝒰\mathcal{U}.

Finally, suppose that aa 2a \geq a_2. In this case, consider the largest value of i2i \geq 2 such that aa ia \geq a_i, take the orderly zigzag from a ia_i to bb, and change a ia_i to aa to get a zigzag from aa to bb. If ili \leq l, then this is orderly since a<a i+<b ia \lt a_{i+} \lt b_i; if i=l+i = l+, then this is orderly since a<b=b ia \lt b = b_i. Either way, (a,b i)(a,b_i) belongs to the same open as (a i,b i)(a_i,b_i) did (since aa ia \geq a_i), so this orderly zigzag of length li+2kl - i + 2 \leq k from aa to bb still has zigs from 𝒰\mathcal{U}.

In any case, we have a zigzag of length at most k+k+ from aa to bb with zigs from 𝒰\mathcal{U}, and the induction is complete.

This lemma is used in the proofs of the infinite distributivity law and some results related to measure.

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, whenever a<a 1a \lt a_1 and b n<bb_n \lt b, there exists a zigzag from a 1a_1 to b nb_n with zigs from GG and HH. 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 properties (3) and (4).

More generally, given any collection 𝒰\mathcal{U} (or family (G k) k(G_k)_k) of opens, their join in the poset of opens, denoted 𝒰\bigcup \mathcal{U} (or kG k\bigcup_k G_k), is defined as follows: (a,b)𝒰(a,b) \subseteq \mathcal{U} if and only if, whenever a<a 1a \lt a_1 and b n<bb_n \lt b, there exists a zigzag from a 1a_1 to b nb_n with zigs from 𝒰\mathcal{U}. (Notice that aba \geq b counts even when 𝒰\mathcal{U} is empty, using zigzags of length 00.) 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 collection.

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 a 1b na_1 \sim b_n through a zigzag of HHs for (a 1,b n)(a,b)(a_1,b_n) \Subset (a,b), then we need that a 1b na_1 \sim b_n through a zigzag in which each zig is related both through GG and through some HH. To prove this, start with the zigzag of HHs, and apply the Zigzag Lemma to get an orderly zigzag of HHs, so that each zig is 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 generalize 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 members of 𝒞\mathcal{C}.

Theorem

(Heine–Borel)

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

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.

Proof

Let JJ be the join of (,0)(-\infty,0), (1,)(1,\infty), and the members of 𝒞\mathcal{C}. Since this equals \mathbb{R}, then in particular (2,3)J(-2,3) \subseteq J, and since (1,2)(2,3)(-1,2) \Subset (-2,3), we get a corresponding zigzag ζ\zeta involving finitely many zigs using finitely many of the members of 𝒞\mathcal{C}. Let 𝒟\mathcal{D} be the collection of these members of 𝒞\mathcal{C}, 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 directly 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 generalizes 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.

Another generalization is Cousin's Theorem?:

Theorem

(Cousin's)

Given any open cover 𝒞\mathcal{C} of the unit interval, there is a partition 0=a 0a 1a n=10 = a_0 \leq a_1 \leq \cdots \leq a_n = 1 such that each subinterval [a i,a i+][a_i, a_{i+}] is covered by a single member UU of 𝒞\mathcal{C} (in that (,a i)U(a i+,)=(-\infty,a_i) \cup U \cup (a_{i+},\infty) = \mathbb{R}).

Proof

As in the previous proof, construct a zigzag ζ\zeta from 1-1 to 22 with zigs from 𝒞\mathcal{C}. Using the Zigzag Lemma , replace this with an orderly zigzag. Let a 0a_0 be 00, let a 1a_1 be the smallest left endpoint of a zig from ζ\zeta satisfying 0<a 1<10 \lt a_1 \lt 1, let a 2a_2 be smallest left endpoint satisfying a 1<a 2<1a_1 \lt a_2 \lt 1, and so on until none are left, and then finish with a n1a_n \coloneqq 1.

A corollary of this theorem, when the open cover is given by a function δ:[0,1](0,)\delta\colon [0,1] \to (0,\infty) (so that 𝒞{(xδ(x),x+δ(x))|x[0,1]}\mathcal{C} \coloneqq \big\{\big(x - \delta(x), x + \delta(x)\big) \;|\; x \in [0,1]\big\}), is used (classically) to prove the uniqueness (indeed, non-vacuity) of the Henstock–Kurzweil integral, which could be used to define Lebesgue measure (see below).

A result on measure

The set of computable real numbers has measure zero in the sense that, given any positive number ϵ\epsilon, there's a collection \mathcal{I} of open intervals (even with rational endpoints), such that every computable real number belongs to at least one member of \mathcal{I}, and the sum of the lengths of any finite list of distinct members of \mathcal{I} is less than ϵ\epsilon. (We can do this by enumerating Turing machines.) This is a problem for a theory of Lebesgue measure in Russian constructivism, where every real number is computable.

From a localic perspective, however, while \mathcal{I} might cover all the points of the real line, it cannot cover all of the pointless parts (which need not be empty). Indeed, we have this result ruling out such shenanigans:

Proposition

Given any open interval I=(a,b)I = (a,b) with rational endpoints and any collection 𝒥\mathcal{J} of such intervals, if I𝒥I \subseteq \bigcup \mathcal{J}, then for any length L<baL \lt b - a, there must be a finite? (in the strictest sense) subcollection {K 1,,K n}\{K_1, \ldots, K_n\} of 𝒥\mathcal{J} such that

L i=1 nlenK i. L \leq \sum_{i=1}^n \len K_i .

In other words, any cover of II by intervals must have a total length (defined as the supremum of the lengths of finite subcollections) at least the length of II.

Proof

Let (c,d)(a,b)(c,d) \Subset (a,b) with dcLd - c \geq L (say with c(a+bL)/2c \coloneqq (a + b - L)/2 and d(a+b+L)/2d \coloneqq (a + b + L)/2). Then there is a zigzag from cc to dd with zigs from 𝒥\mathcal{J}; by the Zigzag Lemma , we may take this zigzag to be orderly, say of length nn. Each zig is from one of the intervals in 𝒥\mathcal{J}, say K 1,,K nK_1, \ldots, K_n. If these intervals are all distinct (which we can decide, since the endpoints are rational), then we're done, since

i=1 nlenK i i=1 n(b ia i)= i=1 n1(b ia i)+(b na n) i=1 n1(a i+a i)+(b na n)=b na 1=dcL, \sum_{i=1}^n \len K_i \geq \sum_{i=1}^n (b_i - a_i) = \sum_{i=1}^{n-1} (b_i - a_i) + (b_n - a_n) \geq \sum_{i=1}^{n-1} (a_{i+} - a_i) + (b_n - a_n) = b_n - a_1 = d - c \geq L ,

or 0L 0 \geq L if n=0n = 0. If they're not distinct, then we instead use the smallest a ia_i and largest b ib_i that appears in a given interval, and the argument still works (possibly even with some overlap now).

This result can be strengthened to intervals without necessarily rational endpoints, by using the rational intervals that they contain, but this is not the most general statement either, and I think that what we really need to do is to develop a theory of measures of open subspaces (or perhaps even more general subspaces) and state a result about that.

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˜:\widetilde{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 \widetilde{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:

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 February 6, 2024 at 15:49:59. See the history of this page for a list of all contributions to it.