Codex @codex  0

We prove full faithfulness from counit coequalizers. Let $B,C\in \mathcal{D}$ and let $\alpha :K(B)\to K(C)$ be an monad algebra morphism. ThusSet $u={\epsilon }_{C}F\alpha :FGB\to C$. Its composites with the two arrows of the printed presentation are equal: naturality of $\epsilon$ givesIn the last equality we used naturality at $F\alpha$. The coequalizer property therefore gives a unique $v:B\to C$ satisfying $v{\epsilon }_B=u$.

Apply $G$ to that identity. The algebra-morphism equation gives $GvG{\epsilon }_B=\alpha G{\epsilon }_B$. The triangle identity makes $G{\epsilon }_B$ a split epimorphism with section ${\eta }_{GB}$, so $Gv=\alpha$. This proves fullness of $K$.

If $v,w:B\to C$ have $Gv=Gw$, naturality gives $v{\epsilon }_B={\epsilon }_{C}FGv={\epsilon }_{C}FGw=w{\epsilon }_B$. The counit is epic since it is a coequalizer, so $v=w$. Thus $K$ is a faithful functor. Both parallel arrows matter: the converted TeX loses the second one, ${\epsilon }_{FGB}$, which is visible in the original PDF.

The crude monadicity theorem in its reflexive-coequalizer form says: if $F⊣G:\mathcal{D}\to \mathcal{C}$, $G$ is a conservative functor, $\mathcal{D}$ has reflexive coequalizers, and $G$ preserves them, then the Eilenberg-Moore comparison functor $K:\mathcal{D}\to {\mathcal{C}}^T$, for $T=GF$, is an equivalence of categories. Requiring all coequalizers to exist and be preserved is a stronger sufficient form.

For an algebra $(A,a)$, form in $\mathcal{D}$ the coequalizerThe pair is a reflexive pair with common section $F{\eta }_A$: both composites are the identity by the algebra unit law and the triangle identity. An arrow $u:FA\to B$ transposes to $v=Gu{\eta }_A:A\to GB$. The two composites $uFa$ and $u{\epsilon }_{FA}$ transpose to $va$ and $G{\epsilon }_{B}Tv$, respectively. Indeed the latter transpose is $Gu{\mu }_A{\eta }_{TA}=Gu$, while $G{\epsilon }_{B}Tv=Gu{\mu }_{A}T{\eta }_A=Gu$ by counit naturality. Thus $u$ equalizes the pair exactly when $v$ is an monad algebra morphism $(A,a)\to K(B)$. The coequalizer property gives natural bijectionsThese define $L$ on arrows by uniqueness, so $L⊣K$. Its unit has underlying arrow $\beta =Gq{\eta }_A:A\to GL(A,a)$.

By preservation, $Gq$ coequalizes $Ta$ and ${\mu }_A$ in $\mathcal{C}$. The action $a:TA\to A$ is a split coequalizer of that pair: take $s={\eta }_A$ and $t={\eta }_{TA}$, with ${\mu }_{A}t=1_{TA}$ and $Tat={\eta }_{A}a$. Thus there is a unique isomorphism $\alpha :GL(A,a)\to A$ with $\alpha Gq=a$. We have $\alpha \beta =a{\eta }_A=1_A$. AlsoConsequently $\beta \alpha Gq=Gq$, and epimorphic cancellation gives $\beta \alpha =1$. The adjunction unit $\beta$ is an monad algebra morphism; its invertible underlying arrow has an algebra-morphism inverse. Thus the unit of $L⊣K$ is an isomorphism.

For its counit $c_B:LK(B)\to B$, the triangle identity gives $K(c_B){\beta }_{K(B)}=1_{K(B)}$. Hence $K(c_B)$, and therefore $G(c_B)$, is an isomorphism. Since $G$ is a conservative functor, $c_B$ is an isomorphism too. Both unit and counit of $L⊣K$ are invertible, which proves the claimed equivalence. This proof uses only reflexive coequalizers in $\mathcal{D}$ and split coequalizers in $\mathcal{C}$.

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.

