The category of topological spaces notoriously lacks some desirable features. There are therefore quite a few attempts to define “big” categories that contain (all) interesting topological spaces but are better behaved categorically. The topological topos was proposed in this vein by Peter Johnstone in the seventies. As it is conceptually based on sequential convergence it plays an important role in constructive mathematics.
Let Top be the category of topological spaces, and let be the full subcategory whose only two objects are a one-point space and , the one-point compactification of the discrete space of natural numbers. Let be the canonical Grothendieck topology on .
Johnstone’s topological topos (specifically, the one described in the eponymous paper) is the topos of canonical sheaves on . The functor
is faithful and factors through , and its restriction to the category of sequential spaces is full.
The category of subsequential spaces can also be found as a full subcategory of this topos (in fact, it consists of the separated objects for the double negation topology ). A general object of the topos can be thought of as being like a subsequential space, but such that a given sequence can converge to a given point in “more than one way.”
Importantly, following an idea by Joyal, the topological topos allows one to represent the geometric realization functor as the inverse image of a geometric morphism from to the topos of simplicial sets. As Johnstone points out, this approach fails for the big topos on and also for Lawvere’s topos for continuum mechanics.
In the internal logic of the topological topos, the limited principle of omniscience (LPO) for the natural numbers is false (and thus excluded middle also fails). Specifically, the space can be constructed internally as the subset of consisting of non-decreasing sequences, and the discrete space includes into it as the set of sequences that are 1 at exactly one place or 0 everywhere. Thus, the non-isomorphy of this map exhibits the failure of LPO.
Since the topological topos is generated by , it is in some sense a “canonical” topos where LPO fails. Moreover, if we localize at the inclusion , we get the subtopos of codiscrete objects, which is equivalent to ; so “forcing LPO to hold” gives classical logic.
On the other hand, the lesser limited principle of omniscience (LLPO) does hold in the topological topos. This is easiest to see from its “analytic” version, which is equivalent to saying that every real number is either or . Equivalently, this means that is surjective. This follows from Johnstone’s Proposition 6.2 on the preservation of closed unions, which implies that is the pushout of and over .
In particular, as Johnstone remarks, this implies that the quotient of the unit interval identifying its endpoints coincides with a “correct” constructive definition of the circle . It also implies that “every real number has a decimal expansion” (though there is no function assigning to every real number a decimal expansion, since no such function can be continuous).
One of the important facts about the topological topos is that its real numbers object is the set of classical real numbers equipped with its usual topology — or more precisely, with the structure of subsequential space given by the usual notion of convergence for sequences of real numbers (arising from the usual Euclidean topology).
In fact, there are two commonly used definitions of “real number” in a topos: the Dedekind real numbers and the Cauchy real numbers. In a general topos the two may not coincide, although they do coincide if the topos is Boolean or satisfies the axiom of countable choice. The topological topos is not Boolean, but does satisfy dependent choice and hence countable choice, see Shulman & Simpson 2024. Thus, the two real numbers objects coincide in the topological topos. In fact, both are the set of classical real numbers with its usual topology.
For the Dedekind real numbers, a proof of this can be found in Johnstone’s paper. Here we sketch a proof for the Cauchy reals.
The Cauchy real numbers object in the topological topos is the classical set of real numbers with its usual notion of sequential convergence.
For simplicity, we use Cauchy sequences with a fixed modulus: is Cauchy if for all . Note that if is the limit of such a Cauchy sequence, then for all , so convergence also has a fixed modulus.
Since the inverse image functor preserves natural numbers objects, the NNO of has the discrete structure (only eventually-constant sequences converge). And since constructively, the “rational numbers object” of is also discrete. It follows, by definition of exponentials in , that the object of sequences of rational numbers has the topology of “pointwise-eventually-constant convergence”: a sequence of sequences converges to a sequence if for each the sequence is eventually constant at .
Now the object of Cauchy sequences is a subobject of defined by
The predicate defines a subobject of , which is the pullback of the predicate on along the map defined by . Now is discrete, and every subobject of a discrete object in is (discrete and) relatively codiscrete, i.e. it has the induced topology. Thus, the predicate also has the induced topology. And since relatively codiscrete maps are the modal maps for a modality, they are closed under arbitrary universal quantification. So the object of Cauchy sequences has the topology induced from of pointwise eventually constant convergence.
In any topos, there is a monomorphism from the Cauchy real numbers to the Dedekind real numbers, and as remarked above, Johnstone proved that the latter have the usual topology. Moreover, it is easy to see that the points of the Cauchy real numbers object are precisely the classical real numbers: any classical Cauchy sequence certainly induces a Cauchy sequence internal to . Thus, it will suffice to show that the Cauchy subobject of the Dedekind reals also contains all convergent sequences.
To this end, suppose we have a sequence of Cauchy sequences and a Cauchy sequence (all in the above fixed-modulus sense) such that the sequence of real numbers converges to the real number in the usual sense. We want to show that this convergence also happens in the Cauchy real numbers object. To this end, define a new sequence of Cauchy sequences by setting if and otherwise. To show that is Cauchy, the only nontrivial case is to show that if ; but since converges to with fixed modulus, we have and the triangle inequality is our friend.
It is also evident that converges to , i.e. . Thus it will suffice to show that converges to in the Cauchy real numbers object. Let ; then and converges twice as fast, i.e. . We claim that is pointwise-eventually-constant convergent to . To see this, by the ordinary convergence of to , for each there exists an such that implies , and hence by the triangle inequality . Thus, by definition of , we have for all , which is to say that is eventually constant at .
Finally, since converges to in the object of Cauchy sequences, the image sequence in the object of Cauchy real numbers (the quotient by equivalence of Cauchy sequences) must also converge to there. Since and , this is what we wanted.
The topological topos was introduced in:
Peter Johnstone, Topos Theory , Academic Press New York 1977. (Dover reprint 2014; exercise 0.10, p.21)
Peter Johnstone, On a topological topos , Proc. London Math. Soc. (3) 38 (1979) 237-271 [pdf]
Review (with somewhat terminology):
Peter Johnstone, Sketches of an Elephant – A Topos Theory Compendium, Oxford UP 2002
see A2.1.11(j), A2.6.4(c), C2.2.14(b); pp. 81, 123,537f
Discussion in the context of convenient categories of spaces:
See also discussion at:
Proof that the topological topos satisfies dependent choice:
A higher topos-analogue of the topological topos models homotopy type theory:
Michael Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, 2015 [arXiv:1509.07584]
Martín Escardó, Thomas Streicher, The intrinsic topology of Martin-Lof universes, APAL (2016). (pdf)
Bas Spitters, Cubical sets and the topological topos , arXiv:1610.05270 (2016). (abstract)
Generalizations of its construction occur in the following two papers:
R. Montañez, Topoi generated by topological spaces , Talk CT15 Aveiro (2015) [pdf-slides]
C. Ruiz, R. Montañez, Elevadores de Estructura , Boletín de Matemáticas XIII 2 (2006) 111-135. [link]
Last revised on September 28, 2024 at 06:00:28. See the history of this page for a list of all contributions to it.