Skip to main content
2 of 3
added 250 characters in body
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

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.

As 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.

Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58