Question

While thinking about monads in the theory of denotational semantics, I have made an observation about the Kleisli category that I would like to check

Suppose $F : \mathcal D \to \mathcal C$, $G : \mathcal C \to \mathcal D$, is an adjunction, so that $T = GF : \mathcal D \to \mathcal D$ is a monad. There is an operator $ * $ on the Kleisli category that takes $f: X \to TY$ to $f^* : TX \to TY$.

I have an intuition and a sketch proof of the following, but my experience with these things is not strong, so I would like confirmation. In fact, this may just be an obvious or basic result on monads and adjunctions, but I'm not sure. The following statements I think I've proved:

$f^* $ is in fact $Gg$ for some $g : FX \to FY$ in $\mathcal C$, and moreover there is a bijection between Kleisli arrows $f : X \to TY$ and morphisms $Gg$ where $g : FX \to FY$. The inverse of the $*$ operation is given by taking $f' : TX \to TY$ to $f' \circ \eta_X$, where $\eta$ is the monad unit.

In a sense this means that the Kleisli category is "as much of $\mathcal C$ as can be represented in $\mathcal D$, given $F$. If what I say is true I suppose it must be something quite elementary, but I don't know where to look. Pointers would be appreciated.

Answer 1

Sure, you could put it that way. I think it's simpler to say that there is a natural bijection between arrows $f: x \to GFy$ in $\mathcal{D}$ and arrows $g: Fx \to Fy$ in $\mathcal{C}$, because that is obvious from the hom-formulation of adjunctions:

$$\hom_{\mathcal{C}}(Fx, Fy) \cong \hom_{\mathcal{D}}(x, GFy).$$

But it is a nice exercise to make this correspondence explicit through the use of triangular equations (see CWM). Rather than test my ability to draw commutative diagrams in MathJax, I'll just write down the equations and leave it to you to draw the diagrams. Let $\eta: 1_\mathcal{D} \to GF$ denote the unit and $\varepsilon: FG \to 1_\mathcal{C}$ the counit. Given $f: x \to GFy$, define $g = f^\wedge = (\varepsilon Fy)(Ff)$. And given $g: Fx \to Fy$, define $f = g^\vee = (Gg)(\eta x)$. Then

$$f^{\wedge \vee} = G((\varepsilon Fy)(Ff))(\eta x) = (G\varepsilon Fy)(GFf)(\eta x) = (G\varepsilon Fy)(\eta GFy)(f) = 1_{GFy} f = f$$

where the second equation uses functoriality of $G$, the third uses naturality of $\eta$, and the fourth is a triangular equation. Similarly,

$$g^{\vee \wedge} = (\varepsilon Fy)F((Gg)(\eta x)) = (\varepsilon Fy)(FGg)(F\eta x) = g(\varepsilon Fx)(F\eta x) = g 1_{Fx} = g$$

where the second equation uses functoriality of $F$, the third uses naturality of $\varepsilon$, and the fourth is the other triangular equation. All this is well-covered in CWM.

Finally, another way to think about this is that the star extension exhibits the Kleisli category as a full subcategory of the Eilenberg-Moore category of $T$-algebras: it is exactly the subcategory consisting of free algebras $Tx$.