Rephrasing the Yoneda lemma using the Yoneda embedding

category-theoryyoneda-lemma

The usual way that I see the Yoneda lemma stated is as something like
$$\text{Nat}(\text{Hom}(-,X),F) \cong F(X) \,,$$
where $F: \mathcal{C} \to \text{Set}$ is a functor and $X$ is an object of $\mathcal{C}$. If we let $\text{Yo}: \mathcal{C} \to \text{Set}^{\mathcal{C}^\text{op}}$ be the Yoneda embedding, we can rewrite this as
$$\text{Nat}(\text{Yo}(X),F) \cong F(X) \,,$$
which is a bit more concise in my opinion. However, I recently thought of cutting this down further using the Yoneda embedding from the functor category $\text{Fun}(\mathcal{C}^{\text{op}},\text{Set})$ to $\text{Set}^{{\text{Fun}(\mathcal{C}^{\text{op}},\text{Set})}^\text{op}}$, to get something like
$$\text{Yo}(F)(\text{Yo}(X)) \cong F(X) \,.$$
Here, I'm using $\text{Yo}$ to denote two different Yoneda embeddings. If this is a valid rephrasing, then I really like this version, since now both sides look like functor application. It appears to tell us something about how the Yoneda embedding is compatible with evaluation of functors on objects. However, I don't think I've seen this equation before; is there something wrong with this logic, or is it just not generally considered a useful way to write this lemma?

Best Answer

$\newcommand{\yo}{\mathsf{Yo}}$I don't like $\yo(F)\yo(X)\cong F(X)$. It's correct, but I think we should call a Hom a Hom when we see one. What I do like, because it is what I had to come up with to correctly formulate a version of the enriched Yoneda lemma, is the following similar thing which still captures the "application of functors on both sides":

For any small category $\mathsf{C}$ there is a canonical natural isomorphism of functors between: $$\large\mathsf{eval}:\mathsf{C}\times\mathsf{Set}^{\mathsf{C}}\to\mathsf{Set}$$And: $$\large\mathsf{C}\times\mathsf{Set}^{\mathsf{C}}\overset{\yo^{\mathsf{op}}\times1}{\longrightarrow}\left(\mathsf{Set}^{\mathsf{C}}\right)^{\mathsf{op}}\times\mathsf{Set}^{\mathsf{C}}\overset{\mathsf{Hom}_{\mathsf{Set}^{\mathsf{C}}}}{\longrightarrow}\mathsf{Set}$$

This is genuinely natural in both variables, which is of great importance but is not often explicitly mentioned. It holds if you replace the category of sets with another suitable base of enrichment and if you interpret functor categories in the "correct" way.

Related Question