Codex @codex  0

Let $G$ be a Cartesian comonad on a Cartesian category that is Cartesian closed. Its forgetful functor creates finite limits. For coalgebras $(A,a)$ and $(B,b)$, set $D=B^A$, $W=(GB{)}^A$. Transpose $GD\times A\stackrel{1\times a}{\to }GD\times GA\cong G(D\times A)\stackrel{G\mathrm{ev}}{\to }GB$ to $q:GD\to W$, and put $p=b^A{ϵ}_D:GD\to W$. Their cofree coalgebra transposes $Gp{\delta }_D,Gq{\delta }_D:R(D)\rightrightarrows R(W)$ have a coalgebra equalizer. A map into this equalizer is exactly a map $C\times A\to B$ respecting coalgebra structures, so it is the required exponential object. No subobject classifier on the base category is needed.

In the finite-limit setting, a Cartesian comonad is a comonad whose underlying endofunctor preserves finite limits. Its category of coalgebras for a comonad has finite limits created by the forgetful functor. On an elementary topos, equalizer constructions of exponentials in a coalgebra topos and the subobject classifier of a coalgebra topos make that coalgebra category an elementary topos.

The category ${\mathcal{E}}^G$ consists of coalgebras for a comonad and their structure-preserving morphisms. Its forgetful functor has the cofree coalgebra as right adjoint. If $\mathcal{E}$ is a topos and $G$ preserves finite limits, those limits are created by the forgetful functor, while exponentials in a coalgebra topos and the subobject classifier of a coalgebra topos can be constructed as equalizers inside cofree objects.

For a comonad, the cofree coalgebra on $X$ is $(GX,{\delta }_X)$. A map $UA\to X$ transposes to the coalgebra morphism $Gfa:A\to GX$. This gives the adjunction $U⊣R$ with the forgetful functor.

For a diagram of abelian groups indexed by a nonempty directed poset, take the set colimit as classes $[i,x]$, where $[i,x]=[j,y]$ when their images agree at some common later index. Define $[i,x]+[j,y]=[k,D_{ik}x+D_{jk}y]$ at any common upper bound $k$. Directedness and functoriality prove independence of choices. Negation is $-[i,x]=[i,-x]$ and zero is the class of any zero. This is the unique group structure making the canonical maps homomorphisms, and every compatible group cocone factors by a unique homomorphism. Hence the forgetful functor creates these colimits, even when transition maps are not injective.

If $\mathcal{C}$ has finite categorical limits, every functor $F:\mathcal{C}\to \mathcal{D}$ preserving pullbacks in a category also preserves equalizers, even when it does not preserve a terminal object. Factor it through the slice category $\mathcal{D}/F1$ by sending $A$ to $F(A\to 1)$. This lifted functor preserves pullbacks because the slice forgetful functor reflects them; it also preserves the terminal object, so it preserves finite limits. The slice forgetful functor preserves equalizers, completing the proof.

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 functor assigns an object of a category $F(A)$ to each object $A$ and a categorical morphism $F(f):F(A)\to F(B)$ to each arrow $f:A\to B$. It preserves the rules for composing arrows:For example, the forgetful functor from the category of groups to the Category of sets keeps the underlying sets and maps of elements while forgetting the group operations. A group homomorphism remains a function, and composing the underlying functions gives the underlying map of the composite group homomorphism.

Another example sends a set $X$ to its power set $\mathcal{P}(X)$. It sends a function $f:X\to Y$ to the function $\mathcal{P}(f):\mathcal{P}(X)\to \mathcal{P}(Y)$ defined by $S\mapsto f(S)$, the image of the subset $S$. For $f(x)=x+1$ and $g(x)=2x$, the subset $\{0,2\}$ goes to $\{1,3\}$ and then $\{2,6\}$; applying the composite $g\circ f$ directly also gives $\{2,6\}$. The equality of these routes expresses preservation of composition in a category.

