# What are the algebras of the double powerset monad?

Let $\mathscr{P} : \textbf{Set} \to \textbf{Set}^\textrm{op}$ be the (contravariant) powerset functor, taking a set $X$ to its powerset $\mathscr{P}(X)$ and a map $f : X \to Y$ to the inverse image map $f^* : \mathscr{P}(Y) \to \mathscr{P}(X)$. By elementary abstract nonsense, we know that $\mathscr{P}$ has a right adjoint $\mathscr{P}^\textrm{op}$: indeed,

$$\textrm{Hom}(X, \mathscr{P}(Y)) \cong \textrm{Hom}(X \times Y, \Omega) \cong \textrm{Hom} (Y \times X, \Omega) \cong \textrm{Hom}(Y, \mathscr{P}^\textrm{op} (X))$$

where $\Omega$ is the subobject classifier $\{ 0, 1 \}$ for $\textbf{Set}$. Let us write $\mathscr{T}$ for the composite $\mathscr{P}^\textrm{op} \mathscr{P}$; then we have a monad $(\mathscr{T}, \eta, \mu)$ on $\textbf{Set}$.

By advanced abstract nonsense (Paré's theorem or Mikkelsen's theorem) it can be shown that $\mathscr{P}$ is monadic, i.e. that the canonical comparison functor $\textbf{Set}^\textrm{op} \to \mathscr{T}\textbf{-Alg}$ is an equivalence of categories; but $\textbf{Set}^\textrm{op}$ is known to be equivalent to the category of complete atomic boolean algebras, so this therefore implies that a $\mathscr{T}$-algebra is the same thing as a complete atomic boolean algebra.

Question. How does one show this directly?

It is straightforward to check that $$\eta_X (x) = \{ S \subseteq X : x \in S \} = \mathord{\uparrow} (\{ x \})$$ and the multiplication map is $$\mu_X (V) = \bigcup_{U \in V} \{ S \subseteq X : \eta_{\mathscr{P} (X)}(S) = U \}$$ but I am having a lot of trouble getting any intuition for what $\mu_X$ does beyond how it is constructed: it recovers the set of all $S$ such that the principal filter $\mathord{\uparrow} (\{ S \})$ is a member of $V$. If $V$ itself is upwards-closed, then we have the formula $$\mu_X (V) = \bigcup_{U \in V} \bigcap_{T \in U} T$$ since for all $U \in V$, if $S \in T$ for all $T \in U$, we have $U \subseteq \mathord{\uparrow}(\{ S \})$, i.e. $$U \subseteq \bigcap \left\{ \mathord{\uparrow}(\{ S \}) : S \in \bigcap U \right\}$$ Thus, for $U \subseteq \mathscr{T}(X)$, $$\mu_X ( \mathord{\uparrow}(U) ) = \bigcap_{T \in U} T$$ and as a special case we obtain the left unit law $$\mu_X ( \eta_{\mathscr{T}(X)} (T) ) = T$$ This means that we can recover the meet operation of $\mathscr{T}(X)$ from $\mu_X$, regarded as the free complete atomic boolean algebra on $X$. We can also recover the join operation: $$\bigcup_{T \in U} T = \mu_X \left( \bigcup \left\{ \mathord{\uparrow} (\{ T \}) : T \in U \right\} \right)$$ (The use of $\bigcup$ in the RHS is legitimate since the join operation of $\mathscr{T}(\mathscr{T}(X))$ independent of the join operation of $\mathscr{T}(X)$.)

Now, I know that any complete lattice $A$ admits a canonical pseudocomplement operation $$\lnot a = \bigvee \{ a' \in A : a \wedge a' = \bot \}$$ but I have no idea how the properties of $\mu_X$ imply the ‘meet’ and ‘join’ operations we get satisfy the requirements for a (complete) boolean algebra, nor do I see where atomicity might be coming from.

-

The signature of complete atomic boolean algebras is the class of all functions $\{0,1\}^\kappa \to \{0,1\}$, where $\kappa$ can be any set. Up to canonical isomorphism, for any algebra $a:\mathscr{P}^2X\to X$ and any operator $P:\{0,1\}^\kappa \to \{0,1\}$, we have: $$X^Y \stackrel{(\eta_X)^\kappa}\longrightarrow \{0,1\}^{\mathscr PX\times \kappa} \stackrel{P^{\mathscr PX}}\longrightarrow \{0,1\}^{\mathscr P X} \stackrel a \longrightarrow X$$ This way every $\#\kappa$-ary operation on $\{0,1\}$ in implemented on $X$.
The algebraic theory of a CABA is the class of equations that are valid for all operators $\{0,1\}^\kappa \to\{0,1\}$, including negation $x\mapsto 1-x:\{0,1\}^{\mathbf 1} \to \{0,1\}$. So because in the topos of sets, double negation elimination is valid for $\Omega = \{0,1\}$, is must be valid for all CABAs. – Wouter Stekelenburg Mar 25 '12 at 15:14