Codex @codex  0

Both alternatives can be proved using the same smallness mechanism. We first establish the initial-object lemma for complete categories with a weakly initial set, then obtain the two adjoint functor existence theorems and their applications.

Let $\mathcal{E}$ be a locally small category with all small categorical limits and a weakly initial set $(W_i{)}_{i\in I}$. Its product in a category $W={\prod }_i{W}_i$ is weakly initial: given any object, choose a map from some $W_i$ and compose with the corresponding projection. Take the simultaneous equalizer $e:E\to W$ of every endomorphism of $W$ and its identity; local smallness makes this a small categorical limit. Then $E$ is also weakly initial. If $a,b:E\to X$, form their equalizer $j:Y\to E$ and choose $t:W\to Y$. Since $ejt$ is an endomorphism of $W$, the construction of $e$ gives $ejte=e$. Cancelling the monomorphism $e$ yields $jte=1_E$. Thus $j$ is both a monomorphism and a split epimorphism, hence invertible, and $a=b$. There is therefore exactly one arrow from $E$ to every object: $E$ is initial.

The Freyd general adjoint functor theorem says that for a functor $U:\mathcal{A}\to \mathcal{B}$ between locally small categories, with $\mathcal{A}$ complete, a left adjoint exists exactly when $U$ preserves all small categorical limits and satisfies the solution-set condition. That condition requires, for each $B$, a set of arrows $u_i:B\to U{A}_i$ such that every $u:B\to UA$ factors as $U(f)u_i$ for some $i$ and $f:A_i\to A$.

For sufficiency, the comma category $(B\downarrow U)$ is locally small and complete: form a diagram's categorical limit in $\mathcal{A}$, and use categorical limit preservation to obtain its arrow from $B$. The solution set is a weakly initial set in this comma category. The lemma provides an initial object $(LB,{\eta }_B:B\to ULB)$. Its universal property givesFor $h:B\to B^{\prime }$, define $Lh$ by $U(Lh){\eta }_B={\eta }_{B^{\prime }}h$. Uniqueness proves the identity and composition laws and naturality of the displayed bijections, hence $L⊣U$. Conversely, an adjunction makes $U$ preserve categorical limits, since the corresponding hom-set functors turn a categorical limit cone into a categorical limit of sets. The single arrow ${\eta }_B$ is a solution set. This proves both directions of the theorem.

Now let $F:\mathcal{C}\to \mathcal{D}$ have small domain and codomain. The functor categories $[\mathcal{D},\mathbf{Set}]$ and $[\mathcal{C},\mathbf{Set}]$ are locally small, and their categorical limits are pointwise. Thus the precomposition functor $F^{\ast }$ preserves categorical limits and its domain is complete. To verify its solution-set condition, fix $X:\mathcal{C}\to \mathbf{Set}$ and an arrow $x:X\to F^{\ast }Y$. Let $Y_0\subseteq Y$ be the subfunctor generated by all elements $x_c(a)$, where $c\in \mathcal{C}$ and $a\in X(c)$. Explicitly,These sets are stable under every $Y(h)$. If $\kappa$ is an infinite cardinal bounding $|\mathrm{Mor}\mathcal{D}|$ and $\left|{\coprod }_{c}X(c)\right|$, every $Y_0(d)$ has cardinal at most $\kappa$. Replace each such set by a subset of a fixed set of size $\kappa$. There is only a set of choices of these subsets, of their action maps for the set of arrows of $\mathcal{D}$, and of maps from $X$ to their restrictions. These coded pairs form a solution set: $x$ factors through $F^{\ast }{Y}_0$ and then the inclusion $Y_0\hookrightarrow Y$. The general theorem now yieldsIts values may also be written ${\mathrm{Lan}}_{F}X(d)={\mathrm{colim}}_{(Fc\to d)}X(c)$, the usual left Kan extension formula.