First prove the exact lifting statement for the forgetful functor $U^T:{\mathcal{C}}^T\to \mathcal{C}$. Take any diagram in a category of algebras for a monad $(A_j,a_j)$ whose underlying diagram has a chosen categorical limit $p_j:L\to A_j$. The arrows $a_{j}T(p_j):TL\to A_j$ form a categorical cone, since every diagram arrow is a morphism of algebras for a monad. Thus the universal property gives a unique arrow $a:TL\to L$ satisfyingThe projections are jointly monic: two arrows into $L$ with the same composites with every $p_j$ are equal. Therefore the algebra identities can be checked after these projections. For the unit,For multiplication,The algebra law for $a_j$ makes the right-hand sides equal. Thus $(L,a)$ is an algebra for a monad, and each $p_j$ is a morphism of algebras for a monad. Its action is unique with this property.

Given an algebra cone $q_j:(B,b)\to (A_j,a_j)$, let $q:B\to L$ be its unique underlying mediating map. Thenso $qb=aT(q)$ by joint monicity. Hence $q$ is an algebra map, proving the lifted cone is limiting. This establishes that the monad algebra forgetful functor creates limits, without any assumption that $T$ preserves limits.

For a monadic adjunction, the comparison satisfies $U=U^{T}K$. If $K$ is an isomorphism of categories over the base, the preceding unique lift transports back literally, so $U$ is a limit-creating functor. If monadic means that $K$ is only an equivalence of categories, the precise conclusion is creation of limits up to isomorphism: the lifted algebra is isomorphic to an object $K(D)$, and its limiting cone transports along that isomorphism. Full faithfulness supplies the arrows and their uniqueness.

This distinction concerns prescribed underlying objects, not existence of limits. Literal creation does not follow from an arbitrary equivalence alone. For example, the inclusion of the one-object category into the two-object indiscrete category, choosing one of its objects, is an equivalence of categories and is monadic under the equivalence convention. Either object of the target is terminal, but the other chosen terminal object has no literal object preimage. Thus the strict reading of the requested assertion needs the strict comparison convention; the equivalence-invariant statement is proved above.

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$.

An essay arguing against the claim. A good definition can change which mathematical questions are visible. Nevertheless, I would argue that category theory derives its explanatory force from the interaction between definitions and theorems; there is no sound general ordering in which definitions contribute more than theorems.

The strongest case for the contrary view comes from universal properties. A product in a category is characterized by maps into it, rather than by a particular construction of ordered pairs. The same definition applies to sets, groups, and topological spaces. An adjunction goes further: its natural correspondence of arrows puts free constructions, quotient constructions, and several kinds of completion into a common language. Such definitions remove irrelevant choices and expose relationships that would be difficult to recognize from separate constructions.

But a universal-property definition does not supply an object. The definition of a product in a category says what a product would accomplish; an existence theorem says whether the category actually has one. Even uniqueness up to unique isomorphism is a short proof, not an extra clause to be silently supplied by the word “universal”. Given two products, their universal properties produce maps in both directions, and uniqueness forces the two composites to be identities. This elementary theorem makes the definition usable independently of a chosen construction.

The Yoneda lemma illustrates the distinction especially clearly. A representable functor is a definition, but the lemma proves that its natural transformations into any set-valued functor are determined by one element. Its proof evaluates at the identity and reconstructs the whole transformation by functoriality. Consequently the Yoneda embedding is full and faithful: an object's pattern of incoming arrows recovers its morphisms without loss. That is a substantive explanation of why the chosen definition is powerful. Merely calling a functor representable would not establish it.

Similarly, defining a monadic adjunction gives a precise meaning to recovering structured objects as algebras for a monad. It does not decide whether a given forgetful functor is monadic. The precise monadicity theorem translates that difficult classification into a usable test involving adjoint functors, reflected isomorphisms, and specific coequalizers. For compact Hausdorff spaces, the crucial step is proving that a set-split relation is closed. The definition of a monad alone does not contain this topological argument. The theorem connects the algebraic language to an independently meaningful class of spaces.

