Exponential in cartesian closed categories behave itself like composition.

Question

MacLane S. "CWM" p96

I have been trying to prove Ex. $4$ the associative (like composition) of natural transformation $c^b \times b^a \overset{\tau}{\to} c^a$ for two months but I didn't succeed, although I managed to construct $\tau$ by applying exponential adjunction to the arrow $c^b \times (b^a \times a) \overset{c^b \times eval}{\to} c^b \times b \overset{eval}{\to} c$. Сould someone help me?

Answer 1

Another way to view the construction of the composition morphism is via Yoneda's lemma: for any object $U$ of the category, we have $\operatorname{Hom}(U, C^B) \simeq \operatorname{Hom}(U \times B, C)$ and similarly for $\operatorname{Hom}(U, B^A)$ and $\operatorname{Hom}(U, C^A)$. Now, we can construct a function map \begin{align*} \operatorname{Hom}(U, C^B \times B^A) & \simeq \operatorname{Hom}(U, C^B) \times \operatorname{Hom}(U, B^A) \\ & \simeq \operatorname{Hom}(U\times B, C) \times \operatorname{Hom}(U\times A, B) \\ & \to \operatorname{Hom}(U\times A, C) \\ & \simeq \operatorname{Hom}(U, C^A) \end{align*} where the map on the second-to-last line takes $(f, g) \in \operatorname{Hom}(U\times B, C) \times \operatorname{Hom}(U\times A, B)$ to $f \circ (\pi_1, g) \in \operatorname{Hom}(U\times A, C)$.

We can furthermore see that each step is natural in $U$, i.e. it forms a morphism (or isomorphism) of contravariant functors $\mathbf{C}^{\operatorname{op}} \to \mathbf{Set}$. Thus, by Yoneda's lemma, the morphism of functors above corresponds to a unique morphism $C^B \times B^A \to C^A$. (Your construction amounts to the unfolding of the proof of Yoneda's lemma on the above morphism of functors, i.e. applying the morphism of functors on $\operatorname{id}_{C^B \times B^A}$.)

Now, in order to verify that the composition is associative, you can break it down into a few parts:

• Showing that $\operatorname{comp} \times \operatorname{id} : D^C \times C^B \times B^A \to D^B \times B^A$ corresponds to \begin{align*} \operatorname{Hom}(-, D^C \times C^B \times B^A) & \simeq \operatorname{Hom}(- \times C, D) \times \operatorname{Hom}(- \times B, C) \times \operatorname{Hom}(- \times A, B) \\ & \to \operatorname{Hom}(-\times B, D) \times \operatorname{Hom}(-\times A, B) \\ & \simeq \operatorname{Hom}(-, D^B \times B^A). \end{align*} where the second map takes $(f, g, h) \mapsto (f \circ (\pi_1, g), h)$; and similarly for $\operatorname{id} \times \operatorname{comp} : D^C \times C^B \times B^A \to D^C \times C^A$.
• Showing that Yoneda's lemma "respects compositions", i.e. if $\phi : \operatorname{Hom}(-, Y) \to \operatorname{Hom}(-, Z)$ corresponds to $f \in \operatorname{Hom}(Y, Z)$ and $\psi : \operatorname{Hom}(-, X) \to \operatorname{Hom}(-, Y)$ corresponds to $g \in \operatorname{Hom}(X, Y)$, then $\phi \circ \psi$ corresponds to $f\circ g \in \operatorname{Hom}(X, Z)$. (This may in fact already have been done in your textbook - perhaps even in the statement of Yoneda's lemma itself if it is in the form of asserting that the functor $\mathbf{C} \to \mathbf{Set}^{\mathbf{C}^{\operatorname{op}}}, A \mapsto \operatorname{Hom}(-, A)$, is fully faithful, in which case the statement here is closely related to the part of the construction of the functor where you show that it respects compositions.)
• Showing that the composition operation is associative at the level of morphisms of functors $\operatorname{Hom}(-\times C, D) \times \operatorname{Hom}(-\times B, C) \times \operatorname{Hom}(-\times A, B) \to \operatorname{Hom}(-\times A, D)$.

Answer 2

Daniel's answer is ultimately the better one, and has the higher payoff for learning thoroughly. But if you're still getting a feel for Yoneda the following may be more transparent. For a bit of notation, I'll use $o_{abc}:c^b\times b^a\to c^a$ to denote the composition map, $ev_{ab}:b^a\times a\to b$ to denote the evaluation map, and $1_a$ to denote the identity on $a$.

To show that composition is associative, what you want is to show that $$ev_{ad}\circ (o_{abd}\times 1_a)\circ (o_{bcd}\times 1_{b^a}\times 1_a)=ev_{ad}\circ (o_{acd}\times 1_a)\circ (1_{d^c}\times o_{abc}\times 1_a).$$ This will show, by uniqueness of transposes, that $o_{abd}\circ(o_{bcd}\times 1_{b^a})=o_{acd}\circ (1_{d^c}\times o_{abc})$. The argument is by straight equation crunching, but it does take some practice to get a sense for which equalities to use. The main ones that come up are the central $$ev_{ac}\circ (o_{abc}\times 1_a)=ev_{bc}\circ(1_{c^b}\times ev_{ab})$$ and that any map of the form $f\times g:A\times B\to C\times D$ can be broken up into $$A\times B\overset{1_A\times g}{\longrightarrow} A\times D\overset{f\times 1_C}{\longrightarrow}C\times D.$$ I also treat $\times$ as associative, and there's a little bit of trickery involved there, but it's not important trickery; one can rewrite this in a way that makes no appeal to $\times$ or associativity, it's just much less readable.

So the actual crunching:

\begin{align*} ev_{ad}\circ (o_{abd}\times 1_a)\circ ((o_{bcd}\times 1_{b^a})\times 1_a) &= ev_{bd}\circ(1_{d^b}\times ev_{ab})\circ(o_{bcd}\times (1_{b^a}\times 1_a)) \\ &= ev_{bd}\circ (o_{bcd}\times ev_{ab}) \\ &= ev_{bd}\circ (o_{bcd}\times 1_b)\circ((1_{d^c}\times 1_{c^b})\times ev_{ab}) \\ &= ev_{cd}\circ(1_{d^c}\times ev_{bc})\circ(1_{d^c}\times (1_{c^b}\times ev_{ab})) \\ &= ev_{cd}\circ (1_{d^c}\times [ev_{bc}\circ (1_{c^b}\times ev_{ab})]) \\ &= ev_{cd}\circ (1_{d^c}\times [ev_{ac}\circ (o_{abc}\times 1_a)]) \\ &= ev_{cd}\circ(1_{d^c}\times ev_{ac})\circ (1_{d^c}\times (o_{abc}\times 1_a)) \\ &= ev_{ad}\circ (o_{acd}\times 1_a)\circ ((1_{d^c}\times o_{abc})\times 1_a) \end{align*} Which is just what we wanted.