The double-dual map in a closed braided monoidal category

Let C be a braided monoidal category and Y an object for which both Y and its internal dual Yᵛ := (Y ⟶[C] 𝟙_ C) are closed. The double-dual map

Y ⟶ (Yᵛ ⟶[C] 𝟙_ C)

is the transpose of the braided evaluation Yᵛ ⊗ Y ⟶ Y ⊗ Yᵛ ⟶ 𝟙_ C. For modules over a commutative ring it is the evaluation map m ↦ (φ ↦ φ m) into the double dual, Module.Dual.eval in Mathlib; for sheaves of modules it is the map 𝓔 ⟶ 𝓗om(𝓗om(𝓔, 𝒪), 𝒪).

The map is natural in Y, and it is an isomorphism whenever Y has a left or a right dual. So in a closed symmetric monoidal category such as QCoh(X) or modules over a commutative ring, every dualizable object is canonically isomorphic to its double dual, with the duals computed by internal homs into the unit. The IsIso instances are found by instance search, so asIso (doubleDualMap Y) is available for any object with a HasLeftDual or HasRightDual instance, for example a finite projective module.

Main declarations

• TauCeti.doubleDualMap: the canonical map Y ⟶ ((Y ⟶[C] 𝟙_ C) ⟶[C] 𝟙_ C), characterized by TauCeti.whiskerLeft_doubleDualMap_comp_ev;
• TauCeti.doubleDualMap_naturality: its naturality in Y;
• TauCeti.doubleDualMap_comp_pre_ihomUnitIso_inv_app: its form for a chosen left dual D, the transpose of the braided pairing D ⊗ Y ⟶ 𝟙_ C;
• TauCeti.isIso_doubleDualMap_of_exactPairing, TauCeti.isIso_doubleDualMap and TauCeti.isIso_doubleDualMap_of_hasRightDual: it is an isomorphism for an object with a left or a right dual.

References

• [A. Dold and D. Puppe, Duality, trace, and transfer][doldpuppe1980], §1

def TauCeti.doubleDualMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Y : C) [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] : Y ⟶ (CategoryTheory.ihom ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The canonical map Y ⟶ ((Y ⟶[C] 𝟙_ C) ⟶[C] 𝟙_ C) from an object to its double dual: the transpose of the evaluation (Y ⟶[C] 𝟙_ C) ⊗ Y ⟶ Y ⊗ (Y ⟶[C] 𝟙_ C) ⟶ 𝟙_ C, braided so that the dual acts on the left.

Equations

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

@[simp]

theorem TauCeti.whiskerLeft_doubleDualMap_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Y : C) [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (doubleDualMap Y)) ((CategoryTheory.ihom.ev ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) = CategoryTheory.CategoryStruct.comp (β_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y).hom ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

Evaluation characterizes the double-dual map: evaluating the double dual of y at φ is evaluating φ at y.

@[simp]

theorem TauCeti.whiskerLeft_doubleDualMap_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Y : C) [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (doubleDualMap Y)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) = CategoryTheory.CategoryStruct.comp (β_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h)

Evaluation characterizes the double-dual map: evaluating the double dual of y at φ is evaluating φ at y.

@[simp]

theorem TauCeti.uncurry_doubleDualMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Y : C) [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] : CategoryTheory.MonoidalClosed.uncurry (doubleDualMap Y) = CategoryTheory.CategoryStruct.comp (β_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y).hom ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

Uncurrying the double-dual map gives the braided evaluation.

theorem TauCeti.doubleDualMap_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {Y Y' : C} [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] [CategoryTheory.Closed Y'] [CategoryTheory.Closed ((CategoryTheory.ihom Y').obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] (f : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp f (doubleDualMap Y') = CategoryTheory.CategoryStruct.comp (doubleDualMap Y) ((CategoryTheory.MonoidalClosed.pre ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

The double-dual map is natural: for f : Y ⟶ Y', following f by the double-dual map of Y' is the double-dual map of Y followed by the double transpose of f, obtained by precomposing twice.

theorem TauCeti.doubleDualMap_comp_pre_ihomUnitIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] (D : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed D] : CategoryTheory.CategoryStruct.comp (doubleDualMap Y) ((CategoryTheory.MonoidalClosed.pre (ihomUnitIso D Y).inv).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (β_ D Y).hom (ε_ D Y))

For a left dual D of Y, identifying (Y ⟶[C] 𝟙_ C) with D through TauCeti.ihomUnitIso turns the double-dual map into the transpose of the braided pairing D ⊗ Y ⟶ Y ⊗ D ⟶ 𝟙_ C.

theorem TauCeti.isIso_doubleDualMap_of_exactPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] (D : C) [CategoryTheory.ExactPairing D Y] : CategoryTheory.IsIso (doubleDualMap Y)

The double-dual map of an object with a left dual D is an isomorphism: Y is a left dual of (Y ⟶[C] 𝟙_ C), and the double-dual map is the inverse of the comparison TauCeti.ihomUnitIso for that pairing.

instance TauCeti.isIso_doubleDualMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] [CategoryTheory.HasLeftDual Y] : CategoryTheory.IsIso (doubleDualMap Y)

The double-dual map of an object with a left dual is an isomorphism.

instance TauCeti.isIso_doubleDualMap_of_hasRightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.Closed ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] [CategoryTheory.HasRightDual Y] : CategoryTheory.IsIso (doubleDualMap Y)

The double-dual map of an object with a right dual is an isomorphism.