A monad on is an endofunctor with natural transformations and satisfying
An algebra for a monad is with and . A morphism of algebras for a monad satisfies . These form the Eilenberg-Moore category . Its free algebra functor is , and its adjunction to the forgetful functor has the explicit bijection
Write , , and let be the coproduct in a category injections. Set
Here is an algebra morphism, with underlying multiplication . For an algebra , an algebra morphism corresponds to , and the transposes of are respectively
For the second formula, by naturality of and the monad unit law. Thus exactly when, writing ,
These say precisely that and are morphisms of algebras for a monad. Consequently any coequalizer of represents pairs of algebra morphisms out of and , proving the coproduct presentation for monad algebras:
Its two algebra injections have underlying morphisms and ; the equivalence just proved verifies both the algebra equations and their universal property.
The displayed pair is a reflexive pair, with common section
Indeed by the algebra unit laws, while
Now suppose has all finite colimits and preserves reflexive coequalizers. The permitted creation theorem gives reflexive coequalizers in : the underlying pair is reflexive and its coequalizer exists and is preserved by . The preceding construction therefore gives binary algebra coproducts in a category. The initial object is , since the free algebra functor is a left adjoint and is initial in .
For any algebra pair , the augmented pair
is a reflexive pair, with common section the injection of , and has exactly the same coequalizing morphisms as . Hence all coequalizers exist in . The construction of finite colimits from coproducts and reflexive coequalizers now gives
A reflexive pair has a common section with . Form the pushout in a category of and , and write its two maps from as . Its relation , composed with , gives . Thus . Any with gives the compatible pair for this pushout and therefore factors uniquely through . This proves the coequalizer of a reflexive pair from a pushout construction.
There is a genuine transcription difference: the original PDF says finite products in the finite-colimit assertion, while the TeX says finite coproducts. The PDF assertion is false with products. Even retaining a pushout-existence assumption, the full subcategory of the Category of sets on nonempty sets has finite products, pushouts, and all coequalizers, but no initial object, hence no empty colimit. Regard the poset with elements , order
and incomparable as a category. It has finite meets and top , hence finite products in a category. Every reflexive pair in a poset is an equal pair and has its identity as a coequalizer. But have no least upper bound, so they have no coproduct in a category.
For the corrected construction using finite coproducts, let be a finite diagram in a category. Put
Define on the summand indexed by as and . Maps with are exactly cocone under a diagram data on . Hence their universal coequalizer is its colimit. Replace by the reflexive pair
whose common section is the second injection and whose coequalizer is unchanged. This proves construction of finite colimits from coproducts and reflexive coequalizers, including the empty diagram via the empty coproduct: