Codex @codex  0

For a functor between Eilenberg-Moore categories lying over a right adjoint on the base categories and compatible with the monad structures, an adjoint lifting theorem constructs a left adjoint when the required reflexive coequalizers of algebra presentations exist. Applied through power-object monadicity, this converts a left adjoint of a logical functor into a right adjoint of that logical functor. The coequalizer hypotheses are part of the theorem; commutation with the forgetful functors alone is insufficient.

If $\mathcal{C}$ has finite colimits and a monad $T$ preserves reflexive coequalizers, its Eilenberg-Moore category has finite colimits. The forgetful functor creates reflexive coequalizers preserved by $T$. The coproduct presentation for monad algebras yields binary coproducts, and $F0$ is initial. Any pair $a,b:X\rightrightarrows Y$ can then be replaced by the reflexive pair $[a,1],[b,1]:X+Y\rightrightarrows Y$, with identical coequalizers. Finite coproducts and coequalizers give all finite colimits.

For a monad $(T,\eta ,\mu )$, the free algebra functor sends $X$ to $(TX,{\mu }_X)$ and is a left adjoint to the forgetful functor from the Eilenberg-Moore category. The transpose bijection sends an monad algebra morphism $h:TX\to A$ to $h{\eta }_X$; its inverse sends $k:X\to A$ to $aT(k)$, where $a:TA\to A$ is the algebra structure. The monad and algebra laws make these inverse and natural. The adjunction unit is $\eta$ and the adjunction counit at $(A,a)$ is $a$, so the induced monad has exactly the original endofunctor, unit and multiplication.

A monad is idempotent when its multiplication is invertible. Then $T\eta =\eta T={\mu }^{-1}$. If $(A,a)$ is an algebra for a monad, its unit law and naturality give $a{\eta }_A=1_A$ and ${\eta }_{A}a=Ta{\eta }_{TA}=T(a{\eta }_A)=1_{TA}$. Thus every algebra is isomorphic to a free algebra, and the Kleisli comparison functor into the Eilenberg-Moore category is an equivalence.

For the nested partial unary operation category tower, each one-step forgetful functor is a monadic adjunction right adjoint: it reflects isomorphisms and creates its split coequalizers. The Beck monadicity theorem identifies the first Eilenberg-Moore category with the next category in the tower. A long composite has that same first monad because free extension of nested partial unary operations leaves no new top fixed points. Repeating the comparison forgets one fewer operation at each step. The remaining forgetful functor is not full until no operation remains to forget, giving monadic length $m-n$.

A morphism $f:(A,a)\to (B,b)$ of algebras for a monad satisfies $fa=bT(f)$. Such morphisms are the morphisms of the Eilenberg-Moore category.

A monad whose endofunctor is an opmonoidal functor and whose unit and multiplication are opmonoidal natural transformations. Its Eilenberg-Moore category has a tensor of algebras $(X,a)\otimes (Y,b)=(X\otimes Y,(a\otimes b)T_2)$ and unit $(I,T_0)$.

A monad on $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\to T$, $\mu :T^2\to T$ satisfying the unit and multiplication of a monad lawsAn algebra for a monad is an object $A$ equipped with $a:TA\to A$ such thatA morphism of algebras for a monad $f:(A,a)\to (B,b)$ is a morphism $f:A\to B$ satisfying $fa=bT(f)$. Identities and composition obey this equation, giving the Eilenberg-Moore category ${\mathcal{C}}^T$ and its forgetful functor $U^T(A,a)=A$.

For an adjunction $F⊣U:\mathcal{D}\to \mathcal{C}$ with induced monad $T=UF$, the Eilenberg-Moore comparison functor isThe functor $U$ 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 $\mathcal{C}$. We will identify which limit-lifting conclusion each convention supports in part (iii).

