## 4.28 Formal properties

In this section we discuss some formal properties of the $2$-category of categories. This will lead us to the definition of a (strict) $2$-category later.

Let us denote $\mathop{\mathrm{Ob}}\nolimits (\textit{Cat})$ the class of all categories. For every pair of categories $\mathcal{A}, \mathcal{B} \in \mathop{\mathrm{Ob}}\nolimits (\textit{Cat})$ we have the “small” category of functors $\text{Fun}(\mathcal{A}, \mathcal{B})$. Composition of transformation of functors such as

$\xymatrix{ \mathcal{A} \rruppertwocell ^{F''}{t'} \ar[rr]_(.3){F'} \rrlowertwocell _ F{t} & & \mathcal{B} } \text{ composes to } \xymatrix{ \mathcal{A} \rrtwocell ^{F''}_ F{\ \ t \circ t'} & & \mathcal{B} }$

is called vertical composition. We will use the usual symbol $\circ$ for this. Next, we will define horizontal composition. In order to do this we explain a bit more of the structure at hand.

Namely for every triple of categories $\mathcal{A}$, $\mathcal{B}$, and $\mathcal{C}$ there is a composition law

$\circ : \mathop{\mathrm{Ob}}\nolimits (\text{Fun}(\mathcal{B}, \mathcal{C})) \times \mathop{\mathrm{Ob}}\nolimits (\text{Fun}(\mathcal{A}, \mathcal{B})) \longrightarrow \mathop{\mathrm{Ob}}\nolimits (\text{Fun}(\mathcal{A}, \mathcal{C}))$

coming from composition of functors. This composition law is associative, and identity functors act as units. In other words – forgetting about transformations of functors – we see that $\textit{Cat}$ forms a category. How does this structure interact with the morphisms between functors?

Well, given $t : F \to F'$ a transformation of functors $F, F' : \mathcal{A} \to \mathcal{B}$ and a functor $G : \mathcal{B} \to \mathcal{C}$ we can define a transformation of functors $G\circ F \to G \circ F'$. We will denote this transformation ${}_ Gt$. It is given by the formula $({}_ Gt)_ x = G(t_ x) : G(F(x)) \to G(F'(x))$ for all $x \in \mathcal{A}$. In this way composition with $G$ becomes a functor

$\text{Fun}(\mathcal{A}, \mathcal{B}) \longrightarrow \text{Fun}(\mathcal{A}, \mathcal{C}).$

To see this you just have to check that ${}_ G(\text{id}_ F) = \text{id}_{G \circ F}$ and that ${}_ G(t_1 \circ t_2) = {}_ Gt_1 \circ {}_ Gt_2$. Of course we also have that ${}_{\text{id}_\mathcal {A}}t = t$.

Similarly, given $s : G \to G'$ a transformation of functors $G, G' : \mathcal{B} \to \mathcal{C}$ and $F : \mathcal{A} \to \mathcal{B}$ a functor we can define $s_ F$ to be the transformation of functors $G\circ F \to G' \circ F$ given by $(s_ F)_ x = s_{F(x)} : G(F(x)) \to G'(F(x))$ for all $x \in \mathcal{A}$. In this way composition with $F$ becomes a functor

$\text{Fun}(\mathcal{B}, \mathcal{C}) \longrightarrow \text{Fun}(\mathcal{A}, \mathcal{C}).$

To see this you just have to check that $(\text{id}_ G)_ F = \text{id}_{G\circ F}$ and that $(s_1 \circ s_2)_ F = s_{1, F} \circ s_{2, F}$. Of course we also have that $s_{\text{id}_\mathcal {B}} = s$.

These constructions satisfy the additional properties

${}_{G_1}({}_{G_2}t) = {}_{G_1\circ G_2}t, \ (s_{F_1})_{F_2} = s_{F_1 \circ F_2}, \text{ and }{}_ H(s_ F) = ({}_ Hs)_ F$

whenever these make sense. Finally, given functors $F, F' : \mathcal{A} \to \mathcal{B}$, and $G, G' : \mathcal{B} \to \mathcal{C}$ and transformations $t : F \to F'$, and $s : G \to G'$ the following diagram is commutative

$\xymatrix{ G \circ F \ar[r]^{{}_ Gt} \ar[d]_{s_ F} & G \circ F' \ar[d]^{s_{F'}} \\ G' \circ F \ar[r]_{{}_{G'}t} & G' \circ F' }$

in other words ${}_{G'}t \circ s_ F = s_{F'}\circ {}_ Gt$. To prove this we just consider what happens on any object $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{A})$:

$\xymatrix{ G(F(x)) \ar[r]^{G(t_ x)} \ar[d]_{s_{F(x)}} & G(F'(x)) \ar[d]^{s_{F'(x)}} \\ G'(F(x)) \ar[r]_{G'(t_ x)} & G'(F'(x)) }$

which is commutative because $s$ is a transformation of functors. This compatibility relation allows us to define horizontal composition.

Definition 4.28.1. Given a diagram as in the left hand side of:

$\xymatrix{ \mathcal{A} \rtwocell ^ F_{F'}{t} & \mathcal{B} \rtwocell ^ G_{G'}{s} & \mathcal{C} } \text{ gives } \xymatrix{ \mathcal{A} \rrtwocell ^{G \circ F} _{G' \circ F'}{\ \ s \star t} & & \mathcal{C} }$

we define the horizontal composition $s \star t$ to be the transformation of functors ${}_{G'}t \circ s_ F = s_{F'}\circ {}_ Gt$.

Now we see that we may recover our previously constructed transformations ${}_ Gt$ and $s_ F$ as ${}_ Gt = \text{id}_ G \star t$ and $s_ F = s \star \text{id}_ F$. Furthermore, all of the rules we found above are consequences of the properties stated in the lemma that follows.

Lemma 4.28.2. The horizontal and vertical compositions have the following properties

1. $\circ$ and $\star$ are associative,

2. the identity transformations $\text{id}_ F$ are units for $\circ$,

3. the identity transformations of the identity functors $\text{id}_{\text{id}_\mathcal {A}}$ are units for $\star$ and $\circ$, and

4. given a diagram

$\xymatrix{ \mathcal{A} \rruppertwocell ^ F{t} \ar[rr]_(.3){F'} \rrlowertwocell _{F''}{t'} & & \mathcal{B} \rruppertwocell ^ G{s} \ar[rr]_(.3){G'} \rrlowertwocell _{G''}{s'} & & \mathcal{C} }$

we have $(s' \circ s) \star (t' \circ t) = (s' \star t') \circ (s \star t)$.

Proof. The last statement turns using our previous notation into the following equation

$s'_{F''} \circ {}_{G'}t' \circ s_{F'} \circ {}_ Gt = (s' \circ s)_{F''} \circ {}_ G(t' \circ t).$

According to our result above applied to the middle composition we may rewrite the left hand side as $s'_{F''} \circ s_{F''} \circ {}_ Gt' \circ {}_ Gt$ which is easily shown to be equal to the right hand side. $\square$

Another way of formulating condition (4) of the lemma is that composition of functors and horizontal composition of transformation of functors gives rise to a functor

$(\circ , \star ) : \text{Fun}(\mathcal{B}, \mathcal{C}) \times \text{Fun}(\mathcal{A}, \mathcal{B}) \longrightarrow \text{Fun}(\mathcal{A}, \mathcal{C})$

whose source is the product category, see Definition 4.2.20.

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).