The Tychonoff theorem is a theorem of topology, which in its classical form is equivalent to the axiom of choice. Spellings vary; the theorem is named after Андрей Николаевиц Тихонов, whose name becomes ‘Andrey Nikolayevich Tikhonov’ in modern English (BGN/PCGN) transliteration, but he originally published in German as ‘A.N. Tychonoff’.
The theorem states that a product of spaces (indexed over an arbitrary set) is compact if each of the spaces is compact. (Compare the axiom of choice: a product of sets is inhabited if each set is inhabited.)
Notice that no choice whatsoever is needed to prove the analogous theorem for locales: even in constructive mathematics, a product of locales is compact if each of the locales is compact. From that perspective, the statement equivalent to the axiom of choice is this: a product of locales is spatial if each of the locales is spatial. Either of these may be considered a Tychonoff theorem for locales.
To prove the Tychonoff theorem for Hausdorff spaces only, the full axiom of choice is not needed; the ultrafilter theorem (and possibly excluded middle) are enough.
One method of proof uses ultrafilter convergence. Let be a family of compact spaces.
Every ultrafilter on the underlying set of converges to some point . (Consider the collection of all closed sets belonging to . Finite subcollections have nonempty intersection, so by compactness the intersection of the collection is also nonempty. Let be a point belonging to that intersection. Every closed set disjoint from belongs to the complement of , hence every open set containing belongs to , i.e., converges to .)
Let be an ultrafilter on . Since the set-of-ultrafilters construction is functorial, we have a push-forward ultrafilter on each , where is a projection map. Choose a point to which converges. Then it is easily checked that converges to the point in the product space.
Since every ultrafilter on converges to a point, the product is compact. (If it were not, then we could find a collection of nonempty closed sets whose intersection is empty, but closed under finite intersections. This collection generates a filter which is contained in some ultrafilter , by the ultrafilter theorem. Since every ultrafilter converges to some , it cannot contain any closed set in the complement of , hence cannot contain some closed set in the original collection, contradiction.)
Todd: Here it’s not so clear that there’s any direct argument. For it’s at this point where we have to use the ultrafilter theorem, in order to produce a witnessing ultrafilter. Witness to what? The statement as it stands involves universal quantification over ultrafilters, so the witness would be in view of a contradiction.
Toby: Note that we use excluded middle in two places for a proof by contradiction; I'll try to remove these if possible. (Todd: I’ve rearranged the argument in the first step; the first formulation I gave looked unnecessarily “choice-y”.) We use the axiom of choice in the middle step to combine the into a single family ; if the were Hausdorff, then the would be unique, and we would not need the axiom of choice here. Finally, we use the ultrafilter theorem in the last step.
Todd: Yes, although I’m not too fussed about using indirect arguments, since in a topos, excluded middle follows from AC. I don’t know whether it also follows from a weaker choice principle equivalent to the ultrafilter theorem, but I guess I wouldn’t be surprised if it did.
Toby: As far as I know, UF and EM are independent (although I'm not certain). So I'm interested in whether the Hausdorff case requires EM as well as UF.
Todd: I wrote John Bell about this, and he kindly responded. Apparently you are right: UF (or BPIT) implies only a weakened version of EM: . He referred me to his paper Boolean Algebras and Distributive Lattices Treated Constructively, for this (among much else).
Toby: Great, hard results! Although I'm not sure that his ultrafilter theorem is the same as mine, since he talks about ultrafilters in arbitrary distributive lattices, while I would use a constructively stronger definition of ultrafilter in a powerset. But I should be able to figure out what carries over, now that I have a result to go for.
Now we will prove that the Tychonoff theorem implies the axiom of choice, while the Tychonoff theorem for Hausdorff spaces implies the ultrafilter theorem. This is done by judicious choice of examples.
Tychonoff theorem implies axiom of choice: let be a family of nonempty sets. Let be obtained by adjoining a point to . Topologize by taking the nontrivial open sets to be and . Then is compact; assuming Tychonoff, is compact. For each , put
Then is closed, and any finite intersection of the is nonempty (use in all but finitely many components). Hence
is nonempty as well, by compactness. Thus the axiom of choice follows.
Tychonoff theorem for Hausdorff spaces implies ultrafilter theorem: let be a filter on a set , i.e., a filter in the Boolean algebra . An ultrafilter containing is tantamount to a Boolean algebra map which sends all of to 1, or equivalently to a Boolean algebra map . Thus it suffices to construct a Boolean algebra map for any Boolean algebra .
Let denote the underlying set of . The set of all functions is a -indexed product of copies of 2; considering 2 as a compact Hausdorff space, this set is compact Hausdorff, assuming the Tychonoff theorem for Hausdorff spaces. For each finite subset , let be the set of functions for which the equations
hold for all . Then is a closed subset of the topological space , and it is easy (and classical) that it is nonempty (the subalgebra generated by is finite and admits such an , and we can take for any outside ). By compactness, the intersection of all the is nonempty, and this is precisely the set of Boolean algebra maps . Thus the ultrafilter theorem follows.