# Constructing a semiadditive structure from binary biproducts #

We show that any category with zero morphisms and binary biproducts is enriched over the category of commutative monoids.

@[simp]
noncomputable def category_theory.semiadditive_of_binary_biproducts.left_add {C : Type u} (X Y : C) (f g : X Y) :
X Y

f +ₗ g is the composite X ⟶ Y ⊞ Y ⟶ Y, where the first map is (f, g) and the second map is (𝟙 𝟙).

Equations
@[simp]
noncomputable def category_theory.semiadditive_of_binary_biproducts.right_add {C : Type u} (X Y : C) (f g : X Y) :
X Y

f +ᵣ g is the composite X ⟶ X ⊞ X ⟶ Y, where the first map is (𝟙, 𝟙) and the second map is (f g).

Equations

In a category with binary biproducts, the morphisms form a commutative monoid.

Equations
theorem category_theory.semiadditive_of_binary_biproducts.add_eq_right_addition {C : Type u} {X Y : C} (f g : X Y) :
f + g =
theorem category_theory.semiadditive_of_binary_biproducts.add_eq_left_addition {C : Type u} {X Y : C} (f g : X Y) :
f + g =
theorem category_theory.semiadditive_of_binary_biproducts.add_comp {C : Type u} {X Y Z : C} (f g : X Y) (h : Y Z) :
(f + g) h = f h + g h
theorem category_theory.semiadditive_of_binary_biproducts.comp_add {C : Type u} {X Y Z : C} (f : X Y) (g h : Y Z) :
f (g + h) = f g + f h