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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
:
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
Instances
@[simp]
theorem
CategoryTheory.MonoidalPreadditive.tensor_zero
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
{W X Y Z : C}
(f : W ⟶ X)
:
@[simp]
theorem
CategoryTheory.MonoidalPreadditive.zero_tensor
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
{W X Y Z : C}
(f : Y ⟶ Z)
:
theorem
CategoryTheory.MonoidalPreadditive.tensor_add
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
{W X Y Z : C}
(f : W ⟶ X)
(g h : Y ⟶ Z)
:
theorem
CategoryTheory.MonoidalPreadditive.add_tensor
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
{W X Y Z : C}
(f g : W ⟶ X)
(h : Y ⟶ Z)
:
instance
CategoryTheory.tensorLeft_additive
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
(X : C)
:
(MonoidalCategory.tensorLeft X).Additive
instance
CategoryTheory.tensorRight_additive
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
(X : C)
:
(MonoidalCategory.tensorRight X).Additive
instance
CategoryTheory.tensoringLeft_additive
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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.{u_4, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
{D : Type u_2}
[Category.{u_3, u_2} D]
[Preadditive D]
[MonoidalCategory D]
(F : Functor D C)
[F.Monoidal]
[F.Faithful]
[F.Additive]
:
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.{u_3, 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.{u_3, 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.{u_3, 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.{u_3, 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
(X : C)
:
instance
CategoryTheory.instPreservesFiniteBiproductsTensorRight
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
(X : C)
:
def
CategoryTheory.leftDistributor
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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
Instances For
theorem
CategoryTheory.leftDistributor_hom
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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)
def
CategoryTheory.rightDistributor
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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
Instances For
theorem
CategoryTheory.rightDistributor_hom
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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_right
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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₂_left
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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₂_right
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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.rightDistributor_ext_left
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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_right
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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₂_left
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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₂_right
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[Limits.HasFiniteBiproducts C]
{J : Type}
[Fintype 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