Structure maps of duals pulled back along a monoidal equivalence

Mathlib's CategoryTheory.hasRightDualOfEquivalence gives an object X of C a right dual by pulling back the right dual of F.obj X along a monoidal equivalence F : C ⥤ D. Its evaluation and coevaluation are defined as preimages under F. This file records their images under F: the evaluation and coevaluation of (F.obj X, (F.obj X)ᘁ), transported across the counit of the equivalence and conjugated by the comparison maps of F.

These identities are how the structure maps of such a dual are computed. For instance, Mathlib makes Action V H right rigid this way, and its evaluation and coevaluation are computed from them on underlying objects.

Main results

• CategoryTheory.map_evaluation_hasRightDualOfEquivalence: the image under F of the evaluation of the pulled-back right dual;
• CategoryTheory.map_coevaluation_hasRightDualOfEquivalence: the image under F of the coevaluation of the pulled-back right dual.

theorem CategoryTheory.map_evaluation_hasRightDualOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : Functor D C} (adj : F ⊣ G) [F.IsEquivalence] (X : C) [HasRightDual (F.obj X)] : F.map (ε_ X Xᘁ) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F (adj.toEquivalence.inverse.obj (F.obj X)ᘁ) X) (CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (adj.toEquivalence.counitIso.app (F.obj X)ᘁ).hom (F.obj X)) (ε_ (F.obj X) (F.obj X)ᘁ)) (Functor.LaxMonoidal.ε F))

The evaluation of a right dual pulled back along a monoidal equivalence F is, by definition, the preimage under F of the evaluation of the right dual of F.obj X transported across the counit.

theorem CategoryTheory.map_coevaluation_hasRightDualOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [MonoidalCategory C] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : Functor D C} (adj : F ⊣ G) [F.IsEquivalence] (X : C) [HasRightDual (F.obj X)] : F.map (η_ X Xᘁ) = CategoryStruct.comp (Functor.OplaxMonoidal.η F) (CategoryStruct.comp (CategoryStruct.comp (η_ (F.obj X) (F.obj X)ᘁ) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (adj.toEquivalence.counitIso.app (F.obj X)ᘁ).inv)) (Functor.LaxMonoidal.μ F X (adj.toEquivalence.inverse.obj (F.obj X)ᘁ)))

The coevaluation of a right dual pulled back along a monoidal equivalence F is, by definition, the preimage under F of the coevaluation of the right dual of F.obj X transported across the counit.