Finite Product in Preadditive Category is Biproduct

Theorem

Binary products

Let $A$ be a preadditive category.

Let $a_1, a_2$ be objects of $A$.

Let $(a_1 \times a_2, p_1, p_2)$ be their binary product, assuming it exists.

Let $i_1 : a_1 \to a_1 \times a_2$ be the unique morphism with:

$p_1 \circ i_1 = 1 : a_1 \to a_1$

$p_2 \circ i_1 = 0 : a_1 \to a_2$

Let $i_2 : a_1 \to a_1 \times a_2$ be the unique morphism with:

$p_1 \circ i_2 = 0 : a_2 \to a_1$

$p_2 \circ i_2 = 1 : a_2 \to a_2$

where $1$ is the identity morphism and $0$ is the zero morphism.

Then $(a_1 \times a_2, i_1, i_2, p_1, p_2)$ is the binary biproduct of $a_1$ and $a_2$.

A particular theorem is missing. In particular: arbitrary finite products You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding the theorem. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{TheoremWanted}} from the code.

Also see

• Finite Coproduct in Preadditive Category is Biproduct