mathlib3 documentation

category_theory.preadditive.of_biproducts

Constructing a semiadditive structure from binary biproducts #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts 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

category_theory.semiadditive_of_binary_biproducts.left_add X Y f g = category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc (𝟙 Y) (𝟙 Y)

@[simp]

noncomputable def category_theory.semiadditive_of_binary_biproducts.right_add {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts 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

category_theory.semiadditive_of_binary_biproducts.right_add X Y f g = category_theory.limits.biprod.lift (𝟙 X) (𝟙 X) ≫ category_theory.limits.biprod.desc f g

theorem category_theory.semiadditive_of_binary_biproducts.is_unital_left_add {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (X Y : C) :

eckmann_hilton.is_unital (λ (_x _y : X ⟶ Y), category_theory.semiadditive_of_binary_biproducts.left_add X Y _x _y) 0

theorem category_theory.semiadditive_of_binary_biproducts.is_unital_right_add {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (X Y : C) :

eckmann_hilton.is_unital (λ (_x _y : X ⟶ Y), category_theory.semiadditive_of_binary_biproducts.right_add X Y _x _y) 0

theorem category_theory.semiadditive_of_binary_biproducts.distrib {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (X Y : C) (f g h k : X ⟶ Y) :

category_theory.semiadditive_of_binary_biproducts.left_add X Y (category_theory.semiadditive_of_binary_biproducts.right_add X Y f g) (category_theory.semiadditive_of_binary_biproducts.right_add X Y h k) = category_theory.semiadditive_of_binary_biproducts.right_add X Y (category_theory.semiadditive_of_binary_biproducts.left_add X Y f h) (category_theory.semiadditive_of_binary_biproducts.left_add X Y g k)

noncomputable def category_theory.semiadditive_of_binary_biproducts.add_comm_monoid_hom_of_has_binary_biproducts {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] (X Y : C) :

add_comm_monoid (X ⟶ Y)

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

Equations

category_theory.semiadditive_of_binary_biproducts.add_comm_monoid_hom_of_has_binary_biproducts X Y = {add := λ (_x _y : X ⟶ Y), category_theory.semiadditive_of_binary_biproducts.right_add X Y _x _y, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 (λ (_x _y : X ⟶ Y), category_theory.semiadditive_of_binary_biproducts.right_add X Y _x _y) _ _, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

theorem category_theory.semiadditive_of_binary_biproducts.add_eq_right_addition {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {X Y : C} (f g : X ⟶ Y) :

f + g = category_theory.limits.biprod.lift (𝟙 X) (𝟙 X) ≫ category_theory.limits.biprod.desc f g

theorem category_theory.semiadditive_of_binary_biproducts.add_eq_left_addition {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {X Y : C} (f g : X ⟶ Y) :

f + g = category_theory.limits.biprod.lift f g ≫ category_theory.limits.biprod.desc (𝟙 Y) (𝟙 Y)

theorem category_theory.semiadditive_of_binary_biproducts.add_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {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} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproducts C] {X Y Z : C} (f : X ⟶ Y) (g h : Y ⟶ Z) :

f ≫ (g + h) = f ≫ g + f ≫ h