Product Category is Product in Category of Categories

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf{Cat}$ be the category of categories.

Let $\mathbf C$ and $\mathbf D$ be small categories, and let $\mathbf C \times \mathbf D$ be their product category.


Then $\mathbf C \times \mathbf D$ is a binary product of $\mathbf C$ and $\mathbf D$ in $\mathbf{Cat}$.


Proof

Let $F: \mathbf A \to \mathbf C$ and $G: \mathbf A \to \mathbf D$ be morphisms in $\mathbf{Cat}$, i.e. functors.

Suppose $X: \mathbf A \to \mathbf C \times \mathbf D$ is a functor such that $\pr_1 \circ X = F$ and $\pr_2 \circ X = G$:

$\begin{xy}\[email protected][email protected][email protected]+3mu{ & \mathbf A \ar[dl]_*{F} \ar[d]^*{X} \ar[dr]^*{G} \\ \mathbf C & \mathbf C \times \mathbf D \ar[l]^*{\pr_1} \ar[r]_*{\pr_2} & \mathbf D }\end{xy}$

Here, $\pr_1$ and $\pr_2$ are projection functors.


Thus, for all objects $A$ of $\mathbf A$, it is required that:

$\map {\pr_1} {X A} = F A$
$\map {\pr_2} {X A} = G A$

meaning that $X A = \tuple {F A, G A}$ by definition of the objects of the product category $\mathbf C \times \mathbf D$.

Similarly, for all morphisms $f$ of $\mathbf A$, it is required that:

$\map {\pr_1} {X f} = F f$
$\map {\pr_2} {X f} = G f$

meaning that $X f = \tuple {F f, G f}$ by definition of the morphisms of the product category $\mathbf C \times \mathbf D$.


This uniquely determines the functor $X$, if it exists.

That this definition actually yields a functor is shown on Functor to Product Category.


Hence $\mathbf C \times \mathbf D$ is a binary product of $\mathbf C$ and $\mathbf D$ in $\mathbf{Cat}$.

$\blacksquare$


Sources