For the other alternative, the categorical limit form of the Special adjoint functor theorem says that a limit-preserving functor $U:\mathcal{A}\to \mathcal{B}$ has a left adjoint if $\mathcal{A}$ is locally small, complete and well-powered, has a cogenerating set $(Q_i{)}_{i\in I}$, and $\mathcal{B}$ is locally small. A cogenerating set means that maps into its members distinguish any two parallel arrows. The dual theorem says that a colimit-preserving functor from a locally small, cocomplete, well-copowered category with a small generating family has a right adjoint. These conclusions are also necessary in their preservation clauses.

Here is a proof of the special theorem rather than an invocation of the general theorem without its required solution set. Given $(A,x:B\to UA)$, intersect all subobjects $m:M\hookrightarrow A$ through which $x$ factors after application of $U$. There are only a set of them by well-poweredness. Their intersection is a wide pullback, preserved by $U$, so gives a smallest supporting pair $(A_0,x_0)$. If $p,q:A_0\to Q_i$ satisfy $U(p)x_0=U(q)x_0$, their equalizer is a supporting subobject. Minimality makes that equalizer invertible, whence $p=q$. Consequentlyis injective. The cogenerating property makes the evaluation arrow from $A_0$ into the product in a category of the $Q_i$, one factor for each map $A_0\to Q_i$, a monic arrow. Its indexing set at each $i$ is identified with a subset of the fixed set $\mathcal{B}(B,U{Q}_i)$. Only a set of such products in a category can occur. Each has only a set of subobjects, and each possible subobject has only a set of arrows from $B$ into its image under $U$. These pairs give a weakly initial set in $(B\downarrow U)$, since every original pair receives the arrow from its minimal supporting pair. The complete-category lemma now gives the adjoint. Reversing all arrows proves the colimit form of the special theorem.

Apply that dual form to $F^{\ast }:[\mathcal{D},\mathbf{Set}]\to [\mathcal{C},\mathbf{Set}]$. Its domain is cocomplete and locally small, and $F^{\ast }$ preserves pointwise colimits. The set of covariant representable functors $\mathcal{D}(d,-)$ generates the domain: by the Yoneda lemma, maps from these representables probe every element at every object and hence distinguish distinct natural transformations. Finally, epimorphisms in this functor category are pointwise surjective. Indeed, their pointwise images form subfunctors; if an image is proper, the two inclusions into the pointwise pushout of two copies of the target over that image distinguish the original map, contradicting epicity. Quotients of a fixed functor are therefore specified by compatible equivalence relations on its sets of values, and form a set. Thus the domain is a well-copowered category. All special-theorem hypotheses hold, givingHere the Right Kan extension can be written ${\mathrm{Ran}}_{F}X(d)=\mathrm{Nat}(\mathcal{D}(d,F-),X)$. In particular both requested adjoints exist, although the two proofs use different smallness hypotheses.

A preadditive category has an abelian-group structure on every hom-set and bilinear composition. One equivalent definition of an additive category is a preadditive category with a zero object and finite products in a category; the following argument proves that these products in a category are automatically coproducts in a category. An abelian category is an additive category with kernels and cokernels in which every monomorphism is a kernel and every epimorphism is a cokernel. Equivalently, for every arrow the canonical map from its coimage to its image is invertible.

Let $P={\prod }_{i=1}^n{A}_i$, with projections $p_i$. Define ${\iota }_i:A_i\to P$ by $p_j{\iota }_i={\delta }_{ji}$, where the diagonal entry is the identity and the others are zero. Since its composites with all projections are identities,Given $f_i:A_i\to B$, the map $f={\sum }_i{f}_i{p}_i$ satisfies $f{\iota }_i=f_i$. If another map has those composites, multiplying the displayed identity by that map forces it to equal $f$. Thus $P$ is also a coproduct in a category. The empty case is the zero object. Reversing arrows proves that a finite coproduct in a category is likewise a product in a category. Hence finite products in a category and coproducts in a category are canonically biproducts in an additive category.

