A monad consists of an endofunctor and natural transformations and satisfying
An algebra for a monad is with satisfying and . A morphism of algebras for a monad obeys . The functor laws show that identities and composites obey this equation, giving the Eilenberg-Moore category .
For an adjunction , let be its adjunction unit and its adjunction counit. The monad induced by an adjunction is
The two unit laws are and , respectively the two triangle identities for an adjunction.
For associativity, naturality of the adjunction counit at says
Apply to obtain . The composites defining and are natural transformations, so all monad axioms have been checked, not only their underlying objectwise types.
Define the forgetful functor , acting as the identity on underlying morphisms. Define the free algebra functor by
The monad laws make an algebra for a monad structure, and naturality of makes an monad algebra morphism.
For , define the transpose maps
The map is an monad algebra morphism, because naturality of and the algebra associativity law give
For , naturality of gives . Conversely, if is an monad algebra morphism, then
Precomposing by a map into or postcomposing by an monad algebra morphism respects both formulas. Thus the bijection is natural and . This is the free-forgetful Eilenberg-Moore adjunction.
Its adjunction unit is the given ; its adjunction counit at is the monad algebra morphism . Hence , and the induced multiplication is the underlying counit at , namely . Therefore this adjunction induces exactly the original monad, including its unit and multiplication of a monad.

Articles by others on the same topic (0)

There are currently no matching articles.