Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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!

share|improve this question
2  
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." –  Mike Shulman May 26 '10 at 0:56
    
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! –  user6082 May 26 '10 at 10:08
    
You could just define the morphisms to be triples $(A, B, f : A \to TB)$. Then you would know which $B$ to choose. –  Neel Krishnaswami May 26 '10 at 11:27
    
I was thinking about this, but that's a different category, isn't it? –  user6082 May 26 '10 at 11:32
1  
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.) –  Neel Krishnaswami May 26 '10 at 11:33
show 1 more comment

3 Answers 3

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

share|improve this answer
    
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. –  user6082 May 26 '10 at 12:56
add comment

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.

share|improve this answer
add comment
up vote 0 down vote accepted

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!

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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