Yoneda’s lemma

Yoneda lemma is a fact about so-called Hom functors. We shall start with the definition and examples for both Covariant Hom functor and Contravariant Hom functor. The definition and examples for Yoneda lemma will be provided after that. In the chapter we shall assume that the category \(\mathbf{C}\) is a Locally small category.

Hom functors

We are going to define the Hom functors. There are 2 hom functors: Covariant functor and Contravariant functor. For the Covariant Hom functor we pick up an object \(a\) from \(\mathbf{C}\) and consider the collection of morphisms from \(a\) to an arbitrary object \(x\) from the category. The collection is a Set as soon as \(\mathbf{C}\) is a Locally small category. Therefore we can associate a set (object from Set category) with the object \(x\) from the category \(C\).

The same approach is used for Contravariant Hom functor. But in the case we consider the set of morphisms from an arbitrary object \(x\) to the picked object \(a\) i.e. we reverse Arrows in this case.

Covariant Hom functor

Let \(\mathbf{C}\) be a Locally small category and \(a \in \mathrm{ob}(\mathbf{C})\). Consider Functor from \(\mathbf{C}\) to the Set category defined by the following rules:

  • \(\forall x \in \mathrm{ob}(\mathbf{C})\) define an object in the set category: \(\mathrm{hom}_{\mathbf{C}}\left(a, x\right) \in \mathrm{ob}(\mathbf{Set})\)

  • \(\forall f: x \to y \in \mathrm{hom}(\mathbf{C})\) define a function in the set category \(\mathrm{hom}_{\mathbf{C}}\left(a, f\right): \mathrm{hom}_{\mathbf{C}}\left(a, x\right) \to \mathrm{hom}_{\mathbf{C}}\left(a, y\right)\) as follows \(\mathrm{hom}_{\mathbf{C}}\left(a, f\right) = \{f \circ g | g \in \mathrm{hom}_{\mathbf{C}}\left(a, x\right)\}\).

The covariant Hom functor is denoted as \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\).

Covariant Hom functor \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) example. Category \(\mathbf{C}\)

Consider category \(\mathbf{C}\) in the Covariant Hom functor. It consists of 4 objects: \[\mathrm{ob}(\mathbf{C}) = \{a,b,c,d\}.\] We are going to construct \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) functor and therefore are interested in the following sets of morphisms: \[\begin{aligned} \mathrm{hom}_{\mathbf{C}}\left(a, a\right) = \{\mathbf{1}_{a \to a}\}, \nonumber \\ \mathrm{hom}_{\mathbf{C}}\left(a, b\right) = \{f_1^{(b)}, f_2^{(b)}\}, \nonumber \\ \mathrm{hom}_{\mathbf{C}}\left(a, c\right) = \{f_1^{(c)}, f_2^{(c)}, g_1 = f \circ f_1^{(b)}, g_2 = f \circ f_2^{(b)}\}, \nonumber \\ \mathrm{hom}_{\mathbf{C}}\left(a, d\right) = \emptyset. \nonumber \end{aligned}\] There is also a single Morphism \(f\) between \(b\) and \(c\).

Covariant Hom functor \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) example. Category \(\mathbf{Set}\)

The corresponding objects in the Set category is described in the Covariant Hom functor: \[\begin{aligned} a' = \mathrm{hom}_{\mathbf{C}}\left(a, a\right) = \{\mathbf{1}_{a \to a}\}, \nonumber \\ b' = \mathrm{hom}_{\mathbf{C}}\left(a, b\right) = \{f_1^{(b)}, f_2^{(b)}\}, \nonumber \\ c' = \mathrm{hom}_{\mathbf{C}}\left(a, c\right) = \{f_1^{(c)}, f_2^{(c)}, g_1, g_2\}, \nonumber \\ d' = \mathrm{hom}_{\mathbf{C}}\left(a, d\right) = \emptyset. \nonumber \end{aligned}\]

