Proving that the horizontal composition of natural transformations is a natural transformation

category-theorynatural-transformations

Is there an easy way to prove that the horizontal composition of natural transformations is a natural transformation?

To fix the notation, here is part of Leinster's textbook:

enter image description here

Suppose $f:A\to A'$ is an arrow in $\mathscr A$. We need to show that $$(\alpha'\ast\alpha)_{A'}\circ (F'\circ F)(f)=(G'\circ G)(f)\circ (\alpha'\ast \alpha)_A$$

I tried substituting both expressions from the definition of $(\alpha'\ast\alpha)_{A'}$ (and also of $(\alpha'\ast \alpha)_A$), but it's not clear how to simplify either of them.


(the vertical arrows are $\alpha_A$ and $\alpha_{A'}$)
$$
\require{AMScd}
\begin{CD}
F(A) @>{F(f)}>> F(A');\\
@VVV @VVV \\
G(A) @>{G(f)}>> G(A');
\end{CD}$$

Best Answer

Fix an arrow $f : A \to B$ in $\mathcal{A}$.

By the naturality of $\alpha$, we recover the following (commutative) diagram.

$\begin{CD} FA @>Ff>> FB\\ @VV\alpha_AV @VV\alpha_BV\\ GA @>Gf>> GB \end{CD}$

Now we eventually want to have a diagram involving $F'F$, so let's hit the diagram with $F'$. Recall functors preserve commutative diagrams, so the following still commutes.

$\begin{CD} F'FA @>F'Ff>> F'FB\\ @VVF'\alpha_AV @VVF'\alpha_BV\\ F'GA @>F'Gf>> F'GB \end{CD}$

We also want $G'G$ to be in the picture somewhere, and we know how to turn an $F'$ into a $G'$, so...

$\begin{CD} F'FA @>F'Ff>> F'FB\\ @VVF'\alpha_AV @VVF'\alpha_BV\\ F'GA @>F'Gf>> F'GB\\ @VV\alpha'_{GA}V @VV\alpha'_{GB}V\\ G'GA @>G'Gf>> G'GB \end{CD}$

Since the top and bottom squares both commute, it is a simple exercise to show the outer square does too.

Thus we obtain a commutative diagram:

$\begin{CD} F'FA @>F'Ff>> F'FB\\ @VV\alpha'_{GA} \circ F'\alpha_AV @VV\alpha'_{GB} \circ F'\alpha_BV\\ G'GA @>G'Gf>> G'GB \end{CD}$

But recall (as your question mentions) $(\alpha' * \alpha)_A = \alpha'_{GA} \circ F' \alpha_A$.

Renaming our diagram using this definition gives:

$\begin{CD} F'FA @>F'Ff>> F'FB\\ @VV(\alpha' * \alpha)_AV @VV(\alpha' * \alpha)_BV\\ G'GA @>G'Gf>> G'GB \end{CD}$

Since the same argument works for any $A,B,f$, this square witnesses the naturality of $\alpha' * \alpha$.


As is often the case in category theory, we found this argument by doing the only thing available to us. We wanted a diagram of a certain type, and at each step there was really only one choice. Unfortunately, this means that if we struggle to find the "one choice", we can really struggle to solve these kinds of problems! But that's ok, everyone has difficulty with these kinds of arguments, but we all become comfortable with them in time.


I hope this helps ^_^

Related Question