Proposition 9.9.5.1.3 (0187): Properties of Horizontal Composition of Natural Transformations

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Let $\mathcal{C}$, $\mathcal{D}$, and $\mathcal{E}$ be categories.

Functionality. The assignment $\webleft (\beta ,\alpha \webright )\mapsto \beta \mathbin {\star }\alpha $ defines a function
\[ \mathbin {\star }_{\webleft (F,G\webright ),\webleft (H,K\webright )}\colon \text{Nat}\webleft (H,K\webright )\times \text{Nat}\webleft (F,G\webright )\to \text{Nat}\webleft (H\circ F,K\circ G\webright ). \]
Associativity. Let

be a diagram in $\mathsf{Cats}_{\mathsf{2}}$. The diagram
commutes, i.e. given natural transformations

we have

\[ \webleft (\gamma \mathbin {\star }\beta \webright )\mathbin {\star }\alpha =\gamma \mathbin {\star }\webleft (\beta \mathbin {\star }\alpha \webright ). \]
Interaction With Identities. Let $F\colon \mathcal{C}\to \mathcal{D}$ and $G\colon \mathcal{D}\to \mathcal{E}$ be functors. The diagram

commutes, i.e. we have

\[ \text{id}_{G}\mathbin {\star }\text{id}_{F}=\text{id}_{G\circ F}. \]
Middle Four Exchange. Let $F_{1},F_{2},F_{3}\colon \mathcal{C}\to \mathcal{D}$ and $G_{1},G_{2},G_{3}\colon \mathcal{D}\to \mathcal{E}$ be functors. The diagram
commutes, i.e. given a diagram

in $\mathsf{Cats}_{\mathsf{2}}$, we have

\[ \webleft (\beta '\mathbin {\star }\alpha '\webright )\circ \webleft (\beta \mathbin {\star }\alpha \webright )=\webleft (\beta '\circ \beta \webright )\mathbin {\star }\webleft (\alpha '\circ \alpha \webright ). \]

Item 1: Functionality

Clear.

Item 2: Associativity

Omitted.

Item 3: Interaction With Identities

We have

\begin{align*} \webleft (\text{id}_{G}\mathbin {\star }\text{id}_{F}\webright )_{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{id}_{G}\webright )_{F_{A}}\circ G_{\webleft (\text{id}_{F}\webright )_{A}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{id}_{G_{F_{A}}}\circ G_{\text{id}_{F_{A}}}\\ & = \text{id}_{G_{F_{A}}}\circ \text{id}_{G_{F_{A}}}\\ & = \text{id}_{G_{F_{A}}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\text{id}_{G\circ F}\webright )_{A} \end{align*}

for each $A\in \text{Obj}\webleft (\mathcal{C}\webright )$, showing the desired equality.

Item 4: Middle Four Exchange

Let $A\in \text{Obj}\webleft (\mathcal{C}\webright )$ and consider the diagram

The top composition

is given by $\webleft (\webleft (\beta '\circ \beta \webright )\mathbin {\star }\webleft (\alpha '\circ \alpha \webright )\webright )_{A}$, while the bottom composition

is given by $\webleft (\webleft (\beta '\mathbin {\star }\alpha '\webright )\circ \webleft (\beta \mathbin {\star }\alpha \webright )\webright )_{A}$. Now, Subdiagram (1) corresponds to the naturality condition

for $\beta \colon G_{1}\Longrightarrow G_{2}$ at $\alpha '_{A}\colon F_{2}\webleft (A\webright )\to F_{3}\webleft (A\webright )$, and thus commutes. Thus we have

\[ \webleft (\webleft (\beta '\circ \beta \webright )\mathbin {\star }\webleft (\alpha '\circ \alpha \webright )\webright )_{A} = \webleft (\webleft (\beta '\mathbin {\star }\alpha '\webright )\circ \webleft (\beta \mathbin {\star }\alpha \webright )\webright )_{A} \]

for each $A\in \text{Obj}\webleft (\mathcal{C}\webright )$ and therefore

\[ \webleft (\beta '\mathbin {\star }\alpha '\webright )\circ \webleft (\beta \mathbin {\star }\alpha \webright )=\webleft (\beta '\circ \beta \webright )\mathbin {\star }\webleft (\alpha '\circ \alpha \webright ). \]

This finishes the proof.