2 Definitions and statement
I first recall some definitions from Mathlib. A subset \(S\) of a topological space is preconnected if, whenever \(U\) and \(V\) are open subsets such that \(S \subseteq U \cup V\), \(S \cap U \neq \emptyset \) and \(S \cap V \neq \emptyset \), we have \(S \cap U \cap V \neq \emptyset \). A topological space is totally disconnected if any preconnected subset is a subsingleton. A Boolean space is a compact Hausdorff totally disconnected space. 1 The category \(\mathbf{BoolSp}\) of Boolean spaces is the full subcategory of topological spaces based on Boolean spaces.
A Boolean algebra is by definition a bounded distributive lattice with complements. This means that it is a structure of the form \((A, \vee , \wedge , 0, 1, \neg )\) satisfying a number of axioms. We do not really care what the axioms are precisely. What is important to know is:
For any set \(X\), the structure \((\mathcal{P}(X), \cup , \cap , \emptyset , X, (-)^{\c })\) is a Boolean algebra.
In particular, I write \(\mathbf{2} = \{ 0, 1\} \) for the unique two-element Boolean algebra; it can be seen that it is a Boolean algebra because it is the power set algebra of a singleton set. A Boolean algebra homomorphism is a structure-preserving function between Boolean algebras. In fact, to be a homomorphism, it suffices to preserve \(\vee \), \(0\), and \(\neg \), because the operations \(1\) and \(\wedge \) are term-definable from those. In particular, for a subset \(S\) of a Boolean algebra \(A\) to be a subalgebra, it suffices for \(S\) to contain \(0\), and be closed under the operations \(\vee \) and \(\neg \). An ideal of a Boolean algebra is a subset \(I\) which contains \(0\) and is such that \(a \vee b \in I\) if, and only if, both \(a \in I\) and \(b \in I\) (this is equivalent to the usual definition for rings but formulated in a more convenient way for Boolean algebras). An ideal is proper if it does not contain \(1\). The partial order on a Boolean algebra \(A\) can be defined by \(a \leq b\) iff \(a \vee b = b\), or equivalently iff \(a \wedge b = a\). Our aim is to prove:
The categories \(\mathbf{BoolAlg}\) and \(\mathbf{BoolSp}\) are dually equivalent.
It will also be useful and interesting to actually have concrete definitions of the dual equivalence functors both ways, as we will do below.
An alternative proof, which is shorter on paper but does not give explicit access to the definition of the dual equivalence functors, would be to use the fact that any fully faithful essentially surjective functor is part of an equivalence (this is ). However, the inverse part of the equivalence that is produced by that fact only exists thanks to an application of axiom of choice, and it seems like it would be hard to work with. I could of course be wrong about this, and implementing this road towards the proof might be an interesting alternative experiment. It may have the advantage of avoiding getting into the weeds of natural transformation arguments as I need to do in proposition 24, proposition 25, and proposition 27 below.