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.

Define maps between the hom-sets byUsing naturality of the proposed counit of an adjunction and then the first triangle identity for an adjunction,Using naturality of the proposed unit of an adjunction and then the other triangle identity for an adjunction,Hence $\Phi$ and $\Psi$ are inverse bijections. They are natural in both variables: for $a:A^{\prime }\to A$ and $b:B\to B^{\prime }$, the unit of an adjunction identity givesThis constructs an adjunction $F⊣G$. Taking $f=1_{FA}$ and $g=1_{GB}$ recovers the prescribed unit of an adjunction and counit of an adjunction. Conversely, part (i) shows that any adjunction with those components must have exactly these transpose formulas. The adjunction exists and is unique with the prescribed unit and counit.

Write the adjunction as the natural bijectionThe unit of an adjunction and counit of an adjunction are the natural transformations whose components areNaturality of the hom-set bijections gives, for $f:FA\to B$ and $g:A\to GB$,For example, postcomposition by $f$ in the first hom-set corresponds to postcomposition by $Gf$ in the second, giving the first formula; naturality in $A$ gives the second. The same naturality says that, for $a:A\to A^{\prime }$ and $b:B\to B^{\prime }$,Thus these components do define the asserted natural transformations $1_{\mathcal{C}}\to GF$ and $FG\to 1_{\mathcal{D}}$.

A Cartesian closed category has finite products in a category and, for all $X,Y$, an exponential object $Y^X$ with a natural bijectionEquivalently the functor $-\times X$ has a right adjoint. Its counit of an adjunction is the evaluation map of an exponential object $Y^X\times X\to Y$.

For the presheaf category, define the exponential in a presheaf category byFor $f:D\to C$, its restriction sends $\alpha$ to $\alpha \circ (h_f\times 1_X)$. Composition of these restriction maps follows from composition of the $h_f$, so this is a categorical presheaf. Define evaluation map of an exponential object byFor $f:D\to C$, naturality of $\alpha$ givesThus $e$ is a natural transformation.

Given a natural transformation $\beta :Z\times X\to Y$, define its currying byNaturality of $\beta$ proves that ${\hat{\beta }}_C(z)$ is a natural transformation $h_C\times X\to Y$. For $f:C^{\prime }\to C$, the same formula proves that $\hat{\beta }:Z\to Y^X$ is natural. Evaluating at $g=1_C$ gives $e(\hat{\beta }\times 1_X)=\beta$.

Conversely, if $\gamma :Z\to Y^X$ and $\beta =e(\gamma \times 1_X)$, thenby naturality of $\gamma$. Hence the two constructions are inverse and natural in $Z,Y$. Products are available pointwise, including the terminal singleton presheaf, so the presheaf category is Cartesian closed. The exponential uses natural transformations out of $h_C\times X$; simply exponentiating the individual values generally does not give this object.

For $F⊣U$ with unit of an adjunction $\eta$ and counit of an adjunction $\epsilon$, putThe triangle identities for an adjunction giveFor associativity, naturality of $\epsilon$ at ${\epsilon }_{FA}:FUFA\to FA$ saysApply $U$ to obtain ${\mu }_{A}T({\mu }_A)={\mu }_A{\mu }_{TA}$. Thus this is the monad induced by an adjunction.

Conversely, start with a monad $(T,\eta ,\mu )$. The free algebra functor sends $A$ to $(TA,{\mu }_A)$ and $f$ to $Tf$. The monad laws ensure that these are algebras for a monad and morphisms of algebras for a monad. For an algebra $(B,b)$, there are inverse bijectionsThe inverse really is an algebra map becauseFor a free-algebra map $g$, its algebra equation and the monad unit law giveFor a base map $f$, naturality and the algebra unit law give $bT(f){\eta }_A=b{\eta }_{B}f=f$. The formulas are natural, establishing the free-forgetful Eilenberg-Moore adjunction $F^T⊣U^T$. Its unit is ${\eta }_A$, and its counit at $(B,b)$ is $b$. Hence its induced multiplication is $\mu$, and every monad arises from an adjunction.