# The Stacks Project

## 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 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{\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 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.27.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.

The code snippet corresponding to this tag is a part of the file categories.tex and is located in lines 4392–4633 (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}.

There are no comments yet for this tag.

## Add a comment on tag 003D

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).