Can a general version of the covariant powerset monad be derived from the universal property of power objects?

Question

As the title asks, I'm wondering if one can generally squeeze a "covariant power object monad" out of a topos (following the usual example in $\mathcal{Set}$ with functor part the direct image powerset functor), or if there's a nice counterexample showing why not.

I am guessing that the answer to this is negative, since I only see this monad discussed in the case of $\mathcal{Set}$ so I suspect it depends on more special properties of that category; in which case I'm curious what special properties make it work.

Edit: In particular, I understand the usual construction of the functor part, but have myself been unable to verify that the obvious candidates for the unit and multiplication actually work as such.

Answer 1

In fact, the answer is yes. The algebras for the monad are, of course, the internal complete join semilattices.

First things first: the unit $\eta_X : X \to P X$ is given by the transpose of the morphism $X \times X \to \Omega$ that classifies the diagonal $\Delta : X \to X \times X$. To see that it is a natural transformation, it is easiest to use internal logic: given $f : X \to Y$, we want to show $$x : X \vdash \exists_f (\eta_X (x)) = \eta_Y (f (x))$$ which by "extensionality" is equivalent to $$x : X, y : Y \vdash y \in \exists_f (\eta_X (x)) \leftrightarrow y \in \eta_Y (f (x))$$ which by definition of $\exists_f$ is equivalent to $$x : X, y : Y \vdash (\exists x' : X . x' \in \eta_X (x) \land f (x') = y) \leftrightarrow y \in \eta_Y (f (x))$$ which by definition of $\eta$ is equivalent to $$x : X, y : Y \vdash (\exists x' : X . x' = x \land f (x') = y) \leftrightarrow y = f (x)$$ which is obviously a tautology.

The multiplication $\mu_X : P P X \to P X$ has a simple description in internal logic: $$\mu_X (t) = \left\{ x : X \mid \exists s : P X . s \in t \land x \in s \right\}$$ If you unfold this, it amounts to saying that $\mu_X$ is the transpose of the morphism $P P X \times X \to \Omega$ that classifies the image of the composite $$R \rightarrowtail P P X \times P X \times X \to P P X \times X$$ where the second arrow is the obvious projection and the first arrow is defined by the following pullback diagram, $$\require{AMScd} \begin{CD} R @>>> [\ni] \times [\ni] \\ @VVV @VVV \\ P P X \times P X \times X @>>{\mathrm{id} \times \Delta \times \mathrm{id}}> P P X \times P X \times P X \times X \end{CD}$$ where $[\ni] \rightarrowtail P P X \times P X$ and $[\ni] \rightarrowtail P X \times X$ are the universal binary relations. Of course, it would be a nightmare to verify that $\mu_X$ defined this way is natural in $X$, so it's better to stick with the description in internal logic. I leave the verification to you – naturality amounts to saying that $\exists$ commutes with $\exists$.

It remains to be shown that $\eta$ and $\mu$ satisfy the monad axioms. It should go without saying that the best way to proceed is to use internal logic.

• The left unit axiom is easy enough: it translates to $$s : P X \vdash \mu_X (\eta_{P X} (s)) = s$$ which is equivalent to $$s : P X, x : X \vdash x \in \mu_X (\eta_{P X} (s)) \leftrightarrow x \in s$$ which expands to $$s : P X, x : X \vdash (\exists s' : P X . s' \in \eta_{P X} (s) \land x \in s') \leftrightarrow x \in s$$ which expands to $$s : P X, x : X \vdash (\exists s' : P X . s' = s \land x \in s') \leftrightarrow x \in s$$ which is a tautology.
• The right unit axiom is more complicated: it translates to $$s : P X \vdash \mu_X (\exists_{\eta_X} (s)) = s$$ which is equivalent to $$s : P X, x : X \vdash x \in \mu_X (\exists_{\eta_X} (s)) \leftrightarrow x \in s$$ which is expands to $$s : P X, x : X \vdash (\exists s' : P X . s' \in \exists_{\eta_X} (s) \land x \in s') \leftrightarrow x \in s$$ which is expands to $$s : P X, x : X \vdash (\exists s' : P X . \exists x' : X . x' \in s \land \eta_X (x') = s' \land x \in s') \leftrightarrow x \in s$$ which is equivalent to $$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x \in \eta_X (x')) \leftrightarrow x \in s$$ which expands to $$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x = x') \leftrightarrow x \in s$$ which is a tautology.
• The associativity axiom is even more complicated to write out, but it is still straightforward – it amounts to the associativity of $\exists$.