jwbuurlage / category-theory-programmers

Category theory in the context of (functional) programming
MIT License
513 stars 38 forks source link

Yoneda lemma diagrams #7

Closed jmgimeno closed 7 years ago

jmgimeno commented 7 years ago

The diagram in page 40 which relates the components of Yf at c and d, shouldn't have the "columns" reversed?

I mean, Yf goes from h^b to h^a so its component at c should go from Hom(b, c) to Hom(a, c).

And, in the same figure, shouldn't be the vertical arrows be h^a(k^op) and h^b(k^op) ? Because the functors h^a and h^a are covariant hom-functors.

In page 41 the diagram, I think, is also wrong. If g goes from b to a, g^op goes from a to b, so Y(g^op) at c, should go grom Hom(b, c) to Hom(a,c). Now the vertical arrows are rightly labelled as h^a(k) because now k goes from c to d.

jwbuurlage commented 7 years ago

The diagram in page 40 which relates the components of Yf at c and d, shouldn't have the "columns" reversed? I mean, Yf goes from h^b to h^a so its component at c should go from Hom(b, c) to Hom(a, c).

I think the confusing part is that I did not go back far enough to explicitely denote opposite arrows everywhere. It is very common in the literature to never speak about them explicitely but let the context define 'where they live'. I have now fixed it so that it explicitely considers f^op there too, and then reversed the columns.

And, in the same figure, shouldn't be the vertical arrows be h^a(k^op) and h^b(k^op) ? Because the functors h^a and h^a are covariant hom-functors.

No, k: c -> d is simply an arrow in the normal category C, since h^a is covariant. I wrote a misleading sentence above ('note the reversed order'), but I was describing k^op there.

In page 41 the diagram, I think, is also wrong. If g goes from b to a, g^op goes from a to b, so Y(g^op) at c, should go grom Hom(b, c) to Hom(a,c).

Here the diagram is right. If g^op goes from a to b, then Y(g^op)_c should go from Hom(a, c) to Hom(b, c). Here it is reversed because I defined g to go from b -> a, which is reversed w.r.t. to the f in the diagram on the previous page.

Please let me know if this solves the confusion!

JW

jmgimeno commented 7 years ago

Yes. Now it's much clearer (at least for me).

Thanks!!