Dévissage: finite-dimensional cohomology from a class of generators

The descending induction behind Serre's finiteness theorem, stated once for any variety and any supply of generators.

The argument

Suppose every coherent F sits in a short exact sequence 0 → K → G → F → 0 of coherent sheaves whose middle term has finite-dimensional cohomology in every degree. Above the cohomological bound of a finite affine cover every group vanishes (coherent_H_subsingleton_of_cohomologicalBound), which starts a descending induction on the degree; at each step the exact, k-linear Hⁱ(G) → Hⁱ(F) → Hⁱ⁺¹(K) (linearCoherentH_exact₃) has finite-dimensional outer terms -- the left by hypothesis, the right by the inductive hypothesis applied to K -- so its middle term is finite-dimensional (Function.Exact.module_finite_of_finite).

The linearity of the connecting map is what makes this work over the base field; see LinearConnecting.lean for why an additive exact sequence would not suffice.

The generators are a hypothesis here

On projective space the generators are the twisted structure sheaves, supplied by Serre's theorem in the form ∐ O(-N) ↠ F (ProjectiveSpectrum/Modules/TwistInverse.lean); Projective.lean instantiates this file there. Nothing about them enters the induction beyond the finiteness of their cohomology, which is why the induction is stated abstractly.

module_finite_linearCoherentH_coproduct supplies the one bookkeeping fact the instantiation needs: cohomology of a finite coproduct of sheaves with finite-dimensional cohomology is finite-dimensional, because linearCoherentH is additive and so carries finite coproducts to finite products of vector spaces.

theorem AlgebraicGeometry.Cohomology.module_finite_linearCoherentH_coproduct {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsLocallyNoetherian X] {J : Type u} [Finite J] (G : J → Coh X) (i : ℕ) (hG : ∀ (j : J), Module.Finite k ↑((linearCoherentH k X i).obj (G j))) : Module.Finite k ↑((linearCoherentH k X i).obj (∐ G))

Cohomology of a finite coproduct of coherent sheaves with finite-dimensional cohomology is finite-dimensional. linearCoherentH is additive, so it preserves finite coproducts, and a finite coproduct in ModuleCat k is a finite product of vector spaces.

Additivity of linearCoherentH needs no variety hypothesis, so IsVariety is omitted rather than carried: runLinter's unusedArguments rejects a section instance a declaration does not use.

theorem AlgebraicGeometry.Cohomology.module_finite_linearCoherentH_of_devissage {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsNoetherian X] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] (hgen : ∀ (F : Coh X), ∃ (S : CategoryTheory.ShortComplex (Coh X)) (_ : S.ShortExact) (x : S.X₃ ≅ F), ∀ (i : ℕ), Module.Finite k ↑((linearCoherentH k X i).obj S.X₂)) (i : ℕ) (F : Coh X) : Module.Finite k ↑((linearCoherentH k X i).obj F)

Dévissage. If every coherent sheaf on X is the quotient of a coherent sheaf with finite-dimensional cohomology in every degree, by a coherent kernel, then every coherent sheaf has finite-dimensional cohomology in every degree.

Descending induction on the degree, from the vanishing bound of a finite affine cover, along the linear exact sequence Hⁱ(G) → Hⁱ(F) → Hⁱ⁺¹(K).