Exact pairings under strong monoidal functors

A strong monoidal functor F : C ⥤ D carries an exact pairing ExactPairing X Y in C to an exact pairing ExactPairing (F.obj X) (F.obj Y) in D: its evaluation and coevaluation are the images of those of (X, Y), conjugated by the unit and tensor comparisons of F (CategoryTheory.Functor.mapExactPairing). In particular, a strong monoidal functor preserves objects with a left or right dual (CategoryTheory.Functor.mapHasLeftDual and CategoryTheory.Functor.mapHasRightDual).

Consequently, if Y has a left dual X and both Y and F.obj Y are closed, then the internal Hom comparison F.obj (Y ⟶[C] B) ⟶ (F.obj Y ⟶[D] F.obj B) of F is an isomorphism (CategoryTheory.Functor.ihomComparison_isIso_of_exactPairing): TauCeti.ihomIsoTensorLeft identifies its source with F.obj (X ⊗ B) through the pairing in C, and its target with F.obj X ⊗ F.obj B through the image pairing in D.

A strong monoidal functor also carries the dual-tensor comparison TauCeti.dualTensorIhom Y : (Y ⟶[C] 𝟙_ C) ⊗ Z ⟶ (Y ⟶[C] Z) to the dual-tensor comparison of F.obj Y, up to its internal Hom comparisons (CategoryTheory.Functor.map_dualTensorIhom_app_comp_ihomComparison). So when those comparisons are invertible, invertibility of the dual-tensor comparison of F.obj Y reflects back to the image of that of Y (CategoryTheory.Functor.isIso_map_dualTensorIhom_app). For restriction of sheaves of modules to the members of a cover, this is how the dual-tensor comparison, and hence dualizability, is checked locally.

The dual transfers are the forward counterparts of Mathlib's CategoryTheory.hasLeftDualOfEquivalence and CategoryTheory.hasRightDualOfEquivalence in Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence, which pull duals back along a monoidal equivalence.

Main declarations

• CategoryTheory.Functor.mapExactPairing: the image of an exact pairing under a strong monoidal functor, with evaluation and coevaluation computed by CategoryTheory.Functor.mapExactPairing_evaluation and CategoryTheory.Functor.mapExactPairing_coevaluation;
• CategoryTheory.Functor.mapHasLeftDual and CategoryTheory.Functor.mapHasRightDual: the image of an object with a left or right dual has the image of that dual as a dual;
• CategoryTheory.Functor.ihomComparison_isIso_of_exactPairing: the internal Hom comparison of a strong monoidal functor is invertible at an object with a left dual;
• CategoryTheory.Functor.whiskerLeft_ihomComparison_app_unit_comp_map_η_comp_ev: the comparison of duals is compatible with evaluation;
• CategoryTheory.Functor.map_dualTensorIhom_app_comp_ihomComparison and CategoryTheory.Functor.isIso_map_dualTensorIhom_app: the dual-tensor comparison under a strong monoidal functor.

@[instance_reducible]

def CategoryTheory.Functor.mapExactPairing {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) [ExactPairing X Y] : ExactPairing (F.obj X) (F.obj Y)

The image of an exact pairing under a strong monoidal functor F. The evaluation of (F.obj X, F.obj Y) is the image of the evaluation of (X, Y), preceded by the tensor comparison and followed by the inverse unit comparison; dually for the coevaluation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.mapExactPairing_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (X Y : C) [ExactPairing X Y] : ε_ (F.obj X) (F.obj Y) = CategoryStruct.comp (LaxMonoidal.μ F Y X) (CategoryStruct.comp (F.map (ε_ X Y)) (OplaxMonoidal.η F))

The evaluation of the image of an exact pairing under a strong monoidal functor.

@[simp]

theorem CategoryTheory.Functor.mapExactPairing_coevaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (X Y : C) [ExactPairing X Y] : η_ (F.obj X) (F.obj Y) = CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (F.map (η_ X Y)) (OplaxMonoidal.δ F X Y))

