The Eilenberg-Moore cat of a monad is isomorphic to the presheaves on its Kreisli cat that restrict to representable functors (elementary proof?)

53 Views Asked by At

$\def\C{\mathsf{C}}$I am trying to prove by hand the following result from Riehl's Category Theory in Context (I slightly adapted the statement)¹:

Exercise 5.2.vii. Let $(T,\eta,\mu)$ be a monad on a category $\mathsf{C}$. Denote $\C_T$ and $\C^T$ respectively to the Kreisli category and the Eilenberg-Moore category of $T$. Let $K:\C_T\to\C^T$ be the canonical full embedding of $\C_T$ into the subcategory of free $T$-algebras. The functor\begin{equation} \begin{gathered} \mathsf{C}^T \xrightarrow{\mathsf{C}^T\left(K-,-\right)} \mathsf{Set}^{\mathsf{C}_T^{\text {op }}} \\ (A, \alpha) \quad \mapsto \quad \mathsf{C}^T(K-,(A, a)) \end{gathered} \end{equation} is a full embedding into the category of presheaves of sets on $\C_T$ that when restricted along $F_T:\C\to\C_T$ give a representable presheaf $\C^\mathrm{op}\to\mathsf{Set}$.

(Note the map is well-defined, since $$ \tag{1}\label{eq} \mathsf{C}^T(KF_T-,(A, a))=\mathsf{C}^T(F^T-,(A, a))=\mathsf{C}(-,U^T(A,a))=\mathsf{C}(-,A), $$ here $F^T\dashv U^T$ is the canonical adjunction $F^T:\mathsf{C}\rightleftarrows\mathsf{C}^T:U^T$ with induced monad $(T,\eta,\mu)$.)

The proof is in R. Street, The formal theory of monads, Theorem 14, but I was trying to reconstruct the proof myself. In the nLab article for the Eilenberg-Moore category, this result is Proposition 3.2, and there one finds the following sketch of a proof:

Assume that $P:\C_T^\mathrm{op}\to \mathsf{Set}$ is a presheaf on the Kleisli category and $A$ is an object of $\C$ such that $\C(-,A)=P\cdot F_T$ [to be rigorous, we should actually write $P\cdot F_T^\mathrm{op}$ but we do not do this to simplify notation]. Then a $T$-algebra structure $\alpha:TA\to A$ on $A$ is given by $\alpha=P(1_{TA})(1_A)$, where $1_{TA}$ is viewed as a Kleisli morphism from $TA$ to $A$ in $C_T$.

Here's what I've done so far:

We first need to verify that indeed $(A,\alpha)$ is a $T$-algebra. First, we verify that $\alpha\cdot\eta_A=1_A$. I will denote as $A\rightsquigarrow B$ to a morphism in $C^T$ from $A$ to $B$ (represented by some morphism $A\to TB$ in $\C$). Note that the composite $A\stackrel{F_T\eta_A}{\rightsquigarrow}TA\stackrel{1_{TA}}{\rightsquigarrow} A$ in $\C_T$ equals the identity $A\rightsquigarrow A$ in $\C_T$. Hence, $1_A=P(1_{TA}\cdot F_T\eta_A)(1_A)=P(F_T\eta_A)P(1_{TA})(1_A)=\eta_{A}^*(\alpha)=\alpha\cdot\eta_A$, where we've used $P\cdot F_T=\C(-,A)$, so that $P F_T\eta_A=\eta_A^*$.

Next, we need to show that $\alpha\cdot T\alpha=\alpha\cdot\mu_A$. Here's where I get stuck. I don't know which trick now one may use. Also, even if we take this last formula for granted, how one would show $P=\C^T(K-,(A,a))$? By hypothesis, the action on objects of these two functors is the same, and so is the action on morphisms on the image of $F_T$. But what about the action on an arbitrary morphism of $\C^T$? If one could write an arbitrary morphism $A\xrightarrow{f}TB$ as a Kleisli composite of morphisms of the form $A_i\xrightarrow{f_i}A_{i+1}\xrightarrow{\eta_{A_i}}TA_{i+1}$, then we would win, but I'm not sure this is possible.

(I guess one possible answer is "just read Street's paper," but his proof seems to rely on a bunch of different results he proves before the statement; I am unsure whether all that machinery—that I haven't read—is necessary to prove this.)


¹ The way Riehl phrases it makes it unclear whether she wants us to prove the full statement or rather we should just derive \eqref{eq} and then know—as a curiosity, not for us to prove—that “in fact, this functor defines an isomorphism between the Eilenberg–Moore category and the full subcategory of presheaves on the Kleisli category that restrict along $F_T$ to representable functors.”