Dualizable quasicoherent sheaves on an affine scheme

A quasicoherent sheaf E on Spec R is dualizable in the symmetric monoidal category QuasicoherentSheaf (Spec R) if and only if its module of global sections is finitely generated and projective. More generally, a quasicoherent sheaf E on an affine scheme X is dualizable in QuasicoherentSheaf X if and only if it is finite locally free.

Since M ↦ M~ is a fully faithful monoidal functor whose essential image consists of the quasicoherent sheaves, exact pairings between quasicoherent sheaves on Spec R are the images of exact pairings between R-modules, and an R-module is dualizable exactly when it is finite projective (ModuleCat.nonempty_hasLeftDual_iff_finite_projective). The sheaf associated with a finite projective module is finite locally free (TauCeti.AlgebraicGeometry.isFiniteLocallyFree_tilde), and finite locally free sheaves are dualizable (TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_of_isFiniteLocallyFree). An affine scheme X is identified with Spec Γ(X, ⊤) by X.isoSpec; pullback along this isomorphism preserves left and right dualizability, as does any pullback to an affine target (TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_pullback and TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasRightDual_pullback), and finite local freeness can be checked after it (AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_forall_pullback).

Main declarations

• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_finite_projective: a quasicoherent sheaf on Spec R is dualizable if and only if its global sections form a finite projective R-module;
• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree: a quasicoherent sheaf on an affine scheme is dualizable if and only if it is finite locally free;
• TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasRightDual_iff_isFiniteLocallyFree: the corresponding characterization in terms of right duals.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_finite_projective {R : CommRingCat} (E : QuasicoherentSheaf (AlgebraicGeometry.Spec R)) : Nonempty (CategoryTheory.HasLeftDual E) ↔ Module.Finite ↑R ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj E.obj) ∧ Module.Projective ↑R ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj E.obj)

A quasicoherent sheaf on Spec R is dualizable in QuasicoherentSheaf (Spec R) if and only if its global sections form a finitely generated projective R-module.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (E : QuasicoherentSheaf X) : Nonempty (CategoryTheory.HasLeftDual E) ↔ AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X E.obj

A quasicoherent sheaf on an affine scheme X is dualizable in QuasicoherentSheaf X if and only if it is finite locally free.

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasRightDual_iff_isFiniteLocallyFree {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (E : QuasicoherentSheaf X) : Nonempty (CategoryTheory.HasRightDual E) ↔ AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X E.obj

A quasicoherent sheaf on an affine scheme X has a right dual in QuasicoherentSheaf X if and only if it is finite locally free.