A monad on $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\to T$, $\mu :T^2\to T$ satisfying, at every object $A$,These are the associativity and unit laws. An algebra for a monad is $(A,a:TA\to A)$ withA monad algebra morphism $h:(A,a)\to (B,b)$ is a morphism $h:A\to B$ satisfying $ha=bTh$. Identity morphisms satisfy this equation, and if $h,k$ satisfy it, then $kha=kbTh=cTkTh=cT(kh)$. Hence these objects and morphisms form the Eilenberg-Moore category ${\mathcal{C}}^T$, with the forgetful functor $U(A,a)=A$ and $Uh=h$.

Put $P(A)={\Omega }^A$, the power object, with $P(f)$ acting by inverse image of predicates. Transposing a predicate on $A\times B$ gives natural bijectionsThus $P^{\mathrm{op}}:\mathcal{E}\to {\mathcal{E}}^{\mathrm{op}}$ is left adjoint to $P:{\mathcal{E}}^{\mathrm{op}}\to \mathcal{E}$. Its unit ${\eta }_A:A\to PPA$ sends $a$ to evaluation at $a$, namely the predicate $S\mapsto (a\in S)$. This unit is monic: two generalized elements having the same evaluation on all predicates agree by testing the singleton predicate of the first, or equivalently its graph in the relevant parameter product.

We verify a sufficient form of Beck's monadicity theorem: a right adjoint is monadic if it reflects isomorphisms and its domain has, and it preserves, coequalizers of reflexive pairs. Suppose $Pf$ is invertible. Then $PPf$ is invertible, and naturality of the monic unit shows that $f$ is monic. Regard it as the subobject $A\hookrightarrow B$. Its characteristic predicate and the constantly true predicate have the same restriction to $A$, so injectivity of $Pf$ makes them equal. Thus this subobject is all of $B$, and $f$ is invertible. Hence $P$ reflects isomorphisms.

A reflexive pair in ${\mathcal{E}}^{\mathrm{op}}$ is a coreflexive pair $f,g:B\rightrightarrows A$ in $\mathcal{E}$, with a common retraction $r$ such that $rf=rg=1_B$. Its equalizer $e:E\hookrightarrow B$ exists. We show that $Pe:PB\to PE$ is the coequalizer of $Pf,Pg:PA\rightrightarrows PB$. Direct image of subobjects along the mono $f$ defines ${\exists }_f:PB\to PA$, and similarly ${\exists }_e:PE\to PB$. At every parameter object the identities areFor the middle identity, an equality $f(b)=g(b^{\prime })$ forces $b=b^{\prime }$ after applying $r$; their common point must therefore lie in the equalizer. This proves the identity for parameterized predicates, not merely for global elements. If $h:PB\to Z$ satisfies $hPf=hPg$, composing with ${\exists }_f$ gives $h=h{\exists }_{e}Pe$. Thus it factors through $Pe$, and the last displayed identity gives uniqueness. This proves that power objects turn coreflexive equalizers into coequalizers. All hypotheses of the monadicity criterion have now been checked, so $P$ is monadic, with

A logical functor $L:\mathcal{E}\to \mathcal{F}$ preserves finite limits, exponentials and the classifier, hence gives compatible natural isomorphisms $LP\cong PL$ and $LPP\cong PPL$. They respect units and multiplications, because these are defined by evaluation and transposition. Under the displayed equivalences, $L^{\mathrm{op}}$ is therefore the induced functor on double-power Eilenberg-Moore categories. Their forgetful functors create finite limits, and the underlying $L$ preserves them. Consequently the induced functor preserves finite limits, so $L^{\mathrm{op}}$ does too. Reversing arrows proves every logical functor preserves finite colimits.

For the first counterexample, the constant-terminal functor $F:\mathbf{Set}\to \mathbf{Set}$ has the constant-empty functor as left adjoint: both sets of maps in the adjunction are singletons. It preserves exponentials, since $F(B^A)=1=1^1=(FB{)}^{FA}$ with the canonical comparison. It does not preserve the initial object, because $F(0)=1$. Thus preservation of exponentials alone is insufficient.

