# Naturality in Yoneda's Lemma

Edited (Thanks to Kevin Carlson and Zhen Lin for pointing out the mistakes in my definitions.)

Assuming $C$ is a locally small category, Yoneda lemma says that for any given object $e \in \text{Ob}(C)$ and any functor $F: C \to \text{Set}$, the collection of natural isomorphisms from $\hom_C(e, {-})$ to $F$ is isomorphic to $F(e)$. This isomorphism is natural in $F$ and $e$.

When I try to formulate naturality rigorously, I encounter a problem about size. Here's my attempt.

Define $Y: C^{\text{op}} \to \text{Set}^C$ by $Y(c)(c') = \hom_C(c, c')$ where $\hom_C: C^{\text{op}} \times C \to \text{Set}$ is the $\hom$ bifunctor in $C$.

Define $G: \text{Set}^C \times C \to \text{Set}^C$ by $G(\eta, c) = \hom_{\text{Set}^C}(Y(c), \eta)$ where $\hom_{\text{Set}^C}: (\text{Set}^C)^{\text{op}} \times \text{Set}^C \to \text{Class}$ is the $\hom$ bifunctor in $\text{Set}^C$.

Define $E: \text{Set}^C \times C \to \text{Set}$ by $E(\eta, c) = \eta(c)$. This is the evaluation functor.

Yoneda lemma says that there exists a natural isomorphism from $G$ to $E$. My problem is that I do not know if the codomain of $G$ can be restricted to $\text{Set}$. ($\text{Class}$ is, strictly speaking, not a category, but probably a metacategory?)

My first attempt to fix this is to establish the isomorphism on each object of $\text{Set}^C \times C$ first. This will give smallness of $G(F, e) \cong F(e)$ for $F \in \text{Ob}(\text{Set}^C)$ and $e \in \text{Ob}(C)$. But then, I still have a problem proving local smallness of the image of $G$ on morphisms. Even though I know $G(F, e)$ and $G(F', e')$ are small, I do not know if the image of $G$ on $\hom_{\text{Set}^C \times C}((F, e), (F', e'))$ is small.

-
Why are you using the internal hom? Use the external hom-functor $[\mathcal{C}, \mathbf{Set}]^\mathrm{op} \times [\mathcal{C}, \mathbf{Set}] \to \mathbf{Set}$. (Also, assume $\mathcal{C}$ is small if you want to avoid size issues.) –  Zhen Lin Jun 24 '14 at 21:54
@ZhenLin Thank you. I guess my issue was trying to define the external hom-functor from the internal hom-functor. I cannot really see why the external hom-functor has $\mathbf{Set}$ as the codomain. Is this the consequence of $C$ being locally small? By the way, I don't want to assume that $C$ is small because most sources only assume local smallness. It also seems unnecessary to me, but may be it actually isn't... –  Tunococ Jun 24 '14 at 23:53
$[\mathcal{C}, \mathbf{Set}]$ is locally small if $\mathcal{C}$ is small; otherwise $[\mathcal{C}, \mathbf{Set}$] may not be locally small (exercise). But if you really want to deal with that, use Mac Lane's $\mathbf{Ens}$ device. –  Zhen Lin Jun 25 '14 at 7:17

Naturality in the object argument just says that if $f:A\to A'$ is a morphism in $C$ then the map $f:\text{Nat}(\hom(A,-),F)\to\text{Nat}(\hom(A',-),F)$ sits in a commutative square with $Ff:FA\to FA'$, and similarly for the functor argument. This is really all you need.
But if you want a natural transformation between functors, it must of course be between roughly the functors you describe, but as quickly became apparent your codomains are not correct. There is indeed a hom bifunctor $(\text{Set}^C)^{op}\times \text{Set}^C\to \text{Set}^C$: we have $\hom_{\text{Set}^C}(F,H)(A)=\hom_{\text{Set}}(FA,HA)$. But this bifunctor has nothing to do with the Yoneda lemma-there are no natural transformations in sight! Rather, for the functor you called $G$ you want the assignment $(F,H)\mapsto\text{Nat}(F,H),$ which takes values in sets. Then your problem evaporates.
Your codomain for $\hom_C$ is more problematic still, because in general there's no way at all to make the hom functor take values in $C$: local smallness is exactly the condition that it take values in $\text{Set}$, whereas in general it's not defined as a functor at all.
I'm not sure what you feel you need to check regarding size and morphisms. Once you've established there's only a set of natural transformations between $\hom(A,-)$ and $F$, then $G$ lands in $\text{Set}$ because its image on morphisms consists of functions between fixed sets, which form sets. –  Kevin Carlson Jun 25 '14 at 0:29