Left and right traces in a pivotal category #

In a pivotal category C, every object X is both a right dual of Xᘁ, through the pairing TauCeti.pivotalExactPairing X : ExactPairing Xᘁ X, and a left dual of Xᘁ, through the rigid structure. So an endomorphism f : X ⟶ X can be closed up into a loop in two ways, giving two scalars 𝟙_ C ⟶ 𝟙_ C:

the left trace leftTrace f = η_ Xᘁ X ≫ Xᘁ ◁ f ≫ ε_ X Xᘁ, whose coevaluation is that of pivotalExactPairing X;
the right trace rightTrace f = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ ε_ Xᘁ X, whose evaluation is that of pivotalExactPairing X.

Unfolding the pivotal pairing writes the pivotal isomorphism φ_X : X ≅ Xᘁᘁ out explicitly: leftTrace f = η_ Xᘁ Xᘁᘁ ≫ Xᘁ ◁ φ_X⁻¹ ≫ Xᘁ ◁ f ≫ ε_ X Xᘁ and rightTrace f = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ φ_X ▷ Xᘁ ≫ ε_ Xᘁ Xᘁᘁ. The left and right dimensions of X are the traces of its identity.

We prove the basic properties of the two traces: both are cyclic, so in particular invariant under conjugation by an isomorphism; the right adjoint mate exchanges them, by the Freyd–Yetter identity φ_{Xᘁ} = (φ_X⁻¹)ᘁ, so that the left dimension of Xᘁ is the right dimension of X; both are the identity on scalars 𝟙_ C ⟶ 𝟙_ C, so that the unit has dimension 𝟙; and both are compatible with extracting scalar actions from the outside of a loop; and both are additive, and R-linear in an R-linear monoidal category. The zero object has both dimensions zero in a preadditive monoidal category.

The traces depend on the pivotal structure only through an automorphism of X: if φ and ψ are the pivotal isomorphisms of two pivotal structures on C, the left trace of f for φ is the left trace for ψ of ψ_X ≫ φ_X⁻¹ ≫ f, and the right trace of f for φ is the right trace for ψ of f ≫ φ_X ≫ ψ_X⁻¹.

Main declarations #

TauCeti.leftTrace and TauCeti.rightTrace: the two traces of an endomorphism, with their defining formulas TauCeti.leftTrace_def and TauCeti.rightTrace_def and their unfolded forms TauCeti.leftTrace_eq_pivotalIsoApp and TauCeti.rightTrace_eq_pivotalIsoApp;
TauCeti.leftDim and TauCeti.rightDim: the two dimensions of an object, the traces of its identity, and invariant under isomorphism by TauCeti.leftDim_congr and TauCeti.rightDim_congr;
TauCeti.leftTrace_comm and TauCeti.rightTrace_comm: cyclicity;
TauCeti.leftTrace_comp_whiskerLeft_scalar and TauCeti.rightTrace_scalar_whiskerRight_comp: a scalar acting on the outer side of a loop factors out of the trace;
TauCeti.leftTrace_rightAdjointMate and TauCeti.rightTrace_rightAdjointMate: the mate exchanges the two traces, and TauCeti.leftDim_rightDual and TauCeti.rightDim_rightDual exchange the two dimensions;
TauCeti.leftTrace_unit and TauCeti.rightTrace_unit: the trace of a scalar is itself, and TauCeti.leftDim_unit, TauCeti.rightDim_unit;
TauCeti.leftTrace_add, TauCeti.leftTrace_smul and their right-handed versions: additivity in a preadditive monoidal category, and R-linearity in an R-linear one;
TauCeti.leftTrace_eq_leftTrace_comp and TauCeti.rightTrace_eq_rightTrace_comp: changing the pivotal structure, with the corollaries TauCeti.leftDim_eq_leftTrace and TauCeti.rightDim_eq_rightTrace for the dimensions.

References #

A. Henriques, D. Penneys, J. Tener, Categorified trace for module tensor categories over braided tensor categories, arXiv:1509.02937, §2.1
[P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.7
leanprover-community/mathlib4#42191, for the names leftTrace and rightTrace and their packaging through pivotalExactPairing