21.8. LaurentTail.RiemannRochFirstForm
Jacobians.LaurentTail.RiemannRochFirstForm — source
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 H¹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 h¹ 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