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.

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

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

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

@[instance_reducible]

noncomputable def CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) : AddCommMonoid (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.

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

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

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

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