# 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