A monad on consists of an endofunctor and natural transformations , satisfying and . Its Eilenberg-Moore category has objects with , and . A morphism satisfies . An adjunction , with unit and counit , induces , . It is a monadic adjunction if the Eilenberg-Moore comparison functor is an equivalence with the Eilenberg-Moore category.
A fork is a split coequalizer if and there are , with , and . It is indeed a coequalizer: if , then , so factors uniquely through , which is split epic. Every functor preserves these splitting identities, making such coequalizers absolute.
The precise monadicity theorem states: for an adjunction , the comparison is an equivalence if and only if reflects isomorphisms and every pair in whose -image admits a split coequalizer has a coequalizer which preserves. Equivalently, the right adjoint creates these split-underlying coequalizers, with creation understood up to the canonical isomorphism of the prescribed underlying coequalizer. Here is a proof.
First consider the forgetful functor from monad algebras. It reflects isomorphisms: the inverse of an invertible algebra morphism also obeys the algebra-morphism identity, by multiplying that identity by the inverses. For an algebra pair with a split underlying coequalizer , all powers of preserve its coequalizer. If is the algebra structure on , the map coequalizes , so there is a unique with
The unit law follows by composing with the epimorphism : . For associativity, naturality and the algebra law give
Cancel the epimorphism to obtain . Thus is an algebra and is an algebra morphism. Any algebra morphism coequalizing the pair factors through on underlying objects, and its factor is an algebra morphism by cancellation of the epimorphism . This creates the coequalizer. Transporting these facts through an equivalence proves necessity.
For sufficiency, let be a -algebra. In consider the free pair
Its underlying pair is , with split coequalizer : the splittings are and , using the algebra unit law, the monad unit law and naturality of . By hypothesis its coequalizer exists and is preserved. Identify with by the unique coequalizer isomorphism, so . Naturality of the counit makes an algebra morphism, hence the comparison structure on satisfies . The map is split epic because , so . Every algebra is therefore isomorphic to a comparison algebra.
For an actual object , its counit is a coequalizer of the analogous free pair. It coequalizes that pair by counit naturality. Compare it with the coequalizer furnished by the hypothesis; applying gives an isomorphism, since both underlying arrows coequalize the same split pair. Reflection of isomorphisms makes the comparison map an isomorphism. This proves the counit's asserted coequalizer property.
Let be an algebra morphism. Its transpose is . The two composites of with the free pair have adjunct transposes and , equal because is an algebra morphism. Consequently factors uniquely through as . Applying gives ; the last factor is split epic, so . Conversely any lift of must satisfy by naturality and hence is unique. Thus is full and faithful, and the earlier construction makes it essentially surjective. The comparison is an equivalence, completing the theorem's proof.
Now take . Its left adjoint exists by the permitted topological result; it can be realized as the Stone-Čech compactification of the discrete input set. A bijective continuous map from a compact space to a Hausdorff space is a homeomorphism, so reflects isomorphisms.
For continuous with a split underlying fork , let be the relation of having the same -image. We claim
For the forward inclusion choose , : and supply the equality. For the reverse inclusion use . The subset is closed, because is Hausdorff, and compact. Its continuous image is compact and hence closed. A closed equivalence relation on a compact Hausdorff space has a compact Hausdorff quotient; its quotient map is a coequalizer here, since it identifies exactly the generated relation. Its underlying set coequalizer is the specified one up to the unique isomorphism. Thus preserves the needed coequalizers, and
The closedness argument is the closed relation generated by a set-split pair of compact Hausdorff maps lemma; the splitting maps themselves need not be continuous.