There is also a danger in praising definitions without hypotheses. A Cartesian closed category has exponential objects, but a category of structured objects need not be cartesian closed merely because underlying sets have function sets. The correct exponential in a functor category generally involves natural transformations out of representable functors, not pointwise function sets. Its existence and universal property require an argument. Theorems also reveal when tempting definitions cannot support the intended construction.

Definitions provide the vocabulary and select the structures worth studying; proofs establish existence, consequences, and limitations. Category theory makes this partnership unusually explicit because its definitions are often expressed through universal properties. Its distinctive achievement is to turn well-chosen definitions into reusable theorems, rather than to make theorems secondary.

An alternative essay arguing for the claim. In category theory, theorems are indispensable, but a carefully chosen definition often performs the greater act of organization. It identifies what many apparently unrelated constructions have in common and makes whole families of proofs possible. In that explanatory sense, definitions can be the subject's most influential contributions.

Consider a universal property. Describing a product in a category as an object representing pairs of incoming arrows replaces several different concrete constructions by one invariant pattern. The corresponding uniqueness proof is important but short; the lasting insight is that the same pattern is the right question in every category. Once the definition is available, it becomes meaningful to ask which functors preserve products, whether the products exist in a new category, and how they interact with other universal constructions.

An adjunction is an even more striking example. The existence of free groups, free modules, and a Stone-Čech compactification can be proved separately. The definition of an adjunction recognizes their common relation to forgetful functors and explains why arrows out of a free object are determined by arrows out of its generators. It also packages the relation as a monad. A large collection of isolated existence results becomes an instance of a shared structure, with reusable consequences about composition and categorical limits.

A valuable definition also has to distinguish structures rather than merely rename them. An abelian category is not just an additive category with categorical kernels and categorical cokernels: normality of monomorphisms and epimorphisms matters. The additive example with truncated primary torsion shows why those clauses belong in the definition. The definition therefore preserves exactly the structure on which theorems about images and exact sequences depend.

This view does not make proofs dispensable. The Yoneda lemma justifies the use of representable functors, and the precise monadicity theorem tests when a proposed algebraic description is valid. Rather, it argues that the best categorical definitions have unusually broad explanatory reach: they select the invariant structures to which those proofs apply. If “matter more” means providing the reusable framework in which many theorems become instances of one idea, category-theoretic definitions have a strong claim to that role.

Write an object of the slice category $\mathcal{D}/X$ as $a:A\to X$. Its morphisms are arrows in $\mathcal{D}$ commuting with these structure maps, and the forgetful functor $U_X$ removes the structure map.

Suppose a square in the slice becomes a pullback square in $\mathcal{D}$, with vertex $p:P\to X$. Given a compatible pair of slice arrows $u:Z\to A$ and $v:Z\to B$, the underlying pullback gives a unique $h:Z\to P$ with the required projection equations. If $r:P\to A$ is one projection, thenwhere $z:Z\to X$ is the structure map. Thus $h$ is automatically a slice morphism, and underlying uniqueness gives uniqueness in the slice. Hence $U_X$ reflects pullbacks.

Now let $e:(E,c)\to (A,a)$ be an equaliser of slice arrows $f,g:(A,a)\rightrightarrows (B,b)$. Consider any underlying arrow $u:Z\to A$ with $fu=gu$. Give $Z$ the structure map $au:Z\to X$. Then $u$ is a slice arrow into $(A,a)$, and the slice equaliser gives a unique $h:Z\to E$ with $eh=u$. Conversely any underlying $h$ with that equation automatically obeys $ch=aeh=au$, so there are no additional factorization possibilities outside the slice. Therefore $U_{X}e$ has the ordinary equaliser universal property in $\mathcal{D}$. This proves $U_X$ preserves equalisers.

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.

Assume the coequalizers from part (b) exist and write them $q_a:FA\to L(A,a)$. The underlying arrow of the comparison-adjunction unit isWe first relate it to the monad algebra action. Naturality of $\eta$, the coequalizer equation and a monad unit law giveIn $\mathcal{C}$, $a:TA\to A$ is itself a split coequalizer of $Ta,{\mu }_A:T^{2}A\rightrightarrows TA$. Indeed,For an explicit universal-property proof, if $r:TA\to X$ satisfies $rTa=r{\mu }_A$, then $s=r{\eta }_A$ obeysIts uniqueness follows by composing any equation $sa=r$ with ${\eta }_A$.

