26.7. ProperDegree.LinearSystemDegree🔗

Jacobians.ProperDegree.LinearSystemDegree — source

MeromorphicFunction.deg_div

Every principal divisor has degree 0 (Forster Cor. 4.25 / the argument principle), via the degree route: deg (div f) = zerosCount f − polesCount f, and both counts equal a common proper-map degree d (conservation of number), so the difference is 0.

theorem MeromorphicFunction.deg_div (f : MeromorphicFunction X) :
    Divisor.deg X f.div = 0

lDim_eq_zero_of_deg_neg

l(D) = 0 when deg D < 0. Any f ∈ L(D) with nonzero germ would give (by faithfulness) a divisor div f ≥ −D with deg(div f) = 0 ≥ −deg D > 0, impossible; so every f ∈ L(D) is germ- zero, the quotient L(D)/germZero is trivial, and its dimension is 0.

theorem lDim_eq_zero_of_deg_neg (D : Divisor X) (hD : Divisor.deg X D < 0) :
    lDim (X := X) D = 0