19.24. Finiteness.CohomologicalH0Finiteness🔗

Jacobians.Finiteness.CohomologicalH0Finiteness — source

OmegaD_le_add_single

The 𝒪_D-functions on U are contained in the 𝒪_{D+P}-functions (adding the effective point P only weakens the order bound −(D+P) ≤ −D).

theorem OmegaD_le_add_single (U : Opens X) :
    OmegaD D U ≤ OmegaD (D + Finsupp.single P 1) U

sections0_le_add_single

The 𝒪_D 0-sections are contained in the 𝒪_{D+P} 0-sections.

theorem sections0_le_add_single' :
    𝔘.sections0 D ≤ 𝔘.sections0 (D + Finsupp.single P 1)

globalSections_le_add_single

The global 𝒪_D-sections are contained in the global 𝒪_{D+P}-sections (same ker δ⁰, weaker sheaf condition).

theorem globalSections_le_add_single' :
    𝔘.globalSections D ≤ 𝔘.globalSections (D + Finsupp.single P 1)

finiteDimensional_globalSections_quotient

globalSections (D+P) ⧸ globalSections D is finite-dimensional. globalSections = ker δ⁰ ⊓ sections0, so the quotient injects (via K = ker δ⁰) into the finite section quotient sections0 (D+P) ⧸ sections0 D (finiteDimensional_inf_quotient, finiteDimensional_sections0_quotient).

theorem finiteDimensional_globalSections_quotient :
    FiniteDimensional ℂ
      (𝔘.globalSections (D + Finsupp.single P 1) ⧸
        (𝔘.globalSections D).submoduleOf (𝔘.globalSections (D + Finsupp.single P 1)))

finiteDimensional_globalSections_add_single_of

Forward per-point step. H⁰(𝒪_D) finite ⟹ H⁰(𝒪_{D+P}) finite. H⁰(𝒪_{D+P}) is the extension of the finite submodule H⁰(𝒪_D) (via the order-weakening inclusion) by the finite correction quotient globalSections (D+P) ⧸ globalSections D (Module.Finite.of_submodule_quotient).

theorem finiteDimensional_globalSections_add_single_of
    (h : FiniteDimensional ℂ ↥(𝔘.globalSections D)) :
    FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))

finiteDimensional_globalSections_of_add_single

Backward per-point step. H⁰(𝒪_{D+P}) finite ⟹ H⁰(𝒪_D) finite: H⁰(𝒪_D) is (via the order-weakening inclusion, injective) a submodule of the finite-dimensional H⁰(𝒪_{D+P}).

theorem finiteDimensional_globalSections_of_add_single
    (h : FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1))) :
    FiniteDimensional ℂ ↥(𝔘.globalSections D)

finiteDimensional_globalSections_add_single_iff

The bidirectional per-point step. H⁰(𝒪_{D+P}) is finite iff H⁰(𝒪_D) is.

theorem finiteDimensional_globalSections_add_single_iff :
    FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P 1)) ↔
      FiniteDimensional ℂ ↥(𝔘.globalSections D)

finiteDimensional_globalSections_add_singlePoint_iff

H⁰(𝒪_{D + single P k}) is finite iff H⁰(𝒪_D) is, for any integer k (Int.induction_on; ±1 at a time is the per-point step).

theorem finiteDimensional_globalSections_add_singlePoint_iff (k : ℤ) :
    FiniteDimensional ℂ ↥(𝔘.globalSections (D + Finsupp.single P k)) ↔
      FiniteDimensional ℂ ↥(𝔘.globalSections D)

finiteDimensional_globalSections_zero

Base case (Liouville). H⁰(𝒪) is finite-dimensional: finrank ℂ H⁰(0) = h0Dim 0 = l(0) = 1 is positive (h0Dim_eq_lDim + lDim_zero_eq_one), so FiniteDimensional.of_finrank_pos.

theorem finiteDimensional_globalSections_zero :
    FiniteDimensional ℂ ↥(𝔘.globalSections (0 : Divisor X))

finiteDimensional_globalSections_of_zero

Finiteness of H⁰(𝒪_D) for any divisor D, on a FIXED cover, from the D = 0 base (the divisor induction). Finsupp.induction on D adds one point at a time; each addition is the single-point step.

theorem finiteDimensional_globalSections_of_zero (D : Divisor X) :
    FiniteDimensional ℂ ↥(𝔘.globalSections D)

finiteDimensional_globalSections

Finiteness of H⁰(𝔘, 𝒪_D) for any cover and any divisor (Forster §14/§16 compactness; l(D) = h⁰(D) < ∞). The Liouville base H⁰(0) (finrank 1) is climbed to general D one point at a time via the principal-part skyscraper stalk quotient (finiteDimensional_globalSections_of_zero): the [FiniteDimensional ℂ H⁰(𝒪_{D+P})] instance hypothesis of the χ-additivity skyscraper LES.

theorem finiteDimensional_globalSections (𝔘 : FiniteCover X) (D : Divisor X) :
    FiniteDimensional ℂ ↥(𝔘.globalSections D)