Preadditive monoidal categories

A monoidal category is MonoidalPreadditive if it is preadditive and tensor product of morphisms is linear in both factors.

class CategoryTheory.MonoidalPreadditive (C : Type u_1) [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] : Prop

A category is MonoidalPreadditive 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.

• whiskerLeft_zero {X Y Z : C} : MonoidalCategoryStruct.whiskerLeft X 0 = 0
• zero_whiskerRight {X Y Z : C} : MonoidalCategoryStruct.whiskerRight 0 X = 0
• whiskerLeft_add {X Y Z : C} (f g : Y ⟶ Z) : MonoidalCategoryStruct.whiskerLeft X (f + g) = MonoidalCategoryStruct.whiskerLeft X f + MonoidalCategoryStruct.whiskerLeft X g
• add_whiskerRight {X Y Z : C} (f g : Y ⟶ Z) : MonoidalCategoryStruct.whiskerRight (f + g) X = MonoidalCategoryStruct.whiskerRight f X + MonoidalCategoryStruct.whiskerRight g X

@[simp]

theorem CategoryTheory.MonoidalPreadditive.tensor_zero {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X) : MonoidalCategoryStruct.tensorHom f 0 = 0

@[simp]

theorem CategoryTheory.MonoidalPreadditive.zero_tensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (f : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom 0 f = 0

theorem CategoryTheory.MonoidalPreadditive.tensor_add {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom f (g + h) = MonoidalCategoryStruct.tensorHom f g + MonoidalCategoryStruct.tensorHom f h

theorem CategoryTheory.MonoidalPreadditive.add_tensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom (f + g) h = MonoidalCategoryStruct.tensorHom f h + MonoidalCategoryStruct.tensorHom g h

instance CategoryTheory.MonoidalPreadditive.instAdditiveTensorLeft {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : (MonoidalCategory.tensorLeft X).Additive

instance CategoryTheory.MonoidalPreadditive.instAdditiveTensorRight {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : (MonoidalCategory.tensorRight X).Additive

instance CategoryTheory.MonoidalPreadditive.instAdditiveFunctorCurriedTensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] : (MonoidalCategory.curriedTensor C).Additive

instance CategoryTheory.MonoidalPreadditive.instAdditiveFunctorFlipCurriedTensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] : (MonoidalCategory.curriedTensor C).flip.Additive

instance CategoryTheory.tensorLeft_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : (MonoidalCategory.tensorLeft X).Additive

instance CategoryTheory.tensorRight_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : (MonoidalCategory.tensorRight X).Additive

instance CategoryTheory.tensoringLeft_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : ((MonoidalCategory.tensoringLeft C).obj X).Additive

instance CategoryTheory.tensoringRight_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : ((MonoidalCategory.tensoringRight C).obj X).Additive

theorem CategoryTheory.monoidalPreadditive_of_faithful {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Preadditive D] [MonoidalCategory D] (F : Functor D C) [F.Monoidal] [F.Faithful] [F.Additive] : MonoidalPreadditive D

A faithful additive monoidal functor to a monoidal preadditive category ensures that the domain is monoidal preadditive.

theorem CategoryTheory.whiskerLeft_sum {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (P : C) {Q R : C} {J : Type u_2} (s : Finset J) (g : J → (Q ⟶ R)) : MonoidalCategoryStruct.whiskerLeft P (∑ j ∈ s, g j) = ∑ j ∈ s, MonoidalCategoryStruct.whiskerLeft P (g j)

theorem CategoryTheory.sum_whiskerRight {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {Q R : C} {J : Type u_2} (s : Finset J) (g : J → (Q ⟶ R)) (P : C) : MonoidalCategoryStruct.whiskerRight (∑ j ∈ s, g j) P = ∑ j ∈ s, MonoidalCategoryStruct.whiskerRight (g j) P

theorem CategoryTheory.tensor_sum {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {P Q R S : C} {J : Type u_2} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) : MonoidalCategoryStruct.tensorHom f (∑ j ∈ s, g j) = ∑ j ∈ s, MonoidalCategoryStruct.tensorHom f (g j)

theorem CategoryTheory.sum_tensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {P Q R S : C} {J : Type u_2} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) : MonoidalCategoryStruct.tensorHom (∑ j ∈ s, g j) f = ∑ j ∈ s, MonoidalCategoryStruct.tensorHom (g j) f

instance CategoryTheory.instPreservesFiniteBiproductsTensorLeft {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : Limits.PreservesFiniteBiproducts (MonoidalCategory.tensorLeft X)

instance CategoryTheory.instPreservesFiniteBiproductsTensorRight {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] (X : C) : Limits.PreservesFiniteBiproducts (MonoidalCategory.tensorRight X)

noncomputable def CategoryTheory.leftDistributor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) : MonoidalCategoryStruct.tensorObj X (⨁ f) ≅ ⨁ fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)

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

Equations

• CategoryTheory.leftDistributor X f = (CategoryTheory.MonoidalCategory.tensorLeft X).mapBiproduct f

theorem CategoryTheory.leftDistributor_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (leftDistributor X f).hom = ∑ j : J, CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.π f j)) (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j)

