From TopCom, Volume 8, #1
In this note, originally posted as a discussion on a bulletin board, the author tries to correct misguided perceptions about topological and localic versions of Tychonoff's theorem.
On the Ask a Topologist Bulletin Board [1], someone asked "In [3], it is stated that Tychonoff's theorem is equivalent to the axiom of choice (AC), but [10] says that there is a choice-free proof of it (via locales). What is right?"
Henno Brandsma, the bulletin board maintainer, replied:
"It depends on your foundations. If you work in set theory = ZF axioms, then AC implies Tychonoff's theorem, and I even posted a proof once [2] (it's due to Kelly). But locales etc work in Category Theory, for which other foundations of maths are needed: at least classes and such stuff. So Category Theory assumes more and doesn't need AC in the same way. From what I've gathered, AC can be proved in Category Theory but the foundations are not as well understood (and often glossed over). It's a matter of what foundation for maths you believe in, really."
Chris Good added:
"Henno is right ... compactness in locales has enough choice built in to it that the Tychonoff product theorem holds for locales. In fact, you play the same kind of game in topological spaces. For example, with the standard definition of normality, you cannot prove Urysohn's Lemma without (some form of) AC. But if you redefine normality by saying that a space is normal iff there is a function assigning to each closed C subset of open U an open set V such that C is a subset of V and the closure of V is a subset of U, then Urysohn's Lemma becomes a theorem of ZF. Essentially all the choosing you need to do (plus a lot more beside) is now wrapped up in the function."
My own reply to these two replies is:
Having said that, the original question still remains unanswered. True, the category of locales has a subcategory (those with enough points) which is equivalent to a subcategory of spaces (those which are sober). Here I am using the word "category" as a convenient linguistic device-no category theory is really needed for the purposes of this discussion.
This equivalence uses choice (please don't ask me how equivalent this is to choice-it might be PIT but I don't remember anymore). Hence any proof for spaces using locales would anyway require choice.
However, even with the equivalence, we don't get Tychonoff for spaces from Tychonoff for locales. The reason is that a product of locales with enough points doesn't have enough points itself in general (even in the binary case).
What is compactness for a locale? Ok, we must first say what a locale is. A frame is a complete lattice with finite meets that distribute over arbitrary joins. Hence the topology of a topological space is, by definition, a subframe of a powerset. Locale theory considers frames which don't necessarily arise in this way. Such frames are the topologies of generalized spaces which are called locales. A locale can be identified with the largest member of its topology (i.e., the biggest open). The definition of compactness for locales is the same as that for spaces: a locale is compact if and only if any of its open covers has a finite subcover.
So, the choice-free proof is not achieved by changing the definition of compactness and building choice functions into it. But how does choice manage to vanish? One reason is that products of locales don't in general coincide with those of spaces (although they do in important cases). But this is not the main reason. Suppose that you have some locales which are actually (sober) spaces (i.e., their topologies are subframes of powersets), and that their product is again a space. It is this last step which (when true) requires choice.
In other words, Tychonoff shows that a product of compact locales is compact, but doesn't say anything about the spatiality of the product. For references to the localic Tychonoff theorem, see Johnstone's survey on the history of locales [8].
One can say that the points are to blame: it is our insistence in having subframes of powersets that makes us dependent on choice in topology. By ignoring the question of whether the frames that one has at hand happen to be subframes of powersets, the axiom of choice is avoided in several theorems in locale theory.
(Even more remarkably, not even the principle of excluded middle is needed for most important theorems, including Tychonoff. The principle of excluded middle "(p or not p) for every proposition p" is equivalent to saying that powersets are boolean algebras. (Without it, we can still prove that they are frames and even completely distributive lattices.) The lattice of sublocales of a locale is not complemented (even assuming the principle of excluded middle), but the open sublocales do have boolean complements (the closed sublocales, of course), which doesn't require excluded middle, as opposed to the situation in the topological case.)
But most mathematicians don't like logic or foundations: There are some marvelous things that happen in the mathematical world of locales.
A subgroup of a topological group doesn't need to be closed (which is something one would like to be true, and hence there are many closed-subgroup theorems ensuring that this is the case in favourable circumstances). But a subgroup of a localic group is always closed [5, 7].
Products of paracompact locales are again paracompact. This fails for spaces. In particular, if you take two paracompact spaces, and hence locales, and form their product in the category of locales, you get a locale which is paracompact-but this locale can't be a space.
And now, believe it or not: every locale has a smallest dense sublocale (in particular, intersections of dense sublocales are dense-a rather strong form of the Baire category theorem). Sober spaces, and in particular Hausdorff spaces, and in particular the real line, are locales. If you take the intersection of the rationals and the irrationals, you of course get the empty space (this is the largest subspace contained in both). But if you take this intersection in the lattice of sublocales (the largest sublocale contained in both), you get a non-trivial dense sublocale, which doesn't have points. However, it still has plenty of opens, to the extent that continuous maps from the real line to itself are uniquely determined by their retriction to this dense sublocale.
(And, as a joke, but is true: one can now explicitly exhibit a non-measurable sublocale. Take the interval [0,1] regarded as a space, and hence a locale, in the usual way. Its smallest dense sublocale has outer measure one, because its open neighbourhoods are the dense open sets of [0,1]. However, because it doesn't have compact sublocales other than the null sublocale, it has inner measure zero.)
The book on locale theory is Johnstone's Stone spaces [6], published by CUP in 1982, but obviously there have been many developments since then. Part of them are contained in his 2002 two-volume book Sketches of an Elephant: A topos theory compendium [9], published by OUP, in chapters C1 and C4 of volume 2. Unfortunately, there is no textbook on locales for beginners.
The idea of regarding frames as the topologies of generalized (sober) spaces is due to Isbell [4], who proved the results on products of paracompact locales and smallest dense sublocales, among others. Using modern terminology, the title of Isbell's paper translates to Pointfree sublocales of topological spaces.