# 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 additive 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.

Instances of this typeclass
Instances of other typeclasses for category_theory.monoidal_preadditive
@[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
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem category_theory.tensor_sum (C : Type u_1) {P Q R S : C} {J : Type u_3} (s : finset J) (f : P Q) (g : J → (R S)) :
f s.sum (λ (j : J), g j) = s.sum (λ (j : J), f g j)
theorem category_theory.sum_tensor (C : Type u_1) {P Q R S : C} {J : Type u_3} (s : finset J) (f : P Q) (g : J → (R S)) :
s.sum (λ (j : J), g j) f = s.sum (λ (j : J), g j f)
@[protected, instance]
Equations
@[protected, instance]
Equations
noncomputable def category_theory.left_distributor {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
X f λ (j : J), X f j

The isomorphism showing how tensor product on the left distributes over direct sums.

Equations
@[simp]
theorem category_theory.left_distributor_hom {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
= finset.univ.sum (λ (j : J), category_theory.limits.biproduct.ι (λ (j : J), X f j) j)
@[simp]
theorem category_theory.left_distributor_inv {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
= finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π (λ (j : J), X f j) j (𝟙 X
theorem category_theory.left_distributor_assoc {C : Type u_1} {J : Type} [fintype J] (X Y : C) (f : J → C) :
≪≫ (λ (j : J), Y f j) = (α_ X Y ( f)).symm ≪≫ ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), α_ X Y (f j))
noncomputable def category_theory.right_distributor {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
( f) X λ (j : J), f j X

The isomorphism showing how tensor product on the right distributes over direct sums.

Equations
@[simp]
theorem category_theory.right_distributor_hom {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
= finset.univ.sum (λ (j : J), category_theory.limits.biproduct.ι (λ (j : J), f j X) j)
@[simp]
theorem category_theory.right_distributor_inv {C : Type u_1} {J : Type} [fintype J] (X : C) (f : J → C) :
= finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π (λ (j : J), f j X) j 𝟙 X))
theorem category_theory.right_distributor_assoc {C : Type u_1} {J : Type} [fintype J] (X Y : C) (f : J → C) :
≪≫ (λ (j : J), f j X) = α_ ( f) X Y ≪≫ ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), (α_ (f j) X Y).symm)
theorem category_theory.left_distributor_right_distributor_assoc {C : Type u_1} {J : Type} [fintype J] (X Y : C) (f : J → C) :
≪≫ (λ (j : J), X f j) = α_ X ( f) Y ≪≫ ≪≫ (λ (j : J), f j Y) ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), (α_ X (f j) Y).symm)