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 representableif 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.∎