The free algebra functor isThe monad laws make an algebra action, and naturality of makes a morphism of algebras for a monad. Let forget the action. DefineThe proposed inverse is an algebra morphism becauseNaturality of and the algebra unit law give . If is an algebra morphism, thenThe formulas are natural in both variables, so . Its unit is , and its counit at has underlying map . Thus the monad induced by an adjunction has endofunctor , unit , and multiplication . It is exactly the original monad, not merely a monad with the same endofunctor.
Articles by others on the same topic
There are currently no matching articles.