Finiteness and amplitude of Ext from a line bundle

For a projectively presented variety, the linear comparison

Extⁿ_{X.Modules}(L, N) ≃ₗ[k] Hⁿ(X, L⁻¹ ⊗ N)

transports both halves of Serre finiteness: every degree is finite-dimensional, and the Ext groups vanish above the finite-affine-cover cohomological bound of the coherent inverse twist. Thus the natural-number finrank support is finite.

These results concern Ext in X.Modules with a line-bundle source. They do not claim Ext finiteness for arbitrary coherent sources and do not compare with Ext internal to Coh X.

Main results

• ProjectivePresentation.module_finite_lineBundleExt proves degreewise finite-dimensionality;
• ProjectivePresentation.lineBundleExt_subsingleton_of_bound_lt gives the explicit amplitude;
• ProjectivePresentation.lineBundleExt_finrankSupport_finite packages finite support.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_lineBundleExt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) [Nontrivial P.index] (L : Scheme.Modules.LineBundleData X) (N : X.Modules) (hN : Scheme.Modules.IsCoherent X N) (n : ℕ) : Module.Finite k (CategoryTheory.Abelian.Ext L.line N n)

Ext in X.Modules from a line bundle to a coherent module sheaf is finite-dimensional in every nonnegative degree on a projectively presented variety.

theorem AlgebraicGeometry.ProjectivePresentation.lineBundleExt_subsingleton_of_bound_lt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (L : Scheme.Modules.LineBundleData X) (N : X.Modules) (hN : Scheme.Modules.IsCoherent X N) (n : ℕ) (hn : P.finiteCohomology.bound { obj := L.inverse.tensorObj N, property := ⋯ } < n) : Subsingleton (CategoryTheory.Abelian.Ext L.line N n)

Ext from L to N vanishes strictly above the cohomological bound of L⁻¹ ⊗ N.

theorem AlgebraicGeometry.ProjectivePresentation.lineBundleExt_finrankSupport_subset_range {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (L : Scheme.Modules.LineBundleData X) (N : X.Modules) (hN : Scheme.Modules.IsCoherent X N) : (Function.support fun (n : ℕ) => ↑(Module.finrank k (CategoryTheory.Abelian.Ext L.line N n))) ⊆ ↑(Finset.range (P.finiteCohomology.bound { obj := L.inverse.tensorObj N, property := ⋯ } + 1))

The finrank support of ambient Ext from a line bundle lies below the cohomological bound of the coherent inverse twist.

theorem AlgebraicGeometry.ProjectivePresentation.lineBundleExt_finrankSupport_finite {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (L : Scheme.Modules.LineBundleData X) (N : X.Modules) (hN : Scheme.Modules.IsCoherent X N) : (Function.support fun (n : ℕ) => ↑(Module.finrank k (CategoryTheory.Abelian.Ext L.line N n))).Finite

Only finitely many nonnegative Ext degrees from L to N have nonzero finrank.