For with unit of an adjunction and counit of an adjunction , put
The triangle identities for an adjunction give
For associativity, naturality of at says
Apply to obtain . Thus this is the monad induced by an adjunction.
Conversely, start with a monad . The free algebra functor sends to and to . The monad laws ensure that these are algebras for a monad and morphisms of algebras for a monad. For an algebra , there are inverse bijections
The inverse really is an algebra map because
For a free-algebra map , its algebra equation and the monad unit law give
For a base map , naturality and the algebra unit law give . The formulas are natural, establishing the free-forgetful Eilenberg-Moore adjunction . Its unit is , and its counit at is . Hence its induced multiplication is , and every monad arises from an adjunction.
For with unit and counit , set
Naturality of the unit and counit makes these natural transformations. The two triangle identities give and . Naturality of at gives . Applying proves . Thus this is the monad induced by an adjunction.
Conversely, for any monad take the free-algebra functor and the forgetful functor . For an algebra , the assignments and give inverse bijections between algebra maps and arrows . For the inverse identities, , while . The algebra and monad laws also make an algebra morphism, since . These bijections are natural, giving the free-forgetful Eilenberg-Moore adjunction. Its unit is , its counit at is , and its induced multiplication is exactly . Thus every monad arises from an adjunction.
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 .
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.