For inducing , the Eilenberg-Moore comparison functor has a left adjoint exactly when every algebra has a coequalizer of . Transposition identifies maps equalizing this pair with monad algebra morphisms , proving both directions of the criterion. The unit is and satisfies . In the base category, is a split coequalizer of , split by and . Consequently is invertible exactly when is also a coequalizer. The unit is invertible everywhere precisely when preserves all these specified coequalizers; preservation of arbitrary coequalizers is not required.
If each standard counit presentation is a coequalizer, the Eilenberg-Moore comparison functor is full and faithful. An monad algebra morphism makes equalize and ; its unique descent is the required morphism . The triangle identities for an adjunction make a split epimorphism, so descent has underlying arrow exactly . Epimorphic cancellation at proves faithfulness.
Monadic length Created 2026-09-24 Updated 2026-10-03
When each comparison functor has a left adjoint, iterating the Eilenberg-Moore comparison functor produces the monadic tower. Its monadic length is the least number of comparison steps needed to reach an equivalence; an equivalence has length zero and a non-equivalence that is already monadic has length one.
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).
Write the adjunction unit and adjunction counit of as . Its induced monad is , with multiplication . The Eilenberg-Moore comparison functor is
The unit law for is , a triangle identity for an adjunction. Naturality of at gives ; applying gives . Naturality at gives the monad algebra morphism equation for . Thus is well-defined.
For each , consider the fork in
It commutes by the naturality equation just used. Its image under is the fork of the preceding question, with parallel morphisms and final map . It is split using and . By the assumed reflection, is the coequalizer of this pair in .
For faithfulness, if for , naturality gives . A coequalizer is an epimorphism, so .
For fullness, let be a monad algebra morphism. Thus satisfies . Set . We verify explicitly that equalizes the two morphisms of the displayed fork. The monad algebra morphism equation gives
Naturality of first at and then at gives
The coequalizer therefore supplies a unique with . Applying yields . The map is split epic with section , so cancellation gives . This proves fullness, and the earlier cancellation proves faithfulness. Hence
No claim that is essentially surjective is needed; that stronger conclusion needs the corresponding existence hypotheses.
For , define the Eilenberg-Moore comparison functor
The algebra unit law is a triangle identity. Naturality of the counit at gives its algebra associativity law; naturality at gives , making an algebra morphism.
Suppose first that reflects G-split coequalizers. For every , consider the counit presentation
It equalizes the pair by counit naturality. After applying it becomes , with parallel maps . This is split: take and . The identities , and follow from the algebra law, a monad unit law, and naturality of . Reflection therefore makes a coequalizer in .
For faithfulness, if then naturality gives . Coequalizers are epic, so .
For fullness, let be an algebra morphism, so . Put . Its two composites with the counit-presentation pair are equal: by counit naturality they are and . Hence there is a unique with . Applying gives . Since is split epic, . This proves full faithfulness directly by descent.
Conversely suppose is full and faithful. We need the following explicit algebra lifting fact. For algebra morphisms with a split underlying coequalizer , the arrow equalizes . The split diagram is preserved by , so is their coequalizer and there is a unique with . Precomposing the unit equation with the epimorphism gives ; precomposing the associativity equation with the epimorphism gives equality by . Thus is an algebra action. If an algebra map equalizes , its unique underlying factor satisfies . Cancelling shows . This proves monad algebra forgetful functor creates split coequalizers.
Now take any existing equalizing arrow in whose image is such a coequalizer. The lifting fact makes the unique compatible action on its already given action , since preserves that action. Hence is a coequalizer of in the algebra category. For any arrow equalizing the pair, its unique algebra factor lifts to an arrow by fullness of ; faithfulness gives its factorization equation and uniqueness. Therefore is a coequalizer in . We have proved the full comparison and reflection of split coequalizers equivalence
An adjunction induces the monad with unit and multiplication . The Eilenberg-Moore comparison functor sends to . A monadic adjunction is one for which that comparison is an equivalence of categories. Iterating comparisons, when their left adjoints exist, gives a tower; its monadic length is the number of steps until equivalence, with length zero for an equivalence and length one for a monadic adjunction that is not already an equivalence.
The precise monadicity theorem says that a right adjoint is monadic exactly when it reflects isomorphisms and creates coequalizers of pairs whose images admit split coequalizers.
Write for one-step forgetting. For , the free extension of nested partial unary operations is the familiar set , with and unit . A map into a set with endomorphism extends uniquely by .
For , let
Keep and all its old operations, and adjoin the disjoint set . On the new points define ; every old operation with is undefined there. Define the new top operation only at the old eligible points, by for .
These domains satisfy the defining rules of the nested partial unary operation category: the new points have no -fixed points, so none has any higher operation defined. Given , extend it by
The expression is defined because sends eligible points to eligible points and is total. It preserves every defined operation; preservation of at old points determines , and preservation of determines the whole chain. Thus it is the unique extension, proving .
Figure 1.
The free new operation sends each eligible point to a new value with a free chain under the first operation
. Details.
For monadicity, reflects isomorphisms: an isomorphism of the lower structures takes bijectively to , so the inverse of a map preserving the new operation preserves it too.
Next prove the split-coequalizer lifting for a fixed-point-domain operation. Let be -morphisms and suppose their lower images have a split coequalizer , with , satisfying
Equip with on its required eligible domain. The lower-structure maps preserve eligibility. For eligible ,
so preserves the top operation. If coequalizes , its lower factor satisfies
Thus it is a morphism of the full structures. Uniqueness of the lifted operation follows from the eligible section and surjectivity of . This creates the specified coequalizer, so the Beck monadicity theorem proves each one-step adjunction is monadic.
Finally, every free top operation just constructed has no fixed points: for it shifts the free chain, while for it sends old eligible points to new distinct points and is undefined on the new points. Freely adjoining any further operation therefore changes nothing, since its required domain is empty. For , the monad induced on by the long free-and-forgetful adjunction is consequently the same monad, including unit and multiplication, as that for .
The first comparison category is thus equivalent to . Its algebra action evaluates the new formal value by , so the comparison from retains precisely that next operation and is the remaining forgetful functor. Iteration recovers one additional operation at each step. These remaining comparisons are not equivalences while an operation is still forgotten: take a two-element set with all retained operations equal to the identity, and choose the next operation to be the identity in one extension and the transposition in another. Higher operations can be identities in the first case and undefined in the second. The identity on the retained structure is not a morphism between these extensions, so the forgetful functor is not full. This includes .
The monadic tower for nested partial unary operations therefore has exactly the claimed length:
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.
For , let be the induced monad. The Eilenberg-Moore comparison functor is
The adjunction is a monadic adjunction if this functor is an equivalence of categories. To define monadic length, start with and form the comparison into the Eilenberg-Moore category of its induced monad. When has a left adjoint, repeat this construction, and continue with the subsequent comparison adjunctions. The length is the least number of comparison steps after which the comparison is an equivalence; an equivalence has length zero and a monadic non-equivalence has length one. The successive left adjoints will all be explicit in this example.
The precise monadicity theorem states: a functor with a left adjoint is monadic if and only if it reflects isomorphisms and every parallel pair in whose image admits a split coequalizer in has a coequalizer in preserved by . Here a split coequalizer of consists of , and satisfying
These identities imply the coequalizer property and survive every functor. We shall identify the relevant algebra categories directly, which proves monadicity without having to check quotient constructions separately.
Write for one step in the nested partial unary operation category tower. For , its left adjoint is
A function extends uniquely by , proving the adjunction.
For , take and let
The free extension of nested partial unary operations has underlying set
Keep the old operations on . On every new chain set , and leave the other old operations undefined on new points. Define the new operation by for , and nowhere else. This is a valid object: the new chains have no fixed points under , so all later operations are correctly undefined on them; the new top operation has exactly the required domain.
If preserves the old operations, it carries into . Its unique extension is
The formula preserves the first operation along each chain, the new operation at its old fixed-point source, and all the other defined operations. Conversely these requirements force the formula. This proves the one-step adjunction in every case.
Let . For , this is the usual free unary-operation monad: , with multiplication . An algebra action obeys and . It is uniquely determined by the total unary operation , since . Algebra morphisms are exactly functions commuting with . Thus .
For , no new chain point belongs to , so . The set consists of and two copies of the free chain at every . Multiplication is the identity on and folds both copies onto the corresponding chain in .
An algebra action must be the identity on the old copy of , by its unit law. Preservation of forces
The choices , for , are otherwise arbitrary. There are no higher old operations to preserve on new points. Associativity is automatic: on an inner chain both and apply the displayed formula, and on an outer chain sends to the inner chain point with the same label because ; multiplication does the same. Therefore on every point.
The data of the algebra are consequently exactly a partial operation whose domain is , that is, an object of . For a map in , the algebra-morphism equation at says precisely ; equality on the rest of the chain then follows from preservation of . Thus we have identified objects and morphisms, not just their underlying sets:
Under this isomorphism the comparison functor for is the identity identification. Hence every one-step forgetful adjunction is monadic.
Now take . In the free extension just constructed, the newly added operation has no fixed points: it sends an old point to a distinct new point, or, for , shifts along a free chain. Therefore all further operations can only be undefined. Adding them freely adds no more points. The same extension formula gives a left adjoint to .
After forgetting to , its induced monad is exactly , independent of . This includes the unit and multiplication: the unit is the old-point inclusion, and the counit formula gives the same addition of chain indices for or the same folding of the two chain copies for . Its comparison functor, after the identification , is exactly
Indeed, the comparison action on the first point of each free chain recovers , while the higher operations are forgotten. Thus each comparison step recovers exactly one additional operation. After steps from sets, the comparison is the identity of .
No earlier step is an equivalence. For , put all of the first operations equal to the identity on a three-element set. In one structure choose to be the cycle , and in another choose its reverse . Both have no fixed points at this stage, so every higher operation is undefined. The identity function between their underlying objects is a morphism there, but does not preserve . Hence is not full, and cannot be an equivalence. This also applies for , when there are no old operations. We conclude
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.
With , unit and multiplication , the Eilenberg-Moore comparison functor is
Here is the monad algebra action, and the underlying functor satisfies . The triangle identities and counit naturality provide the monad algebra laws and the compatibility of , as required for this definition.
Put . The initial free construction sends to with . A function extends uniquely by . Its induced monad is , with unit and multiplication . An algebra for a monad is determined by the action of , so its Eilenberg-Moore category is . Thus this first free–forgetful adjunction is a monadic adjunction without needing the given assumption for .
The monadic length counts successive Eilenberg-Moore comparison functor steps until the comparison becomes an equivalence. Fix . For , the free construction in the preceding part adds the st operation with no fixed points. For , the free first operation also has no fixed points. Consequently the left adjoint to the composite forgetful functor is obtained by the one-step free construction, followed by empty higher operations. In particular, its underlying object of , unit and multiplication are exactly those of the one-step adjunction:
as monads, not merely as object functions. The multiplication agrees because both counits evaluate the same first new operation and the same chains; no later operation has a value on a free object.
By the assumed one-step monadic adjunction property, or the explicit argument above when , the Eilenberg-Moore category is equivalent to . Under this equivalence the comparison is precisely . Indeed, its algebra action evaluates each newly adjoined chain using , and evaluates the first new value using ; it retains that operation and ignores all higher ones. The comparison has a left adjoint by the same explicit free extension. Thus the whole monadic tower for nested partial unary operations is
with the remaining comparison at stage equal to , and stage the identity.
It does not terminate earlier. If , take the same underlying two-element set in two objects of , making every operation up to the identity. In the first object make all remaining operations identities; in the second make exchange the two elements, and leave all subsequent operations undefined. Both satisfy the nesting rule. The identity function is a morphism after forgetting to , but is not a morphism between the original objects. Thus is not a full functor, and cannot be an equivalence. Therefore
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.
The crude monadicity theorem in its reflexive-coequalizer form says: if , is a conservative functor, has reflexive coequalizers, and preserves them, then the Eilenberg-Moore comparison functor , for , is an equivalence of categories. Requiring all coequalizers to exist and be preserved is a stronger sufficient form.
For an algebra , form in the coequalizer
The pair is a reflexive pair with common section : both composites are the identity by the algebra unit law and the triangle identity. An arrow transposes to . The two composites and transpose to and , respectively. Indeed the latter transpose is , while by counit naturality. Thus equalizes the pair exactly when is an monad algebra morphism . The coequalizer property gives natural bijections
These define on arrows by uniqueness, so . Its unit has underlying arrow .
By preservation, coequalizes and in . The action is a split coequalizer of that pair: take and , with and . Thus there is a unique isomorphism with . We have . Also
Consequently , and epimorphic cancellation gives . The adjunction unit is an monad algebra morphism; its invertible underlying arrow has an algebra-morphism inverse. Thus the unit of is an isomorphism.
For its counit , the triangle identity gives . Hence , and therefore , is an isomorphism. Since is a conservative functor, is an isomorphism too. Both unit and counit of are invertible, which proves the claimed equivalence. This proof uses only reflexive coequalizers in and split coequalizers in .
Write and , with adjunction counit . The induced monad has and . Define the Eilenberg-Moore comparison functor by
The action satisfies by a triangular equation. Naturality of at gives
Applying yields , the other algebra identity. For , naturality gives
so is a monad algebra morphism. Identities and compositions are respected because is a functor. Finally,
and the same equalities hold on morphisms. Thus both comparison identities hold, strictly when is the specified induced monad:
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
For with unit and counit , the monad induced by an adjunction is
with unit . An algebra for a monad is satisfying and .
The Eilenberg-Moore comparison functor is
If has coequalizers of reflexive pairs, define
for a -algebra . The pair has common section . Maps correspond by the coequalizer property and the adjunction exactly to algebra morphisms , naturally in both variables. Hence this is the Left adjoint to the Eilenberg-Moore comparison functor. The monadic length is the least number of successive comparison steps required for the resulting monadic tower to become an equivalence.
For , let . The free -object has underlying set
Retain all old operations on . Put
and on every new chain put
For , is undefined on the new points because none is fixed by . These definitions satisfy the domain conditions. If is a -morphism, its unique extension sends
This proves the required left adjoint.
After adjoining freely, the newly added points lie on fixed-point-free -chains, while each old point where was added is no longer fixed by . Consequently there are no points at which a further free operation must be adjoined. Thus for every the endofunctor and unit/multiplication of the monad induced on are already those induced by .
By assumption each adjacent adjunction is a monadic adjunction. The first comparison for therefore recovers , and iteration successively recovers . None of the intervening forgetful functors is an equivalence, since the next partial operation can be chosen differently on a fixed point. Starting at takes exactly steps:
For an adjunction with induced monad , the Eilenberg-Moore comparison functor is
The adjunction is monadic when is an equivalence.
The Crude monadicity theorem states that a right adjoint is monadic if it reflects isomorphisms, its source has coequalizers of reflexive pairs, and it preserves those coequalizers. The dual statement is the crude comonadicity theorem.
For with , the monad induced by an adjunction is , with unit the adjunction unit and multiplication . An algebra for a monad is a map satisfying and . The Eilenberg-Moore comparison functor is
and sends a morphism to .
Given a -algebra , form in the coequalizer
The pair is reflexive, with common section , so it exists by hypothesis. A map is equivalently a map equalizing the pair. Under adjunction this is exactly a map satisfying the -algebra homomorphism equation. Hence
naturally, and . Iterating these comparison adjunctions gives the monadic tower; the monadic length is the least number of steps required to reach an equivalence.
For a pair of sets , define
A pair of maps , extends uniquely to a commutative square from this inclusion to any injection , proving that is left adjoint to the forgetful functor .
The induced monad sends to . Its algebra unit laws show that an algebra is precisely an arbitrary function , with no injectivity requirement. Thus its Eilenberg-Moore category is the arrow category , and the comparison functor is the full inclusion of injections into all functions. This inclusion is not an equivalence, so the original adjunction is not monadic. It is reflective: a function maps to its image inclusion . The supplied result that reflections are monadic says that the next comparison is an equivalence. Therefore the original adjunction has monadic length .