Pivotal categories

A pivotal structure on a rigid monoidal category C is a monoidal natural isomorphism φ : 𝟭 C ≅ doubleRightDualFunctor C from the identity functor to the double right dual functor X ↦ Xᘁᘁ. Monoidality is Mathlib's NatTrans.IsMonoidal, taken with respect to the strong monoidal structure on doubleRightDualFunctor C; a bare natural isomorphism to the double dual is not a pivotal structure. A pivotal structure is what makes the left and right categorical traces of an endomorphism, and the left and right dimensions of an object, definable.

Unwinding the definition, the components φ_X : X ≅ Xᘁᘁ are natural in X, so that the double mate of a morphism is its conjugate by φ, and they are compatible with the unit and tensor comparisons of the double right dual functor. The classical definition of Freyd and Yetter adds a further axiom φ_{Xᘁ} = (φ_X⁻¹)ᘁ. This axiom is redundant: it follows from monoidality, because the double right dual functor carries the evaluation of (X, Xᘁ) to the evaluation of (Xᘁᘁ, Xᘁᘁᘁ).

Through φ_X, the object X becomes a right dual of Xᘁ, so in a pivotal category every right dual is also a left dual. The same observation shows that a pivotal structure needs only right duals to make sense: in a right rigid category, a monoidal natural isomorphism 𝟭 C ≅ doubleRightDualFunctor C makes Xᘁ a left dual of X, and is then a pivotal structure for the resulting rigid structure.

Main declarations

• TauCeti.PivotalCategory: a pivotal structure on a rigid monoidal category, with fields pivotalIso and the instance pivotalIso_isMonoidal;
• TauCeti.pivotalIsoApp: the component φ_X : X ≅ Xᘁᘁ;
• TauCeti.pivotalIsoApp_hom_naturality and TauCeti.rightAdjointMate_rightAdjointMate: the double mate fᘁᘁ of f : X ⟶ Y is φ_X⁻¹ ≫ f ≫ φ_Y;
• TauCeti.pivotalIsoApp_unit_hom, TauCeti.pivotalIsoApp_unit_inv and TauCeti.pivotalIsoApp_tensor_hom: monoidality of φ, in components;
• TauCeti.pivotalIsoApp_rightDual: the Freyd–Yetter identity φ_{Xᘁ} = (φ_X⁻¹)ᘁ, with its inverse form TauCeti.pivotalIsoApp_rightDual_inv;
• TauCeti.pivotalExactPairing: the exact pairing ExactPairing Xᘁ X obtained from φ_X, whose evaluation and coevaluation are dinatural by TauCeti.whiskerLeft_rightAdjointMate_comp_pivotalIsoApp_hom_whiskerRight and TauCeti.pivotalExactPairing_coevaluation_comp_rightAdjointMate_whiskerRight;
• TauCeti.pivotalCategoryOfRightRigid: a monoidal trivialization of the double right dual functor of a right rigid category is a pivotal structure for the rigid structure TauCeti.rigidCategoryOfIsoDoubleRightDual, whose left duals are the right duals.

References

• [P. Freyd, D. Yetter, Braided compact closed categories with applications to low-dimensional topology][freydyetter1989]
• [P. Selinger, A survey of graphical languages for monoidal categories][selinger2011], Lemma 4.11, for the redundancy of the Freyd–Yetter axiom
• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.7
• leanprover-community/mathlib4#42150, for the names PivotalCategory, pivotalIso, pivotalExactPairing and rightAdjointMate_rightAdjointMate

class TauCeti.PivotalCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] : Type (max u v)

A pivotal structure on a rigid monoidal category C: a monoidal natural isomorphism 𝟭 C ≅ doubleRightDualFunctor C from the identity functor to the double right dual functor.

• pivotalIso : CategoryTheory.Functor.id C ≅ doubleRightDualFunctor C

  The pivotal isomorphism, with components X ≅ Xᘁᘁ.

• pivotalIso_isMonoidal : CategoryTheory.NatTrans.IsMonoidal pivotalIso.hom

  The pivotal isomorphism is a monoidal natural transformation.

theorem TauCeti.PivotalCategory.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.RigidCategory C} {x y : PivotalCategory C} (pivotalIso : pivotalIso = pivotalIso) : x = y

theorem TauCeti.PivotalCategory.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.RigidCategory C} {x y : PivotalCategory C} : x = y ↔ pivotalIso = pivotalIso

