26.4. ProperDegree.DegDivResidue🔗

Jacobians.ProperDegree.DegDivResidue — source

div_apply

The value of f.div at x is orderAtPoint f x.

@[simp] lemma div_apply (f : MeromorphicFunction X) (x : X) :
    (f.div : Divisor X) x = f.orderAtPoint x

deg_div_eq_support_sum

The degree of f.div is the support sum of the order function.

lemma deg_div_eq_support_sum (f : MeromorphicFunction X) :
    Divisor.deg X f.div = ∑ x ∈ (f.div : Divisor X).support, f.orderAtPoint x

deg_div_eq_zeros_add_poles

The support sum splits as the zero-part plus the pole-part.

lemma deg_div_eq_zeros_add_poles (f : MeromorphicFunction X) :
    Divisor.deg X f.div =
      (∑ x ∈ (f.div : Divisor X).support with 0 < f.orderAtPoint x, f.orderAtPoint x)
      + (∑ x ∈ (f.div : Divisor X).support with f.orderAtPoint x < 0, f.orderAtPoint x)

zerosCount

The number of zeros of f, counted with multiplicity: the sum of the positive orders over the divisor support.

def zerosCount (f : MeromorphicFunction X) : ℤ

polesCount

The number of poles of f, counted with multiplicity: the sum of the absolute values of the negative orders over the divisor support.

def polesCount (f : MeromorphicFunction X) : ℤ

poles_part_eq_neg_polesCount

The pole-part of the support sum is −polesCount.

lemma poles_part_eq_neg_polesCount (f : MeromorphicFunction X) :
    (∑ x ∈ (f.div : Divisor X).support with f.orderAtPoint x < 0, f.orderAtPoint x)
      = -polesCount f

deg_div_eq_zeros_sub_poles

deg (div f) = zerosCount f − polesCount f: the divisor degree is the number of zeros minus the number of poles, each with multiplicity.

lemma deg_div_eq_zeros_sub_poles (f : MeromorphicFunction X) :
    Divisor.deg X f.div = zerosCount f - polesCount f

zerosCount_nonneg

zerosCount f ≥ 0: it is a sum of positive orders.

lemma zerosCount_nonneg (f : MeromorphicFunction X) : 0 ≤ zerosCount f

exists_properMapDegree_of_zerosCount_eq_polesCount

Reduction to the argument-principle equality. Since both counts are nonnegative (zerosCount_nonneg, polesCount_nonneg), the existence of a common natural-number degree d with zerosCount f = d and polesCount f = d is exactly the equality zerosCount f = polesCount f. The common d is the natural number whose cast is the (nonnegative) shared value.

theorem exists_properMapDegree_of_zerosCount_eq_polesCount (f : MeromorphicFunction X)
    (h : zerosCount f = polesCount f) :
    ∃ d : ℕ, zerosCount f = (d : ℤ) ∧ polesCount f = (d : ℤ)

exists_properMapDegree_of_div_eq_zero

The degree-route conclusion in the trivial case f.div = 0 (constant or germ-zero f): both counts vanish, witnessed by d = 0.

theorem exists_properMapDegree_of_div_eq_zero (f : MeromorphicFunction X)
    (h : (f.div : Divisor X) = 0) :
    ∃ d : ℕ, zerosCount f = (d : ℤ) ∧ polesCount f = (d : ℤ)