theorem CategoryTheory.leftDistributor_inv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (leftDistributor X f).inv = ∑ j : J, CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j))

@[simp]

theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryStruct.comp (leftDistributor X f).hom (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) = MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.π f j)

@[simp]

theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryStruct.comp (leftDistributor X f).hom (CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.π f j)) h

@[simp]

theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) (leftDistributor X f).hom = Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j

@[simp]

theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : (⨁ fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) (CategoryStruct.comp (leftDistributor X f).hom h) = CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) h

@[simp]

theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryStruct.comp (leftDistributor X f).inv (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.π f j)) = Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j

@[simp]

theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryStruct.comp (leftDistributor X f).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.π f j)) h) = CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) h

@[simp]

theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) (leftDistributor X f).inv = MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)

@[simp]

theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Z) : CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryStruct.comp (leftDistributor X f).inv h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) h

theorem CategoryTheory.leftDistributor_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X Y : C) (f : J → C) : (MonoidalCategory.tensorIso (asIso (CategoryStruct.id X)) (leftDistributor Y f) ≪≫ leftDistributor X fun (j : J) => MonoidalCategoryStruct.tensorObj Y (f j)) = (MonoidalCategoryStruct.associator X Y (⨁ f)).symm ≪≫ leftDistributor (MonoidalCategoryStruct.tensorObj X Y) f ≪≫ Limits.biproduct.mapIso fun (x : J) => MonoidalCategoryStruct.associator X Y (f x)

noncomputable def CategoryTheory.rightDistributor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) : MonoidalCategoryStruct.tensorObj (⨁ f) X ≅ ⨁ fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X

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

Equations

• CategoryTheory.rightDistributor f X = (CategoryTheory.MonoidalCategory.tensorRight X).mapBiproduct f

theorem CategoryTheory.rightDistributor_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (rightDistributor f X).hom = ∑ j : J, CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) X) (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j)

theorem CategoryTheory.rightDistributor_inv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (rightDistributor f X).inv = ∑ j : J, CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X)

@[simp]

theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryStruct.comp (rightDistributor f X).hom (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) = MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) X

@[simp]

theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryStruct.comp (rightDistributor f X).hom (CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) X) h

@[simp]

theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) (rightDistributor f X).hom = Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j

@[simp]

theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : (⨁ fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) (CategoryStruct.comp (rightDistributor f X).hom h) = CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) h

@[simp]

theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryStruct.comp (rightDistributor f X).inv (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) X) = Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j

@[simp]

theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryStruct.comp (rightDistributor f X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) X) h) = CategoryStruct.comp (Limits.biproduct.π (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) h

@[simp]

theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) (rightDistributor f X).inv = MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X

@[simp]

theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Z) : CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryStruct.comp (rightDistributor f X).inv h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) h

