Preadditive monoidal categories #

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

source

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

Instances

source

@[simp]

theorem CategoryTheory.MonoidalPreadditive.whiskerLeft_zero {C : Type u_1} :

source

@[simp]

theorem CategoryTheory.MonoidalPreadditive.zero_whiskerRight {C : Type u_1} :

source

@[simp]

theorem CategoryTheory.MonoidalPreadditive.whiskerLeft_add {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.whiskerLeft X (f + g) = CategoryTheory.MonoidalCategory.whiskerLeft X f + CategoryTheory.MonoidalCategory.whiskerLeft X g

source

@[simp]

theorem CategoryTheory.MonoidalPreadditive.add_whiskerRight {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.whiskerRight (f + g) X = CategoryTheory.MonoidalCategory.whiskerRight f X + CategoryTheory.MonoidalCategory.whiskerRight g X

source

@[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 : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) :

CategoryTheory.MonoidalCategory.tensorHom f 0 = 0

source

@[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 : C} {X : C} {Y : C} {Z : C} (f : Y ⟶ Z) :

CategoryTheory.MonoidalCategory.tensorHom 0 f = 0

source

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 : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : Y ⟶ Z) :

CategoryTheory.MonoidalCategory.tensorHom f (g + h) = CategoryTheory.MonoidalCategory.tensorHom f g + CategoryTheory.MonoidalCategory.tensorHom f h

source

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 : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : W ⟶ X) (h : Y ⟶ Z) :

CategoryTheory.MonoidalCategory.tensorHom (f + g) h = CategoryTheory.MonoidalCategory.tensorHom f h + CategoryTheory.MonoidalCategory.tensorHom g h

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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.MonoidalFunctor D C) [F.Faithful] [F.Additive] :

CategoryTheory.MonoidalPreadditive D

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

source

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 : C} {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)

source

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 : C} {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

source

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 : C} {Q : C} {R : C} {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)

source

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 : C} {Q : C} {R : C} {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

source

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

One or more equations did not get rendered due to their size.

source

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

One or more equations did not get rendered due to their size.

source

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

Instances For

source

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)

source

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))

source

@[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

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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)

source

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 : C) (Y : C) (f : J → C) :

((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)

source

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

Instances For

source

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)

source

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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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 : C) (Y : C) :

(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

source

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

source

theorem CategoryTheory.leftDistributor_ext_left_iff {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} {Y : C} {f : J → C} {g : CategoryTheory.MonoidalCategory.tensorObj X (⨁ f) ⟶ Y} {h : CategoryTheory.MonoidalCategory.tensorObj X (⨁ f) ⟶ Y} :

g = h ↔ ∀ (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

source

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 : C} {Y : C} {f : J → C} {g : CategoryTheory.MonoidalCategory.tensorObj X (⨁ f) ⟶ Y} {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

source

theorem CategoryTheory.leftDistributor_ext_right_iff {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} {Y : C} {f : J → C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)} {h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)} :

g = h ↔ ∀ (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))

source

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 : C} {Y : C} {f : J → C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)} {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

source

theorem CategoryTheory.leftDistributor_ext₂_left_iff {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} {Y : C} {Z : C} {f : J → C} {g : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)) ⟶ Z} {h : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)) ⟶ Z} :

g = h ↔ ∀ (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

source

g = h

source

theorem CategoryTheory.leftDistributor_ext₂_right_iff {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} {Y : C} {Z : C} {f : J → C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (CategoryTheory.MonoidalCategory.tensorObj Z (⨁ f))} {h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (CategoryTheory.MonoidalCategory.tensorObj Z (⨁ f))} :

g = h ↔ ∀ (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)))

source

g = h

source

theorem CategoryTheory.rightDistributor_ext_left_iff {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} {Y : C} {g : CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X ⟶ Y} {h : CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X ⟶ Y} :

g = h ↔ ∀ (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

source

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 : C} {Y : C} {g : CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X ⟶ Y} {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

source

theorem CategoryTheory.rightDistributor_ext_right_iff {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} {Y : C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y} {h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y} :

g = h ↔ ∀ (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)

source

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 : C} {Y : C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y} {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

source

theorem CategoryTheory.rightDistributor_ext₂_left_iff {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} {Y : C} {Z : C} {g : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X) Y ⟶ Z} {h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X) Y ⟶ Z} :

g = h ↔ ∀ (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

source

g = h

source

theorem CategoryTheory.rightDistributor_ext₂_right_iff {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} {Y : C} {Z : C} {g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y) Z} {h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y) Z} :

g = h ↔ ∀ (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)

source

g = h

HepLean Documentation

Mathlib.CategoryTheory.Monoidal.Preadditive

Preadditive monoidal categories #