For the monad , an algebra for a monad is with and . A morphism of algebras for a monad satisfies . These objects and arrows form the Eilenberg-Moore category .
The free algebra functor sends to and to . The monad identities verify the algebra laws. For the forgetful functor , the free adjunction is
with inverse . The algebra law makes the latter an monad algebra morphism. The identities and prove the bijection.
In the category of adjunctions inducing a fixed monad, objects are adjunctions with their induced monad identified with . A morphism to is a functor between the right-hand categories satisfying , and compatibility with units and counits. With these strict identifications, define
The triangle identities give the unit algebra law; naturality of at gives the multiplication law. Naturality at makes an monad algebra morphism. Moreover , because , and is the free-adjunction counit at . Hence is a morphism into the Eilenberg-Moore adjunction.
For any other such , its underlying object at must be . Counit compatibility forces its algebra action to be , and the forgetful functor, which is a faithful functor, forces . Thus . This proves terminality of the Eilenberg-Moore adjunction. If adjunctions are specified only up to coherent isomorphisms, the same argument gives uniqueness up to the corresponding compatible natural isomorphism.

Articles by others on the same topic (0)

There are currently no matching articles.