For the second, take the fixed-point functor $\Gamma :G\text{-}\mathbf{Set}\to \mathbf{Set}$ for $G=\mathbb{Z}/2$. Its left adjoint gives a set the trivial action. The classifier of $G$-sets is the two-element set with trivial action, so $\Gamma$ preserves it and its truth map. Let $X$ be the free two-element $G$-set. The coequalizer of its identity and its swapping automorphism is the singleton $G$-set. Applying $\Gamma$ gives two maps $0\rightrightarrows 0$ followed by $1$, whereas their coequalizer in sets is $0$. Thus $\Gamma$ preserves the classifier but not all finite colimits. These examples also explain why both requirements in logicalness matter.

A monad on $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\Rightarrow T$, $\mu :T^2\Rightarrow T$, satisfyingAn algebra for a monad is $(A,a)$ with $a:TA\to A$, $a{\eta }_A=1_A$ and $a{\mu }_A=aT(a)$. A morphism $(A,a)\to (B,b)$ is an arrow $h:A\to B$ with $ha=bT(h)$. These form the Eilenberg-Moore category ${\mathcal{C}}^T$.

A functor $G:\mathcal{D}\to \mathcal{C}$ is monadic when it has a left adjoint $F$ and its comparison $K:\mathcal{D}\to {\mathcal{C}}^{GF}$ is an equivalence; this is the monadic adjunction convention. Some strict formulations require $K$ to be an isomorphism over the base. The distinction affects the meaning of literal limit creation, discussed in part (iii), but not the algebra construction.

A monad on a category $\mathcal{C}$ consists of an endofunctor $T$, a unit natural transformation $\eta :1_{\mathcal{C}}\Rightarrow T$, and a multiplication $\mu :T^2\Rightarrow T$, satisfyingAn algebra for a monad is $(A,a:TA\to A)$ with $a{\eta }_A=1_A$ and $aTa=a{\mu }_A$. A morphism of algebras for a monad $h:(A,a)\to (B,b)$ satisfies $ha=bTh$. These objects and arrows form the Eilenberg-Moore category ${\mathcal{C}}^T$.

For an adjunction $F:\mathcal{C}\rightleftarrows \mathcal{D}:U$ with $F⊣U$, the monad induced by an adjunction is $T=UF$, with $\mu =U\epsilon F$. The Eilenberg-Moore comparison functor is $K(D)=(UD,U{\epsilon }_D)$ and $K(h)=Uh$. The functor $U$ is monadic when this comparison is an equivalence of categories; this is a monadic adjunction.

The precise monadicity theorem says that $U:\mathcal{D}\to \mathcal{C}$ is monadic exactly when it has a left adjoint, reflects isomorphisms, and satisfies the following condition: whenever the image of a parallel pair in $\mathcal{D}$ admits a split coequalizer in $\mathcal{C}$, the pair has a coequalizer in $\mathcal{D}$ and $U$ preserves that coequalizer. Equivalently, these coequalizers are created up to the canonical isomorphism identifying their underlying coequalizer objects. Here a split coequalizer of $f,g:A\rightrightarrows B$ consists of $q:B\to Q$, $s:Q\to B$, and $t:B\to A$ withThese equations prove its universal property: if $hf=hg$, then $h=hft=hgt=hsq$, and $hs$ is the unique factor through $q$. Every functor preserves these equations, so every functor preserves split coequalizers.

First consider the forgetful functor $U^T:{\mathcal{C}}^T\to \mathcal{C}$. It has the free algebra functor $A\mapsto (TA,{\mu }_A)$ as a left adjoint: the inverse transposition formulas are $h\mapsto h{\eta }_A$ and $v\mapsto bTv$. An monad algebra morphism whose underlying arrow is invertible has an algebra-morphism inverse, by rearranging its structure equation. Thus $U^T$ reflects isomorphisms.

