nLab real numbers object

Real numbers object


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


Real numbers object


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 \mathbb{R} in any topos with an NNO.

More generally, we can define a real numbers object (RNO) in any category with sufficient structure; RNOs can be defined for many flavors of category, from cartesian monoidal categories up to topoi. Then we can prove that an RNO exists in any topos with an NNO, as well as in some other situations.


Let \mathcal{E} be a Heyting category. (This means, in particular, that we can interpret full first-order intuitionistic logic using the stack semantics.)


A (located Dedekind) real numbers object in \mathcal{E} is a ring object in \mathcal{E} that satisfies (in the internal logic) the axioms of a Dedekind-complete strictly totally ordered Heyting field.

In detail:

A commutative ring object in \mathcal{E} is an object RR equipped with morphisms 0:1R0\colon \mathbf{1} \to R, :RR{-}\colon R \to R, +:R×RR{+}\colon R \times R \to R, 1:1R1\colon \mathbf{1} \to R, and :R×RR{\cdot}\colon R \times R \to R (where 1\mathbf{1} is the terminal object of \mathcal{E} and ×\times is the product operation in \mathcal{E}) that make the ring object diagrams commute.

Given a commutative ring object RR in \mathcal{E}, we define a binary relation #\# on RR (that is a subobject of R×RR \times R) as

{(x,y):R×R|z:R.xz=yz+1}, \{ (x,y)\colon R \times R \;|\; \exists z\colon R.\, x \cdot z = y \cdot z + 1 \} ,

written in the internal language of \mathcal{E}. Then RR is a (Heyting) field object if #\# is a tight apartness relation; that is if the following axioms (in the internal language) hold:

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

