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.
Take . By assumption has finite limits, so has finite colimits. A filtered category is nonempty, admits a cocone over every pair of objects, and admits a coequalizing arrow for every parallel pair. The initial object of gives nonemptiness, its binary coproducts give the required two-object cocones, and its coequalizers equalize parallel arrows. Consequently . These statements also handle the otherwise possible empty category of elements.
Assume both unit and counit are monic. The unit criterion makes faithful. The triangle identity is . Since is monic, this split epimorphism is an isomorphism: cancelling it in gives . Thus is invertible. As is balanced, the reflection result in the root solution makes invertible. Hence is full and faithful.
Let be a regular epimorphism. Its adjunct factorization is for . A regular epimorphism is extremal: if a coequalizer factors through a monomorphism , its other factor also coequalizes the defining pair, descends through , and gives a right inverse for ; monicity then makes invertible. Apply this to the monic . More explicitly, if coequalizes , monicity gives , so there is with . Then implies , and monicity gives . Therefore . The image is closed under regular quotients, proving .
For each algebra for a monad , consider the specific pair in
Then the exact condition is
Each pair is reflexive, with common section : the two composite identities follow from and . Thus existence of all reflexive coequalizers is sufficient, but the displayed specified pairs give the necessary-and-sufficient condition.
To prove it, take and its adjoint transpose . The transpose of is , by naturality of . The transpose of is
Moreover counit naturality and a triangle identity give
Because transposition is bijective, the coequalizing equation is therefore equivalent to
The right side says exactly that is a monad algebra morphism.
For sufficiency, choose a coequalizer for every monad algebra. Its universal property and the equivalence just proved give natural bijections
To see explicitly that the chosen objects form a functor, an monad algebra morphism makes coequalize the pair for : use and naturality of the counit. Hence there is a unique with . Uniqueness proves its identity and composition laws and the naturality of the displayed bijections. Thus .
Conversely, suppose with unit . Transpose its underlying arrow through to obtain . Since the unit is an monad algebra morphism, the equivalence above shows that coequalizes the specified pair. Any coequalizing transposes to an monad algebra map , which factors uniquely through the unit by . Transposing back gives a unique factorization of through . Thus is the required coequalizer. This proves both directions of the Left adjoint to the Eilenberg-Moore comparison functor criterion.
Assume the coequalizers from part (b) exist and write them . The underlying arrow of the comparison-adjunction unit is
We first relate it to the monad algebra action. Naturality of , the coequalizer equation and a monad unit law give
In , is itself a split coequalizer of . Indeed,
For an explicit universal-property proof, if satisfies , then obeys
Its uniqueness follows by composing any equation with .
Now equalizes and . If it is a coequalizer, then and are coequalizers of the same pair. Their unique comparison map is , since , and is therefore invertible. Conversely, if is invertible, is an isomorphic copy of the coequalizer , so it is a coequalizer too.
The forgetful functor reflects isomorphisms: if an monad algebra morphism has an inverse as an underlying arrow, the equation rearranges to , making that inverse an monad algebra morphism. Thus underlying invertibility here is exactly invertibility of the unit component. For all monad algebras together, the comparison-adjunction unit criterion is
Equivalently, the necessary-and-sufficient conditions for a left adjoint with invertible unit are existence of the coequalizers in part (b) and their preservation by . No preservation of arbitrary coequalizers is required.
Use the elementary, or weak, topos axioms: finite limits and a power object for every object , naturally representing . No arbitrary products or coproducts are assumed. In particular is the subobject classifier. Inverse image of the membership relation defines for .
Interchanging the factors in a relation gives natural bijections
Thus the contravariant power-object functor has left adjoint . Its adjunction unit sends a generalized element to the predicate on given by membership of .
This unit is monic. If have the same image under , membership of and agrees in every -parameterized subobject of . Apply this to the graph of in : membership of is true, so membership of is true, which means . This argument uses parameterized relations, not an assumption that global elements detect morphisms.
The functor reflects isomorphisms. Suppose is invertible. Then is invertible, and naturality together with monicity of shows that is monic. Regard as a subobject of . Its inverse image along itself is the whole of , just as for the whole subobject of . Those two subobjects correspond to maps ; since is monic, they coincide. Therefore the subobject is all of , and is an isomorphism.
We now prove the preservation condition for the crude monadicity theorem. A reflexive pair in is a coreflexive pair in , with for some . Let be its equalizer. For any monomorphism , define on power objects by composing a parameterized subobject with ; no general image construction is needed because is monic. Inverse image followed by this extension obeys .
Here both are monic. For a parameterized subobject of , an element belongs to exactly when for some . Applying gives , so this condition is precisely and . Consequently, as morphisms of power objects,
If equalizes , these identities give
It therefore factors uniquely through , which is a split epimorphism with section . Since , also equalizes . Hence is their coequalizer. This proves explicitly that power objects turn coreflexive equalizers into coequalizers.
Finite equalizers in give all coequalizers of reflexive pairs in , and we have shown that preserves them and reflects isomorphisms. The crude monadicity theorem now yields
Fix a set of cardinality . If has -indexed products in a category, its Eilenberg-Moore category for the double-power monad has them, since the forgetful functor creates existing limits. The displayed equivalence then gives -products in , hence -coproducts in a category in .
For the converse, suppose those coproducts exist. The diagonal is a logical functor, because all the elementary topos structure in is pointwise, and it has left adjoint . Apply power-object monadicity to both toposes. Under their monadic identifications, is the lift of to the double-power Eilenberg-Moore categories. The base functor is a right adjoint to , so the adjoint lifting theorem for monad algebra functors gives a left adjoint to its algebra lift. Its required reflexive coequalizers exist in , since they are opposites of finite equalizers in . Taking opposites gives a right adjoint to , which is exactly the -product functor. Thus the products and coproducts of fixed cardinality in a topos satisfy
Write and for the unit and counit of an adjunction. The induced monad has
The Eilenberg-Moore comparison functor sends to the algebra for a monad
and sends to . The triangle identities for an adjunction give the algebra unit law, and naturality of the counit gives the algebra multiplication law and the algebra-morphism equation for .
If has coequalizers, define the Left adjoint to the Eilenberg-Moore comparison functor at an algebra by
The parallel pair is reflexive through . A morphism is equivalently an arrow with . Under , its transpose is . The transpose of is , while the transpose of is . Hence the coequalizer condition is exactly
the equation for a morphism of algebras for a monad . This supplies the natural bijection proving , and also defines on algebra morphisms by the coequalizer universal property.
A regular category has finite limits, coequalizers of kernel pairs, and regular epimorphisms stable under pullback. Equivalently, every morphism factors as a regular epimorphism followed by a monomorphism, and these factorizations are stable under pullback. A regular functor preserves finite limits and regular epimorphisms, hence also preserves these image factorizations.
For this question, the capital regular category convention is the one in which every well-supported object is a well-pointed object in a category. Here an object is well-supported if is a regular epimorphism. It is well-pointed if a subobject through which every point factors must be the whole object. This convention is documented in Definitions 1.1–1.3. It imposes no such point-detection requirement on objects whose support is a proper subobject of . In particular, it should not be replaced here by the stronger assertion that reflects every isomorphism.
First prove two facts about a capital regular category . Every well-supported object has a point. Otherwise is well-supported and has no points, so its diagonal contains all points and is invertible. That makes a subterminal object; the regular epimorphism is then also monic and hence invertible, contradicting the absence of a point. If is a regular epimorphism and is a point, its pullback in a category is a well-supported object over , so it has a point lifting . Thus the representable functor
preserves regular epimorphisms; it already preserves all existing limits. Hence is a regular functor. Second, if is a singleton, its unique point is a monomorphism, is well-supported, and contains all points of . Well-pointedness makes invertible. Thus reflects terminal objects, even though it need not reflect arbitrary isomorphisms.
Now let be a small category that is a regular category. For each object , its slice category is small and regular: finite limits, images and the stability of regular epimorphisms are computed using the corresponding constructions in . By the permitted capitalization result choose a conservative functor that is regular,
with a small capital regular category. The base-change functor , given by , preserves finite limits and regular epimorphisms. So does
Taking these as the coordinates defines a regular functor
The exponent is a set of indices, so this is a power of the Category of sets, with finite limits and regular epimorphisms computed coordinatewise.
To prove reflection of isomorphisms, suppose is invertible for . In , the object is the pullback of along the point given by the diagonal . Applying shows that is the fibre of the bijection over this diagonal point, and is a singleton. The preceding lemma gives through its canonical arrow to . Since reflects isomorphisms, is invertible. Its underlying morphism is . Therefore
In the small-category setting of this representation result, the elementary condition for replacing the power by one copy of is:
This is almost total support for a regular category. “Strict initial” means initial and every arrow into it is invertible; the condition allows the case in which all objects are well-supported and no initial object exists.
For necessity, let be regular and conservative. If , factor through its support of an object in a regular category . Preservation of images gives . Conservativity makes invertible, so is well-supported. If , then for every the projection is sent to the bijection , hence is invertible. Its inverse followed by the other projection supplies an arrow . For any two such arrows, their equalizer is sent to a bijection onto , hence is invertible, proving uniqueness. Thus is initial. If exists, then exists, so and that arrow is sent to a bijection. Conservativity makes it invertible. Hence is strict initial.
For sufficiency, choose the permitted conservative regular functor into a small capital regular category, and put . This is regular. A well-supported object of is sent to a well-supported object of , which has a point. A non-well-supported object is strict initial by the condition, and is consequently a proper subterminal object. The functor preserves subterminality and reflects the noninvertibility of its arrow to ; its image is a proper subterminal object and has no points. Thus is empty exactly on the non-well-supported objects.
Suppose is a bijection for . If both sets are empty, and are strict initial objects and is invertible. Otherwise are well-supported. Factor as a regular epimorphism followed by a monomorphism . Surjectivity of makes every point of factor through ; capitality of makes invertible. Hence is a regular epimorphism. Its kernel pair is well-supported, because and are regular epimorphisms. Injectivity of implies that every point of has equal coordinates, and therefore factors through the diagonal . Since is well-pointed, this diagonal is invertible. Thus is also monic, hence an isomorphism, and conservativity of makes invertible. This proves sufficiency with actual point and image arguments, rather than asserting that global sections of every capital regular category is conservative.
A split coequalizer consists of , , and with , , and . If , then . Thus factors through , and the factor is unique because has the right inverse . This proves the coequalizer property directly. Every functor preserves the diagram, since all these equations are preserved.
For idempotent splitting through a coequalizer, first suppose with . Then . Any satisfying factors as , uniquely since is a split epimorphism. Hence coequalizes .
Conversely, let coequalize . Since , the arrow itself equalizes the pair, so there is a unique with . Then , and every coequalizer is an epimorphism, so . Thus is a splitting of an idempotent morphism.