The \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) does the following mapping between objects: \[\begin{aligned} a \Rightarrow \mathrm{hom}_{\mathbf{C}}\left(a, a\right) = a', \nonumber \\ b \Rightarrow \mathrm{hom}_{\mathbf{C}}\left(a, b\right) = b', \nonumber \\ c \Rightarrow \mathrm{hom}_{\mathbf{C}}\left(a, c\right) = c', \nonumber \\ d \Rightarrow \mathrm{hom}_{\mathbf{C}}\left(a, d\right) = \emptyset. \nonumber \end{aligned}\] The functor maps morphisms in addition to objects. There are mapping for trivial Identity morphisms: \[\begin{aligned} \mathbf{1}_{a \to a} \Rightarrow \mathbf{1}_{a' \to a'}, \nonumber \\ \mathbf{1}_{b \to b} \Rightarrow \mathbf{1}_{b' \to b'}, \nonumber \\ \mathbf{1}_{c \to c} \Rightarrow \mathbf{1}_{c' \to c'}, \nonumber \\ \mathbf{1}_{d \to d} \Rightarrow \mathbf{1}_{\emptyset \to \emptyset}, \nonumber \end{aligned}\] and for a single non trivial morphism \(f \Rightarrow f'\) that is defined by the following rules: \[\begin{aligned} f'(f_1^{(b)}) = g_1, \nonumber \\ f'(f_2^{(b)}) = g_2, \nonumber \end{aligned}\] i.e. the Image of \(f'\) is a subset of \(\mathrm{hom}_{\mathbf{C}}\left(a, c\right)\): \[\operatorname{Im}{f'} \subsetneq \mathrm{hom}_{\mathbf{C}}\left(a, c\right).\]

Contravariant Hom functor

If we revert Arrows in the Covariant Hom functor then we can get a definition for Contravariant functor as follows.

Let \(\mathbf{C}\) is a Locally small category and \(a \in \mathrm{ob}(\mathbf{C})\). Consider Functor from \(\mathbf{C}^{op}\) to the Set category, equivalently a Contravariant functor from \(\mathbf{C}\) to Set category, defined by the following rules

  • \(\forall x \in \mathrm{ob}(\mathbf{C})\) define an object in the set category: \(\mathrm{hom}_{\mathbf{C}}\left(x, a\right) \in \mathrm{ob}(\mathbf{Set})\)

  • \(\forall h: x \to y \in \mathrm{hom}(\mathbf{C})\) define a function in the set category \(\mathrm{hom}_{\mathbf{C}}\left(h, a\right): \mathrm{hom}_{\mathbf{C}}\left(y, a\right) \to \mathrm{hom}_{\mathbf{C}}\left(x, a\right)\) as follows \(\mathrm{hom}_{\mathbf{C}}\left(h, a\right) = \{g \circ h | g \in \mathrm{hom}_{\mathbf{C}}\left(y, a\right)\}\).

The contravariant Hom functor is denoted as \(\mathrm{Hom}_{C}\left(-, a\right)\).

From the definition of Contravariant functor follows that we can get it simply reverting Arrows in the initial category. Lets do it for Covariant Hom functor as follows

Contravariant Hom functor \(\mathrm{Hom}_{D}\left(-, a\right)\) example. Category \(\mathbf{D}\)

Consider category \(\mathbf{D}\) in the Contravariant Hom functor. It is similar to the category \(\mathbf{C}\) from Covariant Hom functor and has the same set of objects and morphisms but all morphisms are reverted i.e. \(D = \mathbf{C}^{op}\). Therefore the category consists of 4 objects: \[\mathrm{ob}(\mathbf{D}) = \{a,b,c,d\}.\] We are going to construct \(\mathrm{Hom}_{D}\left(-, a\right)\) functor and therefore are interested in the following sets of morphisms: \[\begin{aligned} \mathrm{hom}_{\mathbf{D}}\left(a, a\right) = \{\mathbf{1}_{a \to a}\}, \nonumber \\ \mathrm{hom}_{\mathbf{D}}\left(b, a\right) = \{h_1^{(b)}, h_2^{(b)}\}, \nonumber \\ \mathrm{hom}_{\mathbf{D}}\left(c, a\right) = \{h_1^{(c)}, h_2^{(c)}, g_1 = h_1^{(b)} \circ h, g_2 = h_2^{(b)} \circ h\}, \nonumber \\ \mathrm{hom}_{\mathbf{D}}\left(d, a\right) = \emptyset. \nonumber \end{aligned}\] There is also a single Morphism \(h\) between \(c\) and \(b\).

Contravariant Hom functor \(\mathrm{Hom}_{D}\left(-, a\right)\) example. Category \(\mathbf{Set}\)

The corresponding objects in the Set category is described in the Contravariant Hom functor: \[\begin{aligned} a' = \mathrm{hom}_{\mathbf{D}}\left(a, a\right) = \{\mathbf{1}_{a \to a}\}, \nonumber \\ b' = \mathrm{hom}_{\mathbf{D}}\left(b, a\right) = \{f_1^{(b)}, f_2^{(b)}\}, \nonumber \\ c' = \mathrm{hom}_{\mathbf{D}}\left(c, a\right) = \{f_1^{(c)}, f_2^{(c)}, g_1, g_2\}, \nonumber \\ d' = \mathrm{hom}_{\mathbf{D}}\left(d, a\right) = \emptyset. \nonumber \end{aligned}\]