A (strictly totally) ordered field object in \mathcal{E} is a field object RR equipped with a binary relation <\lt such that the following axioms hold:

  • strong irreflexivity: x:R.y:R.(x<yx#y)\forall x\colon R.\, \forall y\colon R.\, (x \lt y \implies x \# y),
  • strong connectedness: x:R.y:R.(x#y(x<yy<x))\forall x\colon R.\, \forall y\colon R.\, (x \# y \implies (x \lt y \vee y \lt x)),
  • transitivity: x:R.y:R.z:R.((x<yy<z)x<z)\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, ((x \lt y \wedge y \lt z) \implies x \lt z),
  • respecting addition: x:R.y:R.z:R.(x<yx+z<y+z)\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, (x \lt y \implies x + z \lt y + z),
  • respecting multiplication: x:R.y:R.z:R.((x<y0<z)xz<yz)\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, ((x \lt y \wedge 0 \lt z) \implies x \cdot z \lt y \cdot z).

Given an ordered field object RR in \mathcal{E}, any object Γ\Gamma in \mathcal{E}, and subobjects LL and UU of Γ×R\Gamma \times R, we say that (L,U)(L,U) is a Dedekind cut in RR (parametrised by Γ\Gamma) if the following axioms hold:

  • lower bound: a:Γ.x:R.(a,x)L\forall a\colon \Gamma.\, \exists x\colon R.\, (a,x) \in L,
  • upper bound: a:Γ.x:R.(a,x)U\forall a\colon \Gamma.\, \exists x\colon R.\, (a,x) \in U,
  • downward roundedness: a:Γ.x:R.y:R.((x<y(a,y)L)(a,x)L)\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, ((x \lt y \wedge (a,y) \in L) \implies (a,x) \in L),
  • upward roundedness: a:Γ.x:R.y:R.(((a,x)Ux<y)(a,y)U)\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (((a,x) \in U \wedge x \lt y) \implies (a,y) \in U),
  • upward openness: a:Γ.x:R.((a,x)Lb:Γ.y:R.((b,y)Lx<y))\forall a\colon \Gamma.\, \forall x\colon R.\, ((a,x) \in L \implies \exists b\colon \Gamma.\, \exists y\colon R.\, ((b,y) \in L \wedge x \lt y)),
  • downward openness: a:Γ.x:R.((a,x)Ub:Γ.y:R.((b,y)Uy<x))\forall a\colon \Gamma.\, \forall x\colon R.\, ((a,x) \in U \implies \exists b\colon \Gamma.\, \exists y\colon R.\, ((b,y) \in U \wedge y \lt x)),
  • locatedness: a:Γ.x:R.y:R.(x<y((a,x)L(a,y)U))\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (x \lt y \implies ((a,x) \in L \vee (a,y) \in U)),
  • separation: a:Γ.x:R.y:R.(((a,x)L(a,y)U)x<y)\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (((a,x) \in L \wedge (a,y) \in U) \implies x \lt y).

An ordered field object RR in \mathcal{E} is Dedekind complete if, given any object Γ\Gamma of \mathcal{E} and any Dedekind cut (L,U)(L,U) in RR parametrised by Γ\Gamma, there exists a morphism x:ΓRx\colon \Gamma \to R such that

L={(a,b):Γ×R|b<x(a)}, L = \{ (a,b)\colon \Gamma \times R \;|\; b \lt x(a) \} ,
U={(a,b):Γ×R|x(a)<b}. U = \{ (a,b)\colon \Gamma \times R \;|\; x(a) \lt b \} .

Finally, a real numbers object in \mathcal{E} is a Dedekind-complete ordered field object.


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


This morphism is in fact unique.

Here is an explicit ‘external’ proof:


Suppose that x,x:ΓRx, x'\colon \Gamma \to R both satisfy the required properties, and consider x#xx \# x', which is a subobject of Γ\Gamma. By the strong connectedness of <\lt, x#xx \# x' is contained in (factors through) x<xx<xx \lt x' \vee x' \lt x, which is the union of x<xx \lt x' and x<xx' \lt x.

Now consider x<xx \lt x', and let aa be a generalised element of Γ\Gamma. If aa belongs to (factors through) x<xx \lt x', or equivalently (x(a),x(a))(x(a), x'(a)) belongs to <\lt, it follows that (a,x(a))(a,x(a)) belongs to LL. Thus, (x(a),x(a))(x(a), x(a)) also belongs to <\lt, or equivalently aa belongs to x<xx \lt x. By the strong irreflexivity of <\lt, this is contained in x#xx \# x; by the irreflexivity of #\#, this is contained in \bot (as a subobject of Γ\Gamma). Since every aa that belongs to x<xx \lt x' belongs to \bot, x<xx \lt x' is contained in (and so equals as a subobject) \bot.

Similarly (either by swapping xx with xx' or by using UU instead of LL), x<xx' \lt x is also \bot. Therefore, x#xx \# x' is \bot. By the tightness of #\#, x=xx = x'.

Here is an ‘internal’ proof, to be interpreted in the stack semantics of \mathcal{E}:


Suppose that x,x:Rx, x'\colon R both satisfy the required properties, and suppose that x#xx \# x'. By the strong connectedness of <\lt, x<xx \lt x' or x<xx' \lt x.

Now suppose that x<xx \lt x'. It follows that xx belongs to LL, so x<xx \lt x. By the strong irreflexivity of <\lt, x#xx \# x; by the irreflexivity of #\#, we have a contradiction.

Similarly (either by swapping xx with xx' or by using UU instead of LL), x<xx' \lt x is also false. Therefore, x#xx \# x' is false. By the tightness of #\#, x=xx = x'.

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.


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


It would be nice to say that a Heyting category with an RNO must have an NNO; after all, \mathbb{N} is contained in \mathbb{R}. However, my only argument is impredicative; although I don’t know a specific example, there could be a Π-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.)


If RR is an RNO in an infinitary Heyting category or topos, then there is unique subobject NN of RR that is both a sub-rig object of RR and an NNO under the operations 0:1N0\colon \mathbf{1} \to N and ()+1:NN({-}) + 1\colon N \to N.


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


If RR and RR' are both RNOs in a Heyting category \mathcal{E} with an NNO, then there is a unique isomorphism from RR to RR' that preserves the structures on them (00, -, ++, 11, \cdot, <\lt).



If RR is an RNOs in a Heyting category \mathcal{E} with an NNO and RR' is an Archimedean ordered field extension of RR, then there is a unique isomorphism from RR to RR' that preserves the structures on them (00, -, ++, 11, \cdot, <\lt).



Any RNO RR in a Heyting category \mathcal{E} with an NNO is the terminal Archimedean ordered field object in \mathcal{E}.



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 \mathcal{E} be an elementary topos with a natural numbers object \mathbb{N}. The Dedekind real numbers object of \mathcal{E} 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×a, b\colon E \to \mathbb{N} \times \mathbb{N} be the kernel pair of the addition map +:×{+}\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}, and let π 1,π 2:×\pi_1, \pi_2\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N} be the product projections. We define \mathbb{Z} to be the coequalizer of (π 1a,π 2b),(π 1b,π 2a):E(\pi_1 \circ a, \pi_2 \circ b), (\pi_1 \circ b, \pi_2 \circ a)\colon E \to \mathbb{N}. A similar construction yields a rational numbers object \mathbb{Q}.

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

  1. Non-degenerate:

    q:.qL; \exists q\colon \mathbb{Q}.\, q \in L ;
    r:.rU. \exists r\colon \mathbb{Q}.\, r \in U .
  2. Inward-closed:

    q:.r:.((q<rrL)qL); \forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((q \lt r \wedge r \in L) \implies q \in L) ;
    q:.r:.((r<qrU)qU). \forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((r \lt q \wedge r \in U) \implies q \in U) .
  3. Outward-open:

    q:.(qLr:.(rLq<r)) \forall q\colon \mathbb{Q}.\, (q \in L \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge q \lt r))
    q:.(qUr:.(rLr<q)). \forall q\colon \mathbb{Q}.\, (q \in U \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge r \lt q)) .
  4. Located:

    q:.r:.(q<r(qLrU)). \forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, (q \lt r \implies (q \in L \vee r \in U)) .
  5. Mutually exclusive:

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

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

