Dualizable objects in a closed monoidal category

Let C be a monoidal category and Y a closed object of C, so that Y ⊗ - has the right adjoint (Y ⟶[C] -). Write Yᵛ := (Y ⟶[C] 𝟙_ C) for the internal hom into the unit. Evaluation induces the dual-tensor comparison

Yᵛ ⊗ Z ⟶ (Y ⟶[C] Z),

natural in Z: it is the transpose of Y ⊗ (Yᵛ ⊗ Z) ⟶ (Y ⊗ Yᵛ) ⊗ Z ⟶ 𝟙_ C ⊗ Z ⟶ Z. For modules over a commutative ring it is the map Mᵛ ⊗ N → Hom(M, N), φ ⊗ n ↦ (m ↦ φ m • n), formalized as dualTensorHom in Mathlib.LinearAlgebra.Contraction. At Z = 𝟙_ C it is the right unitor.

The main result is the dual-basis criterion for dualizability. If the identity of Y, viewed as a global element 𝟙_ C ⟶ (Y ⟶[C] Y), lifts along the comparison at Z = Y, then Y has left dual Yᵛ: the lift is the coevaluation and the internal-hom evaluation Y ⊗ Yᵛ ⟶ 𝟙_ C is the evaluation (TauCeti.exactPairingOfDualTensorIhom). In particular this applies when the comparison at Y is an isomorphism. Conversely, if Y has any left dual then the comparison is an isomorphism at every Z, since it factors through TauCeti.ihomIsoTensorLeft. Hence a closed object is dualizable exactly when the dual-tensor comparison at Y itself is invertible (TauCeti.nonempty_hasLeftDual_iff_isIso_dualTensorIhom_app). For a module M, this is the statement that M is finite projective exactly when the identity of M is a finite sum of φᵢ ⊗ mᵢ, that is, exactly when M admits a dual basis.

For sheaves of modules the comparison is 𝓔ᵛ ⊗ 𝓕 ⟶ 𝓗om(𝓔, 𝓕). Whether it is an isomorphism can be checked on an open cover, and once it is known to be invertible this criterion produces the coevaluation; so it is the route by which finite locally free sheaves are shown to be dualizable, with dual 𝓗om(𝓔, 𝒪).

Main declarations

• TauCeti.dualTensorIhom: the dual-tensor comparison, as a natural transformation tensorLeft (Y ⟶[C] 𝟙_ C) ⟶ ihom Y, characterized by TauCeti.whiskerLeft_dualTensorIhom_app_comp_ev;
• TauCeti.exactPairingOfDualTensorIhom: Y has left dual (Y ⟶[C] 𝟙_ C) once the identity of Y lifts along the comparison, and TauCeti.exactPairingOfIsIsoDualTensorIhom when the comparison at Y is an isomorphism;
• TauCeti.dualTensorIhom_app_eq_ihomUnitIso_hom_whiskerRight_comp and TauCeti.isIso_dualTensorIhom: for an object with a left dual the comparison is an isomorphism, so (Y ⟶[C] Z) ≅ (Y ⟶[C] 𝟙_ C) ⊗ Z;
• TauCeti.nonempty_hasLeftDual_iff_isIso_dualTensorIhom_app: the dualizability criterion.

References

• [A. Dold and D. Puppe, Duality, trace, and transfer][doldpuppe1980], §1
• [L. G. Lewis, J. P. May and M. Steinberger, Equivariant stable homotopy theory][lms1986], Chapter III, §1

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

The dual-tensor comparison (Y ⟶[C] 𝟙_ C) ⊗ Z ⟶ (Y ⟶[C] Z) of a closed object Y, natural in Z: the transpose of Y ⊗ ((Y ⟶[C] 𝟙_ C) ⊗ Z) ⟶ (Y ⊗ (Y ⟶[C] 𝟙_ C)) ⊗ Z ⟶ 𝟙_ C ⊗ Z ⟶ Z, built from the evaluation of the internal hom into the unit.

Equations

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

theorem TauCeti.dualTensorIhom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (Y : C) [CategoryTheory.Closed Y] (Z : C) : (dualTensorIhom Y).app Z = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom))

The component of the dual-tensor comparison at Z is the transpose of (Y ⊗ (Y ⟶[C] 𝟙_ C)) ⊗ Z ⟶ 𝟙_ C ⊗ Z ⟶ Z.

@[simp]

theorem TauCeti.whiskerLeft_dualTensorIhom_app_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (Y : C) [CategoryTheory.Closed Y] (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((dualTensorIhom Y).app Z)) ((CategoryTheory.ihom.ev Y).app Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom)

Evaluation characterizes the dual-tensor comparison: after it, the evaluation of the internal hom at Z is the evaluation into the unit, whiskered by Z.

@[simp]

