topos theory

# 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.)

###### Definition

A (located Dedekind) real numbers object in $ℰ$ is a ring object in $ℰ$ that satisfies (in the internal logic) the axioms of a Dedekind-complete linearly ordered Heyting field.

In detail:

A commutative ring object in $ℰ$ is an object $R$ equipped with morphisms $0:1\to R$, $-:R\to R$, $+:R×R\to R$, $1:1\to R$, and $\cdot :R×R\to R$ (where $1$ is the terminal object of $ℰ$ and $×$ 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×R$) as

$\left\{\left(x,y\right):R×R\phantom{\rule{thickmathspace}{0ex}}\mid \phantom{\rule{thickmathspace}{0ex}}\exists z:R.\phantom{\rule{thinmathspace}{0ex}}x\cdot z=y\cdot z+1\right\},$\{ (x,y)\colon R \times R \;|\; \exists z\colon R.\, x \cdot z = y \cdot z + 1 \} ,

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.\phantom{\rule{thinmathspace}{0ex}}¬\left(x#x\right)$,
• symmetry: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(x#y⇒y#x\right)$ (which can actually be proved using $-$),
• comparison: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\forall z:R.\phantom{\rule{thinmathspace}{0ex}}\left(x#z⇒\left(x#y\vee y#z\right)\right)$,
• tightness: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(¬\left(x#y\right)⇒x=y\right)$.

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.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(x,
• strong connectedness: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(x#y⇒\left(x,
• transitivity: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\forall z:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(x,
• respecting addition: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\forall z:R.\phantom{\rule{thinmathspace}{0ex}}\left(x,
• respecting multiplication: $\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\forall z:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(x.

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

• lower bound: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\exists x:R.\phantom{\rule{thinmathspace}{0ex}}\left(a,x\right)\in L$,
• upper bound: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\exists x:R.\phantom{\rule{thinmathspace}{0ex}}\left(a,x\right)\in U$,
• downward roundedness: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(x,
• upward roundedness: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(\left(a,x\right)\in U\wedge x,
• upward openness: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(a,x\right)\in L⇒\exists b:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\exists y:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(b,y\right)\in L\wedge x,
• downward openness: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(a,x\right)\in U⇒\exists b:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\exists y:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(b,y\right)\in U\wedge y,
• locatedness: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(x,
• separation: $\forall a:\Gamma .\phantom{\rule{thinmathspace}{0ex}}\forall x:R.\phantom{\rule{thinmathspace}{0ex}}\forall y:R.\phantom{\rule{thinmathspace}{0ex}}\left(\left(\left(a,x\right)\in L\wedge \left(a,y\right)\in U\right)⇒x.

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

$L=\left\{\left(a,b\right):\Gamma ×R\phantom{\rule{thickmathspace}{0ex}}\mid \phantom{\rule{thickmathspace}{0ex}}bL = \{ (a,b)\colon \Gamma \times R \;|\; b \lt x(a) \} ,
$U=\left\{\left(a,b\right):\Gamma ×R\phantom{\rule{thickmathspace}{0ex}}\mid \phantom{\rule{thickmathspace}{0ex}}x\left(a\right)U = \{ (a,b)\colon \Gamma \times R \;|\; x(a) \lt b \} .

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.

###### Theorem

This morphism is in fact unique.

Here is an explicit ‘external’ proof:

###### Proof

Suppose that $x,x\prime :\Gamma \to R$ both satisfy the required properties, and consider $x#x\prime$, which is a subobject of $\Gamma$. By the strong connectedness of $<$, $x#x\prime$ is contained in (factors through) $x, which is the union of $x and $x\prime .

Now consider $x, and let $a$ be a generalised element of $\Gamma$. If $a$ belongs to (factors through) $x, or equivalently $\left(x\left(a\right),x\prime \left(a\right)\right)$ belongs to $<$, it follows that $\left(a,x\left(a\right)\right)$ belongs to $L$. Thus, $\left(x\left(a\right),x\left(a\right)\right)$ also belongs to $<$, or equivalently $a$ belongs to $x. By the strong irreflexivity of $<$, this is contained in $x#x$; by the irreflexivity of $#$, this is contained in $\perp$ (as a subobject of $\Gamma$). Since every $a$ that belongs to $x belongs to $\perp$, $x is contained in (and so equals as a subobject) $\perp$.

Similarly (either by swapping $x$ with $x\prime$ or by using $U$ instead of $L$), $x\prime is also $\perp$. Therefore, $x#x\prime$ is $\perp$. By the tightness of $#$, $x=x\prime$.

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

###### Proof

Suppose that $x,x\prime :R$ both satisfy the required properties, and suppose that $x#x\prime$. By the strong connectedness of $<$, $x or $x\prime .

Now suppose that $x. It follows that $x$ belongs to $L$, so $x. By the strong irreflexivity of $<$, $x#x$; by the irreflexivity of $#$, we have a contradiction.

Similarly (either by swapping $x$ with $x\prime$ or by using $U$ instead of $L$), $x\prime is also false. Therefore, $x#x\prime$ is false. By the tightness of $#$, $x=x\prime$.

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.

###### Theorem

An object satisfying all but the last axiom of a field object is precisely a local ring object (so in particular an RNO is a local ring object).

###### Proof

It would be nice to say that a Heyting category with an RNO must have an NNO; after all, $ℕ$ 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.)

###### Theorem

If $R$ is an RNO in an infinitary Heyting category or topos, then there is unique subobject $N$ of $R$ that is both a sub-rig object of $R$ and an NNO under the operations $0:1\to N$ and $\left(-\right)+1:N\to N$.

###### Proof

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.)

###### Theorem

If $R$ and $R\prime$ are both RNOs in a Heyting category $ℰ$ with an NNO, then there is a unique isomorphism from $R$ to $R\prime$ that preserves the structures on them ($0$, $-$, $+$, $1$, $\cdot$, $<$).

## 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 $ℕ$. 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 ℕ×ℕ$ be the kernel pair of the addition map $+:ℕ×ℕ\to ℕ$, and let ${\pi }_{1},{\pi }_{2}:ℕ×ℕ\to ℕ$ be the product projections. We define $ℤ$ to be the coequalizer of $\left({\pi }_{1}\circ a,{\pi }_{2}\circ b\right),\left({\pi }_{2}\circ a,{\pi }_{1}\circ b\right):E\to ℕ$. A similar construction yields a rational numbers object $ℚ$.

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

1. Non-degenerate:

$\exists q:ℚ.\phantom{\rule{thinmathspace}{0ex}}q\in L;$\exists q\colon \mathbb{Q}.\, q \in L ;
$\exists r:ℚ.\phantom{\rule{thinmathspace}{0ex}}r\in U.$\exists r\colon \mathbb{Q}.\, r \in U .
2. Inward-closed:

$\forall q:ℚ.\phantom{\rule{thinmathspace}{0ex}}\forall r:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(\left(q\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((q \lt r \wedge r \in L) \implies q \in L) ;
$\forall q:ℚ.\phantom{\rule{thinmathspace}{0ex}}\forall r:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(\left(r\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:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(q\in L⇒\exists r:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(r\in L\wedge q\forall q\colon \mathbb{Q}.\, (q \in L \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge q \lt r))
$\forall q:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(q\in U⇒\exists r:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(r\in L\wedge r\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:ℚ.\phantom{\rule{thinmathspace}{0ex}}\forall r:ℚ.\phantom{\rule{thinmathspace}{0ex}}\left(q\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:ℚ.\phantom{\rule{thinmathspace}{0ex}}¬\left(q\in L\wedge q\in U\right).$\forall q\colon \mathbb{Q}.\, \neg(q \in L \wedge q \in U) .

The relation $<$ on $ℚ$ is the order relation constructed in the usual way. We define $ℝ$ to be the subobject of $𝒫\left(ℚ\right)×𝒫\left(ℚ\right)$ 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}\left(X\right)$ its category of sheaves. It is well-known that $\mathrm{Sh}\left(X\right)$ is a Grothendieck topos (and so, a fortiori, an elementary topos), and the constant sheaf functor $\Delta :\mathrm{Set}\to \mathrm{Sh}\left(X\right)$ preserves finite limits and has the global section functor $\Gamma :\mathrm{Sh}\left(X\right)\to \mathrm{Set}$ as a right adjoint. (Hence, $\Delta$ and $\Gamma$ are the components of a geometric morphism $\mathrm{Sh}\left(X\right)\to \mathrm{Set}$.) The following claims are essentially immediate:

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

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

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

Thus, for every topological space $X$, the topos $\mathrm{Sh}\left(X\right)$ has a Dedekind real numbers object $ℝ$. Naïvely one might expect $ℝ$ to be isomorphic to the constant sheaf $\Delta \left(R\right)$, 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:

###### Theorem

A Dedekind real numbers object $ℝ$ in the topos $\mathrm{Sh}\left(X\right)$ is isomorphic to the sheaf of real-valued continuous functions on $X$.

###### Proof

See Mac Lane and Moerdijk (Chapter VI, §8).

This allows us to define various further constructions on $X$ in internal terms in $\mathrm{Sh}\left(X\right)$; 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.)

Section D4.7 of