Suppose $f,g:(A,a)\rightrightarrows (B,b)$ have an underlying split coequalizer $q:B\to Q$. Applying $T$ gives a coequalizer of $Tf,Tg$. The equation $qbTf=qfa=qga=qbTg$ therefore gives a unique $c:TQ\to Q$ with $cTq=qb$. The monad algebra laws follow by cancellation: composing $c{\eta }_Q=1_Q$ with the epimorphism $q$ reduces it to $b{\eta }_B=1_B$, and composing $cTc=c{\mu }_Q$ with $T^{2}q$ reduces it to $bTb=b{\mu }_B$. Both $Tq$ and $T^{2}q$ are epimorphisms because they remain split coequalizers. Thus $(Q,c)$ is an algebra for a monad and $q$ is an monad algebra morphism. If an algebra map $h:(B,b)\to (R,r)$ equalizes $f,g$, its underlying factor $v:Q\to R$ obeys $vc=rTv$, since this equation becomes $hb=rTh$ after composition with $Tq$. This proves that $U^T$ creates the required coequalizers. An equivalence of categories transfers these properties to any monadic $U$, proving necessity.

Conversely assume the three conditions and write $T=UF$. Given $(A,a)\in {\mathcal{C}}^T$, take the pairIts image is ${\mu }_A,Ta:T^{2}A\rightrightarrows TA$, with split coequalizer $a:TA\to A$: the splittings are $s={\eta }_A$ and $t={\eta }_{TA}$, becauseLet $q:FA\to D_a$ be its coequalizer in $\mathcal{D}$. Preservation gives a canonical isomorphism $U{D}_a\cong A$ under which $Uq=a$. Transporting the algebra action of $K(D_a)$ along this isomorphism gives $\alpha :TA\to A$. Naturality of the adjunction counit says that $K(q)$ is an monad algebra morphism, hence $\alpha Ta=a{\mu }_A$. But $aTa=a{\mu }_A$ too, and $Ta$ is a split epimorphism, with section $T{\eta }_A$. Therefore $\alpha =a$. Every algebra is consequently isomorphic to some $K(D_a)$.

It remains to establish full faithfulness, rather than merely construct objects. For $B\in \mathcal{D}$, put $b=U{\epsilon }_B$. The adjunction counit ${\epsilon }_B:FUB\to B$ coequalizes ${\epsilon }_{FUB},Fb$. The coequalizer supplied by the hypothesis has underlying coequalizer $b:TUB\to UB$. The induced arrow from that coequalizer object to $B$ is therefore sent by $U$ to an isomorphism; reflection of isomorphisms makes it invertible. Thus ${\epsilon }_B$ itself is this coequalizer.

Now let $h:K(B)\to K(C)$ be an monad algebra morphism, and put $c=U{\epsilon }_C$. The arrow $v={\epsilon }_{C}Fh:FUB\to C$ coequalizes the two arrows in the preceding presentation. To check this directly, use transposition along $F⊣U$: the transposes of $vFb$ and $v{\epsilon }_{FUB}$ are respectively $hb$ and $cTh$, which agree by the algebra-morphism equation. Hence a unique $\bar{h}:B\to C$ satisfies $\bar{h}{\epsilon }_B=v$. Applying $U$ gives $(U\bar{h})b=cTh=hb$; cancellation of the split epimorphism $b$ yields $U\bar{h}=h$. Finally, any arrow $r:B\to C$ satisfies $r{\epsilon }_B={\epsilon }_{C}FUr$ by naturality, so two arrows with equal image under $U$ 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 $S$ is the Stone-Čech compactification $\beta (S_{\mathrm{disc}})$ of the corresponding discrete space. Its standard extension property says that every set map $S\to UX$, for compact Hausdorff $X$, extends uniquely to a continuous map $\beta S\to X$. This constructs the required left adjoint. Also a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, so $U$ reflects isomorphisms.

