Documentation

TauCeti.CategoryTheory.Monoidal.Braided.TensorPow

Cyclic shifts of tensor powers in braided monoidal categories #

In a braided monoidal category C, the first factor of tensorPow X (n + 1) = X ⊗ tensorPow X n can be braided past tensorPow X n and re-bracketed onto the right using tensorPowSuccIso X n. This gives the cyclic shift automorphism TauCeti.tensorPowShiftIso X n of tensorPow X (n + 1).

For n = 0 the shift is the identity (TauCeti.tensorPowShiftIso_zero), and for n + 1 it factors into a single braiding of the first two factors followed by the shift on the remaining n + 1 factors (TauCeti.tensorPowShiftIso_succ_hom). In a symmetric rigid category with its canonical pivotal structure (TauCeti.symmetricPivotalCategory), composing with tensorPowShiftIso X n computes the Ng–Schauenburg Frobenius–Schur rotation operator.

Main declarations #

source
def TauCeti.tensorPowShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (n : ℕ) :
tensorPow X (n + 1) ≅ tensorPow X (n + 1)

The cyclic shift automorphism of tensorPow X (n + 1) in a braided monoidal category: braid the first factor X past tensorPow X n and re-bracket on the right.

Instances For
    source
    theorem TauCeti.tensorPowShiftIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (n : ℕ) :
    (tensorPowShiftIso X n).hom = CategoryTheory.CategoryStruct.comp (β_ X (tensorPow X n)).hom (tensorPowSuccIso X n).hom

    The forward morphism of tensorPowShiftIso.

    source
    theorem TauCeti.tensorPowShiftIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (n : ℕ) :
    (tensorPowShiftIso X n).inv = CategoryTheory.CategoryStruct.comp (tensorPowSuccIso X n).inv (β_ X (tensorPow X n)).inv

    The inverse morphism of tensorPowShiftIso.

    source
    @[simp]
    theorem TauCeti.tensorPowShiftIso_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) :
    tensorPowShiftIso X 0 = CategoryTheory.Iso.refl (tensorPow X 1)

    On the first tensor power X ⊗ 𝟙_ C, the cyclic shift is the identity.

    source
    theorem TauCeti.tensorPowShiftIso_succ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (n : ℕ) :
    (tensorPowShiftIso X (n + 1)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X (tensorPow X n)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X X).hom (tensorPow X n)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X (tensorPow X n)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (tensorPowShiftIso X n).hom)))

    Recursive decomposition of the cyclic shift on tensorPow X (n + 2): swap the first two factors with the braiding, then apply the cyclic shift on the remaining n + 1 factors.

    source
    theorem TauCeti.tensorPowShiftIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + 1)) (tensorPowShiftIso Y n).hom = CategoryTheory.CategoryStruct.comp (tensorPowShiftIso X n).hom (tensorPowMap f (n + 1))

    The cyclic shift commutes with the tensor powers of any morphism.

    source
    theorem TauCeti.tensorPowShiftIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (n : ℕ) {Z : C} (h : tensorPow Y (n + 1) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + 1)) (CategoryTheory.CategoryStruct.comp (tensorPowShiftIso Y n).hom h) = CategoryTheory.CategoryStruct.comp (tensorPowShiftIso X n).hom (CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + 1)) h)

    The cyclic shift commutes with the tensor powers of any morphism.