A machine-checked solution to the Jacobians challenge

19.25. Finiteness.CohomologicalRR🔗

Jacobians.Finiteness.CohomologicalRR — source

six_term_exact_alt_sum

Alternating dimension sum of a 6-term exact sequence (rank–nullity crank). For an exact sequence of finite-dimensional K-vector spaces 0 → A →[f₁] B →[f₂] C →[f₃] D →[f₄] E → 0 (f₁ injective, exact at B, C, D, f₄ surjective) the alternating sum of dimensions is 0: dim A − dim B + dim C − dim D + dim E = 0.

Proof: rank–nullity dim (range fₖ) + dim (ker fₖ) = dim (source) at each of the four maps; exactness rewrites every ker fₖ₊₁ as range fₖ; ker f₁ = 0 (injective) and range f₄ = E (surjective); omega finishes the integer bookkeeping.

theorem six_term_exact_alt_sum {K A B C E F : Type*} [Field K]
    [AddCommGroup A] [Module K A] [FiniteDimensional K A]
    [AddCommGroup B] [Module K B] [FiniteDimensional K B]
    [AddCommGroup C] [Module K C] [FiniteDimensional K C]
    [AddCommGroup E] [Module K E] [FiniteDimensional K E]
    [AddCommGroup F] [Module K F] [FiniteDimensional K F]
    (f₁ : A →ₗ[K] B) (f₂ : B →ₗ[K] C) (f₃ : C →ₗ[K] E) (f₄ : E →ₗ[K] F)
    (hf₁ : Function.Injective f₁)
    (h₁ : Function.Exact f₁ f₂) (h₂ : Function.Exact f₂ f₃) (h₃ : Function.Exact f₃ f₄)
    (hf₄ : Function.Surjective f₄) :
    (Module.finrank K A : ℤ) - Module.finrank K B + Module.finrank K C
      - Module.finrank K E + Module.finrank K F = 0

chi

The Euler characteristic χ(D) := h⁰(D) − h¹(D) (as an integer).

noncomputable def chi (𝔘 : FiniteCover X) (D : Divisor X) : ℤ

h0Dim_zero_eq_one

Base case (Liouville). h⁰(𝔘, 𝒪) = 1: the h⁰ = l(D) bridge identifies the global Čech sections with the linear system, and l(0) = 1 by Liouville on the compact connected X.

theorem h0Dim_zero_eq_one (𝔘 : FiniteCover X) : (𝔘.h0Dim 0 : ℤ) = 1

chi_jump_of_LES

The crank (complete). Given the skyscraper long exact sequence, the single-point χ-jump χ(D+P) = χ(D) + 1 is pure linear algebra: the alternating dimension sum of the six-term exact sequence is 0 (six_term_exact_alt_sum), and finrank ℂ_P = 1 (skyDim). Rearranging h⁰(D) − h⁰(D+P) + 1 − h¹(D) + h¹(D+P) = 0 gives the jump. No analytic content.

theorem chi_jump_of_LES {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (S : SkyscraperLES 𝔘 D P) : 𝔘.chi (D + Finsupp.single P 1) = 𝔘.chi D + 1

exists_localRealizationData

Existence of the local-realization datum (the skyscraper-irreducible core of cohomological Riemann–Roch, Forster §16) — from local realizability of the cover.

LocalRealizationData 𝔘 D P (SkyscraperSnake) packages exactly the two pieces that the snake lemma cannot supply (plus finiteness, discharged unconditionally):

  • e0 : H⁰(Q) ≅ ℂ with hcompat — the local realization of the degree-0 quotient cohomology with the skyscraper stalk ℂ (the order-(−D(P)−1) principal-part coefficient at P);

  • Subsingleton H¹(Q) — acyclicity of the skyscraper quotient complex.

Both are built by the star-of-P cone construction (SkyscraperConeRealization), which drops the impossible singleton-star hypothesis hstar (P ∈ U j → j = i cannot hold at every overlap point on a compact connected X). The construction consumes a single analytic input, LocallyRealizable 𝔘: the principal-part coefficient coeffGermLin is surjective at every cover-set U j ∋ P (local Mittag–Leffler). The apex vertex is any U i ∋ P (exists since 𝔘 covers X).

theorem exists_localRealizationData (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable)
    (D : Divisor X) (P : X) :
    Nonempty (𝔘.LocalRealizationData D P)

exists_skyscraperLES

The skyscraper long exact sequence (Forster §16), from the local-realization datum exists_localRealizationData via the snake assembly skyscraperLES_of_localRealization (which builds the connecting map, all exactness, the LES termination, and carries the finiteness instances).

theorem exists_skyscraperLES (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) (D : Divisor X)
    (P : X) :
    Nonempty (SkyscraperLES 𝔘 D P)

chi_jump

Single-point χ-jump (Forster §16). χ(D + P) = χ(D) + 1: the linear-algebra crank chi_jump_of_LES run on the skyscraper long exact sequence (exists_skyscraperLES).

theorem chi_jump (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) (D : Divisor X) (P : X) :
    𝔘.chi (D + Finsupp.single P 1) = 𝔘.chi D + 1

chi_add_single

Iterated χ-jump. χ(D + n·P) = χ(D) + n for every integer n, by induction on n built on the unit jump chi_jump (both directions). Pure ℤ-arithmetic; no analytic content.

theorem chi_add_single (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) (D : Divisor X) (P : X)
    (n : ℤ) :
    𝔘.chi (D + Finsupp.single P n) = 𝔘.chi D + n

chi_eq_deg_add_chi_zero

χ-additivity over the base. χ(D) = deg D + χ(0) for every divisor D, by induction on the finite support of D (Finsupp.induction): the empty divisor is the base, and each single a b-summand contributes b = deg (single a b) to both sides via the iterated jump chi_add_single and additivity of deg (Divisor.deg_add/deg_single). Pure ℤ-arithmetic.

theorem chi_eq_deg_add_chi_zero (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) (D : Divisor X) :
    𝔘.chi D = Divisor.deg X D + 𝔘.chi 0

cohomological_riemannRoch

Cohomological Riemann–Roch (χ-additivity, Forster §16). h⁰(D) − h¹(D) = deg D + 1 − h¹(0).

Rearrangement of χ(D) = deg D + χ(0) (chi_eq_deg_add_chi_zero, the iterated skyscraper jump + divisor induction) using the Liouville base h⁰(0) = 1 (h0Dim_zero_eq_one), since then χ(0) = 1 − h¹(0).

theorem cohomological_riemannRoch (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) (D : Divisor X) :
    (𝔘.h0Dim D : ℤ) - 𝔘.h1Dim D = Divisor.deg X D + 1 - 𝔘.h1Dim 0