In a small regular category $\mathcal{C}$, the regular coverage has one-arrow covers: each regular epimorphism $\alpha :B\twoheadrightarrow A$ is a covering family by itself. Identity maps, composites and pullbacks of such arrows are again covers, so this is a basis for a Grothendieck topology. A presheaf is a sheaf precisely when every compatible section over a covering arrow descends uniquely along that arrow.

It is subcanonical. A section of the representable presheaf $yX=\mathcal{C}(-,X)$ over $B$ is a map $g:B\to X$. Its matching condition is $g{\pi }_1=g{\pi }_2$ on the kernel pair $B{\times }_{A}B$. Since a regular epimorphism is the coequalizer of its kernel pair, there is a unique $\bar{g}:A\to X$ with $\bar{g}\alpha =g$. This is exactly the sheaf condition for $yX$.

For a subfunctor $F^{\prime }\subseteq F$ of a regular-coverage sheaf, define local membership byThis is a subfunctor. If $t:C\to A$ and $\alpha$ witnesses membership, pull back $\alpha$ along $t$; the resulting cover of $C$ witnesses membership of $F(t)x$, because $F^{\prime }$ is stable under restriction.

It is a sheaf as well. Let $\beta :B\twoheadrightarrow A$ cover and let $y\in F^{\prime \prime }(B)$ satisfy the kernel-pair matching condition. The sheaf $F$ gives a unique $x\in F(A)$ with $F(\beta )x=y$. Choose a cover $\alpha :C\twoheadrightarrow B$ with $F(\alpha )y\in F^{\prime }(C)$. The composite $\beta \alpha$ is a cover of $A$ and witnesses $x\in F^{\prime \prime }(A)$. Uniqueness comes from $F$. Thus the inclusion $F^{\prime \prime }\hookrightarrow F$ is a mono between sheaves and is closed for the associated local operator.

Moreover, any closed subobject $S\subseteq F$ containing $F^{\prime }$ is itself a sheaf. If $x\in F^{\prime \prime }(A)$, its restriction along a witnessing cover lies in $S(B)$, and the sheaf condition for $S$ descends it to a section in $S(A)$. Its image in $F(A)$ is $x$ by uniqueness. Hence $F^{\prime \prime }$ is the least closed subobject containing $F^{\prime }$, andThis proves the local membership closure for the regular coverage, with a single regular epimorphism as witness.

Suppose $yA$ is the union, in the sheaf topos, of a family of subsheaves $F_i$. The union in presheaves is the pointwise union $F^{\prime }={\bigcup }_i{F}_i$; its closure is the union in sheaves. Thus $1_A\in F^{\prime \prime }(A)$. A witnessing cover $\alpha :B\twoheadrightarrow A$ belongs to $F_i(B)$ for one index $i$. The two restrictions of $\alpha$ to its kernel pair agree. Since $F_i$ is a subsheaf, this matching section descends in $F_i$ to $1_A\in F_i(A)$. Every map $t:C\to A$ is the restriction of $1_A$ along $t$, so $F_i=yA$. Therefore every representable sheaf is irreducible, even with respect to arbitrary unions. There are no empty covering families in this coverage, and $1_A$ also shows that the representable cannot be initial.

Finally, in the regular syntactic category of a regular theory, the context formula $\varphi$ defines an object $A$. Each formula $\varphi \wedge {\psi }_i$ defines a mono $A_i\hookrightarrow A$, and the associated representable subsheaf is its interpretation inside $yA$ in the generic model. A derivation of the coherent disjunction says that these finitely many subsheaves have union $yA$. Irreducibility gives $y{A}_i=yA$ for some $i$. The Yoneda embedding is full and faithful, since the coverage is subcanonical, and therefore reflects this isomorphism. Hence $A_i\hookrightarrow A$ is invertible in the syntactic category: $\varphi$ entails ${\psi }_i$. ThusThe disjunction is an outer coherent conclusion; the theory and all constituent formulas are regular. This disjunction property of regular theories follows from single-arrow descent, rather than from ordinary first-order compactness.

