3
$\begingroup$

For a monad $(T,\mu,\eta)$ if $T(A) = T(B)$, does this imply that $\mu_A = \mu_B$? I want to know because in the bijection between Kleisli triples and monads, given a monad, we define $f^* := T(f) ; \mu_B$ if $f : A\to T(B)$ (c.f. Prop 1.6), but this needs to be well defined even when $T$ is not an embedding.

Clarification (more formal): Given a monad $(T,\mu,\eta)$, I need to define ${}^*$ on the class $\{f \;|\; \exists A,B \in |\mathbf{C}| . f : A \to T B \}$. If $T$ were an embedding then I could just take $B := T^{-1}(\mathrm{cod}(f))$. What do I do though when $T$ is not an embedding? All I know about the codomain of an element of this class is that it is in the image of $T$. There may be many $B$'s and the $\mu_B$'s may be different!

$\endgroup$
6
  • 2
    $\begingroup$ The objects of the Kleisli category are the objects of the underlying category, not T of them, so the reconstruction of the monad from the Kleisli category is always perfectly well-defined, even though the answer to your first question is probably "no." $\endgroup$ May 26, 2010 at 0:56
  • $\begingroup$ Maybe I did not make myself clear enough. It is a subtle point (maybe trivial?), and one that I missed until I tried to formally write down a definition in Isabelle. Given a monad $(T,\mu,\eta)$, I need to define $*$ on the class $\{f|\exists A,B \in |\mathbf{C}| . f : A \to T B \}$. If $T$ were an embedding then I could just take $B := T^{-1}(\mathrm{cod}(f))$. What do I do though when $T$ is not an embedding? All I know about the codomain of an element of this class is that it is in the image of $T$. There may be many $B$'s and the $\mu_B$'s may be different! $\endgroup$
    – user6082
    May 26, 2010 at 10:08
  • $\begingroup$ You could just define the morphisms to be triples $(A, B, f : A \to TB)$. Then you would know which $B$ to choose. $\endgroup$ May 26, 2010 at 11:27
  • $\begingroup$ I was thinking about this, but that's a different category, isn't it? $\endgroup$
    – user6082
    May 26, 2010 at 11:32
  • 1
    $\begingroup$ I should add that your difficulty is partly a function of the fact that you are trying to define $*$ on the universal collection of all the morphisms, rather than by considering families of hom-sets indexed by domain and codomain. In a dependent type theory, I would usually try to define Hom to be a type operator dependent upon domain and codomain. Isabelle must have some standard techniques to work around the lack of dependency -- I would look at those. (My previous comment is one way of doing it, but if there's an idiomatic thing you should do that.) $\endgroup$ May 26, 2010 at 11:33

3 Answers 3

2
$\begingroup$

This didn't fit in the comments, so I'm posting it as an answer.

Ignoring size issues, we can define a category as a set of objects, together with a family of sets of morphisms, with one set for each domain and codomain -- ie, as a dependent record:

$$\mathrm{Cat} = \sum \mathrm{Obj}:\mathrm{Set}.\;\sum \mathrm{Mor} : \mathrm{Obj} \times \mathrm{Obj} \to \mathrm{Set}.\; \ldots \mathit{category\; axioms} \ldots$$

So if you have a category $C \equiv (\mathrm{Obj}, \mathrm{Mor}, \ldots)$ and a monad $(T, \mu, \eta)$, the Kleisli category will be of the form $(\mathrm{Obj}, (\lambda AB.\;\mathrm{Mor}(A, TB)), \ldots)$.

Then, the extension operator will be an operation whose type is $\prod A,B:O.\;\mathrm{Mor}(A, TB) \to \mathrm{Mor}(TA, TB)$, which can be defined in the obvious way, as $\lambda A\;B\;f.\;T(f);\mu_B$. Note that the objects for the domain and codomain come in as arguments, so there's no need to reconstruct them from the data of the function $f$.

(In fact, if you spell out the definition of functor for this setup, you'll see that even $T$ will be indexed, so its action on morphisms really ought to be written $T_{A,B}(f)$. I just left them out since these arguments are obvious from context.)

$\endgroup$
1
  • $\begingroup$ Thanks for this. But I'm not talking about the Kleisli Category $C_T$, I am talking about the Kleisli triple over $C$ (sorry, this was my mistake; I'll edit the question). In every place where I have seen the Kleisli triple defined from a Monad, the underlying Category is the same with no indexing of objects. When you index the objects, surely it is a different category, however you present the theory. $\endgroup$
    – user6082
    May 26, 2010 at 12:56
1
$\begingroup$

I agree with Mike that you shouldn't NEED this, BUT the answer is yes. The monad $T$ arises as coming from the adjunction $U:C^T \to C:F$, where $C^T$ is its category of Eilenberg-Moore algebras. Since this adjunction is monadic, it reflects isos. Hence, if $TX=U(FX)$ is iso to $TY=U(FY)$, then $FX$ and $FY$ are iso. Now, consider $id_{UFX}$, then, since here is a bijection DEPENDING NATURALLY ON A=UFX and B=FX between $Hom(FA,B)$ and $Hom(A,UB)$, we have that $\epsilon_{FX}$ and $\epsilon_{FY}$ are the same (up to identification via isomorphisms), where $\epsilon$ represents the counit of the adjunction. Now, multiplication $\mu$ of the monad $T$ has $\mu_X=G(\epsilon_{FX})$. This completes the proof.

$\endgroup$
0
$\begingroup$

In fact, the Kleisli star is a partial map ${}^* : \mathrm{Mor}(\mathbf{C}) \times \mathrm{Obj}(\mathbf{C}) \times \mathrm{Obj}(\mathbf{C}) \to \mathrm{Mor}(\mathbf{C})$. So there is no problem!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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