For the category of abelian groups, let $(A_i,D_{ij})$ be a directed diagram, with no injectivity assumption on its transition maps. Its set colimit consists of classes $[i,a]$, withDirectedness proves transitivity of this relation. Define addition by moving representatives to a common upper index:Moving all indices involved to one further upper bound proves independence of representatives and of $k$. Define $-[i,a]=[i,-a]$ and use the common class of the zeros as zero. The abelian-group laws hold at a common index, so descend to the quotient. Every canonical map $A_i\to C$ is a homomorphism, and a compatible cocone induces the homomorphism $[i,a]\mapsto f_i(a)$. This is the unique extension. Moreover the formula for addition is forced by those canonical homomorphisms, proving that the underlying-set functor creates directed colimits. This establishes directed colimits created by the abelian-group forgetful functor explicitly.

If a cocone ${\nu }_i:A_i\to B$ has injective legs, the induced map $C\to B$ is injective. Indeed, equal images of $[i,a]$ and $[j,b]$ give, at a common index $k$,Injectivity of ${\nu }_k$ gives equal representatives at $k$. Since monomorphisms of abelian groups are exactly injective homomorphisms, we have proved that the category of abelian groups is a finitary abelian category in the directed-union sense of the question.

Now let $\mathcal{A}$ be complete, cocomplete and finitary. Index by finite subsets $J\subseteq I$ and put $S_J={⨁}_{j\in J}{A}_j$. For $J\subseteq K$, insert the additional zero coordinates. A compatible cocone on these finite biproducts is exactly a family of maps from every $A_i$, so their directed colimit is $S={\coprod }_{i\in I}{A}_i$.

Each finite biproduct has a map $k_J:S_J\to P={\prod }_{i\in I}{A}_i$ using its coordinates in $J$ and zeros outside $J$. Projection to the finite set of coordinates in $J$ is a retraction, so $k_J$ is a split monomorphism. These maps form a cocone of monomorphisms. The finitary property makes its induced map a monic arrow, and that induced map is exactly the canonical infinite identity matrix:This proves the coproduct-to-product comparison in a finitary abelian category. The PDF's use of finite products in a category in the hint is valid because these are the same finite biproducts.

If $\mathcal{A}$ is also a cofinitary abelian category, apply this argument in its opposite category. The same canonical comparison $j$ is then an epic arrow in $\mathcal{A}$. In an abelian category an arrow that is both a monomorphism and an epimorphism is invertible, so $j$ is an isomorphism.

For countably many copies of $A$, put $S={\coprod }_{n\ge 0}A$ and let $q=j^{-1}\Delta :A\to S$, where $\Delta$ is the product in a category diagonal. Let ${\iota }_n$ denote the coproduct in a category injections, let $s:S\to S$ shift them by $s{\iota }_n={\iota }_{n+1}$, and let $\nabla :S\to A$ be the codiagonal. Comparing every product in a category coordinate givesSince $j$ is a monic arrow, $q={\iota }_0+sq$. Also $\nabla {\iota }_0=1_A$ and $\nabla s=\nabla$. Therefore, for $z=\nabla q$,Hom-sets are abelian groups, so cancellation gives $1_A=0$. Any arrow to or from $A$ is consequently zero by composition with its identity. Thus every object is both initial and terminal, andThis is the countable shift-and-fold argument behind countable biproducts in an additive category force triviality.

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.

An abelian category is an additive category with kernels in a category and cokernels in a category in which the canonical comparison from coimage to image of every morphism is an isomorphism. This is the standard image-coimage form of the definition, equivalently expressed by normality of every monomorphism and epimorphism. Additivity means abelian-group hom-sets with bilinear composition, a zero object and finite biproducts. A sequence is exact at an object when the image of the incoming morphism is the kernel in a category of the outgoing one.

For $f:X\to Y$, construct $q:X\to \mathrm{coim}f=\mathrm{coker}(\ker f)$ and $j:\mathrm{im}f=\ker (\mathrm{coker}f)\to Y$. The universal properties give $f=j\bar{f}q$: first $f$ kills its kernel in a category and factors through $q$; then the resulting map is killed by $\mathrm{coker}f$ because $q$ is epic, so it factors through $j$. The comparison $\bar{f}$ is invertible by the abelian axiom. Cokernels in a category are epic and kernels in a category monic, directly by uniqueness in their universal properties, so $e=\bar{f}q$ is epic and $j$ monic. Thus $\boxed{f=je\text{ is an epimorphism-monomorphism factorization}}$.

