Wikipedia:Reference desk/Archives/Mathematics/2019 July 6

Mathematics desk
< July 5 << Jun | July | Aug >> Current desk >
Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.


July 6

edit

Describe the Kleisli category of the power-set monad as the category of "sets and relations"

edit

This is left as an exercise in the book Abstract and Concrete Categories and in other references, I've passed by. I would like to have access to a complete proof for understanding it completely as I have made some advancements:

  • The category of sets and relations has sets as objects and relations as morphisms.
  • Functions in the category Set can be described as binary relations.
  • The power-set monad is a monad in Set that has as the unit the morphism that takes an element to a set with it and as the multiplication the union operation in sets.
  • The Kleisli category on the power-set monad is then the category that its objects are sets and morphisms are the equivalent morphisms (those that have the target as the power set).

I couldn't connect those two categories and see how they are equal or even equivalent.Zorkedon (talk) 20:36, 6 July 2019 (UTC)[reply]

(I corrected the link, just so you know.) --RDBury (talk) 21:24, 7 July 2019 (UTC)[reply]
@Zorkedon: Okay, so I think you're basically there. The key thing to note is just that a relation   is the same thing as a function   where   which in turn is a morphism   in the Kleisli category. There are still a couple thing to check with respect to this identification: that the identity relation corresponds to the identity morphism in the Kleisli category (easy), and that composition of relations corresponds to composition of morphisms in the Kleisli category (less easy, but still straightforward). Hope this helps, –Deacon Vorbis (carbon • videos) 02:52, 8 July 2019 (UTC)[reply]
I'm not sure if anyone's still watching this, but I looked back here and realized that I was maybe a bit too quick. What I described above was a functor   (category of sets and relations to the Kleisli category of the power set monad), and then verifying that it's actually a functor. To really be complete, you should also give an inverse functor (and again verify that it's actually a functor) (and verify that both compositions are the identity). But if you can follow the first part, hopefully this should follow without too much more trouble. –Deacon Vorbis (carbon • videos) 14:49, 9 July 2019 (UTC)[reply]
@Deacon Vorbis: First of all: in the category  , the composition of morphisms (functions with target the power-set) should be defined by   as in the definition of the Kleisli category, with   as the union operation understood as a function, how would that be? I can see that in your interpretation of the functor  , the identity   is the   of the power-set monad, and for the proof of composition, one could construct binary relations   and   and their respective functions from the functor   and  , and the composite relation   and it's functor equivalent  . But how can I prove that  ? Zorkedon (talk) 21:33, 9 July 2019 (UTC)[reply]

@Zorkedon: To make the notation a bit easier, for a relation   define   Then, for  

 

So, an element   is in the ultimate image if it's in   for some   but that's exactly the same thing as saying that there's some   such that   and   which in turn is exactly what it means to say that  Deacon Vorbis (carbon • videos) 14:32, 10 July 2019 (UTC)[reply]

@Deacon Vorbis: Ok, I understand the relation of functions with relations, but the union function should be defined as: for some   its   and  , and then the union would take out the brackets, and thus sending a set of sets to its respective set? (  ) Zorkedon (talk) 15:29, 10 July 2019 (UTC)[reply]
Quick side note: you left out one element from   namely   But anyway, maybe a better example for the union would be a bigger set, say   Then for example, one element   might be   Then
 
Deacon Vorbis (carbon • videos) 23:54, 10 July 2019 (UTC)[reply]
But just to verify, in the case of   you mentioned, yes; in fact,   would send both   and   to   while it would send   and   to  Deacon Vorbis (carbon • videos) 00:13, 11 July 2019 (UTC)[reply]