Editing Biproduct (section)

==Properties==

If the biproduct <math display="inline">A \oplus B</math> exists for all pairs of objects ''A'' and ''B'' in the category '''C''', and '''C''' has a zero object, then all finite biproducts exist, making '''C''' both a [[Cartesian monoidal category]] and a co-Cartesian monoidal category.

If the product <math display="inline">A_1 \times A_2</math> and coproduct <math display="inline">A_1 \coprod A_2</math> both exist for some pair of objects ''A''<sub>1</sub>, ''A''<sub>2</sub> then there is a unique morphism <math display="inline">f: A_1 \coprod A_2 \to A_1 \times A_2</math> such that

*<math>p_k \circ f \circ i_k = 1_{A_k},\ (k = 1, 2)</math>
*<math>p_l \circ f \circ i_k = 0 </math> for <math display="inline">k \neq l.</math>{{clarify|reason=Surely we need to require that the category has zero morphisms, or at least a zero object, since otherwise this equation doesn't make sense.|date=April 2020}}

It follows that the biproduct <math display="inline">A_1 \oplus A_2</math> exists if and only if ''f'' is an [[isomorphism]].

If '''C''' is a [[preadditive category]], then every finite product is a biproduct, and every finite coproduct is a biproduct. For example, if <math display="inline">A_1 \times A_2</math> exists, then there are unique morphisms <math display="inline">i_k: A_k \to A_1 \times A_2</math> such that

*<math>p_k \circ i_k = 1_{A_k},\ (k = 1, 2)</math>
*<math>p_l \circ i_k = 0 </math> for <math display="inline">k \neq l.</math>

To see that <math display="inline">A_1 \times A_2</math> is now also a coproduct, and hence a biproduct, suppose we have morphisms <math display="inline">f_k: A_k \to X,\ k=1,2</math> for some object <math display="inline">X</math>. Define <math display="inline">f := f_1 \circ p_1 + f_2 \circ p_2.</math> Then <math display="inline">f</math> is a morphism from <math display="inline">A_1 \times A_2</math> to <math display="inline">X</math>, and <math display="inline">f \circ i_k = f_k</math> for <math display="inline">k = 1, 2</math>.

In this case we always have
*<math display="inline">i_1 \circ p_1 + i_2 \circ p_2 = 1_{A_1 \times A_2}.</math>

An [[additive category]] is a [[preadditive category]] in which all finite biproducts exist. In particular, biproducts always exist in [[abelian categories]].