The Tychonoff theorem for locales states that a small product of compact locales is compact. Remarkably, and in stark contrast to the Tychonoff theorem for compact spaces, this result requires only constructive reasoning for its proof; in particular, the axiom of choice (or some other choice principle) is not needed.
Our account of this result is adapted from Johnstone and Vickers, who provide a convenient conceptual niche for the Tychonoff theorem in terms of the closed category of preframes. Our plan here is to extract just enough from their account to give a relatively short proof of the Tychonoff theorem, without building up much of their theory of preframes – which is of interest in its own right of course and a source of conceptual explanation.
The key result is the finitary case, that the product of two compact locales is compact, or equivalently that the coproduct of two compact frames is compact. For topological spaces the standard argument is well-known, and appears regularly in undergraduate courses, but crucially uses spatiality (existence of enough points) as a kind of “crutch”. The reader might like to try his or her own hand at proving this result for general locales where the crutch is no longer available, to appreciate that a somewhat different approach may be needed even for the finitary case.
The category of locales is by definition opposite to the category of frames; following Joyal and Tierney, we consider frames as idempotent commutative monoids in the symmetric monoidal closed (smc) category consisting of sup-lattices.
The category of frames is the full subcategory of the category of commutative quantales , consisting of the idempotent commutative quantales, meaning that for all (the quantale unit is the top element ), and for all .
(Joyal-Tierney) The coproduct of a collection of frames coincides with their coproduct in the category of commutative quantales.
As commutative quantales are just commutative monoids in , the coproduct of two commutative quantales is given by the tensor product in . This is just the dual form of the general result recounted here. Thus the binary coproduct of two frames is their sup-lattice tensor product . The nullary coproduct is the monoidal unit in . Furthermore,
(Joyal-Tierney) The forgetful functor preserves and reflects filtered colimits. Thus the coproduct of a family of frames may be computed as
where the colimit is over the filtered diagram of finite subsets and inclusions between them.
Much of the proof of the Tychonoff theorem will be concentrated in explicit manipulations with sup-lattice tensor products; we turn to this next.
The closed structure of has internal homs , the poset of sup-preserving maps between sup-lattices , which are sup-lattices. As sup-preserving maps between sup-lattices are left adjoints (by an adjoint functor theorem), we may also denote the internal hom as . Note that sup-lattices are inf-lattices (a poset is a sup-lattice iff is a sup-lattice), and it will be convenient also to consider , the sup/inf-lattice of right adjoints .
We specially point out the sup-lattice (if we are generalizing from to a topos, we use instead the subobject clasifier which is an internal sup-lattice). This is the unit for the smc structure on : we have . Its opposite or plays the role of dualizing object: homming into it, we calculate
Here the first isomorphism takes a left adjoint to its right adjoint in the opposite direction, and it also reverses 2-cells, i.e., takes an inequality of left adjoints to a mated inequality of right adjoints. The second isomorphism is a case of taking a functor to its opposite ; this reverses direction of 2-cells. The double dual embedding
is thus identified (up to canonical isomorphism) with
making a dualizing object: the smc category is a -autonomous category, with .
Being a -autonomous category, we have an isomorphism . This results from the isomorphisms
This observation saves us from having to construct explicitly as a coequalizer of a free sup-lattice (of -valued presheaves on the poset ). We may thus write
this isomorphism takes to the right adjoint defined by . Equally well, there is a canonical isomorphism taking to a right adjoint , and the pair forms a contravariant Galois connection with .
Recall the classical proof that a product of two compact topological spaces is compact. A standard lemma, sometimes called the tube lemma, is that for any open cover of and any , there is an open neighborhood of such that is finitely covered by . Proof: Some finite subset covers ; put . For each there are neighborhoods of and of such that . The collection thus covers , hence there is a finite subcover . Putting , we have for all that (the last inequality is by contravariance), hence , i.e., .
Any can be represented as a supremum of elements of the form , but one virtue of the identification is that it allows one to give a canonical such representation:
For sup-lattices , the canonical representation of (as a sup of tensors with , ) is .
A preframe is a poset with directed joins and finite meets that distribute over directed joins. A preframe map is a poset map that preserves finite meets and directed joins.
A frame is a fortiori a preframe. As far as the Tychonoff theorem is concerned, the decisive advantage of preframes is that the notion of compactness of frames can be described categorically in terms of preframe maps.
Recall that a frame is compact if whenever its top element is the join of a directed subset , then . Equivalently,
Let be a frame, and let be the characteristic map of the poset inclusion . Then is compact iff is a preframe map. (Of course preserves finite meets for any frame, so the essential condition is preservation of directed joins).
An essential insight of Johnstone and Vickers is that since directed joins commute with finite meets, the theory of preframes is essentially a commutative theory, and thus the category of preframes forms a symmetric monoidal closed category; moreover, frames are exactly those preframes such that the binary join operation is a preframe map in each separate variable. Thus, frames can be described either as commutative monoids in the smc category of sup-lattices, or as commutative monoids in the smc category of preframes. In either case, coproducts of frames can be described as tensor products in either of these smc categories, with preframe tensors offering a description that is, roughly speaking, “De Morgan dual” to the sup-lattice tensor description.
This motivates a construction that is “De Morgan dual” to tensor products for elements .
For elements and in frames , define their par in the sup-lattice by the formula .
The following proposition is easily checked.
(Johnstone-Vickers) If are frames, then
For each , the map is a preframe map, and similarly for each the map is a preframe map.
The map preserves arbitrary sups (jointly in the two arguments).
.
Given frames , any finite join of tensors can be expressed as a finite meet of pars.
For each subset , put and , and let denote the complement .
Exploiting Proposition 3 and finite distributivity in the frame , we have
which proves the proposition.
This leads to a canonical preframe representation of elements in a frame coproduct, where is expressed as a directed join of finite meets of par expressions. We have
Now suppose are compact frames, which by Proposition 2 means precisely that the characteristic maps and preserve directed joins and finite meets.
(Finitary Tychonoff theorem) The frame is compact.
Before giving the proof, we might as well say where it comes from. We have remarked earlier that the category of preframes is symmetric monoidal closed; let denote its monoidal product. Then, as is a frame, the map is a preframe map in each separate variable, and thus induces a canonical preframe map (which we again denote by ): . Since and are preframe maps by assumption, we may form a composite of preframe maps
Call this preframe map . Now, as remarked earlier, the preframe tensor gives the coproduct of and . Then one proves that implies ; that is to say, , meaning that the coproduct of and is compact.
Or so this is how Johnstone and Vickers proceed; our account circumvents the building up of the closed category infrastructure of preframes which lies in the conceptual background.
Exploiting the canonical preframe representation of elements from the previous section, define by the formula
Now preserves directed joins and finite meets, due to the fact that directed joins and finite meets commute with directed joins and finite meets, and that preserves directed joins and finite meets in separate variables, and that is a poset isomorphism (so preserves directed joins and finite meets).
Now suppose . Then for some finite subset we have, for every subset , that either or . But since for any , we conclude
Thus we have shown is a preframe map.
(Tychonoff theorem) An arbitrary coproduct of compact frames is compact.
We may assume all the frames are non-trivial, i.e. non-terminal. Then each coproduct inclusion , where are finite subsets of and , is an embedding. (…)
Peter Johnstone and Steven Vickers, Preframe presentation present, in A. Carboni, M.C. Pedicchio, G. Rosolini (eds.) Category Theory (Proceedings, Como 1990), Springer Lectures Notes in Mathematics 1488 (1991), 193-212. (online pdf)
http://dml.cz/bitstream/handle/10338.dmlcz/106680/CommentatMathUnivCarol_029-1988-4_3.pdf