The \(\mathrm{Hom}_{D}\left(-, a\right)\) does the following mapping between objects: \[\begin{aligned} a \Rightarrow \mathrm{hom}_{\mathbf{D}}\left(a, a\right) = a', \nonumber \\ b \Rightarrow \mathrm{hom}_{\mathbf{D}}\left(b, a\right) = b', \nonumber \\ c \Rightarrow \mathrm{hom}_{\mathbf{D}}\left(c, a\right) = c', \nonumber \\ d \Rightarrow \mathrm{hom}_{\mathbf{D}}\left(d, a\right) = \emptyset. \nonumber \end{aligned}\] The functor maps morphisms in addition to objects. There are mapping for trivial Identity morphisms: \[\begin{aligned} \mathbf{1}_{a \to a} \Rightarrow \mathbf{1}_{a' \to a'}, \nonumber \\ \mathbf{1}_{b \to b} \Rightarrow \mathbf{1}_{b' \to b'}, \nonumber \\ \mathbf{1}_{c \to c} \Rightarrow \mathbf{1}_{c' \to c'}, \nonumber \\ \mathbf{1}_{d \to d} \Rightarrow \mathbf{1}_{\emptyset \to \emptyset}, \nonumber \end{aligned}\] and for a single non trivial morphism \(h \Rightarrow h'\) that is defined by the following rules: \[\begin{aligned} h'(h_1^{(b)}) = g_1, \nonumber \\ h'(h_2^{(b)}) = g_2, \nonumber \end{aligned}\] i.e. the Image of \(h'\) is a subset of \(\mathrm{hom}_{\mathbf{D}}\left(c, a\right)\): \[\operatorname{Im}{h'} \subsetneq \mathrm{hom}_{\mathbf{D}}\left(c, a\right).\]

Representable functor

Let \(\mathbf{C}\) is a Locally small category. The functor \(F: \mathbf{C} \Rightarrow \mathbf{Set}\) is called representable if it is naturally isomorphic (see Natural isomorphism) to \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) for some object \(a \in \mathrm{ob}(\mathbf{C})\).

Representation of \(F\) is a pair \((a, \alpha)\) where \[\alpha: \mathrm{Hom}_{\mathbf{C}}\left(a, -\right) \xrightarrow{.} F\] is a Natural isomorphism.

Consider a Representable functor \(F\). we shall mark it as a small letter f in the example. 1 Representable functor is defined by a pair: \((a, \alpha)\) where \(a\) is the object from \(\mathbf{C}\) and \(\alpha\) is a Natural isomorphism. The first condition for \(a\) can be written as follows in Hask category

        type Rep f :: *

where Rep f is the type \(a\) that represent our functor \(f\).

The second condition for Natural isomorphism requires 2 Natural transformations: \[\begin{aligned} \mathrm{tabulate} : \mathrm{Hom}_{\mathbf{C}}\left(a, -\right) \xrightarrow{.} F, \nonumber \\ \mathrm{index} : F \xrightarrow{.} \mathrm{Hom}_{\mathbf{C}}\left(a, -\right). \nonumber \end{aligned}\] In Haskell the 2 functions can be written as follows

        tabulate :: (Rep f -> x) -> f x
        index :: f x -> Rep f -> x

From Reynolds we know that such functions are Natural transformations and therefore can be 2 parts of the required Natural isomorphism \(\alpha\). Combining these conditions together we can obtain the following definition for Representable functor in Hask category

    class Representable f where 
        type Rep f :: *
        tabulate :: (Rep f -> x) -> f x
        index :: f x -> Rep f -> x

Consider the following type as a concrete example of the Representable functor

data Pair a = P a a

The representation type for Pair is Bool

instance Representable Pair where
  type Rep Pair = Bool

  index :: Pair a -> (Bool -> a)
  index (P x _) False = x
  index (P _ y) True  = y

  tabulate :: (Bool -> a) -> Pair a
  tabulate generate = P (generate False) (generate True)

