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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C) [CategoryTheory.BraidedCategory C] [X.HasTensor Y] [Y.HasTensor X] : CategoryTheory.GradedObject.Monoidal.tensorObj X Y ≅ CategoryTheory.GradedObject.Monoidal.tensorObj Y 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.

theorem CategoryTheory.GradedObject.Monoidal.braiding_naturality_right {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.GradedObject I C) {Y Z : CategoryTheory.GradedObject I C} [CategoryTheory.BraidedCategory C] [X.HasTensor Y] [Y.HasTensor X] [X.HasTensor Z] [Z.HasTensor X] (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerLeft X f) (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom (CategoryTheory.GradedObject.Monoidal.whiskerRight f X)

theorem CategoryTheory.GradedObject.Monoidal.braiding_naturality_left {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.GradedObject I C} (Z : CategoryTheory.GradedObject I C) [CategoryTheory.BraidedCategory C] [Y.HasTensor Z] [Z.HasTensor Y] [X.HasTensor Z] [Z.HasTensor X] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight f Z) (CategoryTheory.GradedObject.Monoidal.braiding Y Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom (CategoryTheory.GradedObject.Monoidal.whiskerLeft Z f)

theorem CategoryTheory.GradedObject.Monoidal.hexagon_forward {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.GradedObject I C) [CategoryTheory.BraidedCategory C] [X.HasTensor Y] [Y.HasTensor X] [Y.HasTensor Z] [Z.HasTensor X] [X.HasTensor Z] [(CategoryTheory.GradedObject.Monoidal.tensorObj X Y).HasTensor Z] [X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y Z).HasTensor X] [Y.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Z X)] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y X).HasTensor Z] [Y.HasTensor (CategoryTheory.GradedObject.Monoidal.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] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)).hom (CategoryTheory.GradedObject.Monoidal.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator Y X Z).hom (CategoryTheory.GradedObject.Monoidal.whiskerLeft Y (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom))

theorem CategoryTheory.GradedObject.Monoidal.hexagon_reverse {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.GradedObject I C) [CategoryTheory.BraidedCategory C] [X.HasTensor Y] [Y.HasTensor Z] [Z.HasTensor X] [Z.HasTensor Y] [X.HasTensor Z] [(CategoryTheory.GradedObject.Monoidal.tensorObj X Y).HasTensor Z] [X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)] [Z.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)] [(CategoryTheory.GradedObject.Monoidal.tensorObj Z X).HasTensor Y] [X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Z Y)] [(CategoryTheory.GradedObject.Monoidal.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] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding (CategoryTheory.GradedObject.Monoidal.tensorObj X Y) Z).hom (CategoryTheory.GradedObject.Monoidal.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerLeft X (CategoryTheory.GradedObject.Monoidal.braiding Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Z Y).inv (CategoryTheory.GradedObject.Monoidal.whiskerRight (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom Y))

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.symmetry {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C) [CategoryTheory.SymmetricCategory C] [X.HasTensor Y] [Y.HasTensor X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom (CategoryTheory.GradedObject.Monoidal.braiding Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.symmetry_assoc {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C) [CategoryTheory.SymmetricCategory C] [X.HasTensor Y] [Y.HasTensor X] {Z : CategoryTheory.GradedObject I C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding Y X).hom h) = h

noncomputable instance CategoryTheory.GradedObject.braidedCategory {I : Type u_1} [AddCommMonoid I] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] [∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] [∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (CategoryTheory.GradedObject I C)

Equations

• CategoryTheory.GradedObject.symmetricCategory = CategoryTheory.SymmetricCategory.mk ⋯

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.