Understanding the maps between $F(A)$ and the natural transformations used in the proof of the Yoneda lemma.

128 Views Asked by At

Understanding the Yoneda lemma maps.

I'm trying to understand the maps between the natural transformations and $F(A)$ in the proof of the Yoneda lemma. I've been struggling for a bit to understand the Yoneda lemma, so I'm trying to understand the mapping construction as a recipe and using that to understand the theorem and gain an intuition for it rather than vice versa.

What, exactly, are the two maps between the natural transformations and $F(A)$ in the proof of the (covariant) Yoneda lemma?


This entry on ProofWiki shows explicit constructions for the maps from $F(A)$ to $\mathrm{Nat}(h_A, F(A))$ and the reverse.

I'm going to change the notation slightly and use a superscript to denote which category an object is in. $x^C$ is an object in the category $C$. $f^{\mathrm{Mor}(C)}$ is an arrow in the category $C$. I will sometimes use a specific set, such as $F(A)$, as an annotation. $x^{F(A)}$ means $x^{\mathrm{Set}}$ and, additionally, $x$ is an element of the set $F(A)$.

The map $\alpha$ goes from $\mathrm{Nat}(h_A, F)$ to $F(A)$. The map is defined as follows.

$$ \alpha \;\;\text{is}\;\; \eta \mapsto \eta_A(\text{id}_A) $$

I am really confused why the RHS is not just $\eta_A$. Since $\eta$ is a natural transformation between functors from $C$ to $\mathrm{Set}$, this would mean that $\eta_A$ is in $\text{Mor}(\mathrm{Set})$. However, $\text{id}_A$ is also in $\text{Mor}(\mathrm{Set})$. I don't know how this construction produces an object in $\mathrm{Set}$.

With type annotations, I think you get

$$ \eta^{\mathrm{Nat}(h_A, F(A))} \mapsto \eta_A^{\mathrm{Mor}(\mathrm{Set})}(\text{id}_A^{\mathrm{Mor}(\mathrm{Set})}) $$

I'm also confused about the $\beta$ map. $\beta$ goes from $F(A)$ to $\mathrm{Nat}(h_A, F)$.

Here is what $\beta$ looks like with type annotations on parameters alone and the ultimate RHS. I inferred the types myself, but the overall expression is similar to the presentation on ProofWiki.

$$ u^{F(A)} \mapsto x^C \mapsto f^{\mathrm{Mor}(C)} \mapsto (Ff)(u)^{\mathrm{Set}} $$

I'm also confused by this expression. A given, specific natural transformation $\eta$ can be though of as a map from $C$ to $\mathrm{Mor}(\mathrm{Set})$, i.e. it associates morphisms in the target category to objects in the source category.

Given this, it's hard for me to see why we don't end up with something of the following form for $\beta$, i.e. we're given an element of $F(A)$, and our map $\beta$ kicks out the component map of a natural transformation.

$$ u^{F(A)} \mapsto x^C \mapsto (\cdots)^{\mathrm{Mor}(\mathrm{Set})} $$

So, what exactly are the maps between $F(A)$ and the natural transformations used in the proof of the Yoneda lemma? I'm having a hard time finding the proof presented in a substantially different way (or a more elementary way) from what ProofWiki does. For example, the proof on Wikipedia seems broadly similar in terms of the explicit construction, which makes me think I'm missing something big/obvious.

2

There are 2 best solutions below

0
On
  • No, $\eta$ is a natural transformation between $h^A : C \to \textsf{Set}$ and $F : C \to \textsf{Set}$, so for each object $X$ in $C$ we have the component $\eta_X : h^A(X) \to F(X)$, which is a morphism in $\textsf{Set}$. In particular, $\eta_A : h^A(A) \to F(A)$ maps $\operatorname{id}_A \in h^A(A)$ to an element of the set $F(A)$.
  • Now, fix an element $u$ of the set $F(A)$. We want to define a natural transformation $\beta(u)$ between $h^A : C \to \textsf{Set}$ and $F : C \to \textsf{Set}$, so for each object $X$ in $C$ we want to define a morphism $$\beta(u)_X : h^A(X) \to F(X)$$ in $\textsf{Set}$. The natural way is by mapping $f \in h^A(X)$ (which is a morphism $A \to X$ in $C$) to the value of $F(f) : F(A) \to F(X)$ at $u$, in other words $\beta(u)_X$ maps $f \in h^A(X)$ to $F(f)(u)$.
    Thus $\beta(u)_X$ is "$f \mapsto F(f)(u)$", and $\beta(u)$ is "$X \mapsto (f \mapsto F(f)(u))$".
0
On

Note that since $\eta$ is a natural transformation from $h^A $ to $F$, by definition $\eta_A$ is a function (i.e. an arrow in $\mathsf{Set}$)

$$\eta_A \colon \hom_C(A,A) = h^A(A) \to F(A).$$

In particular, the indentity of $1_A \colon A \to A$ of $A$ is an element of the domain of $\eta_A$, and it makes sense to compute $\eta_A(1_A)$.

Now consider any other object $B$ in $C$. The natural transformation $\eta$ gives you a map $\eta_B \colon \hom_C(A,B) \to F(B)$.

Suppose we want to compute $\eta_B(f)$ where $f \colon A \to B$ is some arrow. Observe that by functoriality $f$ defines a map $f_\ast \colon g \in \hom_C(A,A) \mapsto fg\in \hom_C(A,B)$ and $f$ is nothing else but $f_*(1_A) = f1_A$.

Our question boils down to computing $\eta_B(f) = (\eta_B \circ f_\ast) (1_A)$. By naturality of $\eta$,

$$\eta_B(f) = (\eta_B \circ f_\ast) (1_A) = (F(f) \circ \eta_A)(1_A) = F(f)(\eta_A(1_A)). \tag{$\star$}$$

Hence all expressions $\eta_B(f)$ for any $B \in C$ and $f \colon A \to B$ are determined by (the morphism $f$ given and) $\eta_A(1_A)$.

In other words, $\eta_A$ is characterized completely by $\eta_A(1_A)$ (if you look carefully, this is a proof of injectivity).

To show that the assignment $\eta \mapsto \eta_A(1_A)$ is surjective, we shall pick $x \in F(A)$ and (try to) produce $\eta$ such that $\eta_A(1_A) = x$. Observe that $(\star)$ forces us to have

$$\eta_B(f) = F(f)(x) \qquad (B \in C, f \in \hom_C(A,B)).$$

You can check that this is in fact a natural transformation, completing the proof. Note also that the surjectivity proof is a restatement of the fact that the inverse mapping is well defined.

Finally, to respond to your last question:

A given, specific natural transformation $\eta$ can be though of as a map from $C$ to $\mathsf{Mor(Set)}$.

And indeed, that is what we are doing: to each $X \in C$ we associate a map $\eta_X \colon \hom(A,X) \to F(X)$ which is a function between sets.

To define $\eta_X$ we shall say what is the image of a given morphism $f \colon A \to X$ of the domain set is. We decree $f \mapsto F(f)(x)$.