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]
:
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.tensorHom (CategoryTheory.CategoryStruct.id X) 0 = 0
- zero_whiskerRight : ∀ {X Y Z : C}, CategoryTheory.MonoidalCategory.tensorHom 0 (CategoryTheory.CategoryStruct.id X) = 0
- whiskerLeft_add : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (f + g) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f + CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) g
- add_whiskerRight : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom (f + g) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X) + CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id X)
Instances
@[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)
:
@[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)
:
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)
:
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)
:
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)
:
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)
:
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.Functor.Additive ((CategoryTheory.MonoidalCategory.tensoringLeft C).toPrefunctor.obj X)
Equations
- One or more equations did not get rendered due to their size.
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.Functor.Additive ((CategoryTheory.MonoidalCategory.tensoringRight C).toPrefunctor.obj X)
Equations
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Faithful F.toFunctor]
[CategoryTheory.Functor.Additive F.toFunctor]
:
A faithful additive monoidal functor to a monoidal preadditive category ensures that the domain is monoidal preadditive.
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 (Finset.sum s fun (j : J) => g j) = Finset.sum s fun (j : J) => 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 : C}
{Q : C}
{R : C}
{S : C}
{J : Type u_2}
(s : Finset J)
(f : P ⟶ Q)
(g : J → (R ⟶ S))
:
CategoryTheory.MonoidalCategory.tensorHom (Finset.sum s fun (j : J) => g j) f = Finset.sum s fun (j : J) => CategoryTheory.MonoidalCategory.tensorHom (g j) f
instance
CategoryTheory.instPreservesFiniteBiproductsPreadditiveHasZeroMorphismsTensorLeftPreservesZeroMorphisms_of_additiveTensorLeft_additive
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalPreadditive C]
(X : C)
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.instPreservesFiniteBiproductsPreadditiveHasZeroMorphismsTensorRightPreservesZeroMorphisms_of_additiveTensorRight_additive
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalPreadditive C]
(X : C)
:
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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 = Finset.sum Finset.univ fun (j : J) =>
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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 = Finset.sum Finset.univ fun (j : J) =>
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.π (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.Limits.biproduct.π f j))
h
@[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.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.biproduct.π f 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.tensorHom (CategoryTheory.CategoryStruct.id 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.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.tensorHom (CategoryTheory.CategoryStruct.id 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.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.tensorHom (CategoryTheory.CategoryStruct.id 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.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.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.Limits.biproduct.π (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj X (f j)) 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.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.Limits.biproduct.ι f 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.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.biproduct.ι f j)
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 (j : J) => CategoryTheory.MonoidalCategory.associator X Y (f j)
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
Instances For
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 = Finset.sum Finset.univ fun (j : J) =>
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id 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 = Finset.sum Finset.univ fun (j : J) =>
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biproduct.π (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id 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.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id X))
h
@[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.tensorHom (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.CategoryStruct.id X)
@[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.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id 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.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.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id X))
(CategoryTheory.rightDistributor f X).hom = 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.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id X))
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.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id X)) = CategoryTheory.Limits.biproduct.π (fun (j : J) => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j
@[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.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id X))
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.tensorHom (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.id X)
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 (j : J) => (CategoryTheory.MonoidalCategory.associator (f j) 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.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 (j : J) =>
(CategoryTheory.MonoidalCategory.associator X (f j) 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 : 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.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.Limits.biproduct.ι f j))
g = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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 : 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.tensorHom (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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 : 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}
(w : ∀ (j : J),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.Limits.biproduct.ι f j)))
g = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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 : 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))}
(w : ∀ (j : J),
CategoryTheory.CategoryStruct.comp g
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z)
(CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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 : 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.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id X))
g = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id 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 : 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.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id Y)) = CategoryTheory.CategoryStruct.comp h
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id 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 : 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}
(w : ∀ (j : J),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id X))
(CategoryTheory.CategoryStruct.id Y))
g = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.id X))
(CategoryTheory.CategoryStruct.id 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 : 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}
(w : ∀ (j : J),
CategoryTheory.CategoryStruct.comp g
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id Y))
(CategoryTheory.CategoryStruct.id Z)) = CategoryTheory.CategoryStruct.comp h
(CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.id Y))
(CategoryTheory.CategoryStruct.id Z)))
:
g = h