A monad consists of an endofunctor and natural transformations and satisfyingAn 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 isThe two unit laws are and , respectively the two triangle identities for an adjunction.
For associativity, naturality of the adjunction counit at saysApply 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 byThe monad laws make an algebra for a monad structure, and naturality of makes an monad algebra morphism.
For , define the transpose mapsThe map is an monad algebra morphism, because naturality of and the algebra associativity law giveFor , naturality of gives . Conversely, if is an monad algebra morphism, thenPrecomposing 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
There are currently no matching articles.