noncomputable def TauCeti.pivotalIsoApp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : X ≅ Xᘁᘁ

The component φ_X : X ≅ Xᘁᘁ of the pivotal structure.

@[simp]

theorem TauCeti.pivotalIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : PivotalCategory.pivotalIso.hom.app X = (pivotalIsoApp X).hom

The components of the pivotal isomorphism are the morphisms (pivotalIsoApp X).hom.

@[simp]

theorem TauCeti.pivotalIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : PivotalCategory.pivotalIso.inv.app X = (pivotalIsoApp X).inv

The components of the inverse of the pivotal isomorphism are the morphisms (pivotalIsoApp X).inv.

theorem TauCeti.pivotalIsoApp_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (pivotalIsoApp Y).hom = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).hom (fᘁᘁ)

Naturality of the pivotal isomorphism.

theorem TauCeti.pivotalIsoApp_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Yᘁᘁ ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (pivotalIsoApp Y).hom h) = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).hom (CategoryTheory.CategoryStruct.comp (fᘁᘁ) h)

Naturality of the pivotal isomorphism.

theorem TauCeti.pivotalIsoApp_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (fᘁᘁ) (pivotalIsoApp Y).inv = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).inv f

Naturality of the inverse of the pivotal isomorphism.

theorem TauCeti.pivotalIsoApp_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (fᘁᘁ) (CategoryTheory.CategoryStruct.comp (pivotalIsoApp Y).inv h) = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).inv (CategoryTheory.CategoryStruct.comp f h)

Naturality of the inverse of the pivotal isomorphism.

theorem TauCeti.rightAdjointMate_rightAdjointMate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) : fᘁᘁ = CategoryTheory.CategoryStruct.comp (pivotalIsoApp X).inv (CategoryTheory.CategoryStruct.comp f (pivotalIsoApp Y).hom)

In a pivotal category, the double mate fᘁᘁ of f : X ⟶ Y is the conjugate φ_X⁻¹ ≫ f ≫ φ_Y of f by the pivotal isomorphism.

theorem TauCeti.pivotalIsoApp_unit_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : (pivotalIsoApp (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom = CategoryTheory.Functor.LaxMonoidal.ε (doubleRightDualFunctor C)

The component of the pivotal isomorphism at the unit is the unit comparison of the double right dual functor.

theorem TauCeti.pivotalIsoApp_unit_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] : (pivotalIsoApp (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv = CategoryTheory.Functor.OplaxMonoidal.η (doubleRightDualFunctor C)

The inverse of the component of the pivotal isomorphism at the unit is the inverse unit comparison of the double right dual functor.

theorem TauCeti.pivotalIsoApp_tensor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X Y : C) : (pivotalIsoApp (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (pivotalIsoApp X).hom (pivotalIsoApp Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ (doubleRightDualFunctor C) X Y)

The component of the pivotal isomorphism at a tensor product is the tensor product of the components, followed by the tensor comparison of the double right dual functor.

theorem TauCeti.pivotalIsoApp_tensorHom_comp_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (pivotalIsoApp Xᘁ).hom (pivotalIsoApp X).hom) (ε_ Xᘁᘁ Xᘁᘁᘁ) = ε_ X Xᘁ

The tensor product of the components of the pivotal isomorphism at Xᘁ and at X carries the evaluation of (Xᘁᘁ, Xᘁᘁᘁ) back to the evaluation of (X, Xᘁ).

theorem TauCeti.pivotalIsoApp_tensorHom_comp_evaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (pivotalIsoApp Xᘁ).hom (pivotalIsoApp X).hom) (CategoryTheory.CategoryStruct.comp (ε_ Xᘁᘁ Xᘁᘁᘁ) h) = CategoryTheory.CategoryStruct.comp (ε_ X Xᘁ) h

The tensor product of the components of the pivotal isomorphism at Xᘁ and at X carries the evaluation of (Xᘁᘁ, Xᘁᘁᘁ) back to the evaluation of (X, Xᘁ).

theorem TauCeti.pivotalIsoApp_rightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : (pivotalIsoApp Xᘁ).hom = (pivotalIsoApp X).invᘁ

The Freyd–Yetter identity: the component of the pivotal isomorphism at Xᘁ is the mate of the inverse of its component at X.

theorem TauCeti.pivotalIsoApp_rightDual_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : (pivotalIsoApp Xᘁ).inv = (pivotalIsoApp X).homᘁ

The inverse form of the Freyd–Yetter identity: the inverse of the component of the pivotal isomorphism at Xᘁ is the mate of its component at X.

@[instance_reducible]

noncomputable def TauCeti.pivotalExactPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : CategoryTheory.ExactPairing Xᘁ X

In a pivotal category, X is a right dual of Xᘁ: the pairing of Xᘁ with its right dual Xᘁᘁ, transported along φ_X : X ≅ Xᘁᘁ.

theorem TauCeti.pivotalExactPairing_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : pivotalExactPairing X = CategoryTheory.exactPairingCongrRight (pivotalIsoApp X)

The pivotal pairing is the right transport of the chosen pairing along the pivotal isomorphism.

theorem TauCeti.pivotalExactPairing_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : ε_ Xᘁ X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pivotalIsoApp X).hom Xᘁ) (ε_ Xᘁ Xᘁᘁ)

