# 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.

def CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd {C : Type u} (X : C) (Y : C) (f : X Y) (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
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd {C : Type u} (X : C) (Y : C) (f : X Y) (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
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib {C : Type u} (X : C) (Y : C) (f : X Y) (g : X Y) (h : X Y) (k : X Y) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :
theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Y) (h : Y Z) :
theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.comp_add {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : Y Z) :