21.7. LaurentTail.LinearSystemFiniteDimensional🔗

Jacobians.LaurentTail.LinearSystemFiniteDimensional — source

lDim_eq_finrank_lSysModule

lDim D is by definition the finrank of the junk-free linear-system module.

theorem lDim_eq_finrank_lSysModule {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (D : Divisor X) :
    lDim (X := X) D = finrank ℂ (lSysModule (X := X) D)

finiteDimensional_lSysModule

L(D)/germZero is finite-dimensional (Forster §16 / Miranda Ch. VI Prop. 2.5, by the Čech route: h⁰(𝔘, 𝒪_D) < ∞ + the H⁰ ≅ L(D)/germZero bridge).

instance finiteDimensional_lSysModule (D : Divisor X) :
    FiniteDimensional ℂ (lSysModule (X := X) D)