Preadditive monoidal categories #
A monoidal category is monoidal_preadditive if it is preadditive and tensor product of morphisms
is linear in both factors.
@[class]
structure
category_theory.monoidal_preadditive
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C] :
Type
- tensor_zero' : (∀ {W X Y Z : C} (f : W ⟶ X), f ⊗ 0 = 0) . "obviously"
- zero_tensor' : (∀ {W X Y Z : C} (f : Y ⟶ Z), 0 ⊗ f = 0) . "obviously"
- tensor_add' : (∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + (f ⊗ h)) . "obviously"
- add_tensor' : (∀ {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z), f + g ⊗ h = f ⊗ h + (g ⊗ h)) . "obviously"
A category is monoidal_preadditive if tensoring is linear in both factors.
Note we don't extend preadditive C here, as abelian C already extends it,
and we'll need to have both typeclasses sometimes.
@[simp]
theorem
category_theory.monoidal_preadditive.tensor_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : W ⟶ X) :
@[simp]
theorem
category_theory.monoidal_preadditive.zero_tensor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : Y ⟶ Z) :
theorem
category_theory.monoidal_preadditive.tensor_add
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : W ⟶ X)
(g h : Y ⟶ Z) :
theorem
category_theory.monoidal_preadditive.add_tensor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f g : W ⟶ X)
(h : Y ⟶ Z) :
@[protected, instance]
def
category_theory.tensoring_left_additive
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_right_additive
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :