The twist of a braided pivotal category

A braided rigid category with a pivotal structure φ : 𝟭 C ≅ (-)ᘁᘁ is balanced. Its twist compares the pivotal isomorphism with the Drinfeld isomorphism u_X : X ≅ Xᘁᘁ built from the braiding: θ_X = φ_X ≫ u_X⁻¹. Unfolding u_X⁻¹ (TauCeti.drinfeldIso_inv_eq) gives the explicit formula θ_X = φ_X ≫ (𝟙_{Xᘁᘁ} ⊗ η_X) ≫ (β_{Xᘁᘁ, X} ⊗ 𝟙_{Xᘁ}) ≫ (𝟙_X ⊗ ε_{Xᘁ}) of Henriques–Penneys–Tener, eq. (3), up to associators and unitors.

The balancing axiom holds because the pivotal isomorphism is monoidal, while the Drinfeld isomorphism of X ⊗ Y differs from the tensor product of those of X and Y exactly by the double braiding (TauCeti.braiding_hom_comp_braiding_hom_comp_drinfeldIso_tensor_hom).

In a symmetric rigid category with its canonical pivotal structure, whose components are the Drinfeld isomorphisms, the twist is trivial.

Main declarations

• TauCeti.balancedOfBraidedPivotal: the balanced structure of a braided pivotal category;
• TauCeti.balancedOfBraidedPivotal_twist_hom_app: its twist is φ_X ≫ u_X⁻¹;
• TauCeti.balancedOfBraidedPivotal_twist_eq_refl: in a symmetric rigid category with its canonical pivotal structure, the twist is the identity.

References

• A. Henriques, D. Penneys, J. Tener, Categorified trace for module tensor categories over braided tensor categories, arXiv:1509.02937, §2.1, eq. (3)
• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §8.10

@[instance_reducible]

noncomputable def TauCeti.balancedOfBraidedPivotal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : BalancedCategory C

The balanced structure of a braided pivotal category. Its twist θ_X = φ_X ≫ u_X⁻¹ compares the pivotal isomorphism φ_X : X ≅ Xᘁᘁ with the Drinfeld isomorphism u_X : X ≅ Xᘁᘁ. This is not an instance: the twist depends on the chosen pivotal structure.

@[simp]

theorem TauCeti.balancedOfBraidedPivotal_twist_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : BalancedCategory.twist.hom.app X = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).hom (drinfeldIso X).inv

The twist of a braided pivotal category is the pivotal isomorphism followed by the inverse Drinfeld isomorphism.

@[simp]

theorem TauCeti.balancedOfBraidedPivotal_twist_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : BalancedCategory.twist.inv.app X = CategoryTheory.CategoryStruct.comp (drinfeldIso X).hom (pivotalIsoApp X).inv

The inverse twist of a braided pivotal category is the Drinfeld isomorphism followed by the inverse pivotal isomorphism.

theorem TauCeti.balancedOfBraidedPivotal_twist_eq_refl (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] : BalancedCategory.twist = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)

In a symmetric rigid category with its canonical pivotal structure, the twist is the identity.