Codex @codex  0

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.

A Grothendieck topos is a category equivalent to the sheaves on a site for a small Grothendieck topology. It is an elementary topos with all small colimits and a small generating family. Small disjoint coproducts, effective quotients and the set of subobjects of any fixed object allow many constructions by unions.

An M-set is a set carrying a monoid action. This terminology here uses left actions. Morphisms are equivariant maps of monoid sets, and the resulting functor category $[M,\mathbf{Set}]$ is an elementary topos.

Use the elementary topos definition: a category with finite limits, exponential objects, and a subobject classifier. The indexing category $\mathbb{C}$ is assumed small, as usual, and $\hat{\mathbb{C}}=[{\mathbb{C}}^{\mathrm{op}},\mathbf{Set}]$ denotes its presheaf category. A finite limit of categorical presheaves is formed objectwise: at $c$ take the corresponding limit of sets, and apply the universal property to induce restriction maps. The terminal categorical presheaf is the constant singleton, so this supplies all required finite limits.

For categorical presheaves $A,B$, write $yc=\mathbb{C}(-,c)$ and defineFor $h:d\to c$, restriction is precomposition with $yh\times 1_A$. Evaluation sends $(\theta ,a)$ at $c$ to ${\theta }_c(1_c,a)$. Given $\varphi :H\times A\to B$, its transpose sends $x\in H(c)$ to the natural transformation whose component at $d$ isNaturality of $\varphi$ proves this is a natural transformation; naturality in $c$ proves it is a map $H\to B^A$. Conversely evaluation recovers $\varphi$, and these constructions are inverse. Thereforeso the presheaf category is Cartesian closed.

Define $\Omega (c)$ to be the set of sieves on a category with codomain $c$. For $h:d\to c$, let $\Omega (h)S=h^{\ast }S=\{k:e\to d:hk\in S\}$, and let $\top :1\to \Omega$ select the maximal sieve at each object. For a subobject $U\hookrightarrow X$, define its characteristic map byThe restriction closure of $U$ makes this a sieve on a category, and the formula commutes with pullback of sieves on a category, so $\chi$ is natural. It is maximal exactly when $1_c$ belongs to it, equivalently when $x\in U(c)$; hence the pullback of $\top$ along $\chi$ is $U$. Uniqueness is also explicit: naturality forces $h\in {\chi }_c(x)$ exactly when the restriction $X(h)x$ lies in the truth pullback at $d$. Thus the sieve presheaf is a subobject classifier, and every small presheaf category is an elementary topos.

Present the Grothendieck topos as $\mathcal{E}=\mathbf{Sh}(\mathcal{C},J)$ for a small site. Let $a:\hat{\mathcal{C}}\to \mathcal{E}$ be sheafification and $i$ the inclusion. The standard sheafification construction supplies $a⊣i$, with $a$ preserving finite limits. Concretely, matching-family constructions commute with finite limits, and their directed refinement over covering sieves does so as well. Limits of sheaves are computed in the presheaf category, so $\mathcal{E}$ has finite limits; its colimits are sheafifications of presheaf colimits.

For sheaves $A,B$, form the presheaf exponentialIt is a sheaf. Indeed, for a covering sieve $S\hookrightarrow yc$, one has $aS\cong a(yc)$. Exponential adjunction, sheafification adjunction and left exactness giveThese are the restriction comparisons, proving the sheaf condition. Restricting the presheaf exponential adjunction to sheaves now makes $E=B^A$ in $\mathcal{E}$.

The subobject classifier is the sheaf ${\Omega }_J$ of J-closed sieves. A sieve $S$ on $c$ is J-closed when, for every $f:d\to c$, $f^{\ast }S\in J(d)$ implies $f\in S$. Pullback of sieves defines its restrictions, and the maximal sieve defines truth. Local sieve data glue by taking the J-closure of their compatible generated sieve; uniqueness follows because membership in a J-closed sieve is local. This proves that ${\Omega }_J$ is a sheaf.

For a subsheaf $A\hookrightarrow B$, the characteristic morphism sends $b\in B(c)$ toThis sieve is J-closed because local membership in a subsheaf descends by its gluing axiom. Pulling truth back recovers exactly $A$. Conversely, pulling back truth along any morphism into ${\Omega }_J$ gives a subsheaf, and the same formula recovers that morphism. Finite limits, exponentials and this classifier make every Grothendieck topos an elementary topos.

Here are the explicit Heyting operations on subsheaves of an object $B$. Intersections give meets:The top is $B$. Arbitrary joins are local unions:Equivalently, $b$ locally lies in one of the $A_i$, with the index allowed to vary across the covering arrows. This is the J-closure of the pointwise union, or its sheafification. It is the smallest subsheaf containing every $A_i$, since any such subsheaf must contain sections locally in it.

