# 9.5 The Yoneda lemma

Recall that we have a category $\mathcal{S}et$ whose objects are sets and whose morphisms are functions. We now show that every precategory has a $\mathcal{S}et$-valued hom-functor. First we need to define opposites and products of (pre)categories.

###### Definition 9.5.1.

For a precategory $A$, its opposite $A^{\mathrm{op}}$ is a precategory with the same type of objects, with $\hom_{A^{\mathrm{op}}}(a,b):\!\!\equiv\hom_{A}(b,a)$, and with identities and composition inherited from $A$.

###### Definition 9.5.2.

For precategories $A$ and $B$, their product $A\times B$ is a precategory with $(A\times B)_{0}:\!\!\equiv A_{0}\times B_{0}$ and

 $\hom_{A\times B}((a,b),(a^{\prime},b^{\prime})):\!\!\equiv\hom_{A}(a,a^{\prime% })\times\hom_{B}(b,b^{\prime}).$

Identities are defined by $1_{(a,b)}:\!\!\equiv(1_{a},1_{b})$ and composition by $(g,g^{\prime})(f,f^{\prime}):\!\!\equiv((gf),(g^{\prime}f^{\prime})).$

###### Lemma 9.5.3.

For precategories $A,B,C$, the following types are equivalent.

1. 1.

$A\times B\to C$.

2. 2.

Functors $A\to C^{B}$.

###### Proof.

Given $F:A\times B\to C$, for any $a:A$ we obviously have a functor $F_{a}:B\to C$. This gives a function $A_{0}\to(C^{B})_{0}$. Next, for any $f:\hom_{A}(a,a^{\prime})$, we have for any $b:B$ the morphism $F_{(a,b),(a^{\prime},b)}(f,1_{b}):F_{a}(b)\to F_{a^{\prime}}(b)$. These are the components of a natural transformation $F_{a}\to F_{a^{\prime}}$. Functoriality in $a$ is easy to check, so we have a functor $\hat{F}:A\to C^{B}$.

Conversely, suppose given $G:A\to C^{B}$. Then for any $a:A$ and $b:B$ we have the object $G(a)(b):C$, giving a function $A_{0}\times B_{0}\to C_{0}$. And for $f:\hom_{A}(a,a^{\prime})$ and $g:\hom_{B}(b,b^{\prime})$, we have the morphism

 $G(a^{\prime})_{b,b^{\prime}}(g)\circ G_{a,a^{\prime}}(f)_{b}=G_{a,a^{\prime}}(% f)_{b^{\prime}}\circ G(a)_{b,b^{\prime}}(g)$

in $\hom_{C}(G(a)(b),G(a^{\prime})(b^{\prime}))$. Functoriality is again easy to check, so we have a functor $\check{G}:A\times B\to C$.

Finally, it is also clear that these operations are inverses. ∎

Now for any precategory $A$, we have a hom-functor

 $\hom_{A}:A^{\mathrm{op}}\times A\to\mathcal{S}et.$

It takes a pair $(a,b):(A^{\mathrm{op}})_{0}\times A_{0}\equiv A_{0}\times A_{0}$ to the set $\hom_{A}(a,b)$. For a morphism $(f,f^{\prime}):\hom_{A^{\mathrm{op}}\times A}((a,b),(a^{\prime},b^{\prime}))$, by definition we have $f:\hom_{A}(a^{\prime},a)$ and $f^{\prime}:\hom_{A}(b,b^{\prime})$, so we can define

 $\displaystyle(\hom_{A})_{(a,b),(a^{\prime},b^{\prime})}(f,f^{\prime})$ $\displaystyle:\!\!\equiv(g\mapsto(f^{\prime}gf))$ $\displaystyle:\hom_{A}(a,b)\to\hom_{A}(a^{\prime},b^{\prime}).$

Functoriality is easy to check.

By \autorefct:functorexpadj, therefore, we have an induced functor $\mathbf{y}:A\to\mathcal{S}et^{A^{\mathrm{op}}}$, which we call the Yoneda embedding.

###### Theorem 9.5.4 (The Yoneda lemma).