In a Π\Pi-pretopos with WCCWCC

Summary: construct a Cauchy real numbers object and use WCCWCC (weak countable choice) to prove that it is an RNO.

Note that any Boolean topos with an NNO satisfies WCCWCC, 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.


In SetSet

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 SetSet is an elementary topos with an NNO (or more generally a Π-pretopos with NNO and either WCC or subset collection).

In sheaves on a topological space

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

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

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

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

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


A Dedekind real numbers object \mathbb{R} in the topos Sh(X)\mathrm{Sh}(X) is isomorphic to the sheaf of real-valued continuous functions on XX.

This is shown in (MacLane-Moerdijk, Chapter VI, §8, theorem 2); see also below.


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

In sheaves on a gros site of topological spaces


Let {}STop\{\mathbb{R}\} \hookrightarrow S \hookrightarrow Top be a small full subcategory of Top including the real line. If SS is closed under forming open subspaces and pullbacks of open subspaces and we equip it with the open-cover coverage, then the Dedekind real number object internal to Sh(S)Sh(S) is represented by 1\mathbb{R}^1.

This is proven as (MacLane-Moerdijk, chapter VI §9, theorem 2) under the stronger assumption that SS is closed under open subspaces and finite limits, by showing that over each object in the site the argument reduces essentially to that of theorem for that object. However, the finite limits are not necessary; see also below. The more general version includes the cases

(for which Sh(S)Sh(S) is cohesive topos and Sh (S)Sh_\infty(S) is an cohesive (∞,1)-topos).

In a general sheaf topos

We can generalize the above theorem as follows. Let SS be any site, and for any object XSX\in S let L(X)L(X) denote the locale whose frame of opens is the frame of subobjects of the sheafified representable yXSh(S)y X \in Sh(S). We have an induced functor L:SLocL:S\to Loc. We can also regard the ordinary real numbers \mathbb{R} as a locale.


The Dedekind real number object in Sh(S)Sh(S) is the functor Loc(L,)Loc(L-,\mathbb{R}).


The sheaf topos Sh()Sh(\mathbb{R}) is the classifying topos of the geometric theory of a real number, in the sense that for any Grothendieck topos EE, geometric morphisms ESh()E \to Sh(\mathbb{R}) are equivalent to global points of the real numbers object E\mathbb{R}_E in EE. Since pullback functors are logical, they preserve the real numbers object; thus for any XEX\in E, maps X EX\to \mathbb{R}_E are equivalent to geometric morphisms E/XSh()E/X \to Sh(\mathbb{R}). But Sh()Sh(\mathbb{R}) is localic, so such geometric morphisms factor through the localic reflection of E/XE/X, and therefore are equivalent to continuous \mathbb{R}-valued functions defined on the “little locale of XX”, i.e. the locale associated to the frame of subobjects of XX in EE.

Therefore, if E=Sh(S)E = Sh(S) for some site SS, then E\mathbb{R}_E is the sheaf on SS where E(X)=\mathbb{R}_E(X)= the set of continuous \mathbb{R}-valued functions on the little locale of yXEy X \in E, which is what we have called LXL X.

To deduce the previous theorem from this one, it suffices to observe that if STopS\subset Top is closed under open subspaces and their pullbacks and equipped with the open-cover coverage, then every subobject of yXSh(S)y X\in Sh(S), for any XSX\in S, is uniquely representable by an open subset of XX.

There is some dispute about this, see here.

Resolution seems to be here


Cauchy real numbers

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

Classical Dedekind real numbers

In any Π\Pi-pretopos with a NNO, one could define an object that roughly behaves like the Dedekind real numbers in classical mathematics. Instead of using subobjects of \mathbb{Q} in defining a cut, one instead uses the decidable morphisms L,U:11L, U: \mathbb{Q} \rightarrow 1\coprod 1 to define decidable cuts, and constructs the classical Dedekind real numbers as pairs of decidable cuts. The classical and constructive Dedekind real numbers are usually inequivalent, the classical Dedekind real numbers being equivalent to classical Cauchy real numbers and the constructive Dedekind real numbers being equivalent to generalised Cauchy real numbers


Discussion in topos theory is in

Discussion in homotopy type theory is in

Last revised on April 10, 2024 at 23:58:13. See the history of this page for a list of all contributions to it.