## Tag `003D`

## 4.27. 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{\rm Ob}\nolimits(\textit{Cat})$ the class of all categories. For every pair of categories $\mathcal{A}, \mathcal{B} \in \mathop{\rm 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

verticalcomposition. We will use the usual symbol $\circ$ for this. Next, we will definehorizontalcomposition. 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{\rm Ob}\nolimits(\text{Fun}(\mathcal{B}, \mathcal{C})) \times \mathop{\rm Ob}\nolimits(\text{Fun}(\mathcal{A}, \mathcal{B})) \longrightarrow \mathop{\rm 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{\rm 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.27.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

horizontalcomposition $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.27.2. The horizontal and vertical compositions have the following properties

- $\circ$ and $\star$ are associative,
- the identity transformations $\text{id}_F$ are units for $\circ$,
- the identity transformations of the identity functors $\text{id}_{\text{id}_\mathcal{A}}$ are units for $\star$ and $\circ$, and
- 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.

The code snippet corresponding to this tag is a part of the file `categories.tex` and is located in lines 4317–4558 (see updates for more information).

```
\section{Formal properties}
\label{section-formal-cat-cat}
\noindent
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.
\medskip\noindent
Let us denote $\Ob(\textit{Cat})$ the class of all categories.
For every pair of categories
$\mathcal{A}, \mathcal{B} \in \Ob(\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 {\it vertical} composition. We will use the usual
symbol $\circ$ for this. Next, we will define {\it horizontal}
composition. In order to do this we explain a bit more
of the structure at hand.
\medskip\noindent
Namely for every triple
of categories $\mathcal{A}$, $\mathcal{B}$, and $\mathcal{C}$
there is a composition law
$$
\circ : \Ob(\text{Fun}(\mathcal{B}, \mathcal{C}))
\times
\Ob(\text{Fun}(\mathcal{A}, \mathcal{B}))
\longrightarrow
\Ob(\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?
\medskip\noindent
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$.
\medskip\noindent
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$.
\medskip\noindent
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 \Ob(\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.
\begin{definition}
\label{definition-horizontal-composition}
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 {\it horizontal} composition $s \star t$ to be the
transformation of functors ${}_{G'}t \circ s_F = s_{F'}\circ {}_Gt$.
\end{definition}
\noindent
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.
\begin{lemma}
\label{lemma-properties-2-cat-cats}
The horizontal and vertical compositions have the following
properties
\begin{enumerate}
\item $\circ$ and $\star$ are associative,
\item the identity transformations $\text{id}_F$
are units for $\circ$,
\item the identity transformations of the identity functors
$\text{id}_{\text{id}_\mathcal{A}}$
are units for $\star$ and $\circ$, and
\item 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)$.
\end{enumerate}
\end{lemma}
\begin{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.
\end{proof}
\noindent
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 \ref{definition-product-category}.
```

## Comments (0)

## Add a comment on tag `003D`

Your email address will not be published. Required fields are marked.

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 lower-right corner).

All contributions are licensed under the GNU Free Documentation License.

There are no comments yet for this tag.