29.3. RiemannRoch🔗

Jacobians.RiemannRoch — source

exists_riemannRoch_divisor

Riemann–Roch (Forster Thm 16.9, Serre-dual form): a canonical divisor K with l(D) − l(K−D) = deg D + 1 − g for every D.

Proved via the Miranda Ch. VI Laurent-tail route (LaurentTail.exists_riemannRoch_divisor_unconditional): RR-I on the Mittag-Leffler tail spaces (riemannRoch_tailForm), Serre duality for the tail H¹ in the meromorphic pair frame ω = h·dg₀ (h1TailDim_eq_lDim_pairCanonical_sub, every genus — the descent input is the genus-free planar-Stokes residue theorem residueSum_pairForm_mul_eq_zero_unconditional), and l(K) = genus from the §17.4 canonical-form isomorphism (hKgenus_unconditional), with K = div (dg₀) for the nonconstant meromorphic g₀ of exists_nonconstant_meromorphic. The Čech tower — finiteness, skyscraper LES, the Riemann inequality feeding exists_nonconstant_meromorphic — is load-bearing for the tail route's pole-budget bound.

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

lDim_canonical_eq_genus

l(K) = g, from Riemann–Roch at D = 0 (and l(0) = 1).

theorem lDim_canonical_eq_genus {K : Divisor X}
    (hrr : ∀ D : Divisor X, (lDim (X := X) D : ℤ) - (lDim (X := X) (K - D) : ℤ)
      = Divisor.deg X D + 1 - (genus X : ℤ)) : lDim (X := X) K = genus X

deg_canonical

deg K = 2g − 2, from Riemann–Roch at D = K.

theorem deg_canonical {K : Divisor X}
    (hrr : ∀ D : Divisor X, (lDim (X := X) D : ℤ) - (lDim (X := X) (K - D) : ℤ)
      = Divisor.deg X D + 1 - (genus X : ℤ)) : Divisor.deg X K = 2 * (genus X : ℤ) - 2

exists_singleSimplePole_of_genus_zero_of_rr

Touch point. genus X = 0 + Riemann–Roch ⟹ a meromorphic function with a single simple pole. RR at D = P gives l(P) = 2 > 1 = l(0), so L(P)/germZero is not spanned by the constant class; a member outside that span is not germ-constant, hence (by Liouville's contrapositive germ_eq_const_of_mem_linearSystem_zero) has a pole, necessarily a *simple* pole at P — the only pole L(P) permits — and by faithfulness its order is finite everywhere. This discharges exists_singleSimplePole_of_genus_zero modulo {riemannRoch, deg_div}.

theorem exists_singleSimplePole_of_genus_zero_of_rr (hg : genus X = 0) :
    ∃ (P : X) (f : MeromorphicFunction X), f.HasSingleSimplePole P