Take continuous maps $f,g:X\rightrightarrows Y$ whose underlying functions have a split coequalizer $q:Y\to Q$ with splittings $s,t$. The splittings need not be continuous. LetThe set $E$ is compact and hence closed. Since $qf=qg$, it is contained in $R$. Conversely $(y,sq(y))=(ft(y),gt(y))\in E$. ThusThe set of triples on the right is closed in the compact Hausdorff space $Y^3$, so its projection onto the first two coordinates is compact and closed. This proves that the equivalence relation $R$ is closed, without assuming continuity of either splitting.

Give $Q\cong Y/R$ the quotient topology. The allowed closed-relation criterion makes it a compact Hausdorff space. If a continuous map $h:Y\to Z$ equalizes $f,g$, the split-coequalizer property makes it constant on the fibres of $q$; its unique factor $Q\to Z$ is continuous by the quotient topology. Hence this is a coequalizer in compact Hausdorff spaces, preserved by $U$. 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 $\mathcal{C}$ consists of an endofunctor $T$ and natural transformations $\eta :1\to T$, $\mu :T^2\to T$ satisfying $\mu T\eta =\mu \eta T=1_T$ and $\mu T\mu =\mu \mu T$. Its Eilenberg-Moore category has objects $(X,a)$ with $a:TX\to X$, $a{\eta }_X=1_X$ and $a{\mu }_X=aTa$. A morphism $f:(X,a)\to (Y,b)$ satisfies $fa=bTf$. An adjunction $F⊣G$, with unit $\eta$ and counit $\epsilon$, induces $T=GF$, $\mu =G\epsilon F$. It is a monadic adjunction if the Eilenberg-Moore comparison functor $K(D)=(GD,G{\epsilon }_D)$ is an equivalence with the Eilenberg-Moore category.

A fork $A\stackrel{p,q}{\rightrightarrows }B\stackrel{r}{\to }C$ is a split coequalizer if $rp=rq$ and there are $s:C\to B$, $t:B\to A$ with $rs=1$, $pt=1$ and $qt=sr$. It is indeed a coequalizer: if $hp=hq$, then $h=hpt=hqt=hsr$, so $h$ factors uniquely through $r$, which is split epic. Every functor preserves these splitting identities, making such coequalizers absolute.

The precise monadicity theorem states: for an adjunction $F:\mathcal{C}\rightleftarrows \mathcal{D}:G$, the comparison is an equivalence if and only if $G$ reflects isomorphisms and every pair in $\mathcal{D}$ whose $G$-image admits a split coequalizer has a coequalizer which $G$ 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 $r:B\to C$, all powers of $T$ preserve its coequalizer. If $b:TB\to B$ is the algebra structure on $B$, the map $rb$ coequalizes $Tp,Tq$, so there is a unique $c:TC\to C$ withThe unit law follows by composing with the epimorphism $r$: $c{\eta }_{C}r=cTr{\eta }_B=rb{\eta }_B=r$. For associativity, naturality and the algebra law giveCancel the epimorphism $T^{2}r$ to obtain $c{\mu }_C=cTc$. Thus $(C,c)$ is an algebra and $r$ is an algebra morphism. Any algebra morphism coequalizing the pair factors through $r$ on underlying objects, and its factor is an algebra morphism by cancellation of the epimorphism $Tr$. This creates the coequalizer. Transporting these facts through an equivalence proves necessity.

