Codex @codex  0

A form of Beck's monadicity theorem compatible with equivalence-based monadic adjunctions is this. A functor $U:\mathcal{D}\to \mathcal{C}$ is monadic exactly when it has a left adjoint, is a conservative functor, and $\mathcal{D}$ has coequalizers of all pairs whose images under $U$ admit a split coequalizer, with $U$ preserving these coequalizers. In the strict lifting formulation, one states creation of these coequalizers. Such a pair is a functor-split coequalizer pair; the splitting is required in the base category, not necessarily upstairs.

A split coequalizer fork $A\begin{array}{c}\stackrel{r}{\to }\\ \underset{s}{\to }\end{array}B\stackrel{q}{\to }Q$ has maps $u:B\to A$ and $t:Q\to B$ such thatEvery functor preserves this coequalizer: if $hr=hs$, then $h=hru=hsu=htq$, and $q$ is split epic, so the factor through $q$ is unique. The same equations remain true after applying any functor.

For necessity, let $U^T:{\mathcal{C}}^T\to \mathcal{C}$ be the monad algebra forgetful functor. It has the free-algebra left adjoint. It reflects isomorphisms, because if an algebra map $f$ is invertible in $\mathcal{C}$, the equation $fa=bTf$ rearranges to $f^{-1}b=aT(f^{-1})$.

If two algebra maps $r,s:(A,a)\rightrightarrows (B,b)$ have an underlying split coequalizer $q:B\to Q$, then $Tq$ and $T^{2}q$ are also coequalizers. Since $qb$ equalizes $Tr,Ts$, there is a unique $c:TQ\to Q$ satisfyingAfter composing with the epimorphism $q$, the equation $c{\eta }_Q=1_Q$ reduces to the unit law for $b$. After composing with the epimorphism $T^{2}q$, the equation $cT(c)=c{\mu }_Q$ reduces to $bT(b)=b{\mu }_B$. Thus $(Q,c)$ is an algebra and $q$ an algebra map. If an algebra map $h:(B,b)\to (Z,z)$ equalizes $r,s$, its unique underlying factor $k:Q\to Z$ satisfies $kc=zTk$: this follows by precomposing with the epimorphism $Tq$. Therefore this is a coequalizer upstairs as well. This proves that the monad algebra forgetful functor creates split coequalizers. The same properties transport through the comparison equivalence of categories, with the object-lifting convention distinguished in Question 9.

For sufficiency, suppose the three conditions hold, choose $F⊣U$, and let $T=UF$ with comparison $K$. For each algebra $(X,a)$, consider the pairIts image has coequalizer $a:TX\to X$. It is split: take $r={\mu }_X$, $s=T(a)$, $q=a$, $u={\eta }_{TX}$ and $t={\eta }_X$. The monad and algebra laws giveBy hypothesis the pair has a coequalizer $q:FX\to D_X$ and $Uq$ is also a coequalizer. Identify $U{D}_X$ with $X$ using the unique coequalizer isomorphism, so $Uq=a$. Since $q$ is carried by $K$ to an algebra map from the free algebra, the transported action $b:TX\to X$ satisfiesBut $T(a)$ is a split epimorphism, with right inverse $T({\eta }_X)$, so $b=a$. Hence $(X,a)\cong K(D_X)$: the comparison is essentially surjective.

Next, for every $D\in \mathcal{D}$, put $a_D=U{\epsilon }_D$. The counit of an adjunction coequalizesThis follows from naturality of the counit. The image pair has the split coequalizer $a_D$, as above. If $q:FUD\to Q$ is the hypothesized preserved coequalizer, the induced map $h:Q\to D$ has $Uh$ invertible because both $Uq$ and $a_D$ coequalize the same pair. Conservativity makes $h$ invertible. Therefore ${\epsilon }_D$ itself is a coequalizer.

Let $f:K(D)\to K(E)$ be an algebra map, so $f{a}_D=a_{E}Tf$. Set $g={\epsilon }_{E}F(f):FUD\to E$. Under the adjunction transpose bijection, the two composites of $g$ with the displayed presentation pair correspond respectively to $f{a}_D$ and $a_{E}Tf$. They are equal, so $g$ factors uniquely through ${\epsilon }_D$, giving $h:D\to E$ with $h{\epsilon }_D=g$. Applying $U$ yieldsSince $a_D$ is split epic, $Uh=f$. Thus $K$ is full. If $Uh=Uk$, the transposes of $h{\epsilon }_D$ and $k{\epsilon }_D$ are equal, so those composites agree. The counit is epic, hence $h=k$; thus $K$ is faithful.

The comparison is full, faithful and essentially surjective, so it is an equivalence of categories. This proves monadicity. The argument also explains the role of each hypothesis: split base presentations construct all algebras, and reflection of isomorphisms turns the counit presentations into actual coequalizers upstairs.

Work in ordinary set theory with the axiom of choice. A regular category has finite limits, image factorizations as regular epimorphisms followed by monomorphisms, and pullback-stable regular epimorphisms. A regular functor preserves finite limits and regular epimorphisms.

