$\mathbf{Loc}$ is the category of locales, and $\mathbb{P}$ is the double power locale monad on it. Consider the category $\mathbf{Loc}^{\mathbb{P}}$, of algebras of this monad. Does anyone know whether $\mathbf{Loc}^{\mathbb{P}}$ has coequalizers (and/or finitary coproduct)? Thanks, Christopher

Definition of double power locale monad:

Let $\mathbf{dcpo}$ be the category whose objects are directed complete partial orders and whose morphisms are directed join preserving maps (aka Scott continuous maps). Let $\mathbf{Fr}$ be the category whose objects are frames (complete Heyting algebras) and whose morphisms are frame homomorphisms (preserve finite meets and arbitrary jons). The forgetful functor $U: \mathbf{Fr} \rightarrow \mathbf{dcpo}$ has a left adjoint and so induces a comonad on $\mathbf{Fr}$; since $\mathbf{Loc}$ is by definition the opposite of $\mathbf{Fr}$ this gives a monad on $\mathbf{Loc}$; the double power locale monad.

  • $\begingroup$ Christopher, if you could either recall the definition of the double power locale monad, or provide a link to the definition that you think would be most convenient for this problem, that might help readers. Do you have partial progress on this problem? $\endgroup$
    – Todd Trimble
    Jan 18, 2014 at 0:38
  • $\begingroup$ Todd - the Kleisli category embeds (contravariantly) into the category of presheaves on Loc; every Kleisli category embeds into the category of algebras (for any monad) so I am hoping to represent (the opposite of) the category of algebras of the double power monad in this presheaf category. And since equalizers in the presheaf category are easy to construct this might give the required coequalizers. I've not focused on finding a counter-example, so perhaps there is some 'obvious' counter-example that someone might have knowledge of already, and that will put the problem to rest. $\endgroup$ Jan 18, 2014 at 17:55
  • $\begingroup$ Thanks very much, Christopher. I'm sure that you already know that as long as the base category is cocomplete (which is true for the case $\mathbf{Loc}$), if the category of algebras has reflexive coequalizers, then it has all colimits. I naively wondered whether the proof that the monadic functor for the double power-set monad on a topos creates reflexive coequalizers (passing through Beck-Chevalley conditions and so on) could somehow be adapted to your situation, but that's probably very naive since (I gather) you've been thinking on this problem a while. $\endgroup$
    – Todd Trimble
    Jan 18, 2014 at 18:36
  • $\begingroup$ As the "Related" sidebar suggests, this question is about the same topic. $\endgroup$ Jan 30, 2014 at 17:46

1 Answer 1


For anyone other than Chris Townsend or Steve Vickers, I think it is simpler just to ask about the forgetful and free functors $\mathbf{Frm}\rightleftarrows\mathbf{Dcpo}$ between the categories of frames and directed complete partial orders. Not altogether surprisingly, $\mathbf{Frm}$ is the category of algebras for the monad over $\mathbf{Dcpo}$.

There is a general question for any adjunction $\mathcal{C}\rightleftarrows\mathcal{D}$: Suppose we replace $\mathcal C$ by the category of algebras $\mathcal{C}'$ for the monad over $\mathcal D$ that is induced by the adjunction, then $\mathcal D$ by the category $\mathcal{D}'$ of coalgebras for the comonad on $\mathcal{C}'$, and so on.

In fact, this stabilises with the algebras over the coalgebras under the algebras, ie the next step is $\mathcal{D}''\cong\mathcal{D}'$. Indeed, only two steps are needed ($\mathcal{C}''\cong\mathcal{C}'$) if we started with categories in which idempotents split. Steve Lack first gave me the proof of this.

Now suppose in addition that the base category $\mathcal{D}$, in Chris's case $\mathbf{Dcpo}$, has finite products and the monad has a strength, which it does in the case of $\mathbf{Frm}$.

Then the category $\mathcal{D}'$ of coalgebras under the algebras also has finite products. These are the coproducts of algebras over $\mathbf{Loc}$ in Chris's question.

At least so it says in some notes of mine called underlyingset/universal possibly from March 2007. The proof is quite complicated and works with strong monads in the abstract rather than frames, though it was motivated by exactly this question. I might be persuaded to re-upload these notes into my brain to see whether the proof is correct.

The question of the existence of coequalisers of algebras for a monad (or equalisers in $\mathcal{D}'$ in my setting) is a notoriously difficult one.

The objects of the category $\mathbf{Dcpo}'$ in my notation above (which is the opposite of the category of algebras in Chris's question) are called localic locales by Steve Vickers and colocales by me.

If any progress is to be made with the investigation of this category and the furtherance of the motivations behind it, or even in getting more than three people interested, I think some more concrete description is needed of the objects.

Even abstractly, an object of $\mathcal C'$ admits at most one morphism that makes it a coalgebra (object of $\mathcal D'$). Hence a colocale is a special kind of frame, whilst of course a frame is a special dcpo.

The adjunctions that Chris considers in his question contain the monadic one that gives my programme Abstract Stone Duality its name as full subcategories.

The latter relates continuous frames to locally compact locales, so any continuous frame is a colocale. In particular, the free frame on any semilattice qua semilattice is continuous and therefore already a colocale.

My feeling is that Steve Vickers has already provided enough tools in his investigations of presentations of frames and of powerlocales, along with the methods of Formal Topology, to give a useful characterisation of colocales.

Using this, the colocale structure on (the free frame on) any semilattice would be described by some kind of modal logic.

Given the representation of a frame as a cover relation on a semilattice (or a nucleus on the free frame on this semilattice), the question would therefore appear to amount to asking whether the cover relation is compatible with the modal logic.

How can colocales be special frames but also generalise locally compact spaces? The mis-match comes from the application of the functor: the locally compact space corresponds to the colocale structure on its continuous frame of opens. Studying bases would eliminate this excessively free structure.

I look forward to seeing the results of Chris's investigations of this.

  • $\begingroup$ We know that the comonad on $\mathbf{Frm}$ induces a monad on the category of coalgebras. And we know that this 'stops after 2 steps', that is, the category of algebras of this monad is $\mathbf{Frm}$ itself. But I can't see how we can back out the existence of products in a category of algebras, to get products in the underlying category itself? Perhaps, when you say 'stops after two steps' you are saying that $\mathbf{dcpo}$ itself is equivalent to the category of coalgebras on $\mathbf{Frm}$? $\endgroup$ Feb 5, 2014 at 9:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.