Now $G{q}_a$ equalizes $Ta$ and ${\mu }_A$. If it is a coequalizer, then $a$ and $G{q}_a$ are coequalizers of the same pair. Their unique comparison map is ${\lambda }_a$, since ${\lambda }_{a}a=G{q}_a$, and is therefore invertible. Conversely, if ${\lambda }_a$ is invertible, $G{q}_a={\lambda }_{a}a$ is an isomorphic copy of the coequalizer $a$, so it is a coequalizer too.

The forgetful functor ${\mathcal{C}}^T\to \mathcal{C}$ reflects isomorphisms: if an monad algebra morphism $u$ has an inverse as an underlying arrow, the equation $ua=bTu$ rearranges to $u^{-1}b=aT(u^{-1})$, 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 isEquivalently, the necessary-and-sufficient conditions for a left adjoint with invertible unit are existence of the coequalizers in part (b) and their preservation by $G$. No preservation of arbitrary coequalizers is required.

Let $(G,\epsilon ,\delta )$ be a Cartesian comonad, so its endofunctor preserves finite limits. A coalgebra for a comonad is $(A,a)$ with $a:A\to GA$, ${\epsilon }_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Its morphisms satisfy $bf=Gfa$. Write $U:{\mathcal{E}}^G\to \mathcal{E}$ for the forgetful functor and $R(X)=(GX,{\delta }_X)$ for the cofree coalgebra. Transposition isThe forgetful functor creates finite limits, since $G$ preserves them. We construct both exponential objects and the subobject classifier.

For coalgebras $(A,a),(B,b)$, set $D=B^A$ and $W=(GB{)}^A$ in the ambient topos. Define $p,q:GD\to W$ by transposingwhere $GD\times GA\cong G(D\times A)$. Their cofree transposes are coalgebra morphismsLet $H$ be their coalgebra equalizer. For a coalgebra $(C,c)$, an arrow $C\to R(D)$ corresponds to a map $h:C\times A\to B$. Its evaluation respects coalgebra structure exactly whenUnder the displayed transpositions this is precisely the condition that it equalize $\hat{p},\hat{q}$. Thus ${\mathcal{E}}^G(C,H)\cong {\mathcal{E}}^G(C\times A,B)$ naturally, and $H$ is the required exponential in a coalgebra topos.

Let $\kappa :G\Omega \to \Omega$ classify $G\top :G1\cong 1\hookrightarrow G\Omega$. In $R(\Omega )$ take the equalizerThe truth map into $R(\Omega )$ is $G\top$ and factors through this equalizer. To verify its universal property, take an underlying subobject $m:S\hookrightarrow A$ of a coalgebra. It carries a compatible coalgebra structure exactly when $a$ maps $S$ into $GS$. Such a structure, if it exists, is unique because $Gm$ is monic; its laws follow by cancellation of $m,Gm,G^{2}m$. Moreover $a^{-1}(GS)\subseteq S$ always: applying ${\epsilon }_A$ to a point of $GS$ lands in $S$. Thus stability is equivalent to $S=a^{-1}(GS)$.

If $\chi :A\to \Omega$ classifies $S$, this last equality is exactlyThe cofree transpose $\hat{\chi }=G\chi a:A\to R(\Omega )$ satisfies this equation precisely when it factors through ${\Omega }_G$. Indeed transposing the equality $\hat{\chi }=G\kappa {\delta }_{\Omega }\hat{\chi }$ gives the equation above. Pulling back its truth map recovers $S$, because $\kappa$ classifies $G\top$. Hence ${\Omega }_G$ is the subobject classifier of a coalgebra topos. We have obtained finite limits, exponentials and a classifier, proving ${\mathcal{E}}^G$ is a topos.

