Real numbers object

Idea

Recall that it is possible to define an internalization of the set of natural numbers, called a natural numbers object (NNO), in any cartesian monoidal category (a category with finite products). In particular, the notion makes sense in a topos. But a topos supports intuitionistic higher-order logic, so once we have an NNO, it is also possible to repeat the usual construction of the integers, the rationals, and then finally the real numbers; we thus obtain an internalization of $ℝ$ in any topos with an NNO.

More generally, we can define a real numbers object (RNO) in any category with sufficient structure (somewhere between a cartesian monoidal category and a topos). Then we can prove that an RNO exists in any topos with an NNO (and in some other situations).

Definition

Let $ℰ$ be a Heyting category. (This means, in particular, that we can interpret full first-order intuitionistic logic using the stack semantics.)

In detail:

A commutative ring object in $ℰ$ is an object $R$ equipped with morphisms $0:1\to R$, $-:R\to R$, $+:R\times R\to R$, $1:1\to R$, and $\cdot :R\times R\to R$ (where $1$ is the terminal object of $ℰ$ and $\times$ is the product operation in $ℰ$) that make certain diagrams commute. (These diagrams may be found at ring object, in principle, although right now they're not there.)

Given a commutative ring object $R$ in $ℰ$, we define a binary relation $\#$ on $R$ (that is a subobject of $R\times R$) as

written in the internal language of $ℰ$. Then $R$ is a (Heyting) field object if $\#$ is a tight apartness relation; that is if the following axioms (in the internal language) hold:

• irreflexivity: $\forall x:R.\neg (x\#x)$,
• symmetry: $\forall x:R.\forall y:R.(x\#y\Rightarrow y\#x)$ (which can actually be proved using $-$),
• comparison: $\forall x:R.\forall y:R.\forall z:R.(x\#z\Rightarrow (x\#y\vee y\#z))$,
• tightness: $\forall x:R.\forall y:R.(\neg (x\#y)\Rightarrow x=y)$.

A (linearly) ordered field object in $ℰ$ is a field object $R$ equipped with a binary relation $<$ such that the following axioms hold:

• strong irreflexivity: $\forall x:R.\forall y:R.(x<y\Rightarrow x\#y)$,
• strong connectedness: $\forall x:R.\forall y:R.(x\#y\Rightarrow (x<y\vee y<x))$,
• transitivity: $\forall x:R.\forall y:R.\forall z:R.((x<y\wedge y<z)\Rightarrow x<z)$,
• respecting addition: $\forall x:R.\forall y:R.\forall z:R.(x<y\Rightarrow x+z<y+z)$,
• respecting multiplication: $\forall x:R.\forall y:R.\forall z:R.((x<y\wedge 0<z)\Rightarrow x\cdot z<y\cdot z)$.

Given an ordered field object $R$ in $ℰ$, any object $\Gamma$ in $ℰ$, and subobjects $L$ and $U$ of $\Gamma \times R$, we say that $(L,U)$ is a Dedekind cut in $R$ (parametrised by $\Gamma$) if the following axioms hold:

• lower bound: $\forall a:\Gamma .\exists x:R.(a,x)\in L$,
• upper bound: $\forall a:\Gamma .\exists x:R.(a,x)\in U$,
• downward roundedness: $\forall a:\Gamma .\forall x:R.\forall y:R.((x<y\wedge (a,y)\in L)\Rightarrow (a,x)\in L)$,
• upward roundedness: $\forall a:\Gamma .\forall x:R.\forall y:R.(((a,x)\in U\wedge x<y)\Rightarrow (a,y)\in U)$,
• upward openness: $\forall a:\Gamma .\forall x:R.((a,x)\in L\Rightarrow \exists b:\Gamma .\exists y:R.((b,y)\in L\wedge x<y))$,
• downward openness: $\forall a:\Gamma .\forall x:R.((a,x)\in U\Rightarrow \exists b:\Gamma .\exists y:R.((b,y)\in U\wedge y<x))$,
• locatedness: $\forall a:\Gamma .\forall x:R.\forall y:R.(x<y\Rightarrow ((a,x)\in L\vee (a,y)\in U))$,
• separation: $\forall a:\Gamma .\forall x:R.\forall y:R.(((a,x)\in L\wedge (a,y)\in U)\Rightarrow x<y)$.

An ordered field object $R$ in $ℰ$ is Dedekind complete if, given any object $\Gamma$ of $ℰ$ and any Dedekind cut $(L,U)$ in $R$ parametrised by $\Gamma$, there exists a morphism $x:\Gamma \to R$ such that

Finally, a real numbers object in $ℰ$ is a Dedekind-complete ordered field object.

Properties

In the last requirement, of Dedekind completeness, we postulate (under certain conditions) the existence of a morphism $x:\Gamma \to R$ satisfying certain properties.

Here is an explicit ‘external’ proof:

Here is an ‘internal’ proof, to be interpreted in the stack semantics of $ℰ$:

In the definition of a Heyting field object, all of the axioms except the last are coherent and therefore make sense in any coherent category.

It would be nice to say that a Heyting category with an RNO must have an NNO; after all, $\mathbb{N}$ is contained in $ℝ$. However, my only argument is impredicative; although I don’t know a specific example, there could be a $\Pi$-pretopos with an RNO but no NNO. However, the argument works for a geometric Heyting category or a topos. (In light of the constructions below, the existence of an RNO is therefore equivalent to the existence of an NNO in a topos.)

We usually speak of the RNO, if one exists. This is because any two RNOs in a Heyting category with an NNO are isomorphic, in an essentially unique way. (I can’t prove this without an NNO, although the previous theorem shows that we often have one.)

Constructions

We can construct a real numbers object in the following cases (presumably among others):

1. in a topos with an NNO;
2. in a $\Pi$-pretopos with an NNO and weak countable choice;
3. in a $\Pi$-pretopos with an NNO and subset collection.

(Actually, (1) is a special case of (3), but the usual construction in (1) is not available in (3). Thus, we still have three different constructions to consider.)

In a topos with an NNO

Let $ℰ$ be an elementary topos with a natural numbers object $\mathbb{N}$. The Dedekind real numbers object of $ℰ$ is the object of all Dedekind cuts. To be more precise, we will need to make some auxiliary definitions.

We first construct an integers object as follows. Let $a,b:E\to \mathbb{N}\times \mathbb{N}$ be the kernel pair of the addition map $+:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$, and let ${\pi }_1,{\pi }_2:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$ be the product projections. We define $\mathbb{Z}$ to be the coequalizer of $({\pi }_1\circ a,{\pi }_2\circ b),({\pi }_2\circ a,{\pi }_1\circ b):E\to \mathbb{N}$. A similar construction yields a rational numbers object $\mathbb{Q}$.

We denote by $𝒫(A)$ the power object of $A$ in $ℰ$. A Dedekind cut is a generalized element $(L,U)$ of $𝒫(\mathbb{Q})\times 𝒫(\mathbb{Q})$, satisfying the following conditions, expressed in the Mitchell–Bénabou language of $ℰ$ and interpreted under Kripke–Joyal semantics:

1. Non-degenerate:

   $$\exists q:\mathbb{Q}.q\in L;$$\exists q\colon \mathbb{Q}.\, q \in L ;
   $$\exists r:\mathbb{Q}.r\in U.$$\exists r\colon \mathbb{Q}.\, r \in U .

2. Inward-closed:

   $$\forall q:\mathbb{Q}.\forall r:\mathbb{Q}.((q<r\wedge r\in L)\Rightarrow q\in L);$$\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((q \lt r \wedge r \in L) \implies q \in L) ;
   $$\forall q:\mathbb{Q}.\forall r:\mathbb{Q}.((r<q\wedge r\in U)\Rightarrow q\in U).$$\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((r \lt q \wedge r \in U) \implies q \in U) .

3. Outward-open:

   $$\forall q:\mathbb{Q}.(q\in L\Rightarrow \exists r:\mathbb{Q}.(r\in L\wedge q<r))$$\forall q\colon \mathbb{Q}.\, (q \in L \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge q \lt r))
   $$\forall q:\mathbb{Q}.(q\in U\Rightarrow \exists r:\mathbb{Q}.(r\in L\wedge r<q)).$$\forall q\colon \mathbb{Q}.\, (q \in U \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge r \lt q)) .

4. Located:

   $$\forall q:\mathbb{Q}.\forall r:\mathbb{Q}.(q<r\Rightarrow (q\in L\vee r\in U)).$$\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, (q \lt r \implies (q \in L \vee r \in U)) .

5. Mutually exclusive:

   $$\forall q:\mathbb{Q}.\neg (q\in L\wedge q\in U).$$\forall q\colon \mathbb{Q}.\, \neg(q \in L \wedge q \in U) .

The relation $<$ on $\mathbb{Q}$ is the order relation constructed in the usual way. We define $ℝ$ to be the subobject of $𝒫(\mathbb{Q})\times 𝒫(\mathbb{Q})$ consisting of all Dedekind cuts as defined above.

In a $\Pi$-pretopos with $\mathrm{WCC}$

Summary: construct a Cauchy real numbers object and use $\mathrm{WCC}$ (weak countable choice) to prove that it is an RNO.

Note that any Boolean topos with an NNO satisfies $\mathrm{WCC}$, so in all we have three different constructions available in that case.

In a $\Pi$-pretopos with an NNO and subset collection

Summary: modify the construction of a Cauchy real numbers object to use multi-valued Cauchy sequences.

Examples

In $\mathrm{Set}$

The real numbers object in Set is the real line, the usual set of (located Dedekind) real numbers. Note that this is a theorem of constructive mathematics, as long as we assume that $\mathrm{Set}$ is an elementary topos with an NNO (or more generally a $\Pi$-pretopos with NNO and either WCC or subset collection).

In sheaves on a topological space

Let $X$ be a topological space, and $\mathrm{Sh}(X)$ its category of sheaves. It is well-known that $\mathrm{Sh}(X)$ is a Grothendieck topos (and so, a fortiori, an elementary topos), and the constant sheaf functor $\Delta :\mathrm{Set}\to \mathrm{Sh}(X)$ preserves finite limits and has the global section functor $\Gamma :\mathrm{Sh}(X)\to \mathrm{Set}$ as a right adjoint. (Hence, $\Delta$ and $\Gamma$ are the components of a geometric morphism $\mathrm{Sh}(X)\to \mathrm{Set}$.) The following claims are essentially immediate:

1. If $N$ is the set of natural numbers, then $\Delta (N)$ must be an NNO in $\mathrm{Sh}(X)$, since $\Delta$ has a right adjoint.

2. If $Z$ is the set of integers, then $\Delta (Z)$ is an integers object in $\mathrm{Sh}(X)$ (as defined above), since $\Delta$ preserves finite limits and colimits.

3. Similarly, if $Q$ is the set of rational numbers, then $\Delta (Q)$ is a rational numbers object in $\mathrm{Sh}(X)$.

Thus, for every topological space $X$, the topos $\mathrm{Sh}(X)$ has a Dedekind real numbers object $ℝ$. Naïvely one might expect $ℝ$ to be isomorphic to the constant sheaf $\Delta (R)$, where $R$ is the classical set of real numbers, but this turns out not to be the case. Instead, we have a rather more remarkable result:

This allows us to define various further constructions on $X$ in internal terms in $\mathrm{Sh}(X)$; for example, a vector bundle over $X$ is an internal projective $ℝ$-module.

Generalizations

It is also possible to define the notion of a Cauchy real number object and construct one in any $\Pi$-pretopos with an NNO, but as the internal logic in general lacks weak countable choice, these are usually inequivalent. (There is also potentially a difference between the classical Cauchy RNO and the modulated Cauchy RNO; see definitions at Cauchy real number, to be interpreted in the stack semantics.)

Related concepts

• natural number, natural numbers object

• real number, real numbers object

References

Section D4.7 of

• Peter Johnstone, Sketches of an Elephant

See also

• Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic