In a category with equalizers, the equalizer of defines a functor by . It has unit and multiplication characterized by
Cancelling the monomorphisms reduces its unit and associativity laws to those of , so is a monad morphism. The split equalizers associated with a monad show that is invertible. If every is monic, then every is invertible, the naturality square of at is a pullback in a category, and is an idempotent monad. This monicity hypothesis is essential to this last argument; arbitrary functors need not preserve monomorphisms.
Since the full endofunctor subcategory contains and is closed under composition, all belong to it. Terminality supplies unique natural transformations and . The monad unit laws compare arrows , both necessarily the unique endomorphism, namely the identity. The associativity law compares arrows , again necessarily equal. Every monad structure uses these two unique arrows, so .
For a monad with underlying functor in the subcategory, the unique is a monad morphism. Its unit and multiplication compatibility compare, respectively, arrows and and therefore follow from terminality. A -algebra restricts to the -algebra . The unit law is immediate. For multiplication, naturality and the monad-morphism law give
An algebra morphism for also commutes with the restricted action by naturality of . Keeping underlying objects and arrows gives the required functor .
Now define to be the set of ultrafilters on , and for define
Inverse images preserve inclusions, intersections and complements, so this is an ultrafilter; composition of inverse images makes a functor. There are no ultrafilters on the empty set. Every ultrafilter on a disjoint binary union chooses exactly one summand, and restriction to that summand gives an ultrafilter there; extension back is inverse to restriction. Hence canonically, and preserves finite coproducts, including the empty one.
Let be any other finite-coproduct-preserving endofunctor. For , put
The decomposition and coproduct preservation show that exactly one of belongs. Refining two subsets into the four disjoint parts shows that an element lying in both indicated summands lies in their intersection summand. The same refinement for proves upward closure. Thus is an ultrafilter. For , decomposition by and its complement shows
proving naturality.
For uniqueness, suppose is natural. Since is a singleton, naturality on the two inclusions forces to send every element in each of the two summands of to the corresponding principal ultrafilter. Apply naturality to the characteristic map . It gives precisely when lies in the selected summand, which by the decomposition is precisely when lies in . Hence for every . Therefore
This proves ultrafilter functor. For clarity, the resulting unit sends to its principal ultrafilter; multiplication sends an ultrafilter on to the ultrafilter whose members are with . Naturality and the monad laws for these formulas also follow from the terminal construction.
A monad morphism induces a functor between Eilenberg-Moore categories, identical on underlying objects and arrows. Its unit equation gives the restricted algebra's unit law. Naturality and the multiplication equation give . Naturality also preserves algebra morphisms.