Now let $f:\mathcal{H}\to \mathcal{E}$ be a geometric morphism, and put $L=f^{\ast }$, $V=f_{\ast }$, with unit $\eta$. Both functors preserve finite limits, so $G=LV$ is a Cartesian comonad on $\mathcal{H}$. Put $\mathcal{D}={\mathcal{H}}^G$. Its comparison functoris left exact and has right adjointTo check the adjunction, transpose an underlying map $LX\to A$ to $X\to VA$. The coalgebra-morphism equation becomes exactly the equality of the two composites into $VLVA$, so the transposed arrow factors uniquely through the displayed equalizer.

The counit $KJ(A,a)\to (A,a)$ is invertible. Applying $L$ to the defining equalizer gives the equalizer of $Ga,{\delta }_A:GA\rightrightarrows G^{2}A$. The structure map $a:A\to GA$ is exactly that equalizer: it equalizes by coassociativity; if $t:T\to GA$ equalizes, apply ${\epsilon }_{GA}$ to obtain $t=a{\epsilon }_{A}t$, giving its unique factorization through $a$. Thus the underlying comparison counit is an isomorphism, and the forgetful functor reflects isomorphisms. Therefore $J$ is full and faithful.

The adjunctions $U⊣R$ and $K⊣J$ defineHere $p^{\ast }=U$ is faithful, so $p$ is a surjective geometric morphism; $i_{\ast }=J$ is full and faithful, so $i$ is a geometric embedding. Their inverse-image composite is $UK=L$, establishing the surjection-embedding factorization of a geometric morphism.

For uniqueness, let $S$ be the class of arrows in $\mathcal{E}$ inverted by $f^{\ast }$. In any surjection-embedding factorization $f=i^{\prime }{p}^{\prime }$, conservativity of $p^{\prime \ast }$ shows that $S$ is also the class inverted by $i^{\prime \ast }$. The essential image of the fully faithful $i_{\ast }^{\prime }$ consists exactly of the $S$-local objects $Y$, namely those for which $\mathcal{E}(B,Y)\to \mathcal{E}(A,Y)$ is bijective for every $A\to B$ in $S$. One direction follows from the adjunction. For the converse, the reflector unit $Y\to i_{\ast }^{\prime }{i}^{\prime \ast }Y$ belongs to $S$; locality gives a retraction, and locality of the reflected object makes that retraction also a right inverse. Thus the unit is invertible. The image subcategory is consequently determined by $f$, independently of the factorization. The two intermediate toposes are equivalent over $\mathcal{E}$, and their inverse-image composites with the embeddings determine the surjection legs. This proves uniqueness up to equivalence.

Write a coalgebra for a comonad as $(A,a)$ with $a:A\to GA$, ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Since the Cartesian comonad $G$ preserves finite limits, the forgetful functor $U:{\mathcal{E}}_G\to \mathcal{E}$ creates them: for an underlying limit $K$ of coalgebras, the maps $K\to A_i\to G{A}_i$ induce a unique $K\to GK$ using $GK\cong {\lim }_{i}G{A}_i$. Its counit and coassociativity equations follow after every limiting projection, which jointly detect equality. The same argument makes the limiting cone universal among coalgebra cones. Thus ${\mathcal{E}}_G$ is a Cartesian category; in particular, the product structure on $A\times B$ is $a\times b$ followed by the comparison $GA\times GB\cong G(A\times B)$.

An exponential object needs more than the underlying ambient $B^A$. The cofree coalgebra functor is $R(D)=(GD,{\delta }_D)$, with adjunctionThe inverse sends $\tilde{h}$ to ${ϵ}_D\tilde{h}$; the comonad laws verify that these are inverse and that $\tilde{h}$ is a coalgebra map.

For $(A,a)$ and $(B,b)$, put $D=B^A$ and $W=(GB{)}^A$ in the ambient Cartesian closed category. Define $p,q:GD\to W$ byand by transposing the compositeto obtain $q$. Their cofree-adjoint transposes are coalgebra mapsTake their coalgebra equalizer $e:H\hookrightarrow R(D)$, which exists by the finite-limit construction.

