Define the free algebra functor by
The monad laws say precisely that defines an monad algebra structure on , while naturality of makes an monad algebra morphism. We construct the adjunction explicitly.
For an monad algebra and a morphism , put . It is an monad algebra morphism because
Conversely, from an monad algebra morphism obtain . These operations are inverse: naturality of and the monad algebra unit law give
and the algebra-morphism equation together with the monad unit law gives
The formulas commute with precomposition in and composition with monad algebra morphisms in , so the bijections are natural. Therefore the free-forgetful Eilenberg-Moore adjunction is
Its unit is and its counit at is the monad algebra action .

Articles by others on the same topic (0)

There are currently no matching articles.