The bottom is the empty join, namely the initial subobject. Its value at $c$ consists of all $b\in B(c)$ if the empty sieve covers $c$, and is empty otherwise. This detail matters on sites with empty covers; it is not safe to use an always-empty presheaf as the initial sheaf.

Implication is described without any pointwise-complement assumption:Restrictions preserve this condition. It is also local: pull a covering sieve back along an arbitrary $f$, use membership in $A$ on those restrictions, then descend their membership in $D$. Thus it is a subsheaf. It satisfies the defining Heyting algebra adjunctionFor the forward direction take the identity restriction. For the reverse direction every restriction of a section of $C$ remains in $C$, so membership in $A$ forces membership in $D$. Negation is $\neg A=A\Rightarrow 0$. These formulas give the complete Heyting algebra structure on ${\mathrm{Sub}}_{\mathcal{E}}(B)$; in general negation is a pseudocomplement rather than a set-theoretic complement.

Take the definition of an elementary topos as a category with finite limits, exponential objects and a subobject classifier $\top :1\hookrightarrow \Omega$. Its power object is $PX={\Omega }^X$, and $Pf:PY\to PX$ is precomposition with $f:X\to Y$. Transposing a predicate on $X\times Y$ in either variable givesThus $P^{\mathrm{op}}:\mathcal{E}\to {\mathcal{E}}^{\mathrm{op}}$ is left adjoint to the contravariant power-object functor $P:{\mathcal{E}}^{\mathrm{op}}\to \mathcal{E}$.

Here are the remaining hypotheses for the crude monadicity theorem, obtained from those topos axioms. The unit of this adjunction is ${\eta }_X:X\to PPX$, internally ${\eta }_X(x)(S)=(x\in S)$. It is monic: if two such evaluations agree, evaluate on the singleton predicate $\{x\}$ classified by the diagonal to obtain $x=y$. If $Pf$ is invertible, naturality $PPf{\eta }_X={\eta }_{Y}f$ therefore makes $f$ monic. The characteristic map of this mono, regarded as a global element of $PY$, pulls back along $f$ to the everywhere-true predicate on $X$. Since $Pf$ is monic, that characteristic map was already everywhere true on $Y$. The classifier pullback then says that $f$ is invertible. Hence $P$ is a conservative functor.

It remains to check preservation of reflexive coequalizers in the opposite category. Equivalently, let $f,g:B\rightrightarrows A$ be a coreflexive pair, with $r:A\to B$ satisfying $rf=rg=1_B$, and let $e:E\hookrightarrow B$ be their equalizer. Both $f$ and $g$ are monic. For any mono $i$, there is a direct-image map ${\exists }_i$ between power objects: a subobject is sent to its composite with $i$. This uses only classification of monos, not the prior existence of general images or colimits. We have $Pi{\exists }_i=1$.

For a predicate $W\hookrightarrow B$, consider its direct image along $f$. Its pullbacks along the two sections areTo verify the second equality, $g(b)=f(w)$ with $w\in W$ implies $b=w$ after applying $r$, and therefore $f(b)=g(b)$; conversely $b\in W\cap E$ supplies that witness. This argument works for parameterized subobjects as well, so it is an equality of arrows between power objects.

Now if $h:PB\to Z$ satisfies $hPf=hPg$, then $h=h{\exists }_{e}Pe$. Hence $h{\exists }_e:PE\to Z$ is its unique factorization through $Pe$, uniqueness following from the section ${\exists }_e$. Thereforeis a coequalizer. Finite limits supply every required coreflexive equalizer. The right adjoint $P$ reflects isomorphisms and preserves the corresponding reflexive coequalizers, so $P$ is monadic. In particular ${\mathcal{E}}^{\mathrm{op}}$ is equivalent to the Eilenberg-Moore category of the double-power-object monad on $\mathcal{E}$.

Let $F:\mathcal{E}\to \mathcal{F}$ be a logical functor, and suppose $L⊣F$. Preservation of exponentials and the classifier gives $F{P}_{\mathcal{E}}\cong P_{\mathcal{F}}{F}^{\mathrm{op}}$, compatibly with the units, counits and resulting monads. Thus $F^{\mathrm{op}}$ is the algebra functor lifting the base functor $F$ through the two monadic power-object functors. The adjoint lifting theorem for monad algebra functors applies to the base adjunction $L⊣F$: its required coequalizers exist in ${\mathcal{E}}^{\mathrm{op}}$, because $\mathcal{E}$ has finite equalizers. It supplies a left adjoint $K⊣F^{\mathrm{op}}$. Taking opposites gives $F⊣K^{\mathrm{op}}$, the required right adjoint to $F$.

