Could not include topos theory - contents
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).
A commutative ring object in is an object equipped with morphisms , , , , and (where 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.)
A (linearly) ordered field object in is a field object equipped with a binary relation such that the following axioms hold:
Given an ordered field object in , any object in , and subobjects and of , we say that is a Dedekind cut in (parametrised by ) if the following axioms hold:
An ordered field object in is Dedekind complete if, given any object of and any Dedekind cut in parametrised by , there exists a morphism such that
Finally, a real numbers object in is a Dedekind-complete ordered field object.
In the last requirement, of Dedekind completeness, we postulate (under certain conditions) the existence of a morphism satisfying certain properties.
This morphism is in fact unique.
Here is an explicit ‘external’ proof:
Suppose that both satisfy the required properties, and consider , which is a subobject of . By the strong connectedness of , is contained in (factors through) , which is the union of and .
Now consider , and let be a generalised element of . If belongs to (factors through) , or equivalently belongs to , it follows that belongs to . Thus, also belongs to , or equivalently belongs to . By the strong irreflexivity of , this is contained in ; by the irreflexivity of , this is contained in (as a subobject of ). Since every that belongs to belongs to , is contained in (and so equals as a subobject) .
Similarly (either by swapping with or by using instead of ), is also . Therefore, is . By the tightness of , .
Here is an ‘internal’ proof, to be interpreted in the stack semantics of :
Suppose that both satisfy the required properties, and suppose that . By the strong connectedness of , or .
Now suppose that . It follows that belongs to , so . By the strong irreflexivity of , ; by the irreflexivity of , we have a contradiction.
Similarly (either by swapping with or by using instead of ), is also false. Therefore, is false. By the tightness of , .
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, is contained in . 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 is an RNO in an infinitary Heyting category or topos, then there is unique subobject of that is both a sub-rig object of and an NNO under the operations and .
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 and are both RNOs in a Heyting category with an NNO, then there is a unique isomorphism from to that preserves the structures on them (, , , , , ).
We can construct a real numbers object in the following cases (presumably among others):
(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.)
We first construct an integers object as follows. Let be the kernel pair of the addition map , and let be the product projections. We define to be the coequalizer of . A similar construction yields a rational numbers object .
We denote by the power object of in . A Dedekind cut is a generalized element of , satisfying the following conditions, expressed in the Mitchell–Bénabou language of and interpreted under Kripke–Joyal semantics:
The relation on is the order relation constructed in the usual way. We define to be the subobject of consisting of all Dedekind cuts as defined above.
Note that any Boolean topos with an NNO satisfies , so in all we have three different constructions available in that case.
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 is an elementary topos with an NNO (or more generally a Π-pretopos with NNO and either WCC or subset collection).
Let be a topological space, and its category of sheaves. It is well-known that is a Grothendieck topos (and so, a fortiori, an elementary topos), and the constant sheaf functor preserves finite limits and has the global section functor as a right adjoint. (Hence, and are the components of a geometric morphism .) The following claims are essentially immediate:
If is the set of natural numbers, then must be an NNO in , since has a right adjoint.
If is the set of integers, then is an integers object in (as defined above), since preserves finite limits and colimits.
Similarly, if is the set of rational numbers, then is a rational numbers object in .
Thus, for every topological space , the topos has a Dedekind real numbers object . Naïvely one might expect to be isomorphic to the constant sheaf , where 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 in the topos is isomorphic to the sheaf of real-valued continuous functions on .
This is shown in (MacLane-Moerdijk, Chapter VI, §8, theorem 2); see also below.
Let be a small full subcategory of Top including the real line. If 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 is represented by .
This is proven as (MacLane-Moerdijk, chapter VI §9, theorem 2) under the stronger assumption that 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 1 for that object. However, the finite limits are not necessary; see also below. The more general version includes the cases
We can generalize the above theorem as follows. Let be any site, and for any object let denote the locale whose frame of opens is the frame of subobjects of the sheafified representable . We have an induced functor . We can also regard the ordinary real numbers as a locale.
The Dedekind real number object in is the functor .
The sheaf topos is the classifying topos of the geometric theory of a real number, in the sense that for any Grothendieck topos , geometric morphisms are equivalent to global points of the real numbers object in . Since pullback functors are logical, they preserve the real numbers object; thus for any , maps are equivalent to geometric morphisms . But is localic, so such geometric morphisms factor through the localic reflection of , and therefore are equivalent to continuous -valued functions defined on the “little locale of ”, i.e. the locale associated to the frame of subobjects of in .
Therefore, if for some site , then is the sheaf on where the set of continuous -valued functions on the little locale of , which is what we have called .
To deduce the previous theorem from this one, it suffices to observe that if is closed under open subspaces and their pullbacks and equipped with the open-cover coverage, then every subobject of , for any , is uniquely representable by an open subset of .
It is also possible to define the notion of a Cauchy real number object and construct one in any -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.)
Discussion in topos theory is in
Discussion in homotopy type theory is in