# The famous Yoneda lemma

First the ingredients for the lemma.

We will denote by $[C, Sets]$ the category of contravariant functors where objects are contravariant functors of the form $F: C \rightarrow {Sets}$ and the arrows are natural transformations of contravariant functors in that way.

We define the functor $h: C\rightarrow [C, Sets]$ as follows:

In objects: For each $X \in {C}$ we define an object $h_X$ of $[C, Sets]$ as follows: \begin{align}h_X: C \rightarrow {Sets}: & U \mapsto h_X (U) = Mor_C (U, X)\\ & s:U \rightarrow V \,\mapsto h_Xs:h_XV \rightarrow{h_XU}\end{align}

such that $h_Xs (t) = t \circ {s}$, $t: V \rightarrow{X}$, defined thus $h_X$ is a contravariant functor.

In arrows: For each $f: X \rightarrow {Y}$ we define a natural transformation $h_f: h_X \rightarrow {h_Y}$ it's easy to see what it is natural transformation.

Let $F: C \rightarrow {Sets}$ a contravariant functor, denoted by $Mor (h_X, F)$ the set of natural transformations $T: h_X \Rightarrow {F}$.

We define the application $L: FX \rightarrow {Mor (h_X, F)}$ as:

Given a $A \in {FX}$ we can define $T ^ A: h_X \rightarrow {F}$ as follows: given $U \in {C}$, an element of $h_XU = Mor (U, X)$ is an arrow $f: U \rightarrow{X}$, this arrow induces the application $Ff: FX \rightarrow {FU}$. We define an application $T ^ A_U: h_XU \rightarrow {FU}$ by $T ^ A_U (f) = Ff(A)$.

Thus defined $T ^ A$ is a natural transformation.

Yoneda Lemma : Be $C$ a category, $F: C \rightarrow {Sets}$ a contravariant functor and $X \in {C}$.

Then the $L: FX \longrightarrow {Mor (h_X, F)}$ application defined above is bijective.

Proof :

Let $T: h_X \rightarrow {F}$ and suppose that $T = T ^ A$ for some $A \in {FX}$. So $$T_X (1_X) = T ^ A_X (1_X) = F1_XA = 1_ {FX} A = A.$$ This proves the injectivity of $L$.

I do not understand why that means he's injective.

Thank you

Well, suppose $T^A=T^B$ for two elements $A,B\in FX$. Then if $T=T^A=T^B$, we have $T_X(1_X)=A$ and also $T_X(1_X)=B$, so $A=B$.
• Why can I assume that $T=T^A$ for some $A \in FX$ ? – Tomais Mar 20 '18 at 2:11
• $T=T^A$ is just how I'm defining the variable $T$. – Eric Wofsey Mar 20 '18 at 3:07