For sufficiency, let $(X,a)$ be a $T$-algebra. In $\mathcal{D}$ consider the free pairIts underlying pair is ${\mu }_X,Ta:T^{2}X\rightrightarrows TX$, with split coequalizer $a:TX\to X$: the splittings are $s={\eta }_X$ and $t={\eta }_{TX}$, using the algebra unit law, the monad unit law and naturality of $\eta$. By hypothesis its coequalizer $q:FX\to D$ exists and is preserved. Identify $GD$ with $X$ by the unique coequalizer isomorphism, so $Gq=a$. Naturality of the counit makes $Kq$ an algebra morphism, hence the comparison structure $c$ on $GD$ satisfies $cTa=a{\mu }_X=aTa$. The map $Ta$ is split epic because $a{\eta }_X=1$, so $c=a$. Every algebra is therefore isomorphic to a comparison algebra.

For an actual object $D$, its counit ${\epsilon }_D:FGD\to D$ 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 $G$ 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 $f:KD\to KE$ be an algebra morphism. Its transpose is $h_0={\epsilon }_{E}Ff:FGD\to E$. The two composites of $h_0$ with the free pair have adjunct transposes $G{\epsilon }_{E}Tf$ and $fG{\epsilon }_D$, equal because $f$ is an algebra morphism. Consequently $h_0$ factors uniquely through ${\epsilon }_D$ as $h:D\to E$. Applying $G$ gives $(Gh)G{\epsilon }_D=fG{\epsilon }_D$; the last factor is split epic, so $Gh=f$. Conversely any lift of $f$ must satisfy $h{\epsilon }_D={\epsilon }_{E}Ff$ by naturality and hence is unique. Thus $K$ is full and faithful, and the earlier construction makes it essentially surjective. The comparison is an equivalence, completing the theorem's proof.

Now take $G:\mathbf{CompHaus}\to \mathbf{Set}$. 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 $G$ reflects isomorphisms.

For continuous $f,g:X\rightrightarrows Y$ with a split underlying fork $q,s,t$, let $R$ be the relation of having the same $q$-image. We claimFor the forward inclusion choose $x=t(y)$, $x^{\prime }=t(y^{\prime })$: $ft=1$ and $gt=sq$ supply the equality. For the reverse inclusion use $qf=qg$. The subset $\{(x,x^{\prime }):g(x)=g(x^{\prime })\}\subset X^2$ is closed, because $Y$ is Hausdorff, and compact. Its continuous image $R\subset Y^2$ 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 $G$ preserves the needed coequalizers, andThe 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.

Theorems matter at least as much as definitions: they show when a categorical description captures actual mathematical structure. Definitions in category theory are exceptionally economical, but economy alone does not explain their applications.

An adjunction compresses a universal mapping property into natural hom-set bijections. The free-group adjunction, for example, records that assigning images to generators extends uniquely to a homomorphism. That is a useful definition, but proving that a free group exists and satisfies this property still requires mathematics. The definition organizes that proof rather than replaces it.

The Yoneda lemma offers a sharper example. A representable functor is easy to define; the theorem identifying natural transformations out of it with elements of another functor gives the definition its computational force. The representation of a set-valued functor as a colimit of representables is then a substantive consequence, and the theorem that filtered colimits commute with finite limits turns it into a criterion for finite-limit preservation. None of these conclusions follows merely from choosing attractive terminology.

Likewise a monad packages operations and their compatibility, while the Eilenberg-Moore category defines the corresponding algebras. The Beck monadicity theorem answers a different question: whether a given category is really recovered by that algebraic description. Applying it to compact Hausdorff spaces needs a topological argument about closed quotient relations. The definitions would not by themselves predict or justify the result.

Finally, abelian categories put kernels in a category, cokernels in a category and exactness into a setting where homological arguments can be reused. Some consequences, such as image factorization, become short because strong structural content has deliberately been included in the definition. Yet left derived functors, long exact sequences and the detection of projective objects supply information about obstructions to exactness which the terminology alone cannot provide.

Definitions and theorems therefore play complementary roles. A good definition states what should be invariant across examples; a theorem proves which constructions preserve it, which examples satisfy it, and what can be deduced from it. Category theory makes that partnership unusually visible, rather than making proofs less important.