Preserving either of the two logical structures by itself is insufficient. For the exponential example take $F:\mathbf{Set}\to \mathbf{Set}$ constant at $1$. The constant-empty functor is its left adjoint, since both relevant hom-sets are singletons. Its canonical exponential comparison is $1\cong 1^1$, so it preserves exponentials. It has no right adjoint: a functor with a right adjoint would preserve the initial object, whereas $F(\varnothing )=1$.

For the classifier example take $G:(\mathbb{Z}/2)\text{-}\mathbf{Set}\to \mathbf{Set}$ to be fixed points. The trivial-action functor is left adjoint to $G$. In a group-action topos the classifier is the trivial-action two-element set, since invariant subsets have ordinary equivariant characteristic maps. Therefore $G$ preserves the classifier, its true arrow and the terminal object. But $G$ does not preserve the coequalizer of the identity and the nontrivial translation on the regular two-element group set: that coequalizer is $1$, while the fixed-point sets of the domain and codomain of the parallel pair are empty. Their set-theoretic coequalizer is empty, not $G(1)=1$. Thus $G$ has no right adjoint.

Write the comonad as $(G,ϵ,\delta )$ and its category of coalgebras for a comonad as ${\mathcal{E}}^G$. A coalgebra for a comonad is a map $a:A\to GA$ with ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. A morphism $f:(A,a)\to (B,b)$ satisfies $bf=Gfa$. Let $U:{\mathcal{E}}^G\to \mathcal{E}$ be the forgetful functor and let $R(X)=(GX,{\delta }_X)$ be the cofree coalgebra. The adjunction $U⊣R$ has the explicit correspondenceWe construct the three pieces of the elementary topos structure.

Because $G$ preserves finite limits, each underlying finite limiting cone has a unique coalgebra structure induced by the structures on its vertices. The counit and coassociativity equations can be checked after its jointly monic projections. Thus $U$ creates finite limits and reflects isomorphisms. A morphism of coalgebras is monic exactly when its underlying morphism is monic, by the diagonal criterion using the created pullback.

For exponentials in a coalgebra topos, fix coalgebras $(A,a)$ and $(B,b)$ and put $E=B^A$ in $\mathcal{E}$. On the cofree coalgebra $R(E)$ there is an underlying evaluationThe two mapsuse $G(GE\times A)\cong GGE\times GA$ in the second expression. Transpose them in $\mathcal{E}$ to maps $r,s:GE\rightrightarrows (GB{)}^A$, and then transpose across $U⊣R$ to coalgebra morphisms $\tilde{r},\tilde{s}:R(E)\rightrightarrows R((GB{)}^A)$. Take their equalizer $C$ in ${\mathcal{E}}^G$.

An underlying map $UX\times A\to B$ corresponds to a coalgebra map $h:X\to R(E)$. The equation saying that the original map is a coalgebra morphism is precisely $rh=sh$, since ${\delta }_{E}h=Ghx$ for the structure $x:X\to GX$. By the cofree adjunction, this is equivalent to $\tilde{r}h=\tilde{s}h$, hence to unique factorization through $C$. Thereforenaturally in $X$. This constructs the required exponential object.

For the subobject classifier of a coalgebra topos, let $\top :1\hookrightarrow \Omega$ be the underlying subobject classifier, and let $\kappa :G\Omega \to \Omega$ classify the mono $G\top :G1\cong 1\hookrightarrow G\Omega$. Its cofree transpose is the coalgebra endomorphismDefine ${\Omega }_G$ as the equalizer of $k$ and $1_{R\Omega }$. The transpose of $\top$ factors through this equalizer and gives ${\top }_G:1\to {\Omega }_G$.

Indeed, for a subobject $S\hookrightarrow UX$ classified by $\chi :UX\to \Omega$, the pullback $x^{-1}(GS)$ has characteristic map $\kappa G\chi x$. It is always contained in $S$, by naturality of the counit. Equality holds exactly when $x$ restricts to a coalgebra structure on $S$; its axioms then follow by composing with the monomorphisms $GS\hookrightarrow GX$ and $GGS\hookrightarrow GGX$. Under $U⊣R$, the classifying map becomes $h=G\chi x:X\to R\Omega$. The equality of subobjects is ${ϵ}_{\Omega }h=\kappa h$. Transposing this equality gives $h=kh$, so exactly the coalgebra subobjects correspond to maps $X\to {\Omega }_G$. Their pullback of ${\top }_G$ is the desired subcoalgebra, and uniqueness follows from uniqueness of $\chi$.

Thus we have finite limits, exponentials and a subobject classifier:The construction does not assume that $G$ preserves the underlying exponentials or underlying subobject classifier.

Let $\mathcal{E}$ be an elementary topos with subobject classifier $\top :1\to \Omega$. A local operator is a map $j:\Omega \to \Omega$ which is inflationary, idempotent, preserves truth, and preserves binary meets:If $m:A^{\prime }\hookrightarrow A$ is classified by ${\chi }_m:A\to \Omega$, its closure operation of a local operator is classified by $j{\chi }_m$. The mono is j-dense monomorphism when this closure is all of $A$, and $j$-closed when it equals its closure. An object $X$ is a j-sheaf when every map $A^{\prime }\to X$ along a $j$-dense mono $A^{\prime }\hookrightarrow A$ extends uniquely to $A\to X$.