The coevaluation of the image of an exact pairing under a strong monoidal functor.

@[instance_reducible]

def CategoryTheory.Functor.mapHasLeftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y : C) [HasLeftDual Y] : HasLeftDual (F.obj Y)

A strong monoidal functor carries an object with a left dual to an object with a left dual, the image of the dual. Not an instance: the dual it produces depends on F, and several functors may have the same object as a value.

Equations

• F.mapHasLeftDual Y = { leftDual := F.obj ᘁY, exact := F.mapExactPairing (ᘁY) Y }

@[instance_reducible]

def CategoryTheory.Functor.mapHasRightDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) [HasRightDual X] : HasRightDual (F.obj X)

A strong monoidal functor carries an object with a right dual to an object with a right dual, the image of the dual. Not an instance, for the reason given on CategoryTheory.Functor.mapHasLeftDual.

Equations

• F.mapHasRightDual X = { rightDual := F.obj Xᘁ, exact := F.mapExactPairing X Xᘁ }

@[simp]

theorem CategoryTheory.Functor.mapHasLeftDual_leftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (Y : C) [HasLeftDual Y] : ᘁ(F.obj Y) = F.obj ᘁY

The left dual of F.obj Y produced by CategoryTheory.Functor.mapHasLeftDual is the image of the left dual of Y.

@[simp]

theorem CategoryTheory.Functor.mapHasRightDual_rightDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (X : C) [HasRightDual X] : (F.obj X)ᘁ = F.obj Xᘁ

The right dual of F.obj X produced by CategoryTheory.Functor.mapHasRightDual is the image of the right dual of X.

theorem CategoryTheory.Functor.ihomComparison_isIso_of_exactPairing {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) [ExactPairing X Y] [Closed Y] [Closed (F.obj Y)] : IsIso (F.ihomComparison Y).natTrans

A strong monoidal functor inverts the internal Hom comparison at an object Y with a left dual X: both F.obj (Y ⟶[C] B) and F.obj Y ⟶[D] F.obj B are identified with F.obj X ⊗ F.obj B, through the pairing and its image.

theorem CategoryTheory.Functor.whiskerLeft_ihomComparison_app_unit_comp_map_η_comp_ev {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y : C) [Closed Y] [Closed (F.obj Y)] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj Y) (CategoryStruct.comp ((F.ihomComparison Y).natTrans.app (MonoidalCategoryStruct.tensorUnit C)) ((ihom (F.obj Y)).map (OplaxMonoidal.η F)))) ((ihom.ev (F.obj Y)).app (MonoidalCategoryStruct.tensorUnit D)) = CategoryStruct.comp (LaxMonoidal.μ F Y ((ihom Y).obj (MonoidalCategoryStruct.tensorUnit C))) (CategoryStruct.comp (F.map ((ihom.ev Y).app (MonoidalCategoryStruct.tensorUnit C))) (OplaxMonoidal.η F))

The comparison F.obj (Y ⟶[C] 𝟙_ C) ⟶ (F.obj Y ⟶[D] 𝟙_ D) of the duals is compatible with evaluation: evaluating after it is the image of the evaluation of Y, preceded by the tensor comparison and followed by the inverse unit comparison.

theorem CategoryTheory.Functor.whiskerLeft_ihomComparison_app_unit_comp_map_η_comp_ev_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y : C) [Closed Y] [Closed (F.obj Y)] {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj Y) (CategoryStruct.comp ((F.ihomComparison Y).natTrans.app (MonoidalCategoryStruct.tensorUnit C)) ((ihom (F.obj Y)).map (OplaxMonoidal.η F)))) (CategoryStruct.comp ((ihom.ev (F.obj Y)).app (MonoidalCategoryStruct.tensorUnit D)) h) = CategoryStruct.comp (LaxMonoidal.μ F Y ((ihom Y).obj (MonoidalCategoryStruct.tensorUnit C))) (CategoryStruct.comp (F.map ((ihom.ev Y).app (MonoidalCategoryStruct.tensorUnit C))) (CategoryStruct.comp (OplaxMonoidal.η F) h))

