Finiteness of Hom from a line bundle

This file gives the honest reduction from Serre finiteness to finite-dimensional Hom spaces with a line-bundle source. The linear comparison

Hom(L, N) ≃ₗ[k] Γ(X, L⁻¹ ⊗ N)

transports finite-dimensionality from coherent H⁰. Tensoring by the invertible sheaf L⁻¹ preserves finite presentation, so a coherent target N supplies the required coherent tensor without an extra geometric premise.

Main results

• LineBundleData.module_finite_hom_of_finiteHZero isolates the formal transport from finite coherent H⁰ to finite Hom;
• ProjectivePresentation.module_finite_lineBundleHom supplies tensor coherence and the H⁰ input from a coherent target and projective Serre finiteness.

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.module_finite_hom_of_finiteHZero {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (L : LineBundleData Y) (N : Y.Modules) (hTensor : IsCoherent Y (L.inverse.tensorObj N)) (hHZero : Module.Finite k ↑((Cohomology.linearCoherentH k Y 0).obj { obj := L.inverse.tensorObj N, property := hTensor })) : Module.Finite k (L.line ⟶ N)

Finite-dimensional H⁰ of the coherent tensor L⁻¹ ⊗ N implies that Hom(L, N) is finite-dimensional.

theorem AlgebraicGeometry.ProjectivePresentation.module_finite_lineBundleHom {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) : Module.Finite k (L.line ⟶ N)

Hom from a line bundle to a coherent module sheaf on a projectively presented variety is finite-dimensional.