26.10. ProperDegree.ProperMapDegree🔗

Jacobians.ProperDegree.ProperMapDegree — source

zerosCount_eq_polesCount_of_isLocallyConstant

Globalization of the argument principle (the connectedness step).

If N : ℂℙ¹ → ℤ is locally constant with N(0) = zerosCount f and N(∞) = polesCount f, then zerosCount f = polesCount f.

theorem zerosCount_eq_polesCount_of_isLocallyConstant {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (N : RiemannSphere → ℤ) (hN : IsLocallyConstant N)
    (hzero : N ((0 : ℂ) : RiemannSphere) = zerosCount f)
    (hinfty : N OnePoint.infty = polesCount f) :
    zerosCount f = polesCount f

ProperMapDegreeData

Conservation-of-number data for f through F = toRiemannSphere.

Bundles the output of the global argument-principle assembly:

• N : ℂℙ¹ → ℤ — the fibre multiplicity N(w) = ∑_{x ∈ F⁻¹ w} (local degree);

• locallyConstant — the argument principle: N is locally constant (its value is the integer-valued contour integral (1/2πi) ∮ F'/(F − w), continuous in w);

• zero_eq — the zero-fibre reading N(0) = zerosCount f (the finite-value local degree at a zero is the order, summed over the zeros);

• infty_eq — the pole-fibre reading N(∞) = polesCount f (the local degree at a pole is −ord, summed over the poles).

structure ProperMapDegreeData {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) where

zerosCount_eq_polesCount_of_properMapDegreeData

zerosCount = polesCount via the conservation-of-number data. Given a ProperMapDegreeData f (the output of the argument-principle assembly), the number of zeros equals the number of poles.

theorem zerosCount_eq_polesCount_of_properMapDegreeData {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (D : ProperMapDegreeData f) :
    zerosCount f = polesCount f

exists_properMapDegree_of_properMapDegreeData

The proper-map-degree existential (∃ d, zerosCount = d ∧ polesCount = d), derived from a ProperMapDegreeData via the nonnegativity reduction exists_properMapDegree_of_zerosCount_eq_polesCount. This is the exact shape the parent's exists_properMapDegree needs.

theorem exists_properMapDegree_of_properMapDegreeData {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (D : ProperMapDegreeData f) :
    ∃ d : ℕ, zerosCount f = (d : ℤ) ∧ polesCount f = (d : ℤ)