During my attempts to understand the fearsomely difficult Part III course “Introduction to Category Theory” by PT Johnstone, I came across the monadicity of the power-set functor . The monad is given by the triple , where , and is the union operator. So .
It’s easy enough to check that this is a monad. We have a theorem saying that every monad has an associated “Eilenberg-Moore” category - the category of algebras over that monad. What, then, is the E-M category for this monad?
Recall: an algebra over the monad is a pair where is a set and , such that the following two diagrams commute. (That is, here is an operation which takes a collection of elements of , and returns an element of .)
Aha! The second diagram says that the operation is “massively associative”: however we group up terms and successively apply to them, we’ll come up with the same answer. Mathematica calls this attribute “Flat“ness, when applied to finite sets only.
Moreover, it doesn’t matter what order we feed the elements in to , since it works only on sets and not on ordered sets. So is effectively commutative. (Mathematica calls this “Orderless”.)
The first diagram says that applied to a singleton is just the contained element. Mathematica calls this attribute “OneIdentity”.
Finally, , because is implemented by looking at a set of inputs.
So what is an algebra over this monad? It’s a set equipped with an infinitarily-Flat, OneIdentity, commutative operation which ignores repeated arguments. If we forgot that “repeated arguments” requirement, we could use any finite set with any commutative monoid structure; the nonnegative reals with infinity, as a monoid, with addition; and so on. However, this way we’re reduced to monoids which have an operation such that . That’s not many monoids.
What operations do work this way? The Flatten-followed-by-Sort operation in Mathematica obeys this, if the underlying set is a power-set of a well-ordered set. The union operation also works, if the underlying set is a complete poset - so the power-set example is subsumed in that.
Have we by some miracle got every algebra? If we have an arbitrary algebra , we want to define a complete poset which has acting as the union. So we need some ordering on ; and if , we need . That looks like a fair enough definition to me. It turns out that this definition just works.
So the Eilenberg-Moore category of the covariant power-set functor is just the category of complete posets.
(Subsequently, I looked up the definition of “complete poset”, and it turns out I mean “complete lattice”. I’ve already identified the need for unions of all sets to exist, so this is just a terminology issue. A complete poset only has sups of directed sequences. A complete lattice has all sups.)