The braided and symmetric category structures on graded objects #
In this file, we construct the braiding
GradedObject.Monoidal.braiding : tensorObj X Y ≅ tensorObj Y X
for two objects X and Y in GradedObject I C, when I is a commutative
additive monoid (and suitable coproducts exist in a braided category C).
When C is a braided category and suitable assumptions are made, we obtain the braided category
structure on GradedObject I C and show that it is symmetric if C is symmetric.
noncomputable def
CategoryTheory.GradedObject.Monoidal.braiding
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X Y : GradedObject I C)
[BraidedCategory C]
[X.HasTensor Y]
[Y.HasTensor X]
:
The braiding tensorObj X Y ≅ tensorObj Y X when X and Y are graded objects
indexed by a commutative additive monoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GradedObject.Monoidal.braiding_naturality_right
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X : GradedObject I C)
{Y Z : GradedObject I C}
[BraidedCategory C]
[X.HasTensor Y]
[Y.HasTensor X]
[X.HasTensor Z]
[Z.HasTensor X]
(f : Y ⟶ Z)
:
CategoryStruct.comp (whiskerLeft X f) (braiding X Z).hom = CategoryStruct.comp (braiding X Y).hom (whiskerRight f X)
theorem
CategoryTheory.GradedObject.Monoidal.braiding_naturality_left
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
{X Y : GradedObject I C}
(Z : GradedObject I C)
[BraidedCategory C]
[Y.HasTensor Z]
[Z.HasTensor Y]
[X.HasTensor Z]
[Z.HasTensor X]
(f : X ⟶ Y)
:
CategoryStruct.comp (whiskerRight f Z) (braiding Y Z).hom = CategoryStruct.comp (braiding X Z).hom (whiskerLeft Z f)
theorem
CategoryTheory.GradedObject.Monoidal.hexagon_forward
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X Y Z : GradedObject I C)
[BraidedCategory C]
[X.HasTensor Y]
[Y.HasTensor X]
[Y.HasTensor Z]
[Z.HasTensor X]
[X.HasTensor Z]
[(tensorObj X Y).HasTensor Z]
[X.HasTensor (tensorObj Y Z)]
[(tensorObj Y Z).HasTensor X]
[Y.HasTensor (tensorObj Z X)]
[(tensorObj Y X).HasTensor Z]
[Y.HasTensor (tensorObj X Z)]
[X.HasGoodTensor₁₂Tensor Y Z]
[X.HasGoodTensorTensor₂₃ Y Z]
[Y.HasGoodTensor₁₂Tensor Z X]
[Y.HasGoodTensorTensor₂₃ Z X]
[Y.HasGoodTensor₁₂Tensor X Z]
[Y.HasGoodTensorTensor₂₃ X Z]
:
CategoryStruct.comp (associator X Y Z).hom
(CategoryStruct.comp (braiding X (tensorObj Y Z)).hom (associator Y Z X).hom) = CategoryStruct.comp (whiskerRight (braiding X Y).hom Z)
(CategoryStruct.comp (associator Y X Z).hom (whiskerLeft Y (braiding X Z).hom))
theorem
CategoryTheory.GradedObject.Monoidal.hexagon_reverse
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X Y Z : GradedObject I C)
[BraidedCategory C]
[X.HasTensor Y]
[Y.HasTensor Z]
[Z.HasTensor X]
[Z.HasTensor Y]
[X.HasTensor Z]
[(tensorObj X Y).HasTensor Z]
[X.HasTensor (tensorObj Y Z)]
[Z.HasTensor (tensorObj X Y)]
[(tensorObj Z X).HasTensor Y]
[X.HasTensor (tensorObj Z Y)]
[(tensorObj X Z).HasTensor Y]
[X.HasGoodTensor₁₂Tensor Y Z]
[X.HasGoodTensorTensor₂₃ Y Z]
[Z.HasGoodTensor₁₂Tensor X Y]
[Z.HasGoodTensorTensor₂₃ X Y]
[X.HasGoodTensor₁₂Tensor Z Y]
[X.HasGoodTensorTensor₂₃ Z Y]
:
CategoryStruct.comp (associator X Y Z).inv
(CategoryStruct.comp (braiding (tensorObj X Y) Z).hom (associator Z X Y).inv) = CategoryStruct.comp (whiskerLeft X (braiding Y Z).hom)
(CategoryStruct.comp (associator X Z Y).inv (whiskerRight (braiding X Z).hom Y))
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.symmetry
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X Y : GradedObject I C)
[SymmetricCategory C]
[X.HasTensor Y]
[Y.HasTensor X]
:
@[simp]
theorem
CategoryTheory.GradedObject.Monoidal.symmetry_assoc
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
(X Y : GradedObject I C)
[SymmetricCategory C]
[X.HasTensor Y]
[Y.HasTensor X]
{Z : GradedObject I C}
(h : tensorObj X Y ⟶ Z)
:
noncomputable instance
CategoryTheory.GradedObject.braidedCategory
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
[∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂]
[∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃]
[∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃]
[DecidableEq I]
[Limits.HasInitial C]
[∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)]
[∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)]
[∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄]
[BraidedCategory C]
:
BraidedCategory (GradedObject I C)
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.GradedObject.symmetricCategory
{I : Type u_1}
[AddCommMonoid I]
{C : Type u_2}
[Category.{u_3, u_2} C]
[MonoidalCategory C]
[∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂]
[∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃]
[∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃]
[DecidableEq I]
[Limits.HasInitial C]
[∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)]
[∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)]
[∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄]
[SymmetricCategory C]
:
Equations
- CategoryTheory.GradedObject.symmetricCategory = { toBraidedCategory := CategoryTheory.GradedObject.braidedCategory, symmetry := ⋯ }
The braided/symmetric monoidal category structure on GradedObject ℕ C can
be inferred from the assumptions [HasFiniteCoproducts C],
[∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).obj X)] and
[∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).flip.obj X)].
This requires importing Mathlib/CategoryTheory/Limits/Preserves/Finite.lean.