A machine-checked solution to the Jacobians challenge

28.5. H1Genus.CechH1Genus🔗

Jacobians.H1Genus.CechH1Genussource

exists_effective_h1Dim_eq_zero

H¹(𝔘, 𝒪_A) vanishes for a suitable effective A of arbitrarily large degree — step 1 of the dimension count: kill a basis of H¹(𝒪) with the cup-multiplication lemma, then use surjectivity of the inclusion-induced map (Forster 16.8). The lower-degree parameter m adds m·P to push deg A past any prescribed bound.

theorem exists_effective_h1Dim_eq_zero (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable)
    (m : ℕ) :
    ∃ A : Divisor X, 0 ≤ A ∧ (m : ℤ) ≤ Divisor.deg X A ∧ 𝔘.h1Dim A = 0

FiniteCover.h1Dim_zero_eq_genus

The dimension count h¹(𝔘, 𝒪) = genus X (Miranda Prop. X.2.6 / the D = 0 Dolbeault anchor, GAGA-free): on any locally realizable finite cover, the Čech of the structure sheaf has dimension the genus. Proven by vanishing at a large effective A (exists_effective_h1Dim_eq_zero Čech-side, tail Serre duality tail-side) and subtracting cohomological Riemann–Roch from tail Riemann–Roch at A.

theorem FiniteCover.h1Dim_zero_eq_genus (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable) :
    𝔘.h1Dim 0 = genus X