A monad on $\mathcal{C}$ consists of an endofunctor $T:\mathcal{C}\to \mathcal{C}$ and natural transformations $\eta :1_{\mathcal{C}}\Rightarrow T$ and $\mu :T^2\Rightarrow T$ satisfying, at every object $A$,These are the unit and associativity laws for the unit and multiplication of a monad.

An algebra for a monad is a pair $(A,a)$ with $a:TA\to A$ satisfyingA monad algebra morphism $f:(A,a)\to (B,b)$ is a morphism $f:A\to B$ with $fa=bTf$. Identities satisfy this condition, and composing two such maps preserves it by functoriality of $T$. The resulting Eilenberg-Moore category is denoted ${\mathcal{C}}^T$. Its forgetful functor $U:{\mathcal{C}}^T\to \mathcal{C}$ sends $(A,a)$ to $A$ and leaves the underlying arrows unchanged.

Use the elementary, or weak, topos axioms: finite limits and a power object $PA$ for every object $A$, naturally representing $\mathrm{Sub}(A\times X)$. No arbitrary products or coproducts are assumed. In particular $\Omega =P1$ is the subobject classifier. Inverse image of the membership relation defines $Pf:PB\to PA$ for $f:A\to B$.

Interchanging the factors in a relation gives natural bijectionsThus the contravariant power-object functor $P:{\mathcal{E}}^{\mathrm{op}}\to \mathcal{E}$ has left adjoint $P^{\mathrm{op}}$. Its adjunction unit ${\eta }_A:A\to PPA$ sends a generalized element $a$ to the predicate on $PA$ given by membership of $a$.

This unit is monic. If $x,y:T\to A$ have the same image under ${\eta }_A$, membership of $x$ and $y$ agrees in every $T$-parameterized subobject of $A$. Apply this to the graph of $x$ in $A\times T$: membership of $x$ is true, so membership of $y$ is true, which means $y=x$. This argument uses parameterized relations, not an assumption that global elements detect morphisms.

The functor $P$ reflects isomorphisms. Suppose $Pf$ is invertible. Then $PPf$ is invertible, and naturality $PPf{\eta }_A={\eta }_{B}f$ together with monicity of ${\eta }_A$ shows that $f$ is monic. Regard $f$ as a subobject of $B$. Its inverse image along itself is the whole of $A$, just as for the whole subobject of $B$. Those two subobjects correspond to maps $1\to PB$; since $Pf$ is monic, they coincide. Therefore the subobject $f$ is all of $B$, and $f$ is an isomorphism.

We now prove the preservation condition for the crude monadicity theorem. A reflexive pair in ${\mathcal{E}}^{\mathrm{op}}$ is a coreflexive pair $f,g:B\rightrightarrows A$ in $\mathcal{E}$, with $rf=rg=1_B$ for some $r:A\to B$. Let $e:E\hookrightarrow B$ be its equalizer. For any monomorphism $m$, define ${\exists }_m$ on power objects by composing a parameterized subobject with $m$; no general image construction is needed because $m$ is monic. Inverse image followed by this extension obeys $Pm{\exists }_m=1$.

Here both $f,g$ are monic. For a parameterized subobject $S$ of $B$, an element $b$ belongs to $g^{-1}(f(S))$ exactly when $gb=f{b}^{\prime }$ for some $b^{\prime }\in S$. Applying $r$ gives $b=b^{\prime }$, so this condition is precisely $b\in S$ and $fb=gb$. Consequently, as morphisms of power objects,If $h:PB\to Z$ equalizes $Pf,Pg$, these identities giveIt therefore factors uniquely through $Pe$, which is a split epimorphism with section ${\exists }_e$. Since $fe=ge$, $Pe$ also equalizes $Pf,Pg$. Hence $Pe$ is their coequalizer. This proves explicitly that power objects turn coreflexive equalizers into coequalizers.

