27.7. TailDuality.RiemannRochUnconditional🔗

Jacobians.TailDuality.RiemannRochUnconditional — source

lDim_pairCanonicalDivisor_eq_genus

l(K) = genus for the pair-frame canonical divisor K = div (dg₀) (Forster §17.4 at D = 0): pairCanonicalDivisor is by construction the form divisor of the §17.4 datum ω₀ = dg₀.

theorem lDim_pairCanonicalDivisor_eq_genus (g₀ : MeromorphicFunction X)
    (hg₀ : ¬ IsGermConstant g₀) :
    lDim (X := X) (pairCanonicalDivisor g₀ hg₀) = genus X

h1TailDim_zero_eq_genus_unconditional

h¹(0) = genus (Miranda's "three genera", arithmetic = analytic) — every genus: Serre duality at D = 0 reads h¹(0) = l(K), and l(K) = genus by §17.4.

theorem h1TailDim_zero_eq_genus_unconditional : h1TailDim (X := X) 0 = genus X

exists_riemannRoch_divisor_unconditional

Riemann–Roch, unconditional (Forster Thm 16.9 / Miranda Ch. VI Thm 3.11): a canonical divisor K with l(D) − l(K−D) = deg D + 1 − g for every divisor D — every genus. This is the exact statement shape of Jacobians.exists_riemannRoch_divisor.

theorem exists_riemannRoch_divisor_unconditional :
    ∃ K : Divisor X, ∀ D : Divisor X,
      (lDim (X := X) D : ℤ) - (lDim (X := X) (K - D) : ℤ)
        = Divisor.deg X D + 1 - (genus X : ℤ)