For any precategory $A$, any $a:A$, and any functor $F:\mathcal{S}et^{A^{\mathrm{op}}}$, we have an isomorphism

 $\hom_{\mathcal{S}et^{A^{\mathrm{op}}}}(\mathbf{y}a,F)\cong Fa.$ (9.5.4)

Moreover, this is natural in both $a$ and $F$.

###### Proof.

Given a natural transformation $\alpha:\mathbf{y}a\to F$, we can consider the component $\alpha_{a}:\mathbf{y}a(a)\to Fa$. Since $\mathbf{y}a(a)\equiv\hom_{A}(a,a)$, we have $1_{a}:\mathbf{y}a(a)$, so that $\alpha_{a}(1_{a}):Fa$. This gives a function $(\alpha\mapsto\alpha_{a}(1_{a}))$ from left to right in (9.5.4).

In the other direction, given $x:Fa$, we define $\alpha:\mathbf{y}a\to F$ by

 $\alpha_{a^{\prime}}(f):\!\!\equiv F_{a^{\prime},a}(f)(x).$

Naturality is easy to check, so this gives a function from right to left in (9.5.4).

To show that these are inverses, first suppose given $x:Fa$. Then with $\alpha$ defined as above, we have $\alpha_{a}(1_{a})=F_{a,a}(1_{a})(x)=1_{Fa}(x)=x$. On the other hand, if we suppose given $\alpha:\mathbf{y}a\to F$ and define $x$ as above, then for any $f:\hom_{A}(a^{\prime},a)$ we have

 $\displaystyle\alpha_{a^{\prime}}(f)$ $\displaystyle=\alpha_{a^{\prime}}(\mathbf{y}a_{a^{\prime},a}(f))$ $\displaystyle=(\alpha_{a^{\prime}}\circ\mathbf{y}a_{a^{\prime},a}(f))(1_{a})$ $\displaystyle=(F_{a^{\prime},a}(f)\circ\alpha_{a})(1_{a})$ $\displaystyle=F_{a^{\prime},a}(f)(\alpha_{a}(1_{a}))$ $\displaystyle=F_{a^{\prime},a}(f)(x).$

Thus, both composites are equal to identities. We leave the proof of naturality to the reader. ∎

###### Corollary 9.5.6.

The Yoneda embedding $\mathbf{y}:A\to\mathcal{S}et^{A^{\mathrm{op}}}$ is fully faithful.

###### Proof.

By \autorefct:yoneda, we have

 $\hom_{\mathcal{S}et^{A^{\mathrm{op}}}}(\mathbf{y}a,\mathbf{y}b)\cong\mathbf{y}% b(a)\equiv\hom_{A}(a,b).$

It is easy to check that this isomorphism is in fact the action of $\mathbf{y}$ on hom-sets. ∎

###### Corollary 9.5.7.

If $A$ is a category, then $\mathbf{y}_{0}:A_{0}\to(\mathcal{S}et^{A^{\mathrm{op}}})_{0}$ is an embedding. In particular, if $\mathbf{y}a=\mathbf{y}b$, then $a=b$.

###### Proof.

By \autorefct:yoneda-embedding, $\mathbf{y}$ induces an isomorphism on sets of isomorphisms. But as $A$ and $\mathcal{S}et^{A^{\mathrm{op}}}$ are categories and $\mathbf{y}$ is a functor, this is equivalently an isomorphism on identity types, which is the definition of being an embedding. ∎

###### Definition 9.5.8.

A functor $F:\mathcal{S}et^{A^{\mathrm{op}}}$ is said to be representable if there exists $a:A$ and an isomorphism $\mathbf{y}a\cong F$.

###### Theorem 9.5.9.

If $A$ is a category, then the type “$F$ is representable” is a mere proposition.

###### Proof.

By definition “$F$ is representable” is just the fiber of $\mathbf{y}_{0}$ over $F$. Since $\mathbf{y}_{0}$ is an embedding by \autorefct:yoneda-mono, this fiber is a mere proposition. ∎

In particular, in a category, any two representations of the same functor are equal. We can use this to give a different proof of \autorefct:adjprop. First we give a characterization of adjunctions in terms of representability.

###### Lemma 9.5.10.

For any precategories $A$ and $B$ and a functor $F:A\to B$, the following types are equivalent.

1. 1.

$F$ is a left adjoint.

