Pivotal structures from balanced structures

On a braided rigid category, balanced structures and pivotal structures determine each other. If u_X : X ≅ Xᘁᘁ is the Drinfeld isomorphism, a twist θ gives the pivotal isomorphism φ_X = θ_X ≫ u_X. The balancing axiom cancels the failure of u to be monoidal. Conversely, the twist associated to a pivotal structure is θ_X = φ_X ≫ u_X⁻¹.

This file constructs the inverse of balancedOfBraidedPivotal, proves both round trips as equalities of structures, and packages them as pivotalBalancedEquiv. No semisimplicity, sphericity, or compatibility of the twist with duals is required.

References

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

@[instance_reducible]

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

The pivotal structure associated to a balanced rigid category: its pivotal isomorphism is its twist followed by the Drinfeld isomorphism. This is not an instance, since it depends on the chosen twist.

@[simp]

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

The pivotal isomorphism obtained from a twist is θ_X ≫ u_X.

@[simp]

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

The inverse pivotal isomorphism obtained from a twist is u_X⁻¹ ≫ θ_X⁻¹.

@[simp]

theorem TauCeti.pivotalOfBalanced_balancedOfBraidedPivotal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] (P : PivotalCategory C) : pivotalOfBalanced C = P

Passing from a pivotal structure to its twist and back recovers the pivotal structure.

@[simp]

theorem TauCeti.balancedOfBraidedPivotal_pivotalOfBalanced {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] (B : BalancedCategory C) : balancedOfBraidedPivotal C = B

Passing from a twist to its pivotal structure and back recovers the balanced structure.

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

Pivotal structures on a braided rigid category correspond to balanced structures via θ_X = φ_X ≫ u_X⁻¹, with inverse φ_X = θ_X ≫ u_X.

@[simp]

theorem TauCeti.pivotalBalancedEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] (P : PivotalCategory C) : (pivotalBalancedEquiv C) P = balancedOfBraidedPivotal C

The forward map of the correspondence constructs the twist of a pivotal structure.

@[simp]

theorem TauCeti.pivotalBalancedEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.RigidCategory C] (B : BalancedCategory C) : (pivotalBalancedEquiv C).symm B = pivotalOfBalanced C

The inverse correspondence constructs the pivotal structure of a twist.