The comparison F.obj (Y ⟶[C] 𝟙_ C) ⟶ (F.obj Y ⟶[D] 𝟙_ D) of the duals is compatible with evaluation: evaluating after it is the image of the evaluation of Y, preceded by the tensor comparison and followed by the inverse unit comparison.

theorem CategoryTheory.Functor.map_dualTensorIhom_app_comp_ihomComparison {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y Z : C) [Closed Y] [Closed (F.obj Y)] : CategoryStruct.comp (F.map ((TauCeti.dualTensorIhom Y).app Z)) ((F.ihomComparison Y).natTrans.app Z) = CategoryStruct.comp (OplaxMonoidal.δ F ((ihom Y).obj (MonoidalCategoryStruct.tensorUnit C)) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((F.ihomComparison Y).natTrans.app (MonoidalCategoryStruct.tensorUnit C)) ((ihom (F.obj Y)).map (OplaxMonoidal.η F))) (F.obj Z)) ((TauCeti.dualTensorIhom (F.obj Y)).app (F.obj Z)))

A strong monoidal functor carries the dual-tensor comparison of Y to that of F.obj Y: after the internal Hom comparison, the image of (Y ⟶[C] 𝟙_ C) ⊗ Z ⟶ (Y ⟶[C] Z) is the dual-tensor comparison of F.obj Y at F.obj Z, preceded by the tensor comparison of F and the comparison F.obj (Y ⟶[C] 𝟙_ C) ⟶ (F.obj Y ⟶[D] 𝟙_ D) of the duals.

theorem CategoryTheory.Functor.map_dualTensorIhom_app_comp_ihomComparison_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y Z : C) [Closed Y] [Closed (F.obj Y)] {Z✝ : D} (h : (ihom (F.obj Y)).obj (F.obj Z) ⟶ Z✝) : CategoryStruct.comp (F.map ((TauCeti.dualTensorIhom Y).app Z)) (CategoryStruct.comp ((F.ihomComparison Y).natTrans.app Z) h) = CategoryStruct.comp (OplaxMonoidal.δ F ((ihom Y).obj (MonoidalCategoryStruct.tensorUnit C)) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp ((F.ihomComparison Y).natTrans.app (MonoidalCategoryStruct.tensorUnit C)) ((ihom (F.obj Y)).map (OplaxMonoidal.η F))) (F.obj Z)) (CategoryStruct.comp ((TauCeti.dualTensorIhom (F.obj Y)).app (F.obj Z)) h))

A strong monoidal functor carries the dual-tensor comparison of Y to that of F.obj Y: after the internal Hom comparison, the image of (Y ⟶[C] 𝟙_ C) ⊗ Z ⟶ (Y ⟶[C] Z) is the dual-tensor comparison of F.obj Y at F.obj Z, preceded by the tensor comparison of F and the comparison F.obj (Y ⟶[C] 𝟙_ C) ⟶ (F.obj Y ⟶[D] 𝟙_ D) of the duals.

theorem CategoryTheory.Functor.isIso_map_dualTensorIhom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (Y Z : C) [Closed Y] [Closed (F.obj Y)] [IsIso ((F.ihomComparison Y).natTrans.app Z)] [IsIso ((F.ihomComparison Y).natTrans.app (MonoidalCategoryStruct.tensorUnit C))] [IsIso ((TauCeti.dualTensorIhom (F.obj Y)).app (F.obj Z))] : IsIso (F.map ((TauCeti.dualTensorIhom Y).app Z))

If the internal Hom comparisons of a strong monoidal functor F at Y are invertible at Z and at the unit, and the dual-tensor comparison of F.obj Y is invertible at F.obj Z, then the image of the dual-tensor comparison of Y at Z is invertible.