27.6. TailDuality.RiemannRochGenusPos🔗

Jacobians.TailDuality.RiemannRochGenusPos — source

formOrderW_holToMero

The meromorphic order of (the meromorphic-form image of) a holomorphic 1-form is its omegaOrderAt: both read meromorphicOrderAt of the same chart coefficient at the chart centre.

theorem formOrderW_holToMero (ω₀ : HolomorphicOneForms X) (p : X) :
    (holToMero ω₀).formOrderW p = omegaOrderAt ω₀ p

canonicalForm17DataOfHolomorphic

A nonzero holomorphic 1-form is a §17.4 canonical-form datum: ω₀ qua meromorphic 1-form, together with its zero divisor canonicalDivisorOf ω₀ (the tail-duality canonical divisor K).

noncomputable def canonicalForm17DataOfHolomorphic (ω₀ : HolomorphicOneForms X)
    (hω₀ : ω₀ ≠ 0) : CanonicalForm17Data X where

lDim_canonicalDivisorOf_eq_genus

l(K) = genus for the tail-duality canonical divisor K = div ω₀ of a nonzero holomorphic 1-form (Forster §17.4 at D = 0, via hKgenus_unconditional).

theorem lDim_canonicalDivisorOf_eq_genus (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) :
    lDim (X := X) (canonicalDivisorOf ω₀ hω₀) = genus X

h1TailDim_zero_eq_genus

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

theorem h1TailDim_zero_eq_genus (hg : 0 < genus X) : h1TailDim (X := X) 0 = genus X

exists_riemannRoch_divisor_of_genus_pos

Riemann–Roch, positive genus (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. This is the exact statement shape of Jacobians.exists_riemannRoch_divisor, with the 0 < genus hypothesis.

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