# mathlibdocumentation

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)  :
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} [self : category_theory.monoidal_preadditive C] {W X Y Z : C} (f : W X) :
f 0 = 0
@[simp]
theorem category_theory.monoidal_preadditive.zero_tensor {C : Type u_1} [self : category_theory.monoidal_preadditive C] {W X Y Z : C} (f : Y Z) :
0 f = 0
theorem category_theory.monoidal_preadditive.tensor_add {C : Type u_1} [self : category_theory.monoidal_preadditive C] {W X Y Z : C} (f : W X) (g h : Y Z) :
f (g + h) = f g + (f h)
theorem category_theory.monoidal_preadditive.add_tensor {C : Type u_1} [self : category_theory.monoidal_preadditive C] {W X Y Z : C} (f g : W X) (h : Y Z) :
f + g h = f h + (g h)
@[instance]
@[instance]