theorem CategoryTheory.rightDistributor_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X Y : C) : MonoidalCategory.tensorIso (rightDistributor f X) (asIso (CategoryStruct.id Y)) ≪≫ rightDistributor (fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) X) Y = MonoidalCategoryStruct.associator (⨁ f) X Y ≪≫ rightDistributor f (MonoidalCategoryStruct.tensorObj X Y) ≪≫ Limits.biproduct.mapIso fun (x : J) => (MonoidalCategoryStruct.associator (f x) X Y).symm

theorem CategoryTheory.leftDistributor_rightDistributor_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (Y : C) : MonoidalCategory.tensorIso (leftDistributor X f) (asIso (CategoryStruct.id Y)) ≪≫ rightDistributor (fun (j : J) => MonoidalCategoryStruct.tensorObj X (f j)) Y = MonoidalCategoryStruct.associator X (⨁ f) Y ≪≫ MonoidalCategory.tensorIso (asIso (CategoryStruct.id X)) (rightDistributor f Y) ≪≫ (leftDistributor X fun (j : J) => MonoidalCategoryStruct.tensorObj (f j) Y) ≪≫ Limits.biproduct.mapIso fun (x : J) => (MonoidalCategoryStruct.associator X (f x) Y).symm

theorem CategoryTheory.leftDistributor_ext_left {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} (w : ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) h) : g = h

theorem CategoryTheory.leftDistributor_ext_left_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} : g = h ↔ ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (Limits.biproduct.ι f j)) h

theorem CategoryTheory.leftDistributor_ext_right {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj Y (⨁ f)} (w : ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.π f j)) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.π f j))) : g = h

theorem CategoryTheory.leftDistributor_ext_right_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj Y (⨁ f)} : g = h ↔ ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.π f j)) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.π f j))

theorem CategoryTheory.leftDistributor_ext₂_left {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} (w : ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.ι f j))) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.ι f j))) h) : g = h

theorem CategoryTheory.leftDistributor_ext₂_left_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} : g = h ↔ ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.ι f j))) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (MonoidalCategoryStruct.whiskerLeft Y (Limits.biproduct.ι f j))) h

theorem CategoryTheory.leftDistributor_ext₂_right {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorObj Z (⨁ f))} (w : ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerLeft Y (MonoidalCategoryStruct.whiskerLeft Z (Limits.biproduct.π f j))) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerLeft Y (MonoidalCategoryStruct.whiskerLeft Z (Limits.biproduct.π f j)))) : g = h

theorem CategoryTheory.leftDistributor_ext₂_right_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorObj Z (⨁ f))} : g = h ↔ ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerLeft Y (MonoidalCategoryStruct.whiskerLeft Z (Limits.biproduct.π f j))) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerLeft Y (MonoidalCategoryStruct.whiskerLeft Z (Limits.biproduct.π f j)))

theorem CategoryTheory.rightDistributor_ext_left {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} (w : ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) h) : g = h

theorem CategoryTheory.rightDistributor_ext_left_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} : g = h ↔ ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) h

theorem CategoryTheory.rightDistributor_ext_right {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj (⨁ f) Y} (w : ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y)) : g = h

theorem CategoryTheory.rightDistributor_ext_right_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj (⨁ f) Y} : g = h ↔ ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y)

theorem CategoryTheory.rightDistributor_ext₂_left {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} (w : ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) Y) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) Y) h) : g = h

theorem CategoryTheory.rightDistributor_ext₂_left_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} : g = h ↔ ∀ (j : J), CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) Y) g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.ι f j) X) Y) h

theorem CategoryTheory.rightDistributor_ext₂_right {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} (w : ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) Z) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) Z)) : g = h

theorem CategoryTheory.rightDistributor_ext₂_right_iff {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} : g = h ↔ ∀ (j : J), CategoryStruct.comp g (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) Z) = CategoryStruct.comp h (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.whiskerRight (Limits.biproduct.π f j) Y) Z)