Yoneda lemma

Let be a locally small category. For every object and every Presheaf we have

よ

where $よ$ is the Yoneda embedding. Moreover, this bijection is a natural isomorphism in and

よ

where naturality in means for

500|c

commutes; and naturality in means for 500|c

commutes.¹

Proof

For $よ$ we have . Let .

Conversely, given an , we can define $よ$ as follows: Given any , we define the component

whose naturality condition is given by the diagram

Now for we have

so is indeed natural.

Now we calculate for $よ$ . From the above definitions, for we have

but by naturality of

wherefore .

Conversely, for we have

Therefore

よ

defines a bijection for any .

For naturality in , suppose Then for any $よ$ we have

よ

so the required diagram commutes.

For naturality in , suppose . Then for $よ$ we have

よ よ よ よ よ

as required.

Corollaries

#state/tidy | #lang/en | #SemBr