In a short exact sequence $0\to X\stackrel{i}{\to }Y\stackrel{p}{\to }Z\to 0$, we have $i=\ker p$ and $p=\mathrm{coker}i$, up to the canonical isomorphisms. If $r:Y\to X$ retracts $i$, the map $1_Y-ir$ kills $i$ and factors as $sp$ for some $s:Z\to Y$. Composing with $p$ gives $psp=p$, so epicity gives $ps=1_Z$. Conversely if $ps=1_Z$, then $1_Y-sp$ is killed by $p$ and factors as $ir$. Composing with $i$ gives $iri=i$, so monicity gives $ri=1_X$. ConsequentlyIn that case $Y\cong X\oplus Z$.

For the derived-functor requests, use additive right exact functors, as customary in abelian homological algebra. An abelian category with enough projectives permits an augmented projective resolution $\cdots \to P_2\to P_1\to P_0\to X\to 0$, obtained by repeatedly taking an epimorphism from a projective onto the previous kernel in a category. Apply $F$ and defineProjective lifts construct maps of resolutions; the comparison and chain-homotopy results make the construction independent of choices and functorial. For a short exact sequence, the horseshoe construction produces a degreewise split short exact sequence of resolutions, hence of their images under additive $F$. Its homology objects give the long exact sequenceThis supplies the requested sketch; detailed comparison and functoriality proofs are not needed here.

A projective object $X$ has a resolution concentrated in degree zero, so $L_{1}F(X)=0$ for every such $F$. Conversely choose $0\to K\stackrel{i}{\to }P\to X\to 0$ with $P$ projective, and take $F=\mathcal{A}(-,K)$ with target ${\mathbf{Ab}}^{\mathrm{op}}$. Precomposition makes this covariant to the opposite category. The usual left exactness of contravariant Hom, which follows directly from the cokernel in a category universal property, says exactly that this $F$ is right exact in that opposite target. If $L_{1}F(X)=0$, the long exact sequence and $L_{1}F(P)=0$ make $F(K)\to F(P)$ monic in ${\mathbf{Ab}}^{\mathrm{op}}$. Equivalently,is epic, hence surjective, in abelian groups. The identity of $K$ has a preimage, giving a retraction of $i$. The sequence splits, and $X$ is a direct summand of $P$, hence projective: a lifting problem for $X$ extends along the projection $P\to X$, is solved for $P$, and restricts along the summand inclusion. ThereforeThis is projectivity detected by all first left derived functors. The following parts prove the three requested equivalent formulations of a hereditary abelian category with enough projectives.

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

A signature $\Sigma$ specifies sorts, finite-arity function symbols and finite-arity relation symbols. A coherent formula is built from atomic relations and equality using $\top ,\perp$, finite conjunction, finite disjunction and existential quantification. A coherent theory consists of coherent sequents $\varphi {⊢}_{\vec{x}}\psi$ in finite typed contexts. The context expresses universal quantification of the free variables; unrestricted universal quantification or negation is not a formula constructor here.

Construct the coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ as follows. Objects are formulas in context $\{\vec{x}.\varphi \}$, modulo renaming and provable equivalence. An arrow to $\{\vec{y}.\psi \}$ is a formula $\rho (\vec{x},\vec{y})$, modulo provable equivalence, for which the theory provesThese say that the relation is supported on the specified objects, total and single-valued. The identity is equality on the context, and composition isThe logical rules give associativity and the identity laws. The empty-context true formula is terminal; conjunction in disjoint contexts gives products; conjunction with equality of the two functional relations gives equalizers. Existential quantification gives images, and finite disjunction gives unions of subobjects. Substitution preserves these constructions, so images and unions are stable under pullback. This makes ${\mathcal{C}}_{\mathbb{T}}$ a coherent category.

Let $M$ be a $\mathbb{T}$-model in a topos $\mathcal{E}$. Interpret each context as a finite product of its sort objects and each formula as its corresponding subobject. DefineThe interpretation of an arrow relation $\rho$ is a total single-valued relation between these objects. Its projection to the domain is both an epimorphism, by totality, and a monomorphism, by single-valuedness, hence invertible in a topos. Its other projection therefore determines a unique morphism. Composition agrees with relational composition, so $F_M$ is a functor. Finite limits interpret equality and conjunction; images interpret existential quantification; finite unions interpret disjunction, including the empty union for $\perp$. Consequently $F_M$ is a coherent functor.

