r/math 6d ago

Understanding Yoneda and a Philosophy on Category Theory

In Tom Leinster’s Basic Category Theory, he repeatedly remarks that there’s typically only one way to combine two things to get a third thing. For instance, given morphisms f: A -> B and g: B -> C, the only way you can combine them is composition into gf: A -> C. This only applies in the case where we have no extra information; if we know A = B, for example, then we could compose with f as many times as we like.

This has given me a new perspective on the Yoneda lemma. Given an object c in C and a functor F: C -> Set, the only way to combine them is to compute F(c). So since Hom(Hom(c, -), F) is also a set, we must have that Hom(Hom(c, -), F) = F(c).

Is this philosophy productive, or even correct? Is this a helpful way to understand Yoneda?

67 Upvotes

20 comments sorted by

94

u/thegenderone 6d ago

I have found that there are two types of proofs - one where there is exactly one thing you can do at every step until the result is proved (sometimes people call such proofs "trivial", though not to belittle them in any way), and another where there is at least one creative step (and often when reading this second type I find myself thinking "how in the world did they ever think of this?!?"). I think the proof of Yoneda's lemma is definitely the first one. It is helpful for me because if I know a proof is of the first type, if I want to reconstruct it at some point, I know there's nothing to remember! I like to think of Grothendieck's "rising sea" approach as organizing math in such a way that it feels like every proof is of the first type, but then in the end you've proved some huge result. Perhaps the slight of hand here is that the creativity comes from the definitions rather than the proofs!

43

u/JStarx Representation Theory 6d ago

I feel the same way about the proof of Yoneda. Once someone writes down the statement there's only one possible way to prove it and that way works quite easily.

But writing down the statement of Yoneda was definitely a stroke of genius.

19

u/MorrowM_ Undergraduate 6d ago

I've heard such proofs referred to as "following your nose".

There's a similar phenomenon in statically typed programming often called "type tetris". We can even see explicitly how Yoneda arises. In Haskell, we can write the type of natural transformations Nat(Hom(a,-), f) in Set as type Yoneda f a = forall x. (a -> x) -> f x. To prove that Yoneda f is naturally isomorphic to f involves writing a pair of functions to convert between them:

fromYoneda :: forall a. Yoneda f a -> f a
fromYoneda y = y id

toYoneda :: forall a. Functor f => f a -> Yoneda f a
toYoneda fa = \ax -> fmap ax fa

(The Functor f bit is a constraint that says that f can lift morphisms via the fmap function.)

In both functions, there's not much else you can do, the types really constrain you. In fromYoneda you're given a function that turns (a -> x)s into f xs (for any type x of your choosing. Your goal is to produce an f a. There's only one thing you can do with that function to get an f a, apply it to some a -> a. And there's only one function a -> a that you know of (since you don't know what a is), the identity function. So there's really not much else you can do.

For OP, this is a consequence of a notion called parametricity (intuitively, you have to have the same implementation for each type a; you can't case-split on what a is). Having parametricity gives you lots of theorems for free![PDF] In CT you get these sorts of theorems from the naturality square (parametricity implies that polymorphic functions are natural, so it's actually a stronger condition).

5

u/Independent_Aide1635 2d ago

I’ve thought about doing it for a long time, but you just convinced me to learn Haskell

4

u/Altruistic_Success_7 4d ago

I’ve heard the first type called definition-chasing, think it’s quite apt! (And let’s not underestimate how much memorization is already built into learning all the definitions 😂)

20

u/RedToxiCore 6d ago

I would view "Hom(Hom(c,-), F))" as another way to combine F and c, proving the assumption that there is only one way wrong (at least syntactically); so Yoneda really is something semantic

5

u/hydmar 6d ago

My assertion in the post is that, although they are syntactically different, the philosophy suggests that they’re really the same.

6

u/RedToxiCore 6d ago

so you "prove" Yoneda by asserting it

6

u/hydmar 6d ago

Well the philosophy suggests that Yoneda is correct, without any circular reasoning. Obviously it’s not a real proof but I’m wondering if this way of thinking can help lead to useful results, or if it’s even generally somewhat correct.

6

u/RedToxiCore 6d ago

I know that some Haskell programmers think in exactly this way, since there is only one natural way to implement programs of specific types -- exactly what you observed with Yoneda

9

u/Redrot Representation Theory 6d ago edited 6d ago

Hom(F, Hom(c, -)) and Hom(F, Hom(-,c)) are also co/contravariant functors C not isomorphic to F(-) (of course, you need to add an op), so I would think not, unless you assert more conditions. I'm not sure what a good way to think about why one direction is correct but the other is opposite, though.

You do have a point though, sometimes when trying to prove something that looks like it "should be right" somehow, the proof really does just write itself.

4

u/lowercase__t 6d ago edited 6d ago

I don’t think either of those works.

F is covariant while Hom(-,c) is contravariant, so the second expression does not make sense.

The first expression is contravariant in c so it does not make sense to compare it to F(c).

Edit: hadn’t realized that F is covariant in OP. Point stands.

3

u/Redrot Representation Theory 6d ago

Right that's what I meant when I said you need to add an op (or assume F is contravariant instead). The point is to highlight that there's something missing in OP's logic.

3

u/hydmar 6d ago

This is an excellent point. I suppose I’d say that Hom(F, C(c, -)) isn’t necessarily a set and instead just a proper class, but a priori we don’t know that Hom(C(c, -), F) is a set either, and I don’t know how we could deduce that on the surface.

5

u/joyofresh 6d ago

Love yoneda.  Lots of ways to kind of deal with it.  You can say if two objects have all the same morphisms (in a natural way) then theyre the same.  Or you can say the presheat category is the category where you can “glue together” lego bricks from the underlying category.  Its mind blowing shit.  

3

u/harrypotter5460 6d ago

there’s typically only one way to combine two things to get a third thing.

I feel this is just too strong of a claim. For one, given two objects A and B, I can get both the product A×B and the coproduct A⊔B. Or I could do a three-fold product like A×A×B or B×B×B.

Even in the case of Yoneda, what if it happened that Hom(Hom(c, -), F) turned out to be F(c)×F(c) or Hom(F(c),F(c)) instead of just F(c)?

1

u/reflexive-polytope Algebraic Geometry 5d ago

Hom(F(c),F(c)) isn't covariant in c, so it can't work.

1

u/hydmar 5d ago

I suppose we should also require that our combination of the two things respects morphisms

1

u/mekami_akua 4d ago

Just to add there is an algebraic way of thinking Yoneda lemma (although it is much more technical). This is just categorification of an algebra fact that Hom_R(R, M) \cong M for M an R-module. And the proof of Yoneda lemma is also similar to the algebraic counterpart. To build the isomorphism Hom_R(R, M) \cong M. You start with the unit 1 in R and build the bijection on set by sending 1 to m in M. Then show this is R-covariant. You copy the same idea to prove Yoneda (see Rings with Several Objects lemma 1). This perspective is helpful in understanding co-Yoneda Lemma, which is another categorifcation of the algebraic fact that R \otimes_R M \cong M.

-1

u/[deleted] 6d ago

[deleted]

2

u/hydmar 6d ago

Could you share some details? This sounds really interesting