Frobenius–Schur rotation in symmetric rigid categories

In a symmetric rigid category C equipped with its canonical spherical structure (TauCeti.symmetricPivotalCategory), rotating a morphism f : 𝟙_ C ⟶ X ⊗ Y with TauCeti.pivotalRotate simply postcomposes f with the braiding (β_ X Y).hom (TauCeti.pivotalRotate_eq_braiding): by Frobenius reciprocity every such f factors through the coevaluation η_ X Xᘁ, whose rotation is η_ X Xᘁ ≫ (β_ X Xᘁ).hom.

Consequently, the Ng–Schauenburg operator TauCeti.frobeniusSchurRotate V n on 𝟙_ C ⟶ tensorPow V (n + 1) is postcomposition with the cyclic shift TauCeti.tensorPowShiftIso V n (TauCeti.frobeniusSchurRotate_eq_comp_tensorPowShiftIso_hom), and TauCeti.frobeniusSchurEnd k V n equals CategoryTheory.Linear.rightComp k (𝟙_ C) (tensorPowShiftIso V n).hom (TauCeti.frobeniusSchurEnd_eq_rightComp).

Main declarations

• TauCeti.pivotalRotate_eq_braiding: in a symmetric rigid category, pivotalRotate f = f ≫ (β_ X Y).hom;
• TauCeti.frobeniusSchurRotate_eq_comp_tensorPowShiftIso_hom, TauCeti.frobeniusSchurEnd_eq_rightComp, and TauCeti.frobeniusSchurIndicator_eq_trace_rightComp: E_V^{(n+1)} is postcomposition with the cyclic shift tensorPowShiftIso V n, so ν_n(V) is the trace of postcomposition with tensorPowShiftIso V n.natPred.

References

• S.-H. Ng, P. Schauenburg, Higher Frobenius–Schur indicators for pivotal categories, in Hopf algebras and generalizations, Contemp. Math. 441 (2007), 63–90, §§4–5
• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §8.10

theorem TauCeti.pivotalRotate_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X Y : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) : pivotalRotate f = CategoryTheory.CategoryStruct.comp f (β_ X Y).hom

In a symmetric rigid category with its canonical pivotal structure, rotating f : 𝟙_ C ⟶ X ⊗ Y postcomposes f with the braiding (β_ X Y).hom.

theorem TauCeti.frobeniusSchurRotate_eq_comp_tensorPowShiftIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (V : C) (n : ℕ) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ tensorPow V (n + 1)) : frobeniusSchurRotate V n f = CategoryTheory.CategoryStruct.comp f (tensorPowShiftIso V n).hom

In a symmetric rigid category, frobeniusSchurRotate V n postcomposes with the cyclic shift (tensorPowShiftIso V n).hom.

theorem TauCeti.frobeniusSchurEnd_eq_rightComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (k : Type w) [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) (n : ℕ) : frobeniusSchurEnd k V n = CategoryTheory.Linear.rightComp k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (tensorPowShiftIso V n).hom

In a k-linear symmetric rigid category, frobeniusSchurEnd k V n is postcomposition with (tensorPowShiftIso V n).hom.

theorem TauCeti.frobeniusSchurIndicator_succPNat_eq_trace_rightComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (k : Type w) [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) (n : ℕ) : frobeniusSchurIndicator k V n.succPNat = (LinearMap.trace k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ tensorPow V (n + 1))) (CategoryTheory.Linear.rightComp k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (tensorPowShiftIso V n).hom)

In a k-linear symmetric rigid category, ν_{n+1}(V) is the trace of postcomposition with (tensorPowShiftIso V n).hom on 𝟙_ C ⟶ tensorPow V (n + 1).

theorem TauCeti.frobeniusSchurIndicator_eq_trace_rightComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (k : Type w) [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (V : C) (n : ℕ+) : frobeniusSchurIndicator k V n = (LinearMap.trace k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ tensorPow V (n.natPred + 1))) (CategoryTheory.Linear.rightComp k (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (tensorPowShiftIso V n.natPred).hom)

In a k-linear symmetric rigid category, ν_n(V) is the trace of postcomposition with (tensorPowShiftIso V n.natPred).hom on 𝟙_ C ⟶ tensorPow V (n.natPred + 1).