Consider the category \(\mathbf{Set}\). Set of morphisms \(\mathrm{hom}_{\mathbf{Set}}\left(a, x\right)\) is the same as the Exponential object \(x^a\), i.e. \[\mathrm{hom}_{\mathbf{Set}}\left(a, x\right) \cong x^a.\] More generally, the same notation makes sense in a category where the exponential object \(x^a\) is defined and interpreted as the object of morphisms from \(a\) to \(x\). Therefore, in such context, formally, we can write \[\mathrm{Hom}_{\mathbf{C}}\left(a, -\right) \cong \left(-\right)^a.\] If functor \(F\) is a Representable functor then \[F \cong \mathrm{Hom}_{\mathbf{C}}\left(a, -\right) \cong \left(-\right)^a.\] Thus we can define the logarithm operation for a Representable functor as follows \[\log F = a.\]

Yoneda’s lemma

Let \(\mathbf{C}\) is a Locally small category and \(F\) is a functor from \(\mathbf{C}\) to \(\mathbf{Set}\) i.e. \[F \in \mathrm{ob}(\mathbf{[\mathbf{C}, \mathbf{Set}]})\] and also we have \[\mathrm{Hom}_{\mathbf{C}}\left(a, -\right) \in \mathrm{ob}(\mathbf{[\mathbf{C}, \mathbf{Set}]}).\] Then \[\mathrm{hom}_{\mathbf{[\mathbf{C}, \mathbf{Set}}}\left(], \mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\right){F} \cong F(a)\]

Proof.

Category \(\mathbf{C}\). We look at 2 objects \(x\) and \(y\) and a morphism \(f\) between them

Lets start with 2 objects \(x, y\) from category \(\mathbf{C}\) and a morphism \(f\) between the 2 objects Yoneda.

Commutative diagram for components of natural transformation \(\alpha_x\) and \(\alpha_y\)

Functor \(\mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\) maps \(x\) into \(\mathrm{hom}_{\mathbf{C}}\left(a, x\right)\) and \(y\) into \(\mathrm{hom}_{\mathbf{C}}\left(a, y\right)\). Functor \(F\) maps the 2 objects into \(F(x)\) and \(F(y)\) respectively. There is a Natural transformation \(\alpha\) between the functors. I.e. \(\alpha \in \mathrm{hom}_{\mathbf{[\mathbf{C}, \mathbf{Set}}}\left(], \mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\right){F}\). We are interested in 2 components of the natural transformations: \[\alpha_x : \mathrm{hom}_{\mathbf{C}}\left(a, x\right) \to F(x)\] and \[\alpha_y : \mathrm{hom}_{\mathbf{C}}\left(a, y\right) \to F(y).\] The components of natural transformation should satisfy the naturality conditions (Natural transformation) i.e. the commutative diagram Yoneda should commute.

We can replace object \(x\) with \(a\) in \(\mathrm{hom}_{\mathbf{C}}\left(a, x\right)\). The result set \(\mathrm{hom}_{\mathbf{C}}\left(a, a\right)\) should contain Identity morphism \(\mathbf{1}_{a \to a}\). Lets look how the morphism is mapped by the commutative diagram from Yoneda.

Mapping for \(\mathbf{1}_{a \to a}\). The identity morphism is mapped into \(p \in F(a)\) i.e. \(p = \alpha_a(\mathbf{1}_{a \to a})\)

As we can see in Yoneda, morphism \(\alpha_a\) pick up an element \(p\) of the set \(F(a)\). There is an arbitrary element that is determined by \(\alpha_a\). All others elements in Yoneda is completely determined by the choice of \(p\). From Covariant Hom functor we have \[\mathrm{hom}_{\mathbf{C}}\left(a, f\right) = \{f \circ g | g \in \mathrm{hom}_{\mathbf{C}}\left(a, x\right)\}\] i.e. if \(g = \mathbf{1}_{a \to a}\) then \[\mathrm{hom}_{\mathbf{C}}\left(a, f\right)\left(\mathbf{1}_{a \to a}\right) = f \circ \mathbf{1}_{a \to a} = f.\] From other side we have mapping \(F(f): p \to q\) where \(q = (F(f))(p)\). I.e. if we pick an arbitrary object \(y \in \mathrm{ob}(\mathbf{C})\) when we can pick a morphism \(f: a \to y\). This leads to the definition for an arbitrary component \(\alpha_y\) of Natural transformation \(\alpha\) as soon as only one component \(\alpha_a\) is defined: \[\alpha_y(f) = (F(f))(p).\] Therefore from only one element \(p \in F(a)\) we can got the Natural transformation \(\alpha \in \mathrm{hom}_{\mathbf{[\mathbf{C}, \mathbf{Set}}}\left(], \mathrm{Hom}_{\mathbf{C}}\left(a, -\right)\right){F}\). We also can go in other direction i.e. \(\alpha_a(\mathbf{1}_{a \to a})\) will gives as an element \(p\) from the set \(F(a)\). ◻