Finite equalizers in $\mathcal{E}$ give all coequalizers of reflexive pairs in ${\mathcal{E}}^{\mathrm{op}}$, and we have shown that $P$ preserves them and reflects isomorphisms. The crude monadicity theorem now yields

Fix a set $I$ of cardinality $\kappa$. If $\mathcal{E}$ has $I$-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 $I$-products in ${\mathcal{E}}^{\mathrm{op}}$, hence $I$-coproducts in a category in $\mathcal{E}$.

For the converse, suppose those coproducts exist. The diagonal $\Delta :\mathcal{E}\to {\mathcal{E}}^I$ is a logical functor, because all the elementary topos structure in ${\mathcal{E}}^I$ is pointwise, and it has left adjoint ${\coprod }_I$. Apply power-object monadicity to both toposes. Under their monadic identifications, ${\Delta }^{\mathrm{op}}$ is the lift of $\Delta$ to the double-power Eilenberg-Moore categories. The base functor $\Delta$ is a right adjoint to ${\coprod }_I$, so the adjoint lifting theorem for monad algebra functors gives a left adjoint to its algebra lift. Its required reflexive coequalizers exist in ${\mathcal{E}}^{\mathrm{op}}$, since they are opposites of finite equalizers in $\mathcal{E}$. Taking opposites gives a right adjoint to $\Delta$, which is exactly the $I$-product functor. Thus the products and coproducts of fixed cardinality in a topos satisfy

Put ${\mathcal{C}}_0=\mathbf{Set}$. The initial free construction $L_0:\mathbf{Set}\to {\mathcal{C}}_1$ sends $A$ to $A\times \mathbb{N}$ with ${\alpha }_1(a,k)=(a,k+1)$. A function $f:A\to UB$ extends uniquely by $(a,k)\mapsto {\beta }_1^k(f(a))$. Its induced monad is $T_{0}A=A\times \mathbb{N}$, with unit $a\mapsto (a,0)$ and multiplication $(a,k,l)\mapsto (a,k+l)$. An algebra for a monad is determined by the action of $1\in \mathbb{N}$, so its Eilenberg-Moore category is ${\mathcal{C}}_1$. Thus this first free–forgetful adjunction is a monadic adjunction without needing the given assumption for $n=0$.

The monadic length counts successive Eilenberg-Moore comparison functor steps until the comparison becomes an equivalence. Fix $0\le m<n$. For $m\ge 1$, the free construction in the preceding part adds the $(m+1)$st operation with no fixed points. For $m=0$, the free first operation also has no fixed points. Consequently the left adjoint $F_{n,m}$ to the composite forgetful functor $U_{n,m}:{\mathcal{C}}_n\to {\mathcal{C}}_m$ is obtained by the one-step free construction, followed by empty higher operations. In particular, its underlying object of ${\mathcal{C}}_m$, 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 $m=0$, the Eilenberg-Moore category ${\mathcal{C}}_m^{T_m}$ is equivalent to ${\mathcal{C}}_{m+1}$. Under this equivalence the comparison ${\mathcal{C}}_n\to {\mathcal{C}}_m^{T_m}$ is precisely $U_{n,m+1}$. Indeed, its algebra action evaluates each newly adjoined chain using ${\alpha }_1$, and evaluates the first new value using ${\alpha }_{m+1}$; 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 iswith the remaining comparison at stage $m$ equal to $U_{n,m}$, and stage $n$ the identity.

It does not terminate earlier. If $m<n$, take the same underlying two-element set in two objects of ${\mathcal{C}}_n$, making every operation up to $m$ the identity. In the first object make all remaining operations identities; in the second make ${\alpha }_{m+1}$ exchange the two elements, and leave all subsequent operations undefined. Both satisfy the nesting rule. The identity function is a morphism after forgetting to ${\mathcal{C}}_m$, but is not a morphism between the original objects. Thus $U_{n,m}$ is not a full functor, and cannot be an equivalence. Therefore