For the monad define the free algebra functor byThe 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, setThe inverse candidate is a monad algebra morphism, sinceThe 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 .
Write and , with adjunction counit . The induced monad has and . Define the Eilenberg-Moore comparison functor byThe action satisfies by a triangular equation. Naturality of at givesApplying yields , the other algebra identity. For , naturality givesso is a monad algebra morphism. Identities and compositions are respected because is a functor. Finally,and the same equalities hold on morphisms. Thus both comparison identities hold, strictly when is the specified induced monad:
If the multiplication in the unit and multiplication of a monad is invertible, the two unit identities of the monadmake both and its inverse. Hence idempotence implies equality of the two unit insertions:This is the first implication in the characterization of an idempotent monad.
Assume , and let be an algebra for a monad. Its unit identity gives . Naturality of at , followed by the assumed equality, givesThus every algebra action is invertible, with its inverse prescribed by the unit:
Suppose every algebra action is an isomorphism. Its inverse is , by the unit law for a monad algebra. For any underlying morphism between two algebras for a monad, naturality of givesTherefore every underlying morphism is automatically a monad algebra morphism. The forgetful functor is always faithful, because a monad algebra morphism has no data beyond its underlying morphism, and it is now full as well. Hence invertible algebra actions imply
If is fully faithful, the criterion proved for a right adjoint says that the adjunction counit of is a natural isomorphism. Its component at is precisely the algebra action . In particular, its component at the free algebra for a monad has underlying morphism . Thus every is an isomorphism, and the natural transformation is invertible. This closes the cycle and proves all four conditions equivalent:
Articles by others on the same topic
There are currently no matching articles.