biproduct in an ab-enriched category determined by morphisms

1. Proposition

Let 20240220-biproduct_in_an_abelian_category_determined_by_morphism_eb04be82533afa6bcab2b0d2106fd2828974c0d1.svg be an Ab-enriched category, objects with morphisms

20240220-biproduct_in_an_abelian_category_determined_by_morphism_d25d6160b7af537c3faf16d5febe3a08bcbd8733.svg

such that

20240220-biproduct_in_an_abelian_category_determined_by_morphism_48e905b47e0569ebc95366a601b32c987deb029e.svg

and

20240220-biproduct_in_an_abelian_category_determined_by_morphism_f0029c925b740ef5928e36eab2c59f019d332f9f.svg

Then

20240220-biproduct_in_an_abelian_category_determined_by_morphism_e032b295c9fb7576b4bd098b6e191a192ace9e15.svg

is the biproduct

2. Proof

2.1. product

2.1.1. existence

Suppose there exist morphisms

20240220-biproduct_in_an_abelian_category_determined_by_morphism_db765560b5c6442f9a2fc39886b77884f48ede10.svg

Then let

20240220-biproduct_in_an_abelian_category_determined_by_morphism_b199bf456aeeb2a7e7369dc7e6a3eb3694cdfdc0.svg

then this commutes, as for 20240220-biproduct_in_an_abelian_category_determined_by_morphism_a5438ffdb050ae318bc2c594b6669fb33f2d7e65.svg (analogous for )

20240220-biproduct_in_an_abelian_category_determined_by_morphism_3926656ed5f8e18ad9aac73d4646fd447f9cb295.svg

2.1.2. uniqueness

Suppose 20240220-biproduct_in_an_abelian_category_determined_by_morphism_af4d8e4e51def71dfa4a8e9031bb99b3d011fae9.svg are morphisms satisfieng this. Then it follows, that

20240220-biproduct_in_an_abelian_category_determined_by_morphism_242db65be83e636698b069d79830a3324a8d8dfe.svg

2.2. coproduct

corollary of:

isomorphism of the finite product and finite coproduct in an ab-enriched category