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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (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.

def CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (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.

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) (Y : C) : EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) => CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y x1 x2) 0

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) (Y : C) : EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) => CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y x1 x2) 0

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) (Y : C) (f : X ⟶ Y) (g : X ⟶ Y) (h : X ⟶ Y) (k : X ⟶ Y) : CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f g) (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y h k) = CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y f h) (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y g k)

def CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) (Y : C) : AddCommMonoid (X ⟶ Y)

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

Equations

• CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts X Y = AddCommMonoid.mk ⋯

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : f + g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.Limits.biprod.desc f g)

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : f + g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (f + g) h = CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h

theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (g + h) = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h