The evaluation X ⊗ Xᘁ ⟶ 𝟙_ C of pivotalExactPairing X.

theorem TauCeti.pivotalExactPairing_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] (X : C) : η_ Xᘁ X = CategoryTheory.CategoryStruct.comp (η_ Xᘁ Xᘁᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ (pivotalIsoApp X).inv)

The coevaluation 𝟙_ C ⟶ Xᘁ ⊗ X of pivotalExactPairing X.

theorem TauCeti.whiskerLeft_rightAdjointMate_comp_pivotalIsoApp_hom_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (fᘁ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pivotalIsoApp X).hom Xᘁ) (ε_ Xᘁ Xᘁᘁ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Yᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pivotalIsoApp Y).hom Yᘁ) (ε_ Yᘁ Yᘁᘁ))

The evaluation of the pivotal pairing is dinatural: for f : X ⟶ Y, pairing X with Yᘁ through fᘁ or through f gives the same morphism.

theorem TauCeti.whiskerLeft_rightAdjointMate_comp_pivotalIsoApp_hom_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (fᘁ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pivotalIsoApp X).hom Xᘁ) (CategoryTheory.CategoryStruct.comp (ε_ Xᘁ Xᘁᘁ) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Yᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pivotalIsoApp Y).hom Yᘁ) (CategoryTheory.CategoryStruct.comp (ε_ Yᘁ Yᘁᘁ) h))

The evaluation of the pivotal pairing is dinatural: for f : X ⟶ Y, pairing X with Yᘁ through fᘁ or through f gives the same morphism.

theorem TauCeti.pivotalExactPairing_coevaluation_comp_rightAdjointMate_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (η_ Yᘁ Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (fᘁ) Y) = CategoryTheory.CategoryStruct.comp (η_ Xᘁ X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ f)

The coevaluation of the pivotal pairing is dinatural: for f : X ⟶ Y, pairing Yᘁ with Y and then applying fᘁ, or pairing Xᘁ with X and then applying f, gives the same morphism.

theorem TauCeti.pivotalExactPairing_coevaluation_comp_rightAdjointMate_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] [PivotalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Xᘁ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (η_ Yᘁ Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (fᘁ) Y) h) = CategoryTheory.CategoryStruct.comp (η_ Xᘁ X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ f) h)

The coevaluation of the pivotal pairing is dinatural: for f : X ⟶ Y, pairing Yᘁ with Y and then applying fᘁ, or pairing Xᘁ with X and then applying f, gives the same morphism.

@[instance_reducible]

noncomputable def TauCeti.pivotalCategoryOfRightRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (φ : CategoryTheory.Functor.id C ≅ doubleRightDualFunctor C) [CategoryTheory.NatTrans.IsMonoidal φ.hom] : PivotalCategory C

A monoidal trivialization φ : 𝟭 C ≅ doubleRightDualFunctor C of the double right dual functor of a right rigid category is a pivotal structure, for the rigid structure whose left duals are the right duals, paired with X through φ.

theorem TauCeti.pivotalIsoApp_pivotalCategoryOfRightRigid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] (φ : CategoryTheory.Functor.id C ≅ doubleRightDualFunctor C) [CategoryTheory.NatTrans.IsMonoidal φ.hom] (X : C) : pivotalIsoApp X = φ.app X

The components of the pivotal structure built from a monoidal trivialization φ of the double right dual are the components of φ.