Dualizable modules and finite projectivity

An R-module is dualizable in the symmetric monoidal category ModuleCat R exactly when it is finite projective. Under the internal-Hom identification, the categorical dual-tensor map is Mathlib's dualTensorHom; invertibility at the module itself supplies a finite dual basis, and Mathlib's dual-basis criterion yields finite projectivity. Conversely, a finite projective module has an invertible contraction, so the categorical dual-basis criterion constructs its dual.

This is the affine algebraic criterion used in comparing finite locally free sheaves with dualizable quasicoherent sheaves.

The dual-basis criterion used here is from Mathlib's LinearAlgebra.Contraction.

@[instance_reducible]

noncomputable instance ModuleCat.hasLeftDualOfFiniteProjective {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] : CategoryTheory.HasLeftDual M

A finite projective module is dualizable, with internal Hom into the tensor unit as a canonical left dual.

Equations

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

@[instance_reducible]

noncomputable instance ModuleCat.hasRightDualOfFiniteProjective {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] : CategoryTheory.HasRightDual M

A finite projective module also has a right dual in the symmetric monoidal category ModuleCat R.

Equations

• M.hasRightDualOfFiniteProjective = CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual

@[simp]

theorem ModuleCat.leftDual_of_finite_projective {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] : ᘁM = (CategoryTheory.ihom M).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

The chosen left dual of a finite projective module is its internal Hom into the unit.

@[simp]

theorem ModuleCat.rightDual_of_finite_projective {R : Type u} [CommRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Module.Projective R ↑M] : Mᘁ = (CategoryTheory.ihom M).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

The chosen right dual of a finite projective module is its internal Hom into the unit.

theorem ModuleCat.finite_projective_of_hasLeftDual {R : Type u} [CommRing R] (M : ModuleCat R) [CategoryTheory.HasLeftDual M] : Module.Finite R ↑M ∧ Module.Projective R ↑M

A dualizable module is finite projective: its coevaluation gives a finite dual basis.

theorem ModuleCat.finite_projective_of_hasRightDual {R : Type u} [CommRing R] (M : ModuleCat R) [CategoryTheory.HasRightDual M] : Module.Finite R ↑M ∧ Module.Projective R ↑M

A module with a right dual is finite projective.

theorem ModuleCat.nonempty_hasLeftDual_iff_finite_projective {R : Type u} [CommRing R] (M : ModuleCat R) : Nonempty (CategoryTheory.HasLeftDual M) ↔ Module.Finite R ↑M ∧ Module.Projective R ↑M

An R-module is dualizable if and only if it is finite projective.

theorem ModuleCat.nonempty_hasRightDual_iff_finite_projective {R : Type u} [CommRing R] (M : ModuleCat R) : Nonempty (CategoryTheory.HasRightDual M) ↔ Module.Finite R ↑M ∧ Module.Projective R ↑M

An R-module has a right dual if and only if it is finite projective.