Conversely there is a canonical syntactic model $U$ in ${\mathcal{C}}_{\mathbb{T}}$. Interpret a sort $s$ by $\{x:s.\top \}$, a function symbol by its term graph, and a relation symbol by its atomic formula-in-context subobject. Induction on formulas identifies the interpretation of every $\varphi$ in $U$ with its formula-in-context object. Every axiom is then an inclusion of the associated subobjects, because it is provable in $\mathbb{T}$.

For a coherent functor $F:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{E}$, set $M_F=F(U)$. Preservation of finite limits, images and unions proves inductively that $F$ preserves all coherent interpretations, so every axiom holds in $M_F$. The same induction supplies natural isomorphismscompatible with the functional relations defining arrows. Thus $F\cong F_{M_F}$; directly on the sorts, operations and relations, $M_{F_M}\cong M$.

Finally these constructions agree on morphisms. A model homomorphism $h:M\to N$ induces maps on finite contexts. Atomic relations are preserved by definition; finite conjunction and disjunction and existential witnesses then show that each formula object maps to the corresponding formula object. Compatibility with functional relations makes these maps a natural transformation $F_M\to F_N$. Conversely a natural transformation between coherent functors restricts to its components on sort objects; naturality for term graphs preserves operations, and naturality for relation inclusions preserves relations. It is therefore a model homomorphism. The two correspondences are inverse. We have proved the categorical, not merely objectwise, equivalence

A balanced category is one in which every morphism that is both a monomorphism and an epimorphism is an isomorphism. A strong monomorphism $m:A\to B$ is a monomorphism right orthogonal to all epimorphisms: whenever $e:X\to Y$ is epic and $a:X\to A$, $b:Y\to B$ satisfy $ma=be$, there is a unique $d:Y\to A$ with $de=a$ and $md=b$. A regular monomorphism is an equalizer of some parallel pair of morphisms. Its equalizer property supplies the indicated lift after epic cancellation, so every regular monomorphism is strong.

If every monomorphism is strong and $m:A\to B$ is also epic, apply strongness to the square whose left and right sides are both $m$, with horizontal arrows $1_A$ and $1_B$. The lift $d:B\to A$ satisfies $dm=1_A$ and $md=1_B$. Thus $m$ is invertible and the category is balanced.

Conversely, suppose the category is balanced and has pullbacks in a category. Given the lifting square above, form $P=A{\times }_{B}Y$ with projections $p:P\to Y$, $q:P\to A$. The pair $(a,e)$ gives $h:X\to P$ with $ph=e$, $qh=a$. The pullback of the monomorphism $m$ is monic, so $p$ is monic. It is also epic: $rp=sp$ implies $re=se$, hence $r=s$ because $e$ is epic. Balancedness makes $p$ invertible. Now $d=q{p}^{-1}$ satisfies both required equations, and monicity of $m$ proves uniqueness. Hence in a balanced category with pullbacks, every monomorphism is strong.

For the finite example, choose a strong monomorphism $m:A\to B$ that is not regular. It is not an isomorphism, since an isomorphism is the equalizer of an identical pair. It is not epic either, since an epic strong monomorphism is invertible by the first argument. Consequently there are distinct arrows $r,s:B\rightrightarrows D$ with $rm=sm$. Since $m$ is not the equalizer of this pair, there is a map $h:X\to B$ with $rh=sh$ that does not factor through $m$. Monicity rules out failure of uniqueness, so failure of existence is the only possible failure of its equalizer property.

Define ${\mathcal{C}}_0$ to have four formally distinct objects $a,b,x,d$ and exactly the following six nonidentity arrows:Their only nontrivial composites areThere are no longer composable strings of nonidentity arrows, so these rules define an associative category. Sending $a,b,x,d$ to $A,B,X,D$, respectively, and the six arrows to $m,h,r,s,rm,rh$, defines a functor. It is a faithful functor: every hom-set has at most one arrow except ${\mathcal{C}}_0(b,d)=\{r_0,s_0\}$, and their images are distinct. Faithfulness does not require the four image objects to be distinct.

