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
@[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
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) :
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) :