Documentation

Mathlib.CategoryTheory.GradedObject.Braiding

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.

source
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 : CategoryTheory.GradedObject I C) (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.
Instances For
    source
    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 : CategoryTheory.GradedObject I C} {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)
    source
    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 : CategoryTheory.GradedObject I C} {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)
    source
    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 : CategoryTheory.GradedObject I C) (Y : CategoryTheory.GradedObject I C) (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))
    source
    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 : CategoryTheory.GradedObject I C) (Y : CategoryTheory.GradedObject I C) (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))
    source
    @[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 : CategoryTheory.GradedObject I C) (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)
    source
    @[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 : CategoryTheory.GradedObject I C) (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
    source
    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.
    source
    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

    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.