Write the adjunction unit and adjunction counit of as . Its induced monad is , with multiplication . The Eilenberg-Moore comparison functor is
The unit law for is , a triangle identity for an adjunction. Naturality of at gives ; applying gives . Naturality at gives the monad algebra morphism equation for . Thus is well-defined.
For each , consider the fork in
It commutes by the naturality equation just used. Its image under is the fork of the preceding question, with parallel morphisms and final map . It is split using and . By the assumed reflection, is the coequalizer of this pair in .
For faithfulness, if for , naturality gives . A coequalizer is an epimorphism, so .
For fullness, let be a monad algebra morphism. Thus satisfies . Set . We verify explicitly that equalizes the two morphisms of the displayed fork. The monad algebra morphism equation gives
Naturality of first at and then at gives
The coequalizer therefore supplies a unique with . Applying yields . The map is split epic with section , so cancellation gives . This proves fullness, and the earlier cancellation proves faithfulness. Hence
No claim that is essentially surjective is needed; that stronger conclusion needs the corresponding existence hypotheses.

Articles by others on the same topic (0)

There are currently no matching articles.