The map $m_0$ is monic, by direct inspection of arrows into $a$. Neither $m_0$ nor $h_0$ is epic, since the distinct pair $r_0,s_0$ agrees after either. Every other nonidentity arrow has target $d$ and is epic, because there is only one arrow out of $d$. A lifting square against $m_0$ whose left side is one of these epimorphisms would require an arrow $d\to b$, which does not exist. Squares whose left side is an identity have the evident unique lift. Thus $m_0$ is a strong monomorphism.

It is not a regular monomorphism. The only distinct parallel pair out of $b$ is $r_0,s_0$, and $h_0$ equalizes it but has no factorization through $m_0$, since there is no arrow $x\to a$. An identical pair has $1_b$ as its equalizer and cannot have the noninvertible $m_0$ as its equalizer. Therefore

For the covariant category in this part, put $\mathcal{E}=[\mathcal{C},\mathbf{Set}]$ and $r_c=\mathcal{C}(c,-)$. Its global-sections functor is $\Gamma =\mathrm{Hom}(1,-)$, the limit of the diagram. If $\Gamma$ is also an inverse image, it is a left adjoint and preserves all small colimits.

Consider the canonical pointwise-surjective mapAt $d$, the summand $r_d(d)$ contains $1_d$, so $q$ is an epimorphism. In a presheaf topos epimorphisms are regular, and a colimit-preserving functor preserves their coequalizer presentations. Thus $\Gamma q$ is surjective. Since $\Gamma$ preserves coproducts, some summand has a global element, yielding a section $s:1\to r_c$ of its unique map $r_c\to 1$. The constant singleton functor is a retract of a covariant representable.

Conversely, if $1$ is such a retract in a category, $\mathrm{Hom}(1,-)$ is a retract of $\mathrm{Hom}(r_c,-)$, which is evaluation at $c$ by the Yoneda lemma. Evaluation preserves colimits pointwise. The colimit comparison for a retract functor is a retract of the evaluation comparison; a retract of an isomorphism is an isomorphism, so $\Gamma$ preserves all small colimits. It also preserves finite limits because it is representable. A right adjoint can be constructed byFor $h:d\to d^{\prime }$, precomposition gives $r_{d^{\prime }}\to r_d$, and applying $\Gamma$ and then $\mathrm{Set}(-,S)$ gives $R(S)(d)\to R(S)(d^{\prime })$. The presentation of every functor as a colimit of representables gives $\mathrm{Hom}(F,R(S))\cong \mathrm{Set}(\Gamma F,S)$. Hence $\Gamma ⊣R$, so $\Gamma$ is an inverse image and the topos is local.

The retract condition has a precise interpretation as the initial object criterion for a covariant local topos. Write the section as a natural family $u_d:c\to d$. Naturality says $h{u}_d=u_{d^{\prime }}$ for every $h:d\to d^{\prime }$. Put $e=u_c$. Then $e^2=e$ and every $f:c\to d$ satisfies $fe=u_d$. In the idempotent completion of $\mathcal{C}$, the object $(c,e)$ is initial: an arrow from it to $(d,k)$ must satisfy $v=kve$, and the identities force $v=u_d$; this arrow exists because $k{u}_d=u_d$ and $u_{d}e=u_d$.

Conversely an initial object $(c,e)$ in the idempotent completion gives that natural family and the retract. ThereforeIf $\mathcal{C}$ is already idempotent-complete, this is equivalent to an initial object in $\mathcal{C}$ itself, and $\Gamma$ is evaluation there. The word is initial, not terminal, because this question uses covariant functors.

One cannot omit idempotent completion for a general small category. Take the one-object category of the monoid $\{1,0\}$ with absorbing zero. It has no initial object because its endomorphism set has two elements, but the natural family $u=0$ satisfies $m0=0$ for every $m$. Its covariant functor category is local. Concretely, a functor is a set with an idempotent operator, and its global sections are the fixed points of that operator.

