9.5 The Yoneda lemma

Recall that we have a category $𝒮et$ whose objects are sets and whose morphisms are functions. We now show that every precategory has a $𝒮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 ${\mathrm{hom}}_{A^{\mathrm{op}}}\mathrm{(}a\mathrm{,}b\mathrm{)}\mathrm{:}\mathrm{\equiv }{\mathrm{hom}}_A\mathrm{(}b\mathrm{,}a\mathrm{)}$, and with identities and composition inherited from $A$.

Definition 9.5.2.

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

$${\mathrm{hom}}_{A\times B}((a,b),(a^{\prime },b^{\prime })):\equiv {\mathrm{hom}}_A(a,a^{\prime })\times {\mathrm{hom}}_B(b,b^{\prime }).$$

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

Lemma 9.5.3.

For precategories $A\mathrm{,}B\mathrm{,}C$, the following types are equivalent.

1. Functors $A\times B\to C$.

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:{\mathrm{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 $\widehat{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:{\mathrm{hom}}_A(a,a^{\prime })$ and $g:{\mathrm{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 ${\mathrm{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

$${\mathrm{hom}}_A:A^{\mathrm{op}}\times A\to 𝒮et.$$

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

${({\mathrm{hom}}_A)}_{(a,b),(a^{\prime },b^{\prime })}(f,f^{\prime })$ $:\equiv (g\mapsto (f^{\prime }gf))$

$:{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_A(a^{\prime },b^{\prime }).$

Functoriality is easy to check.

By ct:functorexpadj, therefore, we have an induced functor $𝐲:A\to 𝒮e{t}^{A^{\mathrm{op}}}$, which we call the Yoneda embedding.

Theorem 9.5.4 (The Yoneda lemma).

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

$${\mathrm{hom}}_{𝒮e{t}^{A^{\mathrm{op}}}}(𝐲a,F)\cong Fa.$$ (9.5.4)

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

Proof.

Given a natural transformation $\alpha :𝐲a\to F$, we can consider the component ${\alpha }_a:𝐲a(a)\to Fa$. Since $𝐲a(a)\equiv {\mathrm{hom}}_A(a,a)$, we have $1_a:𝐲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 :𝐲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 :𝐲a\to F$ and define $x$ as above, then for any $f:{\mathrm{hom}}_A(a^{\prime },a)$ we have

${\alpha }_{a^{\prime }}(f)$ $={\alpha }_{a^{\prime }}(𝐲a_{a^{\prime },a}(f))$

$=({\alpha }_{a^{\prime }}\circ 𝐲a_{a^{\prime },a}(f))(1_a)$

$=(F_{a^{\prime },a}(f)\circ {\alpha }_a)(1_a)$

$=F_{a^{\prime },a}(f)({\alpha }_a(1_a))$

$=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 $\mathrm{y}\mathrm{:}A\mathrm{\to }\mathrm{S}\mathit{}e\mathit{}{t}^{A^{\mathrm{op}}}$ is fully faithful.

Proof.

By ct:yoneda, we have

$${\mathrm{hom}}_{𝒮e{t}^{A^{\mathrm{op}}}}(𝐲a,𝐲b)\cong 𝐲b(a)\equiv {\mathrm{hom}}_A(a,b).$$

It is easy to check that this isomorphism is in fact the action of $𝐲$ on hom-sets. ∎

Corollary 9.5.7.

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

Proof.

By ct:yoneda-embedding, $𝐲$ induces an isomorphism on sets of isomorphisms. But as $A$ and $𝒮e{t}^{A^{\mathrm{op}}}$ are categories and $𝐲$ 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\mathrm{:}\mathrm{S}\mathit{}e\mathit{}{t}^{A^{\mathrm{op}}}$ is said to be representable if there exists $a\mathrm{:}A$ and an isomorphism $\mathrm{y}\mathit{}a\mathrm{\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 ${𝐲}_0$ over $F$. Since ${𝐲}_0$ is an embedding by ct: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 ct: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\mathrm{:}A\mathrm{\to }B$, the following types are equivalent.

1. $F$ is a left adjoint.

2. For each $b:B$, the functor $(a\mapsto {\mathrm{hom}}_B(Fa,b))$ from $A^{\mathrm{op}}$ to $𝒮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}:{\mathrm{hom}}_B(Fa,b)\cong {\mathrm{hom}}_A(a,G_{0}b)$$

such that ${\gamma }_{a,b}(g\circ Ff)={\gamma }_{a^{\prime },b}(g)\circ f$ for $f:{\mathrm{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 ${ϵ}_b:\equiv {({\gamma }_{Gb,b})}^{-1}(1_{Gb})$. Now for $g:{\mathrm{hom}}_B(b,b^{\prime })$ we define

$$G_{b,b^{\prime }}(g):\equiv {\gamma }_{Gb,b^{\prime }}(g\circ {ϵ}_b)$$

The verifications that $G$ is a functor and $\eta$ and $ϵ$ 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

$${\mathrm{hom}}_B(Fa,b)\stackrel{G_{Fa,b}}{\to }{\mathrm{hom}}_A(GFa,Gb)\stackrel{(\text{–}\circ {\eta }_a)}{\to }{\mathrm{hom}}_A(a,Gb).$$

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

$${\mathrm{hom}}_A(a,Gb)\stackrel{F_{a,Gb}}{\to }{\mathrm{hom}}_B(Fa,FGb)\stackrel{({ϵ}_b\circ \text{–})}{\to }{\mathrm{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:{\mathrm{hom}}_B(Fa,b)$ to

$G(f)\circ {\eta }_a$ $\equiv {\gamma }_{GFa,b}(f\circ {ϵ}_{Fa})\circ {\eta }_a$

$={\gamma }_{GFa,b}(f\circ {ϵ}_{Fa}\circ F{\eta }_a)$

$={\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 }}:{\mathrm{hom}}_B(b,b^{\prime })\to {\mathrm{hom}}_A(Gb,G{b}^{\prime })$ is defined to take $g$ to

${\gamma }_{Gb,b^{\prime }}(g\circ {ϵ}_b)$ $\equiv G(g\circ {ϵ}_b)\circ {\eta }_{Gb}$

$=G(g)\circ G{ϵ}_b\circ {\eta }_{Gb}$

$=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 ${ϵ}_b$ is defined to be ${({\gamma }_{Gb,b})}^{-1}(1_{Gb})\equiv {ϵ}_b\circ F(1_{Gb})$, which also equals the old ${ϵ}_b$. ∎

Corollary 9.5.11.

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

Proof.

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

Title	9.5 The Yoneda lemma