The function \(\eta _A\) is injective: lemma 4 gives that if \(U_a = \operatorname*{\mathsf{Spec}}(A)\) then \(a = 1\). Now if \(a \neq b\) then \((\neg a \vee b) \wedge (\neg b \vee a) \neq 1\), from which one gets that \(\eta (a) \neq \eta (b)\) (this is the Boolean algebra version of the usual argument that a ring homomorphism is injective if it has zero kernel).

The function \(\eta _A\) is surjective: Let \(K \subseteq \operatorname*{\mathsf{Spec}}(A)\) be clopen. By proposition 14, since \(K\) is open, there exists \(I \subseteq A\) such that \(K = \bigcup _{a \in I} U_a\). Since \(K\) is closed and \(\operatorname*{\mathsf{Spec}}(A)\) is compact, \(K\) is compact. Pick a finite subset \(F \subseteq I\) such that \(K = \bigcup _{a \in F} U_a\). By lemma 12, we get \(K = U_{a_0} = \eta _A(a_0)\), where \(a_0 \stackrel{\mathrm{def}}{=}\bigvee F\).

Note that, for any \(x \in X\),

\(\epsilon _X\) is continuous: By proposition 14 and a general fact about continuous functions, it suffices to check that \(\epsilon _X^{-1}(U_K)\) is open for every \(K \in \operatorname*{\mathsf{Clp}}(X)\). This set is equal to \(K\) by lemma 22, and thus open.

\(\epsilon _X\) is injective: For any \(x,y \in X\), if \(x \neq y\), then there is \(K \in \operatorname*{\mathsf{Clp}}(X)\) such that \(x \in K\) and \(y \not\in K\), using the characterization of Boolean spaces given in proposition 7. Thus, \(\epsilon _X(x)(K) = 1\) while \(\epsilon _X(x)(K) = 0\).

\(\epsilon _X\) is surjective: Let \(\xi \in \operatorname*{\mathsf{Spec}}(\operatorname*{\mathsf{Clp}}(X))\). Consider \(F \stackrel{\mathrm{def}}{=}\xi ^{-1}(1) = \{ K \in \operatorname*{\mathsf{Clp}}(X) \ \mid \ \xi (K) = 1\} \). Note that, for any finite collection \(\{ K_1,\dots ,K_n\} \subseteq F\), we also have \(\bigcap _{i=1}^n K_i \in F\), and in particular the intersection is non-empty, since \(\emptyset \not\in F\). Thus, since \(X\) is compact and \(F\) is a filter of closed(-and-open) sets which does not contain \(\emptyset \), the intersection \(\bigcap F\) is non-empty. Pick \(x \in \bigcap F\). We claim that \(\epsilon _X(x) = \xi \). Let \(K \in \operatorname*{\mathsf{Clp}}(X)\) be arbitrary, we need to show that \(\epsilon _X(x)(K) = \xi (K)\). There are two cases. If \(K \in F\), then \(x \in K\), so \(\epsilon _X(x)(K) = 1= \xi (K)\). Otherwise, \(K \not\in F\). Then \(\xi (K) = 0\), and, using that \(\xi \) is a homomorphism, we have \(\xi (K^\c ) = \neg \xi (K) = 1\). Thus, \(K^\c \in F\), from which we get that \(x \in K^\c \), so \(\epsilon _X(x)(K) = 0\), as required.

Now \(\epsilon _X\) is a homeomorphism because it is a continuous bijection from a compact to a Hausdorff space.

Let \(h \colon A \to B\) be a homomorphism and \(a \in A\). For any \(x \in \operatorname*{\mathsf{Spec}}(B)\), we have

where the last equivalence follows from the definitions of \(\operatorname*{\mathsf{Clp}}\) and \(\operatorname*{\mathsf{Spec}}\) on morphisms. We conclude that \(\eta _B(h(a)) = (\operatorname*{\mathsf{Clp}}\circ \operatorname*{\mathsf{Spec}})(h)(\eta _A(a))\), as required.

Let \(f \colon X \to Y\) be a continuous function and \(x \in X\). Write \(\xi _1 \stackrel{\mathrm{def}}{=}\epsilon _Y(f(x))\) and \(\xi _2 \stackrel{\mathrm{def}}{=}((\operatorname*{\mathsf{Spec}}\circ \operatorname*{\mathsf{Clp}})(f))(\epsilon _X(x))\). For any \(K \in \operatorname*{\mathsf{Clp}}(Y)\), we have

where the last equivalence again follows from the definitions of \(\operatorname*{\mathsf{Spec}}\) and \(\operatorname*{\mathsf{Clp}}\) on morphisms. Thus, \(\xi _1 = \xi _2\).

Let \(A\) be a Boolean algebra. We write \(f \stackrel{\mathrm{def}}{=}\operatorname*{\mathsf{Spec}}\eta _A \colon \operatorname*{\mathsf{Spec}}\operatorname*{\mathsf{Clp}}\operatorname*{\mathsf{Spec}}A \to \operatorname*{\mathsf{Spec}}A\) and \(g \stackrel{\mathrm{def}}{=}\epsilon _{\operatorname*{\mathsf{Spec}}A} \colon \operatorname*{\mathsf{Spec}}A \to \operatorname*{\mathsf{Spec}}\operatorname*{\mathsf{Clp}}\operatorname*{\mathsf{Spec}}A\); we need to prove that \(f \circ g\) is the identity. ¹ Let \(x \in \operatorname*{\mathsf{Spec}}A\). We want to show that \(x = (f \circ g)(x)\). Write \(y \stackrel{\mathrm{def}}{=}g(x)\). By definition of \(g\), we have, for any \(K \in \operatorname*{\mathsf{Clp}}\operatorname*{\mathsf{Spec}}A\), that \(y(K) = 1\iff x \in K\). By definition of \(f\), we have, for any \(a \in A\), that \(f(y)(a) = 1\iff y(\eta _A(a)) = 1\). Combining these two facts, we see that, for any \(a \in A\), \(f(y)(a) = 1 \iff x \in \eta _A(a) \iff x(a) = 1\), by definition of \(\eta _A\). Thus, \(f(g(x)) = f(y) = x\).