Serre finiteness on projective space

Every coherent sheaf on Pⁿ_k has finite-dimensional cohomology in every degree, and FiniteDimensionalCohomology k Pⁿ is inhabited by a theorem rather than a supplied field.

This is S3 of #332 (#571). The two inputs are:

• Serre's theorem (exists_epi_coproduct_twistingSheaf_ge): every coherent F is a quotient of ∐ O(-N), with N ≥ 1 chosen so that the twist is negative.
• Cohomology of the twists: Hⁿ⁺¹(Pⁿ, O(d)) is finite-dimensional for every d (module_finite_linearCoherentH_projectiveSpaceTwist, S1), and H⁰(Pⁿ, O(d)) = 0 for d < 0 (polynomialIntTwisting_H_zero_subsingleton). Taking N ≥ 1 is what makes the second statement the one needed: the degree-zero group of a nonnegative twist is the space of homogeneous polynomials, whose finiteness is a separate computation that never has to be made.

The dévissage itself is module_finite_linearCoherentH_of_devissage: descending induction from the finite-cover vanishing bound along the linear exact sequence Hⁱ(∐ O(-N)) → Hⁱ(F) → Hⁱ⁺¹(K).

The surjection, read in Coh

Serre's surjection lives in Pⁿ.Modules; the long exact sequence wants a short exact sequence in Coh Pⁿ. Coh.ι is fully faithful and preserves finite colimits, so the coproduct of the twists in Coh maps to the coproduct in Modules and the surjection lifts along the preimage; faithfulness reflects the epimorphism, and the kernel in Coh completes the sequence.

Not here

Closed subvarieties of Pⁿ. ProjectiveVariety.lean transports finiteness along the closed immersion of a ProjectivePresentation, once the comparison is shown k-linear.

theorem AlgebraicGeometry.Proj.module_finite_linearCoherentH_projectiveSpaceTwist_of_neg (ι k : Type u) [Field k] [Fintype ι] [Nontrivial ι] (d : ℤ) (hd : d < 0) (i : ℕ) : Module.Finite k ↑((Cohomology.linearCoherentH k (Proj (MvPolynomial.polynomialGrading ι k)) i).obj (projectiveSpaceTwist ι k d))

Hⁱ(Pⁿ, O(d)) is finite-dimensional in every degree for a negative twist.

Degree zero vanishes (polynomialIntTwisting_H_zero_subsingleton); positive degrees are S1 (module_finite_linearCoherentH_projectiveSpaceTwist).

theorem AlgebraicGeometry.Proj.exists_shortExact_coproduct_twist (ι k : Type u) [Field k] [Fintype ι] [Nonempty ι] (F : Coh (Proj (MvPolynomial.polynomialGrading ι k))) : ∃ (S : CategoryTheory.ShortComplex (Coh (Proj (MvPolynomial.polynomialGrading ι k)))) (_ : S.ShortExact) (x : S.X₃ ≅ F) (N : ℕ) (_ : 1 ≤ N) (I : Type u) (x : Finite I), S.X₂ = ∐ fun (x : I) => projectiveSpaceTwist ι k (-↑N)

Every coherent sheaf on Pⁿ is the quotient, in Coh Pⁿ, of a finite coproduct of copies of a negative twist, with coherent kernel: Serre's surjection lifted along Coh.ι.

theorem AlgebraicGeometry.Proj.module_finite_linearCoherentH_projectiveSpace (ι k : Type u) [Field k] [Fintype ι] [Nontrivial ι] (i : ℕ) (F : Coh (Proj (MvPolynomial.polynomialGrading ι k))) : Module.Finite k ↑((Cohomology.linearCoherentH k (Proj (MvPolynomial.polynomialGrading ι k)) i).obj F)

Serre finiteness on projective space: every coherent sheaf on Pⁿ_k has finite-dimensional cohomology in every degree.

noncomputable def AlgebraicGeometry.Proj.projectiveSpaceFiniteDimensionalCohomology (ι k : Type u) [Field k] [Fintype ι] [Nontrivial ι] : Cohomology.FiniteDimensionalCohomology k (Proj (MvPolynomial.polynomialGrading ι k))

The finite-dimensional cohomology package of projective space, proved rather than supplied. The linear realization is the canonical one; the finite field is Serre finiteness.

Equations

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

noncomputable def AlgebraicGeometry.Proj.projectiveSpaceFiniteCohomology (ι k : Type u) [Field k] [Fintype ι] [Nontrivial ι] : Cohomology.FiniteCohomology k (Proj (MvPolynomial.polynomialGrading ι k))

The finite cohomology package of projective space: Serre finiteness together with the finite-affine-cover vanishing bound. Every Euler characteristic on Pⁿ now rests on theorems alone.

Equations

• AlgebraicGeometry.Proj.projectiveSpaceFiniteCohomology ι k = (AlgebraicGeometry.Proj.projectiveSpaceFiniteDimensionalCohomology ι k).toFiniteCohomology