CatDat

Uniqueness of preadditive structures

Lemma.

Let C\C be a preadditive category (or more generally, a category enriched in commutative monoids) with finite products and finite coproducts. Then for all objects X,YX,Y the canonical morphism α:XYX×Y\alpha : X \oplus Y \to X \times Y is an isomorphism. Moreover, the preadditive structure is unique: If f,g:ABf,g : A \rightrightarrows B are morphisms, their sum f+g:ABf+g : A \to B is the composite of (f,g):AB×B(f,g) : A \to B \times B, the inverse α1:BBB×B\alpha^{-1} : B \oplus B \to B \times B, and the codiagonal :BBB\nabla : B \oplus B \to B.

Proof. The morphism α:XYX×Y\alpha : X \oplus Y \to X \times Y is defined by the equations p1αi1=idX,p2αi2=idY,p_1 \circ \alpha \circ i_1 = \id_X, \quad p_2 \circ \alpha \circ i_2 = \id_Y, p2αi1=0,p1αi2=0.p_2 \circ \alpha \circ i_1 = 0,\quad p_1 \circ \alpha \circ i_2 = 0. It does not depend on the choice of preadditive structure since zero morphisms are unique. It is an isomorphism: Define βi1p1+i2p2:X×YXY.\beta \coloneqq i_1 \circ p_1 + i_2 \circ p_2 : X \times Y \to X \oplus Y. Then αβ=idX×Y\alpha \circ \beta = \id_{X \times Y} because p1αβ=p1αi1p1+p1αi2p2=id1p1+0p2=p1p_1 \circ \alpha \circ \beta = p_1 \circ \alpha \circ i_1 \circ p_1 + p_1 \circ \alpha \circ i_2 \circ p_2 = \id_1 \circ p_1 + 0 \circ p_2 = p_1 and likewise p2αβ=p2p_2 \circ \alpha \circ \beta = p_2. We also have βα=idXY\beta \circ \alpha = \id_{X \oplus Y} with a very similar calculation that shows βαi1=i1\beta \circ \alpha \circ i_1 = i_1 and βαi2=i2\beta \circ \alpha \circ i_2 = i_2. Therefore, for morphisms f,g:ABf,g : A \rightrightarrows B the composite ABA \to B in the claim is equal to

β(f,g)=(i1p1+i2p2)(f,g)=i1p1(f,g)+i2p2(f,g)=p1(f,g)+p2(f,g)=f+g. \begin{align*} \nabla \circ \beta \circ (f,g) & = \nabla \circ (i_1 \circ p_1 + i_2 \circ p_2) \circ (f,g) \\ & = \nabla \circ i_1 \circ p_1 \circ (f,g) + \nabla \circ i_2 \circ p_2 \circ (f,g) \\ & = p_1 \circ (f,g) + p_2 \circ (f,g) \\ & = f + g. \end{align*}

\square

Author: Martin Brandenburg

Context

This page is referenced by the following properties.