Pivotal traces and dimensions of tensor products #
In a pivotal category, the pivotal pairing pivotalExactPairing (X ⊗ Y) is the tensor product of
the pivotal pairings of Y and of X, transported along the comparison
rightDualTensorIso X Y : (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ. This is where the monoidality of the pivotal
structure enters. Consequently the trace of a tensor product f ⊗ₘ g is computed by two nested
loops.
For the left trace the loop of f lies inside the loop of g, so the scalar leftTrace f acts
on Y from the left:
leftTrace (f ⊗ₘ g) = leftTrace ((λ_ Y).inv ≫ leftTrace f ▷ Y ≫ (λ_ Y).hom ≫ g). A scalar acting
on Y from the right can be moved out of the left trace, so whenever the left and right actions
of leftTrace f on Y agree, the left trace is multiplicative:
leftTrace (f ⊗ₘ g) = leftTrace f ≫ leftTrace g. Symmetrically, the right trace is
multiplicative whenever rightTrace g acts on X in the same way from both sides.
The two actions of a scalar need not agree in a general monoidal category, so the hypothesis cannot be dropped in general. The actions do agree in a braided category, where the left and right traces and dimensions are therefore multiplicative without further hypotheses.
Main declarations #
TauCeti.pivotalExactPairing_tensor_evaluationandTauCeti.pivotalExactPairing_tensor_coevaluation: the pivotal pairing ofX ⊗ Yis the tensor product of the pivotal pairings, up torightDualTensorIso X Y, which is therefore also a comparison of left duals (TauCeti.rightDualTensorIso_hom_eq_leftMate);TauCeti.leftTrace_tensorObj,TauCeti.rightTrace_tensorObj,TauCeti.leftTrace_tensorHomandTauCeti.rightTrace_tensorHom: the traces of endomorphisms ofX ⊗ Yvia partial trace, and off ⊗ₘ gas nested loops;TauCeti.leftTrace_tensorHom_eq_comp,TauCeti.rightTrace_tensorHom_eq_comp,TauCeti.leftDim_tensor_eq_compandTauCeti.rightDim_tensor_eq_comp: multiplicativity of the traces and dimensions when the relevant scalar acts in the same way from both sides;TauCeti.leftTrace_tensorHom_eq_comp_of_braidedand its companions: multiplicativity in a braided pivotal category.
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
The evaluation of the pivotal pairing of X ⊗ Y is that of the tensor product of the pivotal
pairings of Y and of X, after the comparison rightDualTensorIso X Y : (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ.
The comparison rightDualTensorIso X Y : (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ of right duals is also the
comparison of left duals of X ⊗ Y, for the pivotal pairing of X ⊗ Y and the tensor product of
the pivotal pairings of Y and of X.
The coevaluation of the pivotal pairing of X ⊗ Y, followed by the comparison
rightDualTensorIso X Y : (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, is the coevaluation of the tensor product of the
pivotal pairings of Y and of X.
The coevaluation of the pivotal pairing of X ⊗ Y, followed by the comparison
rightDualTensorIso X Y : (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, is the coevaluation of the tensor product of the
pivotal pairings of Y and of X.
Partial-trace decomposition of the left trace: the left trace of h : X ⊗ Y ⟶ X ⊗ Y is the
left trace on Y of the left partial trace of h over X.
Partial-trace decomposition of the right trace: the right trace of h : X ⊗ Y ⟶ X ⊗ Y is
the right trace on X of the right partial trace of h over Y.
The left trace of a tensor product is a nested loop: the left trace of f acts on Y
from the left, inside the left trace of g.
The right trace of a tensor product is a nested loop: the right trace of g acts on X
from the right, inside the right trace of f.
Multiplicativity of the left trace: if the left trace of f acts on Y in the same way
from the left and from the right, then leftTrace (f ⊗ₘ g) = leftTrace f ≫ leftTrace g.
Multiplicativity of the right trace: if the right trace of g acts on X in the same way
from the left and from the right, then rightTrace (f ⊗ₘ g) = rightTrace f ≫ rightTrace g.
Multiplicativity of the left dimension: if the left dimension of X acts on Y in the
same way from the left and from the right, then leftDim (X ⊗ Y) = leftDim X ≫ leftDim Y.
Multiplicativity of the right dimension: if the right dimension of Y acts on X in the
same way from the left and from the right, then rightDim (X ⊗ Y) = rightDim X ≫ rightDim Y.
In a braided pivotal category, the left trace is multiplicative.
In a braided pivotal category, the right trace is multiplicative.
In a braided pivotal category, the left dimension is multiplicative.
In a braided pivotal category, the right dimension is multiplicative.