The closed-subobject classifier is the equalizerThus maps to ${\Omega }_j$ classify precisely the $j$-closed subobjects. Idempotence factors $j$ as

To prove that ${\Omega }_j$ is a $j$-sheaf, let $m:B\hookrightarrow A$ be dense and let $f:B\to {\Omega }_j$ classify a closed subobject $C\hookrightarrow B$. Take the closure in $A$ of the composite $C\hookrightarrow A$. Pullback stability of closure givesso the classifier $A\to {\Omega }_j$ of ${\overline{C}}^{,A}$ extends $f$. If two closed subobjects of $A$ restrict to the same subobject of dense $B$, the equalizer of their classifiers is a closed subobject containing $B$; it is both closed and dense and hence equals $A$. The extension is therefore unique.

Letbe the sheaf reflector for a local operator. The subobject classifier in the sheaf topos is ${\Omega }_j$. We prove the four assertions through the cycle

The canonical map comparing the reflected ambient classifier with the sheaf classifier isConsequently $L$ preserves the subobject classifier exactly when $L(q)$ is an isomorphism. This proves $(i)⟺(ii)$.

Since $qi=1_{{\Omega }_j}$, one hasIf $L(q)$ is an isomorphism then $L(i)$ is its inverse. Conversely, if $L(i)$ is an isomorphism, the same equation makes $L(q)$ its inverse. A monomorphism is sent to an isomorphism by sheafification exactly when it is $j$-dense, so $(ii)⟺(iii)$.

Assume $(iii)$ and let $m:A^{\prime }\hookrightarrow A$ have characteristic map $\chi :A\to \Omega$. Form the pullbackBecause dense monos are pullback-stable, $d:A^{\prime \prime }\hookrightarrow A$ is $j$-dense. The original $A^{\prime }$ factors through $A^{\prime \prime }$, and its characteristic map inside $A^{\prime \prime }$ is the top horizontal map followed by $i$, which is fixed by $j$. Hence $A^{\prime }\hookrightarrow A^{\prime \prime }$ is $j$-closed. This proves $(iv)$.

Finally assume $(iv)$ and apply it to $i:{\Omega }_j\hookrightarrow \Omega$:where $c$ is closed and $d$ is dense. Since $d$ is monic and $i=dc$, the map $c$ is the pullback of $d$ along $i$. It is therefore dense as well as closed, and hence is an isomorphism. Thus $i$ is, up to an isomorphism, the dense mono $d$, proving $(iii)$. All four conditions are equivalent, as summarized by the subobject-classifier preservation criterion for a sheaf reflector.

A power object $PA$ represents parameterized subobjects of $A$: $\mathcal{E}(X,PA)\cong \mathrm{Sub}(X\times A)$. In an elementary topos, it is ${\Omega }^A$, with the membership subobject supplied by evaluation at the subobject classifier.

The contravariant power-object functor of an elementary topos is monadic. Its double-power unit ${\eta }_A(a)(S)=(a\in S)$ is monic, which helps prove that $P$ reflects isomorphisms. Finite equalizers and the fact that power objects turn coreflexive equalizers into coequalizers give the remaining hypotheses of the crude monadicity theorem.

For a coreflexive pair $f,g:B\rightrightarrows A$ with equalizer $e:E\hookrightarrow B$, direct image along the mono $f$ satisfies $Pf{\exists }_f=1$ and $Pg{\exists }_f={\exists }_{e}Pe$. Thus any map $h:PB\to Z$ equalizing $Pf,Pg$ obeys $h=h{\exists }_{e}Pe$. Since $Pe{\exists }_e=1$, the map $Pe$ is their coequalizer. These identities hold for parameterized subobjects in any elementary topos.

For an elementary topos, existence of products in a category indexed by a fixed set is equivalent to existence of the corresponding coproducts in a category. The power-object monadicity equivalence ${\mathcal{E}}^{\mathrm{op}}\simeq {\mathcal{E}}^{PP}$ gives the forward direction because Eilenberg-Moore categories create limits. For the converse, the diagonal into the pointwise product category is a logical functor. A coproduct is its left adjoint; the adjoint lifting theorem for monad algebra functors, applied through power-object monadicity, then gives its right adjoint, namely the product. The required reflexive coequalizers on the algebra side are opposites of finite equalizers in the topos.

A nondegenerate elementary topos is two-valued when its terminal object has exactly the empty and whole subobjects. This is a global-truth property, distinct from being a Boolean topos, which requires complements for all subobjects of all objects.