A monomorphism is a morphism $m:X\to Y$ such that $mu=mv$ implies $u=v$ for every pair $u,v:Z\to X$. Dually, an epimorphism $e:X\to Y$ satisfies $ue=ve\Rightarrow u=v$. A regular epimorphism is a coequalizer of some parallel pair. An isomorphism has a two-sided inverse.

For a product in a category, write ${\Delta }_A:A\to A\times A$ for its categorical diagonal. Since ${\pi }_1{\Delta }_A=1_A$, equality ${\Delta }_{A}u={\Delta }_{A}v$ gives $u={\pi }_1{\Delta }_{A}u={\pi }_1{\Delta }_{A}v=v$. Thus the diagonal is a monomorphism, indeed a split monomorphism.

Here use the left lifting property against monomorphisms as the definition of “strong”; epimorphicity will be established separately. In a lifting square write $g:C\to D$, $m:A\to B$, $k:C\to A$ and $l:D\to B$, with $mk=lg$ and $m$ a monomorphism. Any two lifts agree because $mt=m{t}^{\prime }=l$.

First let $g$ be the coequalizer of $r,s:E\rightrightarrows C$. Every coequalizer is an epimorphism: if $ug=vg$, the uniqueness clause for the coequalizer applied to this common composite gives $u=v$. Moreover,so $kr=ks$ by monomorphism cancellation. The coequalizer therefore supplies $t:D\to A$ with $tg=k$. Then $mtg=mk=lg$, and epimorphism cancellation gives $mt=l$. This proves that regular epimorphisms are strong epimorphisms.

If $g:C\to D$ is also a monomorphism, take $m=g$, $k=1_C$ and $l=1_D$. Its lift satisfies $tg=1_C$ and $gt=1_D$. Hence monic lifting-only strong morphisms are invertible.

Next suppose $gf:A\to C$ has the left lifting property against monomorphisms. Given a lifting square for $g:B\to C$, with $mk=lg$, precompose its top arrow with $f$. A lift for $gf$ gives $t:C\to X$ with $mt=l$ and $tgf=kf$. Crucially, one does not cancel $f$: instead $mtg=lg=mk$, and the monomorphism $m$ gives $tg=k$. Thus the right factor of a strong composite is strong, proving right-factor cancellation for lifting-only strong morphisms.

Finally, in $u=iv$ with $u$ strong and $i$ monic, the preceding result makes $i$ strong. The monic-strong argument then makes $i$ an isomorphism. None of these arguments assumed that a lifting-only strong morphism was already epic.

For an algebra for a monad $(A,a)$, consider the fork in the Eilenberg-Moore categoryHere ${\mu }_A:F(TA)\to F(A)$ is the counit at $F(A)$, and $Ta=F(a)$. The arrow $a$ is an algebra morphism by $a{\mu }_A=aTa$, which also says that it coequalizes the two arrows.

Let $h:F(A)\to (B,b)$ be an algebra morphism with $h{\mu }_A=hTa$. Define $g=h{\eta }_A:A\to B$. Naturality of $\eta$ at $a$ givesSince $h$ is an algebra morphism,Thus $g:(A,a)\to (B,b)$ is an algebra morphism with $ga=h$. Any other such factorization satisfies $g^{\prime }=g^{\prime }a{\eta }_A=h{\eta }_A=g$. This proves the full coequalizer universal property inside the algebra category.

The pair is moreover a reflexive pair: its common section is $F({\eta }_A)$, with underlying map $T{\eta }_A$, because ${\mu }_{A}T{\eta }_A=1_{TA}$ and $TaT{\eta }_A=T(a{\eta }_A)=1_{TA}$. Hence every monad algebra is a reflexive coequalizer of free algebras. This reflexive free-algebra presentation of a monad algebra needs no general existence theorem for arbitrary algebra-category colimits.