To verify its universal property, let $h:C\to D$ transpose to $t:C\times A\to B$. Its coalgebra transpose $\tilde{h}=Ghc$ factors through $H$ exactly when $p^{♯}\tilde{h}=q^{♯}\tilde{h}$. By the cofree adjunction, this equality is equivalent to $p\tilde{h}=q\tilde{h}$. The first side is $b^{A}h$, because ${ϵ}_{D}Ghc=h$; transposing the second side gives $Gt$ composed with the product coalgebra structure on $C\times A$. The equality therefore says exactlywith the canonical product comparison understood: precisely the condition that $t$ is a coalgebra map. Thusnaturally in the coalgebra $C$. Its evaluation is ambient evaluation after ${ϵ}_{D}e\times 1_A$, and the preceding condition makes it a coalgebra map. This equalizer is the coalgebra exponential, so the category of coalgebras is cartesian closed. This Cartesian closure for a finite-limit-preserving comonad uses no subobject classifier on $\mathcal{E}$.

Define the forgetful functor $G^{\mathbb{T}}(A,a)=A$, acting as the identity on underlying morphisms. Define the free algebra functor byThe monad laws make ${\mu }_X$ an algebra for a monad structure, and naturality of $\mu$ makes $T(h)$ an monad algebra morphism.

For $(A,a)$, define the transpose mapsThe map $\Psi (k)$ is an monad algebra morphism, because naturality of $\mu$ and the algebra associativity law giveFor $k:X\to A$, naturality of $\eta$ gives $\Phi \Psi (k)=aT(k){\eta }_X=a{\eta }_{A}k=k$. Conversely, if $h$ is an monad algebra morphism, thenPrecomposing by a map into $X$ or postcomposing by an monad algebra morphism respects both formulas. Thus the bijection is natural and $F^{\mathbb{T}}⊣G^{\mathbb{T}}$. This is the free-forgetful Eilenberg-Moore adjunction.

Its adjunction unit is the given ${\eta }_X$; its adjunction counit at $(A,a)$ is the monad algebra morphism $a:(TA,{\mu }_A)\to (A,a)$. Hence $G^{\mathbb{T}}{F}^{\mathbb{T}}=T$, and the induced multiplication is the underlying counit at $(TX,{\mu }_X)$, namely ${\mu }_X$. Therefore this adjunction induces exactly the original monad, including its unit and multiplication of a monad.

Construct pointwise limits in a functor category. For $H:\mathcal{J}\to [\mathcal{D},\mathcal{C}]$, choose at each object $d$ a categorical limit $L(d)$ of $j\mapsto H_j(d)$, with projections $p_j(d)$. For $u:d\to d^{\prime }$, the family $H_j(u)p_j(d)$ is compatible; define $L(u)$ uniquely byThe universal property gives $L(1_d)=1_{L(d)}$ and $L(vu)=L(v)L(u)$, since those equalities hold after every projection. Thus $L$ is a functor, and each $p_j:L\Rightarrow H_j$ is a natural transformation.

For any categorical cone $(M,(a_j))$, the pointwise categorical limits give unique maps $a(d):M(d)\to L(d)$. To check naturality, compose $L(u)a(d)$ and $a(d^{\prime })M(u)$ with every $p_j(d^{\prime })$; both become $H_j(u)a_j(d)=a_j(d^{\prime })M(u)$. The projections distinguish arrows into their categorical limit, so the two maps agree. Componentwise uniqueness gives uniqueness of the natural transformation $a$. This proves that $(L,p_j)$ really is the required categorical limit, rather than merely a family of objectwise candidates.

A specified categorical limit categorical cone in ${\mathcal{C}}^{\mathrm{ob}\mathcal{D}}$ fixes these objectwise vertices and projections. The displayed equation forces every arrow $L(u)$, and the argument forces every categorical cone factorization. Hence the forgetful functor uniquely lifts that categorical cone and is a limit-creating functor. The construction only takes small categorical limits in $\mathcal{C}$; it does not require $\mathcal{D}$ to be small. As usual, the functor categories are understood in a universe where their collections of transformations are meaningful.

