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 .
Write and , with adjunction counit . The induced monad has and . Define the Eilenberg-Moore comparison functor by
The action satisfies by a triangular equation. Naturality of at gives
Applying yields , the other algebra identity. For , naturality gives
so 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 monad
make 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, gives
Thus 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 gives
Therefore 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 (0)

There are currently no matching articles.