Product of Composite Morphisms

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf C$ be a metacategory.

Let $f \times f': A \times A' \to B \times B'$ and $g \times g': B \times B' \to C \times C'$ be two composable products of morphisms in $\mathbf C$.


Then:

$\paren {g \circ f} \times \paren {g' \circ f'} = \paren {g \times g'} \circ \paren {f \times f'}$

where $\times$ signifies product of morphisms.


Proof

The situation is efficiently captured in the following commutative diagram:

$\begin{xy} <-5em,0em>*+{A} = "A", <0em,0em>*+{A \times A'} = "P", <5em,0em>*+{A'} = "A2", <-5em,-5em>*+{B} = "B", <0em,-5em>*+{B \times B'} = "Q", <5em,-5em>*+{B'} = "B2", <-5em,-10em>*+{C} = "C", <0em,-10em>*+{C \times C'} = "R", <5em,-10em>*+{C'} = "C2", "P";"A" **@{-} ?>*@{>} ?*!/^.8em/{\pr_1}, "P";"A2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2}, "Q";"B" **@{-} ?>*@{>} ?*!/^.8em/{\pr_1}, "Q";"B2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2}, "R";"C" **@{-} ?>*@{>} ?*!/_.8em/{\pr_1}, "R";"C2" **@{-} ?>*@{>} ?*!/^.8em/{\pr_2}, "A";"B" **@{-} ?>*@{>} ?*!/^.8em/{f}, "A2";"B2" **@{-} ?>*@{>} ?*!/_.8em/{f'}, "P";"Q" **@{--} ?>*@{>} ?*!/_1.4em/{f \times f'}, "B";"C" **@{-} ?>*@{>} ?*!/^.8em/{g}, "B2";"C2" **@{-} ?>*@{>} ?*!/_.8em/{g'}, "Q";"R" **@{--} ?>*@{>} ?*!/_1.4em/{g \times g'}, \end{xy}$

The result is immediate from deleting the $B$s:

$\begin{xy} <-5em,0em>*+{A} = "A", <0em,0em>*+{A \times A'} = "P", <5em,0em>*+{A'} = "A2", <-5em,-10em>*+{C} = "C", <0em,-10em>*+{C \times C'} = "R", <5em,-10em>*+{C'} = "C2", "P";"A" **@{-} ?>*@{>} ?*!/^.8em/{\pr_1}, "P";"A2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2}, "R";"C" **@{-} ?>*@{>} ?*!/_.8em/{\pr_1}, "R";"C2" **@{-} ?>*@{>} ?*!/^.8em/{\pr_2}, "A";"C" **@{-} ?>*@{>} ?*!/^1.1em/{g \circ f}, "A2";"C2" **@{-} ?>*@{>} ?*!/_1.3em/{g' \circ f'}, "P";"R" **@{--} ?>*@{>} ?*!/_2em/{\paren {g \circ f} \times \\ \paren {g' \circ f'} }, \end{xy}$

The uniqueness of $\paren {g \circ f} \times \paren {g' \circ f'}$ implies it equals $\paren {g \times g'} \circ \paren {f \times f'}$.

$\blacksquare$