Todd Trimble Tychonoff theorem for locales


Statement and introduction

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.

Frames and the category of sup-lattices

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 SupSup consisting of sup-lattices.

The category of frames is the full subcategory of the category of commutative quantales (Q,,1)(Q, \cdot, 1), consisting of the idempotent commutative quantales, meaning that x1x \leq 1 for all xQx \in Q (the quantale unit 11 is the top element \top), and xx=xx \cdot x = x for all xQx \in Q.


(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 (Sup,)(Sup, \otimes), the coproduct of two commutative quantales P,QP, Q is given by the tensor product PQP \otimes Q in SupSup. This is just the dual form of the general result recounted here. Thus the binary coproduct of two frames X,YX, Y is their sup-lattice tensor product XYX \otimes Y. The nullary coproduct is the monoidal unit in SupSup. Furthermore,


(Joyal-Tierney) The forgetful functor FrameSupFrame \to Sup preserves and reflects filtered colimits. Thus the coproduct of a family of frames {F i} iS\{F_i\}_{i \in S} may be computed as

iSF i=colim finiteFS iFF i\sum_{i \in S} F_i = colim_{finite\; F \subseteq S} \otimes_{i \in F} F_i

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.

Symmetric monoidal closed structure for sup-lattices

The closed structure of SupSup has internal homs [X,Y][X, Y], the poset of sup-preserving maps between sup-lattices X,YX, Y, 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 Ladj(X,Y)Ladj(X, Y). Note that sup-lattices are inf-lattices (a poset XX is a sup-lattice iff X opX^{op} is a sup-lattice), and it will be convenient also to consider Radj(X,Y)Radj(X, Y), the sup/inf-lattice of right adjoints XYX \to Y.

We specially point out the sup-lattice 2={01}\mathbf{2} = \{0 \leq 1\} (if we are generalizing from SetSet to a topos, we use instead the subobject clasifier Ω\Omega which is an internal sup-lattice). This is the unit for the smc structure on SupSup: we have [2,X]X[\mathbf{2}, X] \cong X. Its opposite 2 op\mathbf{2}^{op} or Ω op\Omega^{op} plays the role of dualizing object: homming into it, we calculate

Ladj(X,2 op)Radj(2 op,X) opLadj(2,X op)X op.Ladj(X, \mathbf{2}^{op}) \cong Radj(\mathbf{2}^{op}, X)^{op} \cong Ladj(\mathbf{2}, X^{op}) \cong X^{op}.

Here the first isomorphism takes a left adjoint f:X2 opf: X \to \mathbf{2}^{op} to its right adjoint g:2 opXg: \mathbf{2}^{op} \to X in the opposite direction, and it also reverses 2-cells, i.e., takes an inequality fff \leq f' of left adjoints to a mated inequality ggg' \leq g of right adjoints. The second isomorphism is a case of taking a functor g:2 opXg: \mathbf{2}^{op} \to X to its opposite g op:2X opg^{op}: \mathbf{2} \to X^{op}; this reverses direction of 2-cells. The double dual embedding

XLadj(Ladj(X,2 op),2 op)X \to Ladj(Ladj(X, \mathbf{2}^{op}), \mathbf{2}^{op})

is thus identified (up to canonical isomorphism) with

XidX opop=XX \stackrel{id}{\to} X^{op\; op} = X

making 2 op\mathbf{2}^{op} a dualizing object: the smc category SupSup is a *\ast-autonomous category, with () *=() op:Sup opSup(-)^\ast = (-)^{op}: Sup^{op} \to Sup.

Being a *\ast-autonomous category, we have an isomorphism XY[X,Y op] opX \otimes Y \cong [X, Y^{op}]^{op}. This results from the isomorphisms

(XY) opLadj(XY,2 op)Ladj(X,Ladj(Y,2 op))Ladj(X,Y op).(X \otimes Y)^{op} \cong Ladj(X \otimes Y, \mathbf{2}^{op}) \cong Ladj(X, Ladj(Y, \mathbf{2}^{op})) \cong Ladj(X, Y^{op}).

This observation saves us from having to construct XYX \otimes Y explicitly as a coequalizer of a free sup-lattice P(X×Y)P(X \times Y) (of 2\mathbf{2}-valued presheaves on the poset X×YX \times Y). We may thus write

XYRadj(X op,Y);X \otimes Y \cong Radj(X^{op}, Y);

this isomorphism takes wXYw \in X \otimes Y to the right adjoint ϕ w:X opY\phi_w: X^{op} \to Y defined by ϕ w(u)= v:uvwv\phi_w(u) = \bigvee_{v: u \otimes v \leq w} v. Equally well, there is a canonical isomorphism XYRadj(Y op,X)X \otimes Y \cong Radj(Y^{op}, X) taking wXYw \in X \otimes Y to a right adjoint ψ w:Y opX\psi_w: Y^{op} \to X, and the pair (ϕ w,ψ w)(\phi_w, \psi_w) forms a contravariant Galois connection with ψ w opϕ w\psi_w^{op} \dashv \phi_w.


Recall the classical proof that a product of two compact topological spaces X,YX, Y is compact. A standard lemma, sometimes called the tube lemma, is that for any open cover AA of X×YX \times Y and any xXx \in X, there is an open neighborhood UU of xx such that U×YU \times Y is finitely covered by AA. Proof: Some finite subset FAF \subseteq A covers {x}×Y\{x\} \times Y; put W=FW = \bigcup F. For each yYy \in Y there are neighborhoods UU of xx and VV of yy such that UVWU \otimes V \leq W. The collection {V:xψ W(V)}\{V: x \in \psi_W(V)\} thus covers YY, hence there is a finite subcover V 1,,V nV_1, \ldots, V_n. Putting U= iψ W(V i)U = \bigwedge_i \psi_W(V_i), we have for all ii that V iϕ W(ψ W(V i))ϕ W(U)V_i \leq \phi_W(\psi_W(V_i)) \leq \phi_W(U) (the last inequality is by contravariance), hence Y= iV iϕ W(U)Y = \bigvee_i V_i \leq \phi_W(U), i.e., U×YWU \times Y \leq W.

Any wXYw \in X \otimes Y can be represented as a supremum of elements of the form uvu \otimes v, but one virtue of the identification XY[X,Y op] op:wϕ wX \otimes Y \cong [X, Y^{op}]^{op}: w \mapsto \phi_w is that it allows one to give a canonical such representation:


For sup-lattices X,YX, Y, the canonical representation of wXYw \in X \otimes Y (as a sup of tensors uvu \otimes v with uXu \in X, vYv \in Y) is w= uXuϕ w(u)w = \bigvee_{u \in X} u \otimes \phi_w(u).

Preframe representations


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 XX is compact if whenever its top element \top is the join of a directed subset JXJ \subseteq X, then J\top \in J. Equivalently,


Let XX be a frame, and let χ :X2\chi_\top: X \to \mathbf{2} be the characteristic map of the poset inclusion :1X\top: 1 \hookrightarrow X. Then XX is compact iff χ \chi_\top is a preframe map. (Of course ϕ \phi_\top 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 XX such that the binary join operation :X×XX\vee: X \times X \to X is a preframe map in each separate variable. Thus, frames can be described either as commutative monoids (X,,)(X, \wedge, \top) in the smc category of sup-lattices, or as commutative monoids (X,,)(X, \vee, \bot) 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 uvu \otimes v for elements uX,vYu \in X, v \in Y.


For elements uXu \in X and vYv \in Y in frames X,YX, Y, define their par uvu \parr v in the sup-lattice XYX \otimes Y by the formula uv=(u Y)( Xv)u \parr v = (u \otimes \top_Y) \vee (\top_X \otimes v).

The following proposition is easily checked.


(Johnstone-Vickers) If X,YX, Y are frames, then

  1. For each uXu \in X, the map u:YXYu \parr -: Y \to X \otimes Y is a preframe map, and similarly for each vYv \in Y the map v:XXY- \parr v: X \to X \otimes Y is a preframe map.

  2. The map :X×YXY\parr: X \times Y \to X \otimes Y preserves arbitrary sups (jointly in the two arguments).

  3. uv=(u Y)( Xv)u \otimes v = (u \parr \bot_Y) \wedge (\bot_X \parr v).


Given frames X,YX, Y, any finite join of tensors iFu iv i\bigvee_{i \in F} u_i \otimes v_i can be expressed as a finite meet of pars.


For each subset SFS \subseteq F, put u S iSu iu_S \coloneqq \bigvee_{i \in S} u_i and v S= iSv iv_S = \bigvee_{i \in S} v_i, and let ¬S\neg S denote the complement FSF \setminus S.

Exploiting Proposition 3 and finite distributivity in the frame XYX \otimes Y, we have

iFu iv i = iF(u i Y)( Xv i) = f:F{u,v}[( if 1(u)u i Y)( if 1(v) Xv i)] = SFu Sv ¬S\array{ \bigvee_{i \in F} u_i \otimes v_i & = & \bigvee_{i \in F} (u_i \parr \bot_Y) \wedge (\bot_X \parr v_i) \\ & = & \bigwedge_{f: F \to \{u, v\}} \left[(\bigvee_{i \in f^{-1}(u)} u_i \parr \bot_Y) \vee (\bigvee_{i \in f^{-1}(v)} \bot_X \parr v_i)\right] \\ & = & \bigwedge_{S \subseteq F} u_S \parr v_{\neg S} }

which proves the proposition.

This leads to a canonical preframe representation of elements wXYw \in X \otimes Y in a frame coproduct, where ww is expressed as a directed join of finite meets of par expressions. We have

w = uXuϕ w(u) = finiteFX uFuϕ w(u) = fin.FX SF[( uSu)( uSϕ w(u))]\array{ w & = & \bigvee_{u \in X} u \otimes \phi_w(u) \\ & = & \bigvee_{finite\; F \subseteq X} \bigvee_{u \in F} u \otimes \phi_w(u) \\ & = & \bigvee_{fin.\; F \subseteq X} \bigwedge_{S \subseteq F} \left[(\bigvee_{u \in S} u) \parr (\bigvee_{u \notin S} \phi_w(u))\right] }

Finitary Tychonoff theorem

Now suppose X,YX, Y are compact frames, which by Proposition 2 means precisely that the characteristic maps χ X:X2\chi_{\top_X}: X \to \mathbf{2} and χ Y:Y2\chi_{\top_Y}: Y \to \mathbf{2} preserve directed joins and finite meets.


(Finitary Tychonoff theorem) The frame XYX \otimes Y 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 \parr denote its monoidal product. Then, as 2\mathbf{2} is a frame, the map :2×22\vee: \mathbf{2} \times \mathbf{2} \to \mathbf{2} is a preframe map in each separate variable, and thus induces a canonical preframe map (which we again denote by \vee): 222\mathbf{2} \parr \mathbf{2} \to \mathbf{2}. Since χ X\chi_{\top_X} and χ Y\chi_{\top_Y} are preframe maps by assumption, we may form a composite of preframe maps

XYχ Xχ Y222.X \parr Y \stackrel{\chi_{\top_X} \parr \chi_{\top_Y}}{\to} \mathbf{2} \parr \mathbf{2} \stackrel{\vee}{\to} \mathbf{2}.

Call this preframe map hh. Now, as remarked earlier, the preframe tensor XYX \parr Y gives the coproduct of XX and YY. Then one proves that h(w)=1h(w) = 1 implies w= XYw = \top_{X \parr Y}; that is to say, h=χ XYh = \chi_{\top_{X \parr Y}}, meaning that the coproduct of XX and YY 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 wXYw \in X \otimes Y from the previous section, define h:XY2h: X \otimes Y \to \mathbf{2} by the formula

h(w)= fin.FX SF[χ X( uSu)χ Y( uSϕ w(u))]h(w) = \bigvee_{fin.\; F \subseteq X} \bigwedge_{S \subseteq F} \left[\chi_{\top_X}(\bigvee_{u \in S} u) \vee \chi_{\top_Y}(\bigvee_{u \notin S} \phi_w(u))\right]

Now hh 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 \vee preserves directed joins and finite meets in separate variables, and that wϕ ww \mapsto \phi_w is a poset isomorphism (so preserves directed joins and finite meets).

Now suppose h(w)=1h(w) = 1. Then for some finite subset FXF \subseteq X we have, for every subset SFS \subseteq F, that either uSu= X\bigvee_{u \in S} u = \top_X or uSϕ w(u)= Y\bigvee_{u \notin S} \phi_w(u) = \top_Y. But since Xv= XY=u Y\top_X \parr v = \top_{X \otimes Y} = u \parr \top_Y for any uX,vYu \in X, v \in Y, we conclude

w = fin.FX SF( uSu)( uSϕ w(u)) = fin.FX SF XY = XY\array{ w & = & \bigvee_{fin.\; F \subseteq X} \bigwedge_{S \subseteq F} (\bigvee_{u \in S} u) \parr (\bigvee_{u \notin S} \phi_w(u)) \\ & = & \bigvee_{fin.\; F \subseteq X} \bigwedge_{S \subseteq F} \top_{X \otimes Y} \\ & = & \top_{X \otimes Y} }

Thus we have shown h=χ XYh = \chi_{\top_{X \otimes Y}} is a preframe map.


(Tychonoff theorem) An arbitrary coproduct of compact frames iIX i\sum_{i \in I} X_i is compact.


We may assume all the frames X iX_i are non-trivial, i.e. non-terminal. Then each coproduct inclusion iFX i jFX j\otimes_{i \in F} X_i \hookrightarrow \otimes_{j \in F'} X_j, where F,FF, F' are finite subsets of II and FFF \subseteq F', 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)

Revised on November 28, 2016 at 17:49:30 by Todd Trimble