Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Applications of the naturality of Yoneda

Ralph Sarkis (Dec 24 2022 at 00:05):

I like to decompose the Yoneda lemma in two parts. First, we prove that $\mathrm{Nat}(H^A,F) \cong F(A)$. Then, we can construct the functor $\mathrm{Nat}(H^-, -)$ and prove the isomorphism above is natural in $A$ and $F$.

I have seen a few applications using the isomorphism, and a few applications of the Yoneda principle (i.e. $H^A \cong H^B \implies A\cong B$) a consequence of that isomorphism, but I don't think I have seen any application that relies on the naturality of the isomorphism. Do you have any examples?

Morgan Rogers (he/him) (Dec 24 2022 at 11:01):

The fact that the Yoneda embedding is a functor relies on this naturality; anything I could propose as an example would probably use that.

Ralph Sarkis (Dec 24 2022 at 13:34):

:thinking: How do you prove naturality without knowing the Yoneda embedding is a functor?
I proved functoriality by recognizing $H^-$ as the currying of $\mathrm{Hom}(-,-)$.

Josselin Poiret (Dec 25 2022 at 09:39):

The naturality basically gives you then fact that "universal elements are natural", which is something that people often use without thinking too much about it. In any case, since you already have a formula for that isomorphism, the naturality isn't really interesting, you could just use the formula directly instead.

Morgan Rogers (he/him) (Dec 26 2022 at 10:27):

The thing I said was confusing because I didn't read what you wrote carefully :upside_down:
I second what @Josselin Poiret said. I don't have any deep applications of naturality for its own sake.

Josselin Poiret (Dec 26 2022 at 15:01):

in general, I think naturality is only interesting as an abstract concept, when it is the only data you have about some family of arrows. As soon as you have a more precise description of that family, with eg. an explicit formula, then it's not interesting anymore. Sure, there is a natural transformation Id → List and List List → List, but that's not interesting per se, it's only interesting in that it lets you plug that in theorems that quantify over "things that have such and such natural transformations".

Ralph Sarkis (Dec 26 2022 at 15:20):

I have stumbled upon several naturality squares where the top path was easier to compute than the bottom path and vice versa. I was hoping that some concrete application used naturality to use one path instead of the other to compute something more easily.