theorem TauCeti.whiskerLeft_dualTensorIhom_app_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (Y : C) [CategoryTheory.Closed Y] (Z : C) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((dualTensorIhom Y).app Z)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom h))

Evaluation characterizes the dual-tensor comparison: after it, the evaluation of the internal hom at Z is the evaluation into the unit, whiskered by Z.

@[simp]

theorem TauCeti.dualTensorIhom_app_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (Y : C) [CategoryTheory.Closed Y] : (dualTensorIhom Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).hom

At the unit, the dual-tensor comparison is the right unitor.

@[instance_reducible]

def TauCeti.exactPairingOfDualTensorIhom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] (η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y) (hη : CategoryTheory.CategoryStruct.comp η ((dualTensorIhom Y).app Y) = CategoryTheory.MonoidalClosed.id Y) : CategoryTheory.ExactPairing ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y

The dual-basis criterion: if the identity of Y, as a global element 𝟙_ C ⟶ (Y ⟶[C] Y), lifts to η : 𝟙_ C ⟶ (Y ⟶[C] 𝟙_ C) ⊗ Y along the dual-tensor comparison, then (Y ⟶[C] 𝟙_ C) is a left dual of Y, with coevaluation η and evaluation the evaluation of the internal hom.

Not an instance: the pairing depends on the chosen lift.

Equations

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

@[simp]

theorem TauCeti.exactPairingOfDualTensorIhom_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] (η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y) (hη : CategoryTheory.CategoryStruct.comp η ((dualTensorIhom Y).app Y) = CategoryTheory.MonoidalClosed.id Y) : ε_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = (CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The evaluation of the pairing produced by the dual-basis criterion is the evaluation of the internal hom into the unit.

@[simp]

theorem TauCeti.exactPairingOfDualTensorIhom_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] (η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y) (hη : CategoryTheory.CategoryStruct.comp η ((dualTensorIhom Y).app Y) = CategoryTheory.MonoidalClosed.id Y) : η_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = η

The coevaluation of the pairing produced by the dual-basis criterion is the given lift of the identity.

@[instance_reducible]

noncomputable def TauCeti.exactPairingOfIsIsoDualTensorIhom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.IsIso ((dualTensorIhom Y).app Y)] : CategoryTheory.ExactPairing ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y

If the dual-tensor comparison of Y is an isomorphism at Y itself, then (Y ⟶[C] 𝟙_ C) is a left dual of Y: the coevaluation is the preimage of the identity of Y and the evaluation is that of the internal hom.

Not an instance: CategoryTheory.HasLeftDual may already provide a different left dual.

Equations

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

theorem TauCeti.exactPairingOfIsIsoDualTensorIhom_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.IsIso ((dualTensorIhom Y).app Y)] : ε_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = (CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

The evaluation of the pairing of an object with invertible dual-tensor comparison is the evaluation of the internal hom into the unit.

theorem TauCeti.exactPairingOfIsIsoDualTensorIhom_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.IsIso ((dualTensorIhom Y).app Y)] : η_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.id Y) (CategoryTheory.inv ((dualTensorIhom Y).app Y))

The coevaluation of the pairing of an object with invertible dual-tensor comparison is the preimage of the identity of Y under the comparison.

theorem TauCeti.dualTensorIhom_app_eq_ihomUnitIso_hom_whiskerRight_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] (D : C) [CategoryTheory.ExactPairing D Y] (Z : C) : (dualTensorIhom Y).app Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ihomUnitIso D Y).hom Z) ((ihomIsoTensorLeft D Y).inv.app Z)

For a left dual D of Y, the dual-tensor comparison factors through the identification (Y ⟶[C] 𝟙_ C) ≅ D and the comparison D ⊗ Z ⟶ (Y ⟶[C] Z) of the pairing.

theorem TauCeti.isIso_dualTensorIhom_of_exactPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] (D : C) [CategoryTheory.ExactPairing D Y] : CategoryTheory.IsIso (dualTensorIhom Y)

The dual-tensor comparison of an object with a left dual D is an isomorphism, so the internal hom out of Y is tensoring with (Y ⟶[C] 𝟙_ C).

instance TauCeti.isIso_dualTensorIhom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] [CategoryTheory.HasLeftDual Y] : CategoryTheory.IsIso (dualTensorIhom Y)

The dual-tensor comparison of an object with a left dual is an isomorphism, so the internal hom out of Y is tensoring with (Y ⟶[C] 𝟙_ C).

theorem TauCeti.nonempty_hasLeftDual_iff_isIso_dualTensorIhom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y : C} [CategoryTheory.Closed Y] : Nonempty (CategoryTheory.HasLeftDual Y) ↔ CategoryTheory.IsIso ((dualTensorIhom Y).app Y)

A closed object Y has a left dual exactly when its dual-tensor comparison at Y itself is an isomorphism; the left dual is then (Y ⟶[C] 𝟙_ C).