26.11. ProperDegree.ProperMapDegreeConstruct🔗

Jacobians.ProperDegree.ProperMapDegreeConstruct — source

localDeg

The local degree of F = f.toRiemannSphere at x, over the value w.

• w = ∞: returns −orderAtPoint f x (the pole order, > 0 at a genuine pole, ≤ 0 otherwise — the local degree of F into ∞).

• w = coe c: returns the chart-pullback meromorphic order of z ↦ f(z) − c at (chartAt ℂ x) x, the order of vanishing of f − c at x (the multiplicity of x as a solution of f = c).

A concrete total function; the genuine analytic content (= local degree of F) is needed only through the local-constancy of its fibre sum, isolated below.

def localDeg {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X)
    (w : RiemannSphere) (x : X) : ℤ

localDeg_zero_eq_order

At a non-pole x with F x = coe 0 (a genuine zero or a value-0 point), the local degree over 0 is orderAtPoint f x: meromorphicOrderAt (f.toFun ∘ chart.symm − 0) = meromorphicOrderAt (f.toFun ∘ chart.symm) = orderAtPoint f x by definition (orderAtPoint = (meromorphicOrderAt (f.toFun ∘ chart.symm) _).untop₀).

lemma localDeg_zero_eq_order {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (x : X) :
    localDeg f ((0 : ℂ) : RiemannSphere) x = f.orderAtPoint x

localDeg_infty

At ∞, the local degree over ∞ is −orderAtPoint f x.

@[simp] lemma localDeg_infty {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (x : X) :
    localDeg f OnePoint.infty x = -f.orderAtPoint x

fibreMult

The fibre-multiplicity sum of F = f.toRiemannSphere over w: ∑_{x ∈ F⁻¹(w)} (local degree of F at x). The genuine "number of preimages of w, counted with multiplicity".

def fibreMult {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X)
    (w : RiemannSphere) : ℤ

N

The fibre-multiplicity function N : ℂℙ¹ → ℤ of f.

Defined to read off the two special fibres exactly — N(∞) = polesCount f, N(coe 0) = zerosCount f — and to be the genuine multiplicity sum fibreMult elsewhere. The special-value plugs *equal* the genuine multiplicity sums there (fibreMult f ∞ = polesCount f, fibreMult f (coe 0) = zerosCount f; the special-fibre identities, Forster §4), so N coincides with the genuine multiplicity sum at every point — it is the fibre-multiplicity function, with the two boundary readings made definitionally available.

def N {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) : RiemannSphere → ℤ

N_infty_eq

Boundary reading at ∞: N f ∞ = polesCount f.

@[simp] lemma N_infty_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    N f OnePoint.infty = polesCount f

N_zero_eq

Boundary reading at 0: N f (coe 0) = zerosCount f.

coe 0 ≠ ∞, so the first branch fails and the second fires.

@[simp] lemma N_zero_eq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    N f ((0 : ℂ) : RiemannSphere) = zerosCount f

ProperMapDegreeData.ofParts

Structural builder. Package a ProperMapDegreeData f from the fibre-multiplicity function N f together with a proof of its local constancy. The two boundary readings are discharged here (N_zero_eq, N_infty_eq); the caller supplies only the local-constancy witness.

def ProperMapDegreeData.ofParts {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (hlc : IsLocallyConstant (N f)) :
    Jacobians.ProperMapDegree.ProperMapDegreeData f where

ProperMapDegreeData.ofConservation

The conservation-of-number data, packaged. Given the honest local constancy of the fibre-multiplicity function N f (the global argument principle), ProperMapDegreeData f exists.

def ProperMapDegreeData.ofConservation {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (hlc : IsLocallyConstant (N f)) :
    Jacobians.ProperMapDegree.ProperMapDegreeData f