We have now seen both the Kleisli and Eilenberg-Moore constructions for a monad , and that they yield adjunctions that induce the original monad. Such an adjunction is sometime referred to as a resolution of .
In order to compare different resolutions of a monad on category , we need a suitable category in which to compare them. Define as the category with:
- Objects: Adjunctions , where has codomain , that induce .
- Morphisms: A morphism is a functor such that and .
Note: All the adjunctions inducing must have the same unit, and the counit of adjunction is determined by its unit. It is therefore sufficient to specify only the functors in the objects of .
Writing and for the counits of the domain and codomain respectively, the conditions for being a -morphism imply
We shall refer to this equation as the key property. Establishing its validity requires some additional work, either via direct calculation, or invoking some theory of adjoint squares, which we shall omit. (Although I should point out there is a short string diagrammatic proof, for those that like that sort of thing!)
The Kleisli Construction
Clearly, is an object of . Let be any other object, with counit of the adjunction . There is a morphism from the Kleisli adjunction to this object, referred to as the Kleisli comparison functor, given by a functor . On objects:
For a -morphism , with underlying morphism :
That identities are preserved by follows from the snake equation:
For the composition, noting that , by definition:
Applying naturality, this is equal to:
Applying naturality again gives:
Which completes verification that composition is preserved by . Verifying that the two equations required of morphisms hold is straightforward as well.
We would like to show that this is the unique such morphism in . This uniqueness is termed “obvious” in some accounts, which in my opinion is rather optimistic, so we sketch the main points. The action on objects of any putative morphism is easily seen to be forced by one of the equations required of morphisms in :
We would like to show that the action on morphisms is also forced, this is a bit trickier. We first note that as is identity on objects, every morphism in is the transpose of a morphism in , that is, it is of the form:
Furthermore, is the underlying -morphism of the Kleisli morphism. (This may need a bit of thought about the Kleisli adjunction to convince yourself this is true). Above, we write the counit of the Kleisli adjunction as . This deviates from our usual convention of using subscripts for Kleisli notions, but saves notational confusion when dealing with components of natural transformations.
Applying the key property, the previous expression is equal to
Finally, applying one of the equations for being a morphism, and its previously established action on objects, we get
This is exactly the expression for the action on morphisms in our definition of . In summary, we have established that the Kleisli adjunction is the initial resolution of .
We now quickly look at some important details of the universal morphisms from the Kleisli adjunction. has image on objects those of the form . For a morphism , is a Kleisli morphism, and its image under is , so is full. Also
By the snake equation, this assignment is injective, so also is faithful.
The Eilenberg-Moore Construction
The Eilenberg-Moore adjunction also yields an object of . For any other -object , we aim to show there is a unique morphism to the Eilenberg-Moore adjunction. The equation tells us that
Where is a to be determined structure map. Write for the counit of the Eilenberg-Moore adjunction. This has components (This is just a matter of examining the details of adjunction if it is unfamiliar). Therefore . Applying the key property, combined with the action of on morphisms, . This completely fixes the only possible construction for . We must confirm that is a valid algebra structure map. The unit axiom follows immediately from the snake equation:
For the multiplication axiom, recalling , and applying naturality:
Functoriality is then obviously inherited from that of . We have therefore established that the Eilenberg-Moore adjunction is the terminal resolution of . The universal morphisms are referred to as (Eilenberg-Moore) comparison functors.
An Important Relationship
As a special case of the initial and terminal resolutions above, there must be a unique morphism from the Kleisli to the Eilenberg-Moore resolution. On objects:
and on morphisms
From our previous remarks, this functor is full and faithful onto the full subcategory generated by objects of the form . Therefore, we can identify the Kleisli category with the full subcategory of free Eilenberg-Moore algebras.