The right dual functor is a monoidal equivalence, and the double right dual functor #
Mathlib's CategoryTheory.rightDualFunctor C : C ⥤ (Cᵒᵖ)ᴹᵒᵖ sends an object X of a right rigid
monoidal category to its right dual Xᘁ and a morphism f to its right adjoint mate fᘁ. Its
target is the monoidal opposite of the opposite category: the functor is contravariant, and it
reverses the order of tensor products, since (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ (Mathlib's
CategoryTheory.rightDualTensorIso).
This file makes rightDualFunctor C a strong monoidal functor. Its tensor comparison is
rightDualTensorIso and its unit comparison is the identification (𝟙_ C)ᘁ ≅ 𝟙_ C of the
right dual of the unit with the unit, through the self-pairing exactPairingUnit. The
coherence conditions are first proved in C, for arbitrary objects with right duals, as
identities between mates; there the comparisons are mates of identities and every coherence
morphism is a mate of a coherence morphism (TauCeti.CategoryTheory.Monoidal.Rigid.Mate).
In a rigid monoidal category, the right dual functor is also an equivalence of categories. Full faithfulness follows because taking a left adjoint mate undoes taking a right adjoint mate, while essential surjectivity follows because every object is the right dual of its left dual. Together with the strong monoidal structure, this makes the right dual functor a monoidal equivalence.
Applying the right dual functor twice gives the double right dual functor C ⥤ C, sending X
to Xᘁᘁ and f to fᘁᘁ. Its second application goes through the opposite monoidal opposite
of the right dual functor (CategoryTheory.Functor.op followed by
CategoryTheory.Functor.opMop), so the double right dual functor is a composite of strong
monoidal functors and inherits a strong monoidal structure. This monoidal structure is what makes
a monoidal natural isomorphism from the identity functor to the double right dual functor, a
pivotal structure, expressible with Mathlib's NatTrans.IsMonoidal. In a rigid monoidal category
the double right dual functor is a monoidal autoequivalence.
Main declarations #
TauCeti.rightDualTensorIso_hom_naturality: naturality ofrightDualTensorIso;TauCeti.rightDualTensorIso_associativity,TauCeti.rightDualTensorIso_leftUnitalityandTauCeti.rightDualTensorIso_rightUnitality: its compatibility with the associator and the unitors;TauCeti.rightDualTensorIso_hom_whiskerRight_evaluation,TauCeti.rightDualTensorIso_inv_whiskerRight_evaluationandTauCeti.coevaluation_comp_whiskerLeft_rightDualTensorIso_hom: it carries the evaluation and coevaluation of(X ⊗ Y, (X ⊗ Y)ᘁ)to those of the tensor product pairing;TauCeti.rightDualFunctorCoreMonoidaland the instanceTauCeti.rightDualFunctorMonoidal: the strong monoidal structure onrightDualFunctor C, with structure morphisms given byTauCeti.rightDualFunctor_ε,TauCeti.rightDualFunctor_η,TauCeti.rightDualFunctor_μandTauCeti.rightDualFunctor_δ;TauCeti.rightDualFunctorFullyFaithful: the explicit full-faithfulness structure whose preimage operation takes left adjoint mates;TauCeti.rightDualFunctorIsEquivalence: right duality is an equivalence; together with itsFunctor.Monoidalinstance, it is a monoidal equivalence;TauCeti.doubleRightDualFunctorand the instanceTauCeti.doubleRightDualFunctorMonoidal: the strong monoidal double right dual functor, with structure morphisms given byTauCeti.doubleRightDualFunctor_ε,TauCeti.doubleRightDualFunctor_η,TauCeti.doubleRightDualFunctor_μandTauCeti.doubleRightDualFunctor_δ(the unit comparison is also given in terms of a right adjoint mate byTauCeti.doubleRightDualFunctor_ε_eq_rightAdjointMate);TauCeti.doubleRightDualFunctor_map_evaluationandTauCeti.doubleRightDualFunctor_map_coevaluation: the double right dual functor carries the evaluation and coevaluation of(X, Xᘁ)to those of(Xᘁᘁ, Xᘁᘁᘁ);TauCeti.rigidCategoryOfIsoDoubleRightDual: a right rigid category with isomorphismsX ≅ Xᘁᘁis rigid, with left duals described byTauCeti.rigidCategoryOfIsoDoubleRightDual_evaluationandTauCeti.rigidCategoryOfIsoDoubleRightDual_coevaluation;TauCeti.doubleRightDualFunctorIsEquivalence: in a rigid monoidal category, the double right dual functor is an equivalence, hence a monoidal autoequivalence.
References #
- [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §2.10
The comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ is natural in X and Y.
The comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ is natural in X and Y.
The comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ is compatible with the associators: the two ways of
identifying (X ⊗ Y ⊗ Z)ᘁ with Zᘁ ⊗ Yᘁ ⊗ Xᘁ agree.
The comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ is compatible with the associators: the two ways of
identifying (X ⊗ Y ⊗ Z)ᘁ with Zᘁ ⊗ Yᘁ ⊗ Xᘁ agree.
The mate Xᘁ ⟶ (𝟙_ C ⊗ X)ᘁ of the left unitor of X, followed by the comparison
(𝟙_ C ⊗ X)ᘁ ≅ Xᘁ ⊗ (𝟙_ C)ᘁ and the identification of (𝟙_ C)ᘁ with 𝟙_ C, is the inverse
right unitor Xᘁ ⟶ Xᘁ ⊗ 𝟙_ C of Xᘁ.
The mate Xᘁ ⟶ (X ⊗ 𝟙_ C)ᘁ of the right unitor of X, followed by the comparison
(X ⊗ 𝟙_ C)ᘁ ≅ (𝟙_ C)ᘁ ⊗ Xᘁ and the identification of (𝟙_ C)ᘁ with 𝟙_ C, is the inverse
left unitor Xᘁ ⟶ 𝟙_ C ⊗ Xᘁ of Xᘁ.
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the evaluation of the tensor product pairing
of (X, Xᘁ) and (Y, Yᘁ) is the evaluation of (X ⊗ Y, (X ⊗ Y)ᘁ).
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the evaluation of the tensor product pairing
of (X, Xᘁ) and (Y, Yᘁ) is the evaluation of (X ⊗ Y, (X ⊗ Y)ᘁ).
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the evaluation of (X ⊗ Y, (X ⊗ Y)ᘁ) is the
evaluation of the tensor product pairing of (X, Xᘁ) and (Y, Yᘁ).
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the evaluation of (X ⊗ Y, (X ⊗ Y)ᘁ) is the
evaluation of the tensor product pairing of (X, Xᘁ) and (Y, Yᘁ).
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the coevaluation of (X ⊗ Y, (X ⊗ Y)ᘁ) is the
coevaluation of the tensor product pairing of (X, Xᘁ) and (Y, Yᘁ).
Through the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ, the coevaluation of (X ⊗ Y, (X ⊗ Y)ᘁ) is the
coevaluation of the tensor product pairing of (X, Xᘁ) and (Y, Yᘁ).
In (Cᵒᵖ)ᴹᵒᵖ, composition and tensor products are those of C in the reverse order, by
definition. So after Quiver.Hom.unmop_inj and Quiver.Hom.unop_inj, each coherence condition
for rightDualFunctor C is definitionally the corresponding identity in C proved above, up to
reassociating the composites.
The right dual functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ of a right rigid monoidal category is strong
monoidal: the tensor comparison is rightDualTensorIso and the unit comparison identifies the
right dual of the unit with the unit.
Instances For
The right dual functor of a right rigid monoidal category is strong monoidal.
The unit comparison of the right dual functor is the identification of the right dual of the unit with the unit.
The inverse unit comparison of the right dual functor.
The tensor comparison of the right dual functor is rightDualTensorIso.
The inverse tensor comparison of the right dual functor.
The right dual functor is fully faithful. Its inverse on each hom-set takes left adjoint mates.
Instances For
The preimage operation for the full faithfulness of the right dual functor takes left adjoint mates.
The right dual functor of a right rigid monoidal category is faithful.
The right dual functor of a right rigid monoidal category is full.
The right dual functor of a rigid monoidal category is an equivalence of categories.
The double right dual functor C ⥤ C of a right rigid monoidal category, sending X to
Xᘁᘁ and f to fᘁᘁ. It applies the right dual functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ twice, the second
time through its opposite monoidal opposite, and returns to C by removing the wrappers.
Instances For
The double right dual functor is strong monoidal, as the composite of the strong monoidal right dual functor, its opposite monoidal opposite, and the removal of the wrappers.
The double right dual functor sends X to Xᘁᘁ.
The double right dual functor sends f to fᘁᘁ.
The structure morphisms of a composite of monoidal functors are composites of the structure
morphisms of its factors (Functor.LaxMonoidal.comp_μ and its relatives). Those of the right dual
functor and of its opposite monoidal opposite are, after removing the wrappers, the morphisms of
C displayed below, while those of the removal of the wrappers are identities.
The unit comparison 𝟙_ C ⟶ (𝟙_ C)ᘁᘁ of the double right dual functor: identify 𝟙_ C with
(𝟙_ C)ᘁ, then take the mate of the identification of (𝟙_ C)ᘁ with 𝟙_ C. The pairings are
explicit because (𝟙_ C)ᘁ is the dual chosen by the rigid structure, which need not be Mathlib's
hasRightDualUnit.
The unit comparison of the double right dual functor, with the mate written as the right
adjoint mate fᘁ for the duals chosen by the rigid structure rather than as an
ExactPairing.rightMate, so that lemmas about right adjoint mates apply to it directly. The
instances are explicit because instance search would pick hasRightDualUnit for 𝟙_ C.
The inverse unit comparison (𝟙_ C)ᘁᘁ ⟶ 𝟙_ C of the double right dual functor.
The tensor comparison Xᘁᘁ ⊗ Yᘁᘁ ⟶ (X ⊗ Y)ᘁᘁ of the double right dual functor: identify
Xᘁᘁ ⊗ Yᘁᘁ with (Yᘁ ⊗ Xᘁ)ᘁ, then take the mate of the comparison (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ.
The inverse tensor comparison (X ⊗ Y)ᘁᘁ ⟶ Xᘁᘁ ⊗ Yᘁᘁ of the double right dual functor.
The double right dual functor carries the evaluation of (X, Xᘁ) to the evaluation of
(Xᘁᘁ, Xᘁᘁᘁ), up to its tensor and unit comparisons.
The double right dual functor carries the coevaluation of (X, Xᘁ) to the coevaluation of
(Xᘁᘁ, Xᘁᘁᘁ), up to its unit and tensor comparisons.
A right rigid category in which every object X is isomorphic to its double right dual
(doubleRightDualFunctor C).obj X = Xᘁᘁ is rigid: transporting the pairing of Xᘁ with Xᘁᘁ
along the isomorphism makes Xᘁ a left dual of X. Not an instance, as the left duals depend on
the chosen isomorphisms.
Instances For
The evaluation X ⊗ Xᘁ ⟶ 𝟙_ C of the left dual of X in
rigidCategoryOfIsoDoubleRightDual φ: the evaluation of (Xᘁ, Xᘁᘁ) precomposed with φ X.
The evaluation X ⊗ Xᘁ ⟶ 𝟙_ C of the left dual of X in
rigidCategoryOfIsoDoubleRightDual φ: the evaluation of (Xᘁ, Xᘁᘁ) precomposed with φ X.
The coevaluation 𝟙_ C ⟶ Xᘁ ⊗ X of the left dual of X in
rigidCategoryOfIsoDoubleRightDual φ: the coevaluation of (Xᘁ, Xᘁᘁ) followed by the inverse
of φ X.
The coevaluation 𝟙_ C ⟶ Xᘁ ⊗ X of the left dual of X in
rigidCategoryOfIsoDoubleRightDual φ: the coevaluation of (Xᘁ, Xᘁᘁ) followed by the inverse
of φ X.
The double right dual functor of a rigid monoidal category is an equivalence of categories;
with its Functor.Monoidal instance, it is a monoidal autoequivalence.