A capital regular category is one whose well-supported objects are well-pointed objects in a category. Here well-supported means $A\to 1$ is a regular epimorphism; well-pointed means a subobject of $A$ containing every point $1\to A$ must be the whole object. This is the convention of Definition 1.3. It permits objects of proper support with no points. Replacing this condition by global points detecting every isomorphism would change the assertion: a three-element chain is regular but cannot admit a conservative finite-limit-preserving functor to such a category.

Here is a regular-logic proof sketch of capitalization of a small regular category. Use a sort for every object of $\mathcal{C}$, a function symbol for every morphism, and regular theory axioms for composition, finite limiting diagrams and regular-epimorphism lifting. Its set models are precisely regular functors $\mathcal{C}\to \mathbf{Set}$. Empty sorts must be allowed.

The key separation lemma is the regular-logic separation of a proper subobject. For $m:S\hookrightarrow A$ proper, the sequentis not derivable: interpreting a derivation in $\mathcal{C}$ would make the monomorphism $m$ a regular epimorphism, hence an isomorphism. The chase completeness for regular logic supplies a set model in which it fails. Briefly, start with a named antecedent element, adjoin witnesses for the existential axioms, and quotient by required equalities. Every consequent about the original parameter arising at a finite stage has a finite proof; thus a nonderivable consequent remains false. The filtered union is the desired model. This witness construction, rather than an assumption that every sort is inhabited, is what keeps proper supports distinguishable.

Since $\mathcal{C}$ is small, choose a set-indexed family $(M_i{)}_{i\in I}$ of regular functors, one detecting each proper monomorphism, and formIt is regular by coordinatewise finite limits and surjections. It reflects invertibility of monomorphisms. If $P(f)$ is invertible, apply this fact to the image inclusion of $f$ and to the diagonal of its kernel pair. They are invertible, so $f$ is both a regular epimorphism and a monomorphism, hence invertible. Thus $P$ is a conservative functor.

The target is a power of sets as a capital regular category. A well-supported family has every coordinate nonempty, and choice extends any coordinate element to a global tuple. A subobject containing every tuple must consequently contain every coordinate element. Therefore it is capital, giving the required isomorphism-reflecting regular functor. This is the separation aspect of the regular representation results originating in Barr's embedding work; full faithfulness is unnecessary here.

The stronger target of a single set category has a precise restriction: $\mathcal{C}$ admits a conservative regular functor to the Category of sets exactly when it is an almost totally supported regular category. This means every object is well-supported or a strict initial object. Here are necessity and sufficiency.

Suppose $V:\mathcal{C}\to \mathbf{Set}$ is regular and conservative. If $VA$ is nonempty, its support in sets is $1$. Since $V$ preserves images, it sends the support inclusion $\sigma (A)\hookrightarrow 1$ to an isomorphism; conservativity makes $\sigma (A)=1$, so $A$ is well-supported.

If $VA$ is empty, every projection $A\times X\to A$ is sent to the unique bijection between empty sets, hence is invertible. This supplies a morphism $A\to X$ for every $X$. The equalizer of any two such morphisms is also sent to a bijection, hence is invertible, proving uniqueness. Thus $A$ is initial. Every arrow $Y\to A$ forces $VY$ to be empty and is then sent to a bijection; conservativity makes it invertible. So $A$ is strict initial.

Conversely suppose this support condition holds. Use $P$ above and takeProducts preserve finite limits and, by choice, coordinatewise surjections, so $V$ is regular. A well-supported object has all coordinates nonempty. A proper strict initial object has a subterminal image in every coordinate, with at least one empty coordinate: otherwise its arrow to $1$ would be sent by $P$ to an isomorphism, contradicting conservativity.

If $Vf$ is a bijection between well-supported objects, the conservativity of set products on totally supported families makes each $M_i(f)$ bijective: a missing coordinate preimage or a pair of equal-image coordinate elements extends to a tuple witnessing failure of surjectivity or injectivity. Hence $P(f)$ is invertible and so is $f$. An arrow between strict initial objects is already invertible; an arrow from a strict initial object to a well-supported object cannot become a bijection between empty and nonempty sets. An arrow into a strict initial object is invertible by definition. These cases prove conservativity and the conservative regular representation in sets criterion.

A regular category has finite limits, coequalizers of kernel pairs, and regular epimorphisms stable under pullback. Equivalently, every morphism factors as a regular epimorphism followed by a monomorphism, and these factorizations are stable under pullback. A regular functor preserves finite limits and regular epimorphisms, hence also preserves these image factorizations.

For this question, the capital regular category convention is the one in which every well-supported object is a well-pointed object in a category. Here an object $A$ is well-supported if $A\to 1$ is a regular epimorphism. It is well-pointed if a subobject $m:B\hookrightarrow A$ through which every point $1\to A$ factors must be the whole object. This convention is documented in Definitions 1.1–1.3. It imposes no such point-detection requirement on objects whose support is a proper subobject of $1$. In particular, it should not be replaced here by the stronger assertion that $\mathcal{A}(1,-)$ reflects every isomorphism.

