In the previous post, we introduced the Eilenberg-Moore category of a monad . It is of course convenient to have mechanisms for constructing new categories, but the Eilenberg-Moore category has a more fundamental purpose. As is usual in category theory, what matters is not just individual mathematical objects, but also their relationships to others.
For a monad on , there is a forgetful functor from the Eilenberg-Moore category to the base category , with action:
There is also a slightly less obvious free algebra functor in the other direction , with action:
There is an adjunction . To see this, we must show a natural bijection between:
- Eilenberg-Moore algebra morphisms .
- -morphism .
In one direction, we define mapping:
and in the the:
That this second mapping results in a valid algebra morphism follows from naturality of , and the Eilenberg-Moore algebra multiplication axiom. We then note that, using that is an algebra morphism, and one of the monad unit axioms:
In the other direction, using natural of , and the Eilenberg-Moore algebra unit axiom:
We therefore have the required bijection establishing the adjunction (leaving confirming naturality of the bijection as an exercise).
Now we consider the monad induced by this adjunction. The endofunctor action on objects is:
The unit of the monad has components the transpose of , that is . Finally, the multiplication at is , with the counit of the adjunction. is the transpose of , that is .
Putting all this together, we have seen that the monad induced by the Eilenberg-Moore adjunction is the original monad . This establishes a point we mentioned earlier. Every adjunction induces a monad, and as we have now seen, every monad arises in this way.