Write the Cartesian comonad as $(G,\epsilon ,\delta )$, with $G$ preserving finite limits. A coalgebra for a comonad is $(A,a)$ with $a:A\to GA$, ${\epsilon }_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Its forgetful functor $U:{\mathcal{E}}^G\to \mathcal{E}$ is faithful, creates finite limits, and has the cofree coalgebra right adjoint $R(X)=(GX,{\delta }_X)$. We construct the two remaining topos structures explicitly.

For exponential objects, take coalgebras $(A,a),(B,b)$ and start with $R(B^A)$. Put $X=G(B^A)$, with structure $\xi ={\delta }_{B^A}$, and letTranspose the following two maps $X\times A\to GB$ into maps $u,v:X\to (GB{)}^A$:using $G(X\times A)\cong GX\times GA$. The cofree adjunction transposes $u,v$ once more into coalgebra morphisms $R(B^A)\rightrightarrows R((GB{)}^A)$. Let $Q$ be their equalizer. A coalgebra map $(C,c)\to R(B^A)$ corresponds to an arbitrary ambient map $h:C\times A\to B$. It factors through $Q$ precisely whenwhich is exactly the condition that $h$ be a coalgebra morphism. Therefore $Q$ represents ${\mathcal{E}}^G(C\times A,B)$ and is the required exponential in a coalgebra topos.

For the subobject classifier, let $\kappa :G\Omega \to \Omega$ classify the mono $G\top :G1\cong 1\hookrightarrow G\Omega$. In the cofree coalgebra $R\Omega$, formBoth arrows are coalgebra morphisms. The cofree transpose of $\top :1\to \Omega$ factors through this equalizer and gives its true arrow. To verify classification, let $S\hookrightarrow X$ have ambient characteristic map $\chi :X\to \Omega$. It supports a subcoalgebra of $(X,x)$ exactly when it is invariant under $x$, equivalentlyThe counit proves the reverse containment in the first equation; the forward containment supplies the restricted structure map, whose coalgebra laws follow through the mono. Under the cofree adjunction, the second equation says exactly that $G\chi x:X\to R\Omega$ factors through ${\Omega }_G$. Pulling back its true arrow recovers $S$, since $\kappa G\chi x=\chi$. This proves the universal property of the subobject classifier of a coalgebra topos. Hence ${\mathcal{E}}^G$ is a topos.

Now let $f:\mathcal{E}\to \mathcal{F}$ be a geometric morphism, with $L=f^{\ast }⊣H=f_{\ast }$. The comonad $G=LH$ is Cartesian: $L$ preserves finite limits and the right adjoint $H$ preserves limits. Put $\mathcal{D}={\mathcal{E}}^G$, already a topos. The forgetful adjunction $U⊣R$ defines $p:\mathcal{E}\to \mathcal{D}$ with $p^{\ast }=U$, so $p^{\ast }$ is faithful.

The comparison functorpreserves finite limits. It has a right adjoint $J$, given on a coalgebra $(A,a)$ byIndeed, the transposed arrow $Y\to HA$ corresponds to a coalgebra map $KY\to (A,a)$ exactly when it equalizes these two maps. Applying the finite-limit-preserving $L$ shows that $LJ(A,a)$ is the equalizer ofThat equalizer is $a:A\to GA$. If $t:Z\to GA$ equalizes the pair, then $a{\epsilon }_{A}t={\epsilon }_{GA}Gat={\epsilon }_{GA}{\delta }_{A}t=t$, proving the claimed universal property. Consequently the counit $KJ(A,a)\to (A,a)$ is invertible. The fully faithful adjoint criterion makes $J$ full and faithful.

Thus $K⊣J$ defines a geometric embedding $i:\mathcal{D}\to \mathcal{F}$, and $UK=L$ identifies the composite with $f$. The requested factorization iswhere $p$ is a surjective geometric morphism and $i_{\ast }=J$ is full and faithful.