2. 2.

For each $b:B$, the functor $(a\mapsto\hom_{B}(Fa,b))$ from $A^{\mathrm{op}}$ to $\mathcal{S}et$ is representable.

###### Proof.

An element of the type 2 consists of a function $G_{0}:B_{0}\to A_{0}$ together with, for every $a:A$ and $b:B$ an isomorphism

 $\gamma_{a,b}:\hom_{B}(Fa,b)\cong\hom_{A}(a,G_{0}b)$

such that $\gamma_{a,b}(g\circ Ff)=\gamma_{a^{\prime},b}(g)\circ f$ for $f:\hom_{A}(a,a^{\prime})$.

Given this, for $a:A$ we define $\eta_{a}:\!\!\equiv\gamma_{a,Fa}(1_{Fa})$, and for $b:B$ we define $\epsilon_{b}:\!\!\equiv{(\gamma_{Gb,b})}^{-1}(1_{Gb})$. Now for $g:\hom_{B}(b,b^{\prime})$ we define

 $G_{b,b^{\prime}}(g):\!\!\equiv\gamma_{Gb,b^{\prime}}(g\circ\epsilon_{b})$

The verifications that $G$ is a functor and $\eta$ and $\epsilon$ are natural transformations satisfying the triangle identities are exactly as in the classical case, and as they are all mere propositions we will not care about their values. Thus, we have a function 2$\to$1.

In the other direction, if $F$ is a left adjoint, we of course have $G_{0}$ specified, and we can take $\gamma_{a,b}$ to be the composite

 $\hom_{B}(Fa,b)\xrightarrow{G_{Fa,b}}\hom_{A}(GFa,Gb)\xrightarrow{(\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}\circ\eta_{a})}\hom_{A}(a,Gb).$

This is clearly natural since $\eta$ is, and it has an inverse given by

 $\hom_{A}(a,Gb)\xrightarrow{F_{a,Gb}}\hom_{B}(Fa,FGb)\xrightarrow{(\epsilon_{b}% \circ\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}\hom_{A}(Fa,b)$

(by the triangle identities). Thus we also have 1$\to$ 2.

For the composite 2$\to$1$\to$ 2, clearly the function $G_{0}$ is preserved, so it suffices to check that we get back $\gamma$. But the new $\gamma$ is defined to take $f:\hom_{B}(Fa,b)$ to

 $\displaystyle G(f)\circ\eta_{a}$ $\displaystyle\equiv\gamma_{GFa,b}(f\circ\epsilon_{Fa})\circ\eta_{a}$ $\displaystyle=\gamma_{GFa,b}(f\circ\epsilon_{Fa}\circ F\eta_{a})$ $\displaystyle=\gamma_{GFa,b}(f)$

so it agrees with the old one.

Finally, for 1$\to$2$\to$ 1, we certainly get back the functor $G$ on objects. The new $G_{b,b^{\prime}}:\hom_{B}(b,b^{\prime})\to\hom_{A}(Gb,Gb^{\prime})$ is defined to take $g$ to

 $\displaystyle\gamma_{Gb,b^{\prime}}(g\circ\epsilon_{b})$ $\displaystyle\equiv G(g\circ\epsilon_{b})\circ\eta_{Gb}$ $\displaystyle=G(g)\circ G\epsilon_{b}\circ\eta_{Gb}$ $\displaystyle=G(g)$

so it agrees with the old one. The new $\eta_{a}$ is defined to be $\gamma_{a,Fa}(1_{Fa})\equiv G(1_{Fa})\circ\eta_{a}$, so it equals the old $\eta_{a}$. And finally, the new $\epsilon_{b}$ is defined to be ${(\gamma_{Gb,b})}^{-1}(1_{Gb})\equiv\epsilon_{b}\circ F(1_{Gb})$, which also equals the old $\epsilon_{b}$. ∎

###### Corollary 9.5.11.

[\autorefct:adjprop] If $A$ is a category and $F:A\to B$, then the type “$F$ is a left adjoint” is a mere proposition.

###### Proof.

By \autorefct:representable-prop, if $A$ is a category then the type in \autorefct:adj-repr2 is a mere proposition. ∎

Title 9.5 The Yoneda lemma
\metatable