Preadditive monoidal categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A monoidal category is monoidal_preadditive if it is preadditive and tensor product of morphisms
is linear in both factors.
@[class]
structure
category_theory.monoidal_preadditive
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C] :
Prop
- tensor_zero' : (∀ {W X Y Z : C} (f : W ⟶ X), f ⊗ 0 = 0) . "obviously"
- zero_tensor' : (∀ {W X Y Z : C} (f : Y ⟶ Z), 0 ⊗ f = 0) . "obviously"
- tensor_add' : (∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h) . "obviously"
- add_tensor' : (∀ {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h) . "obviously"
A category is monoidal_preadditive 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.
@[simp]
theorem
category_theory.monoidal_preadditive.tensor_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : W ⟶ X) :
@[simp]
theorem
category_theory.monoidal_preadditive.zero_tensor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : Y ⟶ Z) :
theorem
category_theory.monoidal_preadditive.tensor_add
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f : W ⟶ X)
(g h : Y ⟶ Z) :
theorem
category_theory.monoidal_preadditive.add_tensor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[self : category_theory.monoidal_preadditive C]
{W X Y Z : C}
(f g : W ⟶ X)
(h : Y ⟶ Z) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.tensoring_left_additive
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_right_additive
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :
theorem
category_theory.monoidal_preadditive_of_faithful
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
{D : Type u_3}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.monoidal_category D]
(F : category_theory.monoidal_functor D C)
[category_theory.faithful F.to_lax_monoidal_functor.to_functor]
[F.to_lax_monoidal_functor.to_functor.additive] :
A faithful additive monoidal functor to a monoidal preadditive category ensures that the domain is monoidal preadditive.
theorem
category_theory.tensor_sum
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
{P Q R S : C}
{J : Type u_3}
(s : finset J)
(f : P ⟶ Q)
(g : J → (R ⟶ S)) :
theorem
category_theory.sum_tensor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
{P Q R S : C}
{J : Type u_3}
(s : finset J)
(f : P ⟶ Q)
(g : J → (R ⟶ S)) :
@[protected, instance]
def
category_theory.monoidal_category.tensor_left.limits.preserves_finite_biproducts
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :
Equations
- category_theory.monoidal_category.tensor_left.limits.preserves_finite_biproducts X = {preserves := λ (J : Type) (_x : fintype J), {preserves := λ (f : J → C), {preserves := λ (b : category_theory.limits.bicone f) (i : b.is_bilimit), category_theory.limits.is_bilimit_of_total ((category_theory.monoidal_category.tensor_left X).map_bicone b) _}}}
@[protected, instance]
def
category_theory.monoidal_category.tensor_right.limits.preserves_finite_biproducts
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
(X : C) :
Equations
- category_theory.monoidal_category.tensor_right.limits.preserves_finite_biproducts X = {preserves := λ (J : Type) (_x : fintype J), {preserves := λ (f : J → C), {preserves := λ (b : category_theory.limits.bicone f) (i : b.is_bilimit), category_theory.limits.is_bilimit_of_total ((category_theory.monoidal_category.tensor_right X).map_bicone b) _}}}
noncomputable
def
category_theory.left_distributor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
The isomorphism showing how tensor product on the left distributes over direct sums.
Equations
@[simp]
theorem
category_theory.left_distributor_hom
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
(category_theory.left_distributor X f).hom = finset.univ.sum (λ (j : J), (𝟙 X ⊗ category_theory.limits.biproduct.π f j) ≫ category_theory.limits.biproduct.ι (λ (j : J), X ⊗ f j) j)
@[simp]
theorem
category_theory.left_distributor_inv
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
(category_theory.left_distributor X f).inv = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π (λ (j : J), X ⊗ f j) j ≫ (𝟙 X ⊗ category_theory.limits.biproduct.ι f j))
theorem
category_theory.left_distributor_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X Y : C)
(f : J → C) :
(category_theory.as_iso (𝟙 X) ⊗ category_theory.left_distributor Y f) ≪≫ category_theory.left_distributor X (λ (j : J), Y ⊗ f j) = (α_ X Y (⨁ f)).symm ≪≫ category_theory.left_distributor (X ⊗ Y) f ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), α_ X Y (f j))
noncomputable
def
category_theory.right_distributor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
The isomorphism showing how tensor product on the right distributes over direct sums.
@[simp]
theorem
category_theory.right_distributor_hom
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
(category_theory.right_distributor X f).hom = finset.univ.sum (λ (j : J), (category_theory.limits.biproduct.π f j ⊗ 𝟙 X) ≫ category_theory.limits.biproduct.ι (λ (j : J), f j ⊗ X) j)
@[simp]
theorem
category_theory.right_distributor_inv
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X : C)
(f : J → C) :
(category_theory.right_distributor X f).inv = finset.univ.sum (λ (j : J), category_theory.limits.biproduct.π (λ (j : J), f j ⊗ X) j ≫ (category_theory.limits.biproduct.ι f j ⊗ 𝟙 X))
theorem
category_theory.right_distributor_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X Y : C)
(f : J → C) :
(category_theory.right_distributor X f ⊗ category_theory.as_iso (𝟙 Y)) ≪≫ category_theory.right_distributor Y (λ (j : J), f j ⊗ X) = α_ (⨁ f) X Y ≪≫ category_theory.right_distributor (X ⊗ Y) f ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), (α_ (f j) X Y).symm)
theorem
category_theory.left_distributor_right_distributor_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_finite_biproducts C]
{J : Type}
[fintype J]
(X Y : C)
(f : J → C) :
(category_theory.left_distributor X f ⊗ category_theory.as_iso (𝟙 Y)) ≪≫ category_theory.right_distributor Y (λ (j : J), X ⊗ f j) = α_ X (⨁ f) Y ≪≫ (category_theory.as_iso (𝟙 X) ⊗ category_theory.right_distributor Y f) ≪≫ category_theory.left_distributor X (λ (j : J), f j ⊗ Y) ≪≫ category_theory.limits.biproduct.map_iso (λ (j : J), (α_ X (f j) Y).symm)