A machine-checked solution to the Jacobians challenge

21.8. LaurentTail.RiemannRochFirstForm🔗

Jacobians.LaurentTail.RiemannRochFirstFormsource

lDim_sub_h1TailDim_sub_deg_eq_of_le

The Euler characteristic l(D) − h¹(D) − deg D is monotone-invariant: equal for D₁ ≤ D₂. Lemma 2.3 computes dim ker (H¹(D₁) ↠ H¹(D₂)), and rank–nullity on the finite-dimensional s (Prop. 2.7) reads the same kernel as h¹(D₁) − h¹(D₂).

theorem lDim_sub_h1TailDim_sub_deg_eq_of_le {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    (lDim (X := X) D₁ : ℤ) - h1TailDim (X := X) D₁ - Divisor.deg X D₁
      = (lDim (X := X) D₂ : ℤ) - h1TailDim (X := X) D₂ - Divisor.deg X D₂

lDim_sub_h1TailDim_sub_deg_const

l(D) − h¹(D) − deg D is constant in D (compare any two divisors through their common upper bound D₁ ⊔ D₂).

theorem lDim_sub_h1TailDim_sub_deg_const (D₁ D₂ : Divisor X) :
    (lDim (X := X) D₁ : ℤ) - h1TailDim (X := X) D₁ - Divisor.deg X D₁
      = (lDim (X := X) D₂ : ℤ) - h1TailDim (X := X) D₂ - Divisor.deg X D₂

riemannRoch_tailForm

Riemann–Roch, first form (Miranda Ch. VI Thm. 3.1, p. 185):

l(D) − h¹(D) = deg D + 1 − h¹(0)

for every divisor D on the compact Riemann surface X, with the Laurent-tail Mittag-Leffler obstruction dimension.

theorem riemannRoch_tailForm (D : Divisor X) :
    (lDim (X := X) D : ℤ) - h1TailDim (X := X) D
      = Divisor.deg X D + 1 - h1TailDim (X := X) 0