If has finite colimits and a monad preserves reflexive coequalizers, its Eilenberg-Moore category has finite colimits. The forgetful functor creates reflexive coequalizers preserved by . The coproduct presentation for monad algebras yields binary coproducts, and is initial. Any pair can then be replaced by the reflexive pair , with identical coequalizers. Finite coproducts and coequalizers give all finite colimits.
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