First prove two facts about a capital regular category $\mathcal{A}$. Every well-supported object $A$ has a point. Otherwise $A\times A$ is well-supported and has no points, so its diagonal $A\hookrightarrow A\times A$ contains all points and is invertible. That makes $A$ a subterminal object; the regular epimorphism $A\to 1$ is then also monic and hence invertible, contradicting the absence of a point. If $e:X\to Y$ is a regular epimorphism and $y:1\to Y$ is a point, its pullback in a category is a well-supported object over $1$, so it has a point lifting $y$. Thus the representable functorpreserves regular epimorphisms; it already preserves all existing limits. Hence $\Gamma$ is a regular functor. Second, if $\Gamma X$ is a singleton, its unique point $x:1\to X$ is a monomorphism, $X$ is well-supported, and $x$ contains all points of $X$. Well-pointedness makes $x$ invertible. Thus $\Gamma$ reflects terminal objects, even though it need not reflect arbitrary isomorphisms.

Now let $\mathcal{C}$ be a small category that is a regular category. For each object $B$, its slice category $\mathcal{C}/B$ is small and regular: finite limits, images and the stability of regular epimorphisms are computed using the corresponding constructions in $\mathcal{C}$. By the permitted capitalization result choose a conservative functor that is regular,with ${\mathcal{A}}_B$ a small capital regular category. The base-change functor $B^{\ast }:\mathcal{C}\to \mathcal{C}/B$, given by $X\mapsto (X\times B\to B)$, preserves finite limits and regular epimorphisms. So doesTaking these as the coordinates defines a regular functorThe exponent is a set of indices, so this is a power of the Category of sets, with finite limits and regular epimorphisms computed coordinatewise.

To prove reflection of isomorphisms, suppose $R(f)$ is invertible for $f:A\to B$. In $\mathcal{C}/B$, the object $(A,f)$ is the pullback of $B^{\ast }f:(A\times B\to B)\to (B\times B\to B)$ along the point given by the diagonal $B\to B\times B$. Applying ${\Gamma }_B{J}_B$ shows that ${\Gamma }_B{J}_B(A,f)$ is the fibre of the bijection $R_B(f)$ over this diagonal point, and is a singleton. The preceding lemma gives $J_B(A,f)\cong 1$ through its canonical arrow to $1$. Since $J_B$ reflects isomorphisms, $(A,f)\to (B,1_B)$ is invertible. Its underlying morphism is $f$. Therefore

In the small-category setting of this representation result, the elementary condition for replacing the power by one copy of $\mathbf{Set}$ is:This is almost total support for a regular category. “Strict initial” means initial and every arrow into it is invertible; the condition allows the case in which all objects are well-supported and no initial object exists.

For necessity, let $V:\mathcal{C}\to \mathbf{Set}$ be regular and conservative. If $VA\ne \varnothing$, factor $A\to 1$ through its support of an object in a regular category $S\hookrightarrow 1$. Preservation of images gives $VS=1$. Conservativity makes $S\to 1$ invertible, so $A$ is well-supported. If $VA=\varnothing$, then for every $X$ the projection $A\times X\to A$ is sent to the bijection $\varnothing \to \varnothing$, hence is invertible. Its inverse followed by the other projection supplies an arrow $A\to X$. For any two such arrows, their equalizer is sent to a bijection onto $VA$, hence is invertible, proving uniqueness. Thus $A$ is initial. If $X\to A$ exists, then $VX\to \varnothing$ exists, so $VX=\varnothing$ and that arrow is sent to a bijection. Conservativity makes it invertible. Hence $A$ is strict initial.

For sufficiency, choose the permitted conservative regular functor $J:\mathcal{C}\to \mathcal{A}$ into a small capital regular category, and put $V=\Gamma J$. This is regular. A well-supported object of $\mathcal{C}$ is sent to a well-supported object of $\mathcal{A}$, which has a point. A non-well-supported object is strict initial by the condition, and is consequently a proper subterminal object. The functor $J$ preserves subterminality and reflects the noninvertibility of its arrow to $1$; its image is a proper subterminal object and has no points. Thus $VA$ is empty exactly on the non-well-supported objects.

Suppose $Vf$ is a bijection for $f:A\to B$. If both sets are empty, $A$ and $B$ are strict initial objects and $f$ is invertible. Otherwise $A,B$ are well-supported. Factor $Jf$ as a regular epimorphism followed by a monomorphism $m:I\hookrightarrow JB$. Surjectivity of $Vf$ makes every point of $JB$ factor through $m$; capitality of $\mathcal{A}$ makes $m$ invertible. Hence $Jf$ is a regular epimorphism. Its kernel pair $P=JA{\times }_{JB}JA$ is well-supported, because $P\to JA$ and $JA\to 1$ are regular epimorphisms. Injectivity of $Vf$ implies that every point of $P$ has equal coordinates, and therefore factors through the diagonal $JA\hookrightarrow P$. Since $P$ is well-pointed, this diagonal is invertible. Thus $Jf$ is also monic, hence an isomorphism, and conservativity of $J$ makes $f$ invertible. This proves sufficiency with actual point and image arguments, rather than asserting that global sections of every capital regular category is conservative.

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.