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.


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$.

| cite | improve this answer | |
  • $\begingroup$ That's great. Now I know I'm barking up the right tree I can start thinking harder about this without fearing I'm on the wrong track. Thanks Todd! $\endgroup$ – Tom Ellis Oct 9 '11 at 14:06
  • $\begingroup$ You're welcome, Tom. By the way, if you found this answer helpful, feel free to upvote it. :-) $\endgroup$ – Todd Trimble Oct 9 '11 at 14:15
  • $\begingroup$ Done. Also worth mentioning is that your second statement is stronger than my observation. I didn't claim my map was injective from $g : Fx \to Fy$ in $\mathcal C$, just from $Gg$ for such $g$, so actually what you've told me is even better for my purposes. $\endgroup$ – Tom Ellis Oct 9 '11 at 14:50
  • $\begingroup$ When I wrote "second statement" I meant "statement in your second sentence". $\endgroup$ – Tom Ellis Oct 9 '11 at 14:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.