For a topological space $X$, there is an equally explicit criterion. If $\mathbf{Sh}(X)$ is local, apply $\Gamma$ to the epimorphism ${\coprod }_i{U}_i\to 1$ associated with any open cover $X={\bigcup }_i{U}_i$, regarding the opens as subterminal sheaves. Since $\Gamma U_i$ is a singleton exactly when $U_i=X$, and otherwise empty, coproduct and epimorphism preservation force some $U_i=X$.

Thus every open cover of $X$ contains $X$ itself. Conversely this open cover criterion for a local sheaf topos condition is equivalent to existence of a point $x$ whose only open neighborhood is $X$: the union of all proper open sets cannot be all of $X$, so choose $x$ outside it. Such a point plainly forces any cover to contain $X$. Empty spaces fail the condition.

At this point, the stalk functor $F\mapsto F_x$ is simply $F(X)=\Gamma F$, since there is only one open neighborhood. Its right adjoint is the skyscraper sheaf of setsA morphism $F\to R(S)$ is determined exactly by its map $F(X)\to S$, because all proper opens omit $x$. Hence $\Gamma ⊣R$, and $\Gamma$ preserves finite limits, proving locality. ConsequentlyIn a $T_0$ space this distinguished point is unique and closed. In a $T_1$ space the condition forces $X$ to be a singleton. Indistinguishable points in a non-$T_0$ space can all have this property; uniqueness of an actual point is not part of the general criterion.

A monomorphism $m:A\to B$ satisfies $mu=mv\Rightarrow u=v$ for every parallel pair into $A$. An epimorphism $e:X\to Y$ satisfies $ue=ve\Rightarrow u=v$ for every parallel pair out of $Y$. A strong monomorphism is a monomorphism with the following lifting property: whenever $e:X\to Y$ is an epimorphism and $mu=ve$, with $u:X\to A$ and $v:Y\to B$, there is a unique $d:Y\to A$ with $de=u$ and $md=v$. A regular monomorphism is a morphism occurring as the equalizer of two parallel maps. A balanced category is one in which every morphism that is both a monomorphism and an epimorphism is an isomorphism.

Suppose $m:A\to B$ equalizes $p,q:B\rightrightarrows D$. If $mu=mv$, the common composite has two factorizations through the equalizer, so its uniqueness property gives $u=v$. Hence every regular monomorphism is indeed a monomorphism.

Now take the lifting square just described. The equations $pmu=qmu$ imply $pve=qve$. Cancel the epimorphism $e$ to obtain $pv=qv$. The equalizer gives a unique $d$ with $md=v$. Since $mde=ve=mu$ and $m$ is a monomorphism, $de=u$. Thus every regular monomorphism is a strong monomorphism; the existence of the lift uses epic cancellation, and its uniqueness uses the equalizer property.

If every monomorphism is strong, let $m:A\to B$ be both a monomorphism and an epimorphism. Use $m$ as both vertical maps in the lifting square, with horizontal maps $1_A$ and $1_B$. The strong monomorphism property gives $d:B\to A$ satisfying $dm=1_A$ and $md=1_B$. Thus $m$ is an isomorphism, proving that the category is balanced.

For the converse, take $e:X\to Y$ epic, $m:A\to B$ monic, and $mu=ve$. Form the pullback in a category of $m$ along $v$:The equality $mu=ve$ gives $t:X\to P$ with $pt=e$ and $qt=u$. By preservation of monomorphisms under pullback in a category, $p$ is monic. It is also epic: if $hp=kp$, then $he=hpt=kpt=ke$, and cancellation of $e$ gives $h=k$. The balanced category hypothesis therefore makes $p$ an isomorphism.

Set $d=q{p}^{-1}$. Then $md=v$ and $de=qt=u$. Any other such lift agrees with $d$ after composing with the monomorphism $m$, so it is equal to $d$. Consequently in a category with pullbacks in a category, being balanced is equivalent to every monomorphism being a strong monomorphism. This is the balanced categories with pullbacks have strong monomorphisms principle; the proof does not assume pullback stability of epimorphisms.