Let continuous maps between compact Hausdorff spaces have an underlying split coequalizer with set maps satisfying , and . Its equivalence relation is the image of the closed subset under . One inclusion follows from ; for the other use and whenever . This image is compact and hence closed in the Hausdorff product . The quotient is therefore compact Hausdorff, giving the preserved coequalizer required by the Beck monadicity theorem.
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.
For , a parallel pair in is G-split if its image admits a split coequalizer in . Reflection of such coequalizers means that an existing equalizing arrow in is a coequalizer whenever its image is the corresponding split coequalizer. This asserts a property of existing arrows; it does not assert that a lift exists for every base quotient.
For algebra maps whose underlying maps have a split coequalizer , every functor preserves the split diagram, including and . Since equalizes , it factors uniquely to the displayed action . Cancellation of the epimorphisms proves the unit and multiplication laws. Any algebra-valued map equalizing the pair factors through , and cancelling proves that its factor preserves the action. This establishes creation of that coequalizer.
A form of Beck's monadicity theorem compatible with equivalence-based monadic adjunctions is this. A functor is monadic exactly when it has a left adjoint, is a conservative functor, and has coequalizers of all pairs whose images under admit a split coequalizer, with preserving these coequalizers. In the strict lifting formulation, one states creation of these coequalizers. Such a pair is a functor-split coequalizer pair; the splitting is required in the base category, not necessarily upstairs.
A split coequalizer fork has maps and such that
Every functor preserves this coequalizer: if , then , and is split epic, so the factor through is unique. The same equations remain true after applying any functor.
For necessity, let be the monad algebra forgetful functor. It has the free-algebra left adjoint. It reflects isomorphisms, because if an algebra map is invertible in , the equation rearranges to .
If two algebra maps have an underlying split coequalizer , then and are also coequalizers. Since equalizes , there is a unique satisfying
After composing with the epimorphism , the equation reduces to the unit law for . After composing with the epimorphism , the equation reduces to . Thus is an algebra and an algebra map. If an algebra map equalizes , its unique underlying factor satisfies : this follows by precomposing with the epimorphism . Therefore this is a coequalizer upstairs as well. This proves that the monad algebra forgetful functor creates split coequalizers. The same properties transport through the comparison equivalence of categories, with the object-lifting convention distinguished in Question 9.
For sufficiency, suppose the three conditions hold, choose , and let with comparison . For each algebra , consider the pair
Its image has coequalizer . It is split: take , , , and . The monad and algebra laws give
By hypothesis the pair has a coequalizer and is also a coequalizer. Identify with using the unique coequalizer isomorphism, so . Since is carried by to an algebra map from the free algebra, the transported action satisfies
But is a split epimorphism, with right inverse , so . Hence : the comparison is essentially surjective.
Next, for every , put . The counit of an adjunction coequalizes
This follows from naturality of the counit. The image pair has the split coequalizer , as above. If is the hypothesized preserved coequalizer, the induced map has invertible because both and coequalize the same pair. Conservativity makes invertible. Therefore itself is a coequalizer.
Let be an algebra map, so . Set . Under the adjunction transpose bijection, the two composites of with the displayed presentation pair correspond respectively to and . They are equal, so factors uniquely through , giving with . Applying yields
Since is split epic, . Thus is full. If , the transposes of and are equal, so those composites agree. The counit is epic, hence ; thus is faithful.
The comparison is full, faithful and essentially surjective, so it is an equivalence of categories. This proves monadicity. The argument also explains the role of each hypothesis: split base presentations construct all algebras, and reflection of isomorphisms turns the counit presentations into actual coequalizers upstairs.
For , consider the reflexive free-algebra presentation of a monad algebra
Both parallel morphisms are monad algebra morphisms: satisfies the monad associativity law, while is the image under of . The map is a monad algebra morphism because , and the same equation says it equalizes the pair.
Suppose is a monad algebra morphism with . Put . Naturality of and the unit law give
Moreover, since is a monad algebra morphism,
Thus is a monad algebra morphism and factors through . If , then , proving uniqueness. Therefore every monad algebra is the stated coequalizer of free algebras.
The underlying fork is a split coequalizer: take , and . Then , , and . Its splitting maps need not be monad algebra morphisms; the preceding argument separately proves the coequalizer in .
For , a functor-split coequalizer pair is a parallel pair such that its image admits a split coequalizer in . In one orientation this means morphisms , and satisfy
These equations prove that is a coequalizer: if , then , so factors ; uniqueness follows from . They remain true under every functor, making a split coequalizer an absolute colimit.
To say that reflects such coequalizers means that any fork in whose image is a split coequalizer is itself a coequalizer in . This is a reflection assertion about an existing fork; it does not by itself require lifting every split fork from , or creating its splitting maps in .
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.
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.
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.
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 .
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
In the nested partial unary operation category, suppose the lower-operation diagram has a split coequalizer with , and . The section takes eligible fixed points to eligible fixed points, so the displayed next operation is defined on exactly the required domain. For eligible , the equations give
Thus preserves the next operation. Every factored morphism preserves it by evaluating at , giving creation of the specified coequalizer. Together with reflection of isomorphisms, the Beck monadicity theorem proves one-step monadicity.