Mates for braided exact pairings #
The braiding turns an exact pairing (X, X') into an exact pairing (X', X).
Taking a right mate with respect to the original pairings and then with respect to these
swapped pairings recovers the original morphism. This makes double duality natural even
when the chosen dual of X' is not X.
The swapped pairing is Mathlib's CategoryTheory.BraidedCategory.exactPairing_swap.
The explicit-pairing statement rightMate_swap_rightMate follows the API proposed in
J. McKoen's Mathlib pull request #42145; its proof uses the evaluation characterization
of mates and naturality of the braiding.
Swapping is compatible with tensor products of pairings up to a double braiding. After the
double braiding β_{X,Y} ≫ β_{Y,X} of X ⊗ Y, the braided evaluation of the tensor product
pairing of (X, X') and (Y, Y') is the evaluation of the tensor product of the swapped
pairings of (Y, Y') and (X, X'), in which the braided loop of Y is nested inside the
braided loop of X
(TauCeti.braiding_comp_braiding_whiskerRight_comp_braiding_comp_tensor_evaluation).
Equivalently, the double braiding can be replaced by the inverse double braiding of Y' and X'
(TauCeti.braiding_comp_tensor_evaluation); the two forms are related by the fact that a
braiding is its own mate with respect to tensor product pairings
(TauCeti.whiskerLeft_braiding_comp_tensor_evaluation). In a symmetric category the double
braidings are identities. This is the identity that computes the Drinfeld isomorphism
X ≅ Xᘁᘁ of a tensor product.
Contracting the first factor of (β_ X X).hom between the braided coevaluation
η_ X X' ≫ (β_ X X').hom and the evaluation ε_ X X' of an exact pairing (X, X') yields the
identity on 𝟙_ C ⊗ X (TauCeti.coevaluation_braiding_comp_braiding_comp_evaluation).
References #
- [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §8.9
The evaluation of the swapped pairing is braided evaluation.
The evaluation of the swapped pairing is braided evaluation.
The coevaluation of the swapped pairing uses the inverse braiding.
The coevaluation of the swapped pairing uses the inverse braiding.
Contracting the first factor of (β_ X X).hom between the braided coevaluation
η_ X X' ≫ (β_ X X').hom and the evaluation ε_ X X' of an exact pairing (X, X') yields the
identity on 𝟙_ C ⊗ X.
Contracting the first factor of (β_ X X).hom between the braided coevaluation
η_ X X' ≫ (β_ X X').hom and the evaluation ε_ X X' of an exact pairing (X, X') yields the
identity on 𝟙_ C ⊗ X.
Taking a right mate and then a right mate with respect to the braided swapped pairings recovers the original morphism. No symmetry of the braiding is needed.
A braiding is its own mate with respect to tensor product pairings: precomposing the
evaluation of the tensor product pairing (X ⊗ Y, Y' ⊗ X') with the braiding of Y past X
is precomposing the evaluation of (Y ⊗ X, X' ⊗ Y') with the braiding of Y' past X'.
The double braiding is its own mate with respect to tensor product pairings: precomposing
the evaluation of (A ⊗ B, B' ⊗ A') with the double braiding β_{A,B} ≫ β_{B,A} of A ⊗ B is
precomposing it with the double braiding β_{B',A'} ≫ β_{A',B'} of B' ⊗ A'.
The braided evaluation of the tensor product pairing (X ⊗ Y, Y' ⊗ X') is the inverse of the
double braiding β_{Y',X'} ≫ β_{X',Y'} of Y' ⊗ X', followed by the braided evaluation of
(Y, Y') nested inside the braided evaluation of (X, X'). In a symmetric category the double
braiding is the identity, so the swapped pairing of a tensor product is the tensor product of
the swapped pairings.
After the double braiding β_{X,Y} ≫ β_{Y,X} of X ⊗ Y, the braided evaluation of the tensor
product pairing (X ⊗ Y, Y' ⊗ X') nests the braided evaluation of (Y, Y') inside that of
(X, X'). The right side is the evaluation of the tensor product of the swapped pairings of
(Y, Y') and (X, X').