In the previous post, we discussed extending algebraic operations on some set to operations on the powerset
. It turned out that the construction we used preserved linear equations, such as those used to define monoids. As promised, we now relate these ideas to monads.
Categories of Algebras
We will work with a category of algebras with:
- Objects: A set
, with a binary operation
and a constant
.
- Morphisms: A morphism
is a function
that preserves the binary operation and constant.
Equationally, the homomorphism conditions are:
The obvious forgetful functor will feature prominently in what follows.
Although we will restrict our discussions to this simple category of algebras, everything we discuss will generalise to categories of algebras with any number of operations with arbitrary arities.
Lifting the Powerset Functor
We would like to lift the powerset functor:
to a functor:
By lift we mean that these functors will commute with the forgetful functor as follows:
We already identified a suitable action on objects in the previous post. The lifting condition means there is only one potential action on morphisms:
This will automatically commute with identities and composition, but we must verify that it yields a legitimate algebra morphism. For the binary operation:
and for the constant:
Lifting the Powerset Monad
As we have successfully lifted the powerset functor, our next steps is to lift the powerset monad
to a monad:
to . By lifting, we mean a lifting of the powerset functor with unit
and
such that:
These conditions force that the unit and multiplication of the lifted monad have the same components as for the original powerset monad. We need to verify that these are legitimate algebra morphisms. For the unit:
and for the multiplication:
That’s actually all we have to check. Naturality of the unit and multiplication, and the monad axioms follow from the forgetful functor being faithful, and the lifting conditions.
Summing up, we have shown that we can lift the powerset monad to the category . Again, we can generalise, and lift the powerset monad to any category of algebraic structures.
Lifting the Powerset to Equational Classes
So far, we have lifted the powerset monad to categories of sets equipped with some completely unconstrained operations. This is moderately interesting, but normally we want such structures such as monoids which are required to satisfy some equations.
This is where the preservation of equations discussed in the previous post comes in. The object mapping
is such that satisfies any linear equation satisfied by
. This means we can restrict our lifted powerset monad to any class of algebras defined by linear equations. Intuitively, when we restrict to classes of algebras defined by linear equations, our lifted monad won’t “jump out” of the class we are interested in.
Example: The powerset monad lifts to the category of monoids, and the category of commutative monoids.
Example: This construction does not lift the powerset monad to the category of meet semilattices, as the idempotence equation is not linear, and will not be preserved in general.
Summing Up
We have shown that the powerset monad can be lifted to any category of algebras defined by linear equations. There are a few questions we should ask ourselves:
- Can we generalise this construction beyond the powerset to other monads?
- What’s going on with the mysterious linearity requirement on the equations?
- Can we do anything with classes of algebras defined by more general equations?
We will move onto these questions in subsequent posts.
One thought on “Lifting the Powerset Monad”