Comonad 2026-10-06
A comonad is an endofunctor with natural transformations and satisfying and . It is the categorical dual of a monad. Its coalgebras for a comonad carry compatible maps into their image under .
Monad morphism 2026-10-14
A morphism of monads on one category is a natural transformation with and . These equations preserve the unit and multiplication. A terminal endofunctor in a full composition-closed subcategory containing the identity receives a unique such morphism from every monad whose functor belongs to that subcategory.
A monad on consists of an endofunctor and natural transformations , satisfying the unit and multiplication of a monad laws
An algebra for a monad is an object equipped with such that
A morphism of algebras for a monad is a morphism satisfying . Identities and composition obey this equation, giving the Eilenberg-Moore category and its forgetful functor .
For an adjunction with induced monad , the Eilenberg-Moore comparison functor is
The functor is monadic when it has such a left adjoint and this comparison is an equivalence of categories; a stricter convention requires an isomorphism of categories over . We will identify which limit-lifting conclusion each convention supports in part (iii).
A monad on consists of an endofunctor and natural transformations , satisfying, at every object ,
These are the associativity and unit laws. An algebra for a monad is with
A monad algebra morphism is a morphism satisfying . Identity morphisms satisfy this equation, and if satisfy it, then . Hence these objects and morphisms form the Eilenberg-Moore category , with the forgetful functor and .
A monad on a category consists of an endofunctor , a unit natural transformation , and a multiplication , satisfying
An algebra for a monad is with and . A morphism of algebras for a monad satisfies . These objects and arrows form the Eilenberg-Moore category .
For an adjunction with , the monad induced by an adjunction is , with . The Eilenberg-Moore comparison functor is and . The functor is monadic when this comparison is an equivalence of categories; this is a monadic adjunction.
The precise monadicity theorem says that is monadic exactly when it has a left adjoint, reflects isomorphisms, and satisfies the following condition: whenever the image of a parallel pair in admits a split coequalizer in , the pair has a coequalizer in and preserves that coequalizer. Equivalently, these coequalizers are created up to the canonical isomorphism identifying their underlying coequalizer objects. Here a split coequalizer of consists of , , and with
These equations prove its universal property: if , then , and is the unique factor through . Every functor preserves these equations, so every functor preserves split coequalizers.
First consider the forgetful functor . It has the free algebra functor as a left adjoint: the inverse transposition formulas are and . An monad algebra morphism whose underlying arrow is invertible has an algebra-morphism inverse, by rearranging its structure equation. Thus reflects isomorphisms.
Suppose have an underlying split coequalizer . Applying gives a coequalizer of . The equation therefore gives a unique with . The monad algebra laws follow by cancellation: composing with the epimorphism reduces it to , and composing with reduces it to . Both and are epimorphisms because they remain split coequalizers. Thus is an algebra for a monad and is an monad algebra morphism. If an algebra map equalizes , its underlying factor obeys , since this equation becomes after composition with . This proves that creates the required coequalizers. An equivalence of categories transfers these properties to any monadic , proving necessity.
Conversely assume the three conditions and write . Given , take the pair
Its image is , with split coequalizer : the splittings are and , because
Let be its coequalizer in . Preservation gives a canonical isomorphism under which . Transporting the algebra action of along this isomorphism gives . Naturality of the adjunction counit says that is an monad algebra morphism, hence . But too, and is a split epimorphism, with section . Therefore . Every algebra is consequently isomorphic to some .
It remains to establish full faithfulness, rather than merely construct objects. For , put . The adjunction counit coequalizes . The coequalizer supplied by the hypothesis has underlying coequalizer . The induced arrow from that coequalizer object to is therefore sent by to an isomorphism; reflection of isomorphisms makes it invertible. Thus itself is this coequalizer.
Now let be an monad algebra morphism, and put . The arrow coequalizes the two arrows in the preceding presentation. To check this directly, use transposition along : the transposes of and are respectively and , which agree by the algebra-morphism equation. Hence a unique satisfies . Applying gives ; cancellation of the split epimorphism yields . Finally, any arrow satisfies by naturality, so two arrows with equal image under are equal by the coequalizer property. The comparison is full and faithful and essentially surjective, hence an equivalence of categories. This proves the theorem.
For the application, the free compact Hausdorff space on a set is the Stone-Čech compactification of the corresponding discrete space. Its standard extension property says that every set map , for compact Hausdorff , extends uniquely to a continuous map . This constructs the required left adjoint. Also a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, so reflects isomorphisms.
Take continuous maps whose underlying functions have a split coequalizer with splittings . The splittings need not be continuous. Let
The set is compact and hence closed. Since , it is contained in . Conversely . Thus
The set of triples on the right is closed in the compact Hausdorff space , so its projection onto the first two coordinates is compact and closed. This proves that the equivalence relation is closed, without assuming continuity of either splitting.
Give the quotient topology. The allowed closed-relation criterion makes it a compact Hausdorff space. If a continuous map equalizes , the split-coequalizer property makes it constant on the fibres of ; its unique factor is continuous by the quotient topology. Hence this is a coequalizer in compact Hausdorff spaces, preserved by . Its topology is forced uniquely, since any continuous surjection from a compact space to a Hausdorff space is a quotient map. All three conditions hold, and therefore the forgetful functor from compact Hausdorff spaces to sets is monadic.
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.
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 on consists of an endofunctor and natural transformations and satisfying, at every object ,
These are the unit and associativity laws for the unit and multiplication of a monad.
An algebra for a monad is a pair with satisfying
A monad algebra morphism is a morphism with . Identities satisfy this condition, and composing two such maps preserves it by functoriality of . The resulting Eilenberg-Moore category is denoted . Its forgetful functor sends to and leaves the underlying arrows unchanged.
Write the adjunction unit as and the adjunction counit as . Define the monad induced by an adjunction by
with unit . Naturality of makes a natural transformation.
The triangle identities for an adjunction give the two unit laws:
For associativity, apply naturality of to the arrow in :
Applying yields
Thus the induced data satisfy all the monad laws, rather than merely supplying an endofunctor and two transformations.
A monad consists of an endofunctor and natural transformations and satisfying
An algebra for a monad is with satisfying and . A morphism of algebras for a monad obeys . The functor laws show that identities and composites obey this equation, giving the Eilenberg-Moore category .
For an adjunction , let be its adjunction unit and its adjunction counit. The monad induced by an adjunction is
The two unit laws are and , respectively the two triangle identities for an adjunction.
For associativity, naturality of the adjunction counit at says
Apply to obtain . The composites defining and are natural transformations, so all monad axioms have been checked, not only their underlying objectwise types.
For an adjunction with unit and counit of an adjunction , the monad induced by an adjunction is , with multiplication . Its Eilenberg-Moore comparison functor is
Here is the Eilenberg-Moore category. If has reflexive coequalizers, the Left adjoint to the Eilenberg-Moore comparison functor is defined on an algebra for a monad by
where the last arrow is a coequalizer. The parallel pair has common section , so it is a reflexive pair. The coequalizer property induces on algebra morphisms and gives .
Starting with , iterate this construction: if , put and let be its comparison. The monadic length is the least for which is an equivalence of categories. Thus an equivalence has length zero, and an already monadic adjunction whose right adjoint is not an equivalence has length one. The assumed reflexive coequalizers ensure the needed left adjoints; in the example we identify them explicitly.
For the nested partial unary operation category , write
For the empty list of operations, take and . We use positive chain indices for new points, so the index zero already labels the copy of . This makes the free-object hint independent of the convention for .
For , the free extension of nested partial unary operations has underlying set
Keep the old operations on the zero layer. On new points define only
and leave every , , undefined there. Define the new top operation by
and leave it undefined elsewhere. These are precisely the permitted domains: the first unary operation on every new point moves it, so none of the higher operations is defined there. When , take with . In either case the unit is .
For , let its operations be . Any morphism extends uniquely to
The value is defined because preserves the previous fixed-point equations. The extension respects the top operation at old fixed points and respects the first operation along each new chain; there are no other defined operations on those chains to check. Uniqueness follows from the same forced formulas. For the formula is . These extensions are natural and prove
On a morphism the free functor sends to .
Crucially, the top operation of has no fixed points: its defined old values move to new points, and it has no defined new values when ; for it is the shift. The next free extension therefore adds no points and equips the object with an everywhere-undefined next operation. The same remains true at every subsequent free extension. Hence, for , the composite left adjoint has the same first operations and underlying set as .
This agreement includes the monad structure, not just its underlying endofunctor. The units are the same zero-layer inclusions. The composite counit on an object of is the same forced extension formula, depending only on its first operations. Applying the composite forgetful functor therefore gives the same multiplication . Thus
Next prove creation of the required split coequalizers. Suppose are arrows in and their images have a split coequalizer in . Choose the splitting orientation
with , morphisms in . Denote the top operations on by . For define
Since preserves the lower operations, and this value exists. For , , so preservation by gives
Thus respects the top operation. The splitting and also show that this is the unique operation on its prescribed domain for which is a morphism. For all these domains mean the whole underlying set.
If is a morphism equalizing , its unique factor in satisfies, on ,
where is the top operation of . Hence is a morphism. This proves creates coequalizers of -split pairs.
Moreover, reflects isomorphisms: an isomorphism of the first operations reflects their fixed-point conditions, hence the domain of the next operation; the inverse of a bijective top-operation-preserving map then preserves that operation too. The Beck monadicity theorem now gives
Under this equivalence, the first Eilenberg-Moore comparison functor for the long composite is exactly forgetting all operations after the st: its algebra structure is the top-operation extension formula already computed. Repeating the argument identifies its monadic tower with the successive categories
At each stage the corresponding comparison has the remaining composite of the already constructed free extensions as a left adjoint.
No earlier stage can be an equivalence of categories. For , take the two-point set with its first operations all identities. One extension to has every later operation the identity; another has its st operation interchange the two points, and all subsequent operations undefined. Both have the same image in , but the identity function between those images is not a morphism between the extensions. Thus forgetting from to is not full. The final comparison at is an equivalence. This proves the monadic tower for nested partial unary operations has