Documentation

TauCeti.CategoryTheory.Monoidal.Pivotal.Symmetric

The canonical pivotal structure on a symmetric rigid category #

In a symmetric rigid category the Drinfeld isomorphisms drinfeldIso X : X ≅ Xᘁᘁ form a monoidal natural isomorphism drinfeldNatIso : 𝟭 C ≅ doubleRightDualFunctor C (TauCeti.drinfeldNatIso_isMonoidal). Hence every symmetric rigid category carries a canonical pivotal structure, registered as the instance TauCeti.symmetricPivotalCategory.

Through the Drinfeld isomorphism, the pivotal pairing of X becomes the braided swap of the pairing (X, Xᘁ), so both traces are computed by the braiding: rightTrace f = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ (β_ X Xᘁ).hom ≫ ε_ X Xᘁ and leftTrace f = η_ X Xᘁ ≫ (β_ X Xᘁ).hom ≫ Xᘁ ◁ f ≫ ε_ X Xᘁ. Naturality of the braiding then shows that the left and right traces of every endomorphism agree: the canonical pivotal structure is spherical, registered as the instance TauCeti.symmetricSphericalCategory.

Contracting the cyclic shift TauCeti.tensorPowShiftIso X n against the tensor power TauCeti.tensorPowMap f (n + 1) of an endomorphism f : X ⟶ X inside the categorical trace yields the categorical trace of the (n + 1)-st iterate (End.of f ^ (n + 1)).asHom (TauCeti.trace_tensorPowMap_comp_tensorPowShiftIso_hom), and in particular the trace of the cyclic shift itself is quantumDim X (TauCeti.trace_tensorPowShiftIso_hom).

Main declarations #

References #

source
@[instance_reducible]
noncomputable instance TauCeti.symmetricPivotalCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] :
PivotalCategory C

The canonical pivotal structure on a symmetric rigid category, given by the Drinfeld isomorphisms.

source
@[simp]
theorem TauCeti.pivotalIsoApp_eq_drinfeldIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) :
pivotalIsoApp X = drinfeldIso X

The components of the canonical pivotal structure on a symmetric rigid category are the Drinfeld isomorphisms.

source
theorem TauCeti.pivotalExactPairing_coevaluation_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) :
η_ Xᘁ X = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (β_ X Xᘁ).hom

In a symmetric rigid category, the coevaluation of pivotalExactPairing X is the coevaluation of (X, Xᘁ) followed by the braiding.

source
theorem TauCeti.pivotalExactPairing_evaluation_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) :
ε_ Xᘁ X = CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (ε_ X Xᘁ)

In a symmetric rigid category, the evaluation of pivotalExactPairing X is the braiding followed by the evaluation of (X, Xᘁ).

source
theorem TauCeti.rightTrace_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) :
rightTrace f = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ) (CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (ε_ X Xᘁ)))

In a symmetric rigid category with its canonical pivotal structure, the right trace of f closes up f with the coevaluation of (X, Xᘁ) and the braided evaluation.

source
theorem TauCeti.leftTrace_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) :
leftTrace f = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ f) (ε_ X Xᘁ)))

In a symmetric rigid category with its canonical pivotal structure, the left trace of f closes up f with the braided coevaluation and the evaluation of (X, Xᘁ).

source
theorem TauCeti.leftTrace_eq_rightTrace_of_symmetric {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) :
leftTrace f = rightTrace f

In a symmetric rigid category with its canonical pivotal structure, the left and right traces of every endomorphism agree.

source
instance TauCeti.symmetricSphericalCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] :
SphericalCategory C

The canonical pivotal structure on a symmetric rigid category is spherical.

source
theorem TauCeti.trace_eq_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) :
trace f = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ) (CategoryTheory.CategoryStruct.comp (β_ X Xᘁ).hom (ε_ X Xᘁ)))

In a symmetric rigid category with its canonical spherical structure, the trace of f closes up f with the coevaluation of (X, Xᘁ) and the braided evaluation.

source
theorem TauCeti.trace_associator_inv_braiding_whiskerRight_associator_hom_comp_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z) :
trace (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X X).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X h)))) = trace h

Contracting the first two factors of (α_ X X Z)⁻¹ ≫ β_{X,X} ▷ Z ≫ α_ X X Z ≫ X ◁ h in the categorical trace leaves the trace of h : X ⊗ Z ⟶ X ⊗ Z.

source
theorem TauCeti.trace_tensorHom_tensorPowMap_comp_tensorPowShiftIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (a f : X ⟶ X) (n : ℕ) :
trace (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a (tensorPowMap f n)) (tensorPowShiftIso X n).hom) = trace (CategoryTheory.CategoryStruct.comp ({ asHom := f } ^ n).asHom a)

Cyclic power-trace induction: in a symmetric rigid category, the categorical trace of (a ⊗ₘ tensorPowMap f n) ≫ (tensorPowShiftIso X n).hom on tensorPow X (n + 1) equals the categorical trace of (End.of f ^ n).asHom ≫ a on X.

source
theorem TauCeti.trace_tensorPowMap_comp_tensorPowShiftIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] {X : C} (f : X ⟶ X) (n : ℕ) :
trace (CategoryTheory.CategoryStruct.comp (tensorPowMap f (n + 1)) (tensorPowShiftIso X n).hom) = trace ({ asHom := f } ^ (n + 1)).asHom

Categorical trace of a tensor power with cyclic shift: in a symmetric rigid category, the categorical trace of tensorPowMap f (n + 1) ≫ (tensorPowShiftIso X n).hom is the categorical trace of the (n + 1)-st iterate (End.of f ^ (n + 1)).asHom.

source
@[simp]
theorem TauCeti.trace_tensorPowShiftIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) (n : ℕ) :
trace (tensorPowShiftIso X n).hom = quantumDim X

The categorical trace of the cyclic shift (tensorPowShiftIso X n).hom on tensorPow X (n + 1) equals the quantum dimension of X.