21.5. LaurentTail.Finiteness🔗

Jacobians.LaurentTail.Finiteness — source

exists_deg_sub_lDim_bound

The M-bound: deg A − l(A) is bounded above, uniformly in the divisor A. This is the Riemann–Roch inequality (deg A + 1 − h¹(0) ≤ l(A) over a locally-realizable cover), substituting for Miranda's algebraicity Lemmas 1.18/2.4–2.5.

theorem exists_deg_sub_lDim_bound :
    ∃ M : ℤ, ∀ A : Divisor X, Divisor.deg X A - (lDim (X := X) A : ℤ) ≤ M

exists_maximizer

A divisor A₀ maximizing deg − l exists (a nonempty, bounded-above set of integers attains its supremum).

theorem exists_maximizer :
    ∃ A₀ : Divisor X, ∀ A : Divisor X,
      Divisor.deg X A - (lDim (X := X) A : ℤ)
        ≤ Divisor.deg X A₀ - (lDim (X := X) A₀ : ℤ)

mittagLefflerH1_subsingleton_of_maximizer

Miranda Lemma 2.6 (Ch. VI §2, p. 183): at a maximizer A₀ of deg − l, every Laurent tail divisor is realized by a global meromorphic function — H¹(A₀) = 0. Proof: a given tail Z truncates to 0 in 𝒯[B] for the deep cutoff B = tailCutoff A₀ Z ≥ A₀, so its class lies in ker (H¹(A₀) → H¹(B)), whose dimension (deg B − l(B)) − (deg A₀ − l(A₀)) is ≤ 0 by maximality.

theorem mittagLefflerH1_subsingleton_of_maximizer {A₀ : Divisor X}
    (hmax : ∀ A : Divisor X, Divisor.deg X A - (lDim (X := X) A : ℤ)
      ≤ Divisor.deg X A₀ - (lDim (X := X) A₀ : ℤ)) :
    Subsingleton (mittagLefflerH1 (X := X) A₀)

instFiniteDimensionalMittagLefflerH1

Miranda Prop. 2.7 (Ch. VI §2, p. 184): H¹(D) is finite-dimensional for every divisor. With E := A₀ ⊓ D: H¹(E) *is* its relative kernel against H¹(A₀) = 0 (finite by Lemma 2.3), and the truncation H¹(E) ↠ H¹(D) is surjective.

instance instFiniteDimensionalMittagLefflerH1 (D : Divisor X) :
    FiniteDimensional ℂ (mittagLefflerH1 (X := X) D)