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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.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}, CategoryTheory.MonoidalCategory.whiskerLeft X 0 = 0
• zero_whiskerRight : ∀ {X Y Z : C}, CategoryTheory.MonoidalCategory.whiskerRight 0 X = 0
• whiskerLeft_add : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.whiskerLeft X (f + g) = CategoryTheory.MonoidalCategory.whiskerLeft X f + CategoryTheory.MonoidalCategory.whiskerLeft X g
• add_whiskerRight : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.whiskerRight (f + g) X = CategoryTheory.MonoidalCategory.whiskerRight f X + CategoryTheory.MonoidalCategory.whiskerRight g X

@[simp]

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

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.monoidalPreadditive_of_faithful {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor D C) [F.Monoidal] [F.Faithful] [F.Additive] : CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (P : C) {Q R : C} {J : Type u_2} (s : Finset J) (g : J → (Q ⟶ R)) : CategoryTheory.MonoidalCategory.whiskerLeft P (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.MonoidalCategory.whiskerLeft P (g j)

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def CategoryTheory.leftDistributor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : CategoryTheory.MonoidalCategory.tensorObj X (⨁ f) ≅ ⨁ fun (j : J) => CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (CategoryTheory.leftDistributor X f).hom = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) (CategoryTheory.Limits.biproduct.ι (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

def CategoryTheory.rightDistributor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X ≅ ⨁ fun (j : J) => CategoryTheory.MonoidalCategory.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (CategoryTheory.rightDistributor f X).hom = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) (CategoryTheory.Limits.biproduct.ι (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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