---- > [!theorem] Theorem. ([[the Yoneda lemma]]) > Let $\mathsf{C}$ be a (locally small) [[category]], $A$ an object of $\mathsf{C}$, and $\mathscr{F}:\mathsf{C} \to \mathsf{Set}$ a [[covariant functor|functor]]. Then > > 1. There is a [[bijection]] $\{ \text{natural transformations } \text{Hom}_{\mathsf{C}}(A, -) \Rightarrow \mathscr{F} \} \leftrightarrow \mathscr{F}(A)$ > associating to a [[natural transformation]] $\alpha:\text{Hom}_{\mathsf{C}}(A,-) \Rightarrow \mathscr{F}$ to the element $\alpha_{A}(1_{A}) \in \mathscr{F}(A)$ and, inversely, an element $x \in \mathscr{F}(A)$ to a [[natural transformation]] $\Psi$ having $B$-component $\Psi_{B}(f: A \to B):=\mathscr{F}(f)(x)$. > 2. This [[bijection]] is [[natural transformation|natural]] in $A$ and $\mathscr{F}$. > > Here, $\text{Hom}_{\mathsf{C}}(A,-)$ represents the [[hom functor]]. > > If instead of a [[covariant functor]] $\mathscr{F}$ we have a [[contravariant functor]] $\mathscr{G}$, then this bijection is $\{ \text{natural transformations } \text{Hom}_{\mathsf{C}}(-, A) \Rightarrow \mathscr{G} \} \xleftrightarrow{\sim} \mathscr{G}(A)$ > [!proposition] Corollary. > (Using contravariant version) If $\mathscr{G}$ is also a [[hom functor]] $\mathscr{G}=\text{Hom}\big(-, Y\big)$ , we get $\{\text{nat. trans. }\text{Hom}_{\mathsf{C}}(-, A) \Rightarrow \text{Hom}_{\mathsf{C}}(-,Y)\} \leftrightarrow \text{Hom}_{\mathsf{C}}(A,Y)$ > In particular, $A \cong Y$ iff $\text{Hom}(-, A) \cong \text{Hom}(-, Y)$. "The collection of morphisms entering an object determines it (up to isomorphism)." > Indeed, if $\text{Hom}(-,A) \xRightarrow{\sim, \Phi} \text{Hom}(-, Y)$, with inverse $\Psi$, then $\Phi_{A}(1_{A})$ is a map $A \to Y$ with inverse $\Psi_{Y}:Y \to A$. > [!proof]- Proof. ([[the Yoneda lemma]]) > (NB: this writing is verbose to be illustrative; the proof itself is very short). > > **Proof of 1.** We will construct a function $\Phi$ and its inverse $\Psi$. > > Given a [[natural transformation]] $\alpha : \text{Hom}_{\mathsf{C}}(A, -) \to \mathscr{F}$, we need to find an element of $\mathscr{F}(A)$ to send it to. There is really only one option: all we know about $\mathsf{C}$ is that it has $A$ as an object, and the only morphism that we know of leaving any object in general is the identity morphism. Thus, with $\alpha_{A}:\text{Hom}_{\mathsf{C}}(A,A) \to \mathscr{F}(A)$ denoting the $A$-component of $\alpha$, we define $\Phi(\alpha):=\alpha_{A}(1_{A})$. > > Now, how should the inverse $\Psi$ be constructed? Let $x \in \mathscr{F}(A)$. Then define a [[natural transformation]] $\Psi(x)$ to have general (say, $B$-) component $\Psi(x)_{B}$ given by the function $\begin{align} > \text{Hom}_{\mathsf{C}}(A, B) &\to \mathscr{F}(B) \\ > f & \mapsto \mathscr{F}(f) (x) . > \end{align}$ > Why is $\Psi(x)$ natural? In short, because $\mathscr{F}$ is a functor. To be explicit, given $f \in \text{Hom}_{\mathsf{C}}(A,B)$, one has for any $h:B \to L$ $\begin{align} > \mathscr{F}(h) \circ \Psi(x)_{B} (f) &= \mathscr{F}(h) \circ \mathscr{F}\big(f \big) (x) \\ > & = \mathscr{F}(h \circ f)(x) > \end{align}$ > (where we used functoriality) and $\begin{align} > \Psi(x)_{L} \circ (h \circ -)(f) &= \mathscr{F}\big( (h \circ -) (f) \big)(x) \\ > &= \mathscr{F}\big( h \circ f \big)(x) > \end{align}$ > as required. > > ![[CleanShot 2024-10-20 at [email protected]]] > > Now we verify that for any $x \in \mathscr{F}(A)$, $\begin{align} > \Phi \circ \Psi (x) & = \Psi(x)_{A}(1_{A}) \\ > & = \mathscr{F}\big( 1_{A} \big)(x) \\ > & = 1_{\mathscr{F}(A)}(x) \\ > &= x. > \end{align}$ > And for any $\alpha: \text{Hom}(A, -) \to \mathscr{F}$, > ---- #### ----- #### References > [!backlink] > ```dataview > TABLE rows.file.link as "Further Reading" > FROM [[]] > FLATTEN file.tags as Tag > WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom" > GROUP BY Tag > ``` > [!frontlink] > ```dataview > TABLE rows.file.link as "Further Reading" > FROM outgoing([[]]) > FLATTEN file.tags as Tag > WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom" > GROUP BY Tag > ```