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$.

  • 1
    $\begingroup$ Why can I assume that $T=T^A$ for some $A \in FX$ ? $\endgroup$ – Tomais Mar 20 '18 at 2:11
  • $\begingroup$ $T=T^A$ is just how I'm defining the variable $T$. $\endgroup$ – Eric Wofsey Mar 20 '18 at 3:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.