For the monad define the free algebra functor by
The unit and associativity identities of the monad make an algebra for a monad, and naturality of makes a morphism of algebras for a monad. Let be the forgetful functor. For in the Eilenberg-Moore category, set
The inverse candidate is a monad algebra morphism, since
The two composites are identities:
These use respectively the unit law for a monad algebra, the algebra-morphism equation, and a unit identity of the monad. The formulas commute with precomposition in and postcomposition by monad algebra morphisms, so they form a natural bijection. Therefore the free-algebra functor is left adjoint to forgetting:
Its adjunction unit is , and its adjunction counit at is .

Articles by others on the same topic (0)

There are currently no matching articles.