The Drinfeld isomorphism #
In a braided monoidal category, an object X with a right dual whose right dual also exists
is canonically isomorphic to its double right dual. The Drinfeld isomorphism compares two
right duals of Xแ: the chosen double dual, and X with the braided swapped pairing.
Its evaluation and coevaluation identities and naturality are recorded here.
In a braided right rigid category the Drinfeld isomorphisms form a natural isomorphism
drinfeldNatIso : ๐ญ C โ
doubleRightDualFunctor C, which is always compatible with the unit
comparison of the double right dual functor. An arbitrary braiding does not make it monoidal:
the Drinfeld isomorphism of X โ Y, precomposed with the double braiding
ฮฒ_{X,Y} โซ ฮฒ_{Y,X}, is the tensor product of the Drinfeld isomorphisms of X and Y followed
by the tensor comparison. This rests on the computation of the swapped pairing of a tensor
product
(TauCeti.braiding_comp_braiding_whiskerRight_comp_braiding_comp_tensor_evaluation). When the
braiding is symmetric the double braiding is the identity, so drinfeldNatIso is a monoidal
natural isomorphism. In a symmetric rigid category it is therefore the underlying isomorphism of
the canonical pivotal structure.
Main declarations #
TauCeti.drinfeldIso: the Drinfeld isomorphismX โ Xแแ, withTauCeti.drinfeldIso_hom_eqandTauCeti.drinfeldIso_inv_eqwriting it and its inverse as explicit braided composites;TauCeti.drinfeldNatIso: the Drinfeld isomorphisms as a natural isomorphism๐ญ C โ doubleRightDualFunctor Cin a braided right rigid category, withTauCeti.drinfeldIso_unit_homits compatibility with the unit comparison;TauCeti.braiding_hom_comp_braiding_hom_comp_drinfeldIso_tensor_hom: the double braiding ofX โ Yfollowed by the Drinfeld isomorphism ofX โ Yis the tensor product of those ofXandY, followed by the tensor comparison of the double right dual functor;TauCeti.drinfeldNatIso_isMonoidal: in a symmetric category,drinfeldNatIsois monoidal.
The construction uses Mathlib's CategoryTheory.ExactPairing.rightDualIso and
CategoryTheory.BraidedCategory.exactPairing_swap. The name drinfeldIso follows
J. McKoen's Mathlib pull request #42192.
References #
- [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], ยง8.9
The Drinfeld isomorphism identifies X with its double right dual by comparing
its braided pairing with Xแ to the chosen right pairing of Xแ.
Instances For
Evaluating the Drinfeld isomorphism against the right dual is braided evaluation.
Evaluating the Drinfeld isomorphism against the right dual is braided evaluation.
The Drinfeld isomorphism inserts the coevaluation of Xแ and contracts X
against Xแ using the braiding.
The inverse Drinfeld isomorphism transforms braided evaluation into double-dual evaluation.
The inverse Drinfeld isomorphism transforms braided evaluation into double-dual evaluation.
The inverse Drinfeld isomorphism inserts the coevaluation of X, braids Xแแ past X, and
contracts Xแแ against Xแ.
Coevaluation into the double dual is obtained by applying the Drinfeld isomorphism after the braided swapped coevaluation.
Coevaluation into the double dual is obtained by applying the Drinfeld isomorphism after the braided swapped coevaluation.
The inverse Drinfeld isomorphism transforms double-dual coevaluation into the braided swapped coevaluation.
The inverse Drinfeld isomorphism transforms double-dual coevaluation into the braided swapped coevaluation.
The Drinfeld isomorphism is natural with respect to double right adjoint mates.
The Drinfeld isomorphism is natural with respect to double right adjoint mates.
Naturality of the inverse Drinfeld isomorphism.
Naturality of the inverse Drinfeld isomorphism.
The Drinfeld isomorphisms X โ
Xแแ of a braided right rigid category, as a natural
isomorphism from the identity functor to the double right dual functor.
Instances For
The components of drinfeldNatIso are the Drinfeld isomorphisms.
The components of the inverse of drinfeldNatIso are the inverse Drinfeld isomorphisms.
At the unit, the Drinfeld isomorphism is the unit comparison of the double right dual
functor. This holds for any braiding. The right dual of ๐_ C is explicit because it is the one
chosen by the rigid structure, which need not be Mathlib's hasRightDualUnit.
The double braiding ฮฒ_{X,Y} โซ ฮฒ_{Y,X} of X โ Y followed by the Drinfeld isomorphism of
X โ Y is the tensor product of the Drinfeld isomorphisms of X and Y, followed by the tensor
comparison of the double right dual functor.
In a symmetric right rigid category, the Drinfeld isomorphisms form a monoidal natural isomorphism from the identity functor to the double right dual functor.