Definition of $[\mathscr A^{\text{op}}, \textbf{Set}](H_A,X)\to [\mathscr A^{\text{op}}, \textbf{Set}](H_B,X)$ in the proof of the Yoneda lemma

Question

Regarding the proof of the Yoneda lemma on p.98:

How does one get that the map $$[\mathscr A^{\text{op}}, \textbf{Set}](H_A,X)\to [\mathscr A^{\text{op}}, \textbf{Set}](H_B,X)$$ is defined by $-\circ H_f$ ? (The definition of $H_f$ is given on p.90.)

And how does one get that the map $$[\mathscr A^{\text{op}}, \textbf{Set}](H_A,X)\to [\mathscr A^{\text{op}}, \textbf{Set}](H_A,X')$$ is defined by $\theta\circ -$ ?

Answer 1

First question. The context is that we want to prove that $$[\mathscr A^{\text{op}}, \textbf{Set}](H_A,X)\cong X(A)$$ naturally in $A$. That is, that the functors $$[\mathscr A^{\text{op}}, \textbf{Set}](H_\bullet,X)\text{ and } X(\bullet)$$ are naturally isomorphic. To see why the map $$[\mathscr A^{\text{op}}, \textbf{Set}](H_A,X)\to [\mathscr A^{\text{op}}, \textbf{Set}](H_B,X)$$ is defined in the way described by Leinster, we decompose the functor in question viz. $[\mathscr A^{\text{op}}, \textbf{Set}](H_\bullet,X)$ as a composition of two functors. This is implicitly done on p.95 (see the related question). The decomposition, according to p.95, is

$$\mathscr A^{op}\to[\mathscr A^{\text{op}}, \textbf{Set}]^{op}\to\mathbf {Set}\\ A\mapsto H_\bullet(A)=H_A\mapsto [\mathscr A^{op},\mathbf{Set}](H_A,X)$$

where the first functor is $H_\bullet^{op}$ and the second functor is $[\mathscr A^{op},\mathbf{Set}](-,X)$.

Here is how the composition works on arrows.

• Let $f:B\to A$ be an arrow in $\mathscr A$ (so that $f^{op}:A\to B$ is an arrow in $\mathscr A^{op}$).

• Under the functor $H_\bullet^{op}:\mathscr A^{op}\to[\mathscr A^{\text{op}}, \textbf{Set}]^{op}$, the arrow $f^{op} $ gets mapped to the arrow $H_\bullet^{op}(f^{op})=H_\bullet(f)^{op}=H_f^{op}:H_A\to H_B$. Here we used Definition 4.1.21 and the definition of the opposite functor.

• Then, under the functor $[\mathscr A^{op},\mathbf{Set}](-,X): [\mathscr A^{\text{op}}, \textbf{Set}]^{op}\to\mathbf {Set}$, the arrow $H_f^{op}$ gets mapped to the arrow $-\circ H_f:[\mathscr A^{op},\mathbf{Set}](H_A,X)\to [\mathscr A^{op},\mathbf{Set}](H_B,X)$. Here we used Definition 4.1.16.

This answers the first question.

For the second question, we are dealing with the functor $[\mathscr A^{op},\mathbf{Set}](H_A,-)$, which is not even a composite functor, so we can directly apply Definition 4.1.1.

Answer 2

For any category $\mathcal C$, the hom functor acts on morphisms by pre- and post composition: if $\alpha:A'\to A$ and $\beta:B\to B'$ are morphisms in $\mathcal C$, then $$\mathcal C(\alpha,\beta):\mathcal C(A,B)\to \mathcal C(A', B')\\ \varphi \ \mapsto\ \beta\circ\varphi\circ\alpha$$ And in particular, it's usual to write $\mathcal C(A,\beta)$ for $\mathcal C(1_A,\beta)$ and $\mathcal C(\alpha, B)$ for $\mathcal C(\alpha, 1_B)$.

Apply it with $\mathcal C =[\mathscr A^{op}, \mathbf{Set}]$, $\ \alpha=H_f\ $ and $\ \beta=\theta$.

Answer 3

The single argument Hom-functors you're probably more familiar with are just what happens when you fix one of the arguments $\mathcal{C}(-,-):\mathcal{C}^{op}\times\mathcal{C}\to\mathbf{Set}$. As functors with that domain, you can absolutely use both the pre- and post-compositions this proof is talking about.

But I don't think you're quite clear on what the proof is trying to do. It's trying to establish a natural isomorphism between two functors $\mathscr{A}^{op}\times[\mathscr{A}^{op},\mathbf{Set}]\to \mathbf{Set}$. One of these functors is the evaluation functor, but the other is the composite $$\hom\circ (H_{-}\times id):\mathscr{A}^{op}\times[\mathscr{A}^{op},\mathbf{Set}]\to[\mathscr{A}^{op},\mathbf{Set}]^{op}\times[\mathscr{A}^{op},\mathbf{Set}]\to\mathbf{Set}$$ where that "$\hom$" is the two-argument Hom-functor. The first half of the stuff on p.98 is establishing naturality of this isomorphism in the first argument, and the second half is establish naturality in the second argument. But to talk about the behavior in both arguments of that big composite above is precisely to talk about instances of both pre- and post-composition.