26.8. ProperDegree.MultiplicityPatching🔗

Jacobians.ProperDegree.MultiplicityPatching — source

orderAt_root_eq_one

Each root is a simple zero of g − w (the simplicity at a root).

Given the substitution data g z − w₀ = v(z)^m on closedBall x₀ ρ with v analytic, deriv v nonvanishing on ball x₀ ε (ε ≤ ρ), and m ≥ 1: at any z₁ ∈ ball x₀ ε with g z₁ = w and w ≠ w₀, the chart-pullback meromorphic order of g − w is exactly 1.

Proof: v(z₁)^m = g z₁ − w₀ = w − w₀ ≠ 0, so v(z₁) ≠ 0; with deriv v z₁ ≠ 0 and the power rule, deriv g z₁ = m·v(z₁)^{m-1}·deriv v z₁ ≠ 0, hence g − w has a simple zero at z₁.

lemma orderAt_root_eq_one
    (hm : 1 ≤ m) {ε : ℝ} (hε_le : ε ≤ ρ)
    (hv_an : AnalyticOnNhd ℂ v (closedBall x₀ ρ))
    (hg_an : AnalyticOnNhd ℂ g (closedBall x₀ ε))
    (hdv : ∀ z ∈ ball x₀ ε, deriv v z ≠ 0)
    (hpow : ∀ z ∈ closedBall x₀ ρ, g z - w₀ = (v z) ^ m)
    {z₁ w : ℂ} (hz₁ : z₁ ∈ ball x₀ ε) (hgz₁ : g z₁ = w) (hw_ne : w ≠ w₀) :
    (meromorphicOrderAt (fun ζ => g ζ - w) z₁).untop₀ = 1

MultiplicityPatchingData

Multiplicity patching package for the holomorphic proper map F = f.toRiemannSphere at a value w₀ : ℂℙ¹.

Bundles, around the (finite) fibre F⁻¹(w₀) = ↑xs:

• a sheet U x around each x ∈ xs, open and pairwise disjoint;

• a weight m x : ℤ (the local degree localDeg f w₀ x);

• a common neighbourhood W of w₀;

• for each sheet and each w ∈ W, the multiplicity-conservation identity ∑_{y ∈ U x ∩ F⁻¹(w)} localDeg f w y = m x;

• finiteness of every fibre over W;

• the no-escape property F⁻¹(W) ⊆ ⋃ x ∈ xs, U x;

• the value reading N f w₀ = ∑ x ∈ xs, m x.

From these, the fibre-multiplicity N f is constantly ∑ m x on W, hence locally constant at w₀.

structure MultiplicityPatchingData (f : MeromorphicFunction X) (w₀ : RiemannSphere) where

fibre_eq_iUnion_sheets

The fibre over w ∈ W is the disjoint union of the sheet slices U x ∩ F⁻¹(w).

lemma fibre_eq_iUnion_sheets (h : MultiplicityPatchingData f w₀)
    {w : RiemannSphere} (hw : w ∈ h.W) :
    f.toRiemannSphere ⁻¹' {w} = ⋃ x ∈ (h.xs : Set X), (h.U x ∩ f.toRiemannSphere ⁻¹' {w})

fibreMult_eq_sum_weights

Multiplicity sum over a nearby fibre = total weight. For w ∈ W, the global fibre-multiplicity sum fibreMult f w equals ∑ x ∈ xs, m x.

lemma fibreMult_eq_sum_weights (h : MultiplicityPatchingData f w₀)
    {w : RiemannSphere} (hw : w ∈ h.W) :
    fibreMult f w = ∑ x ∈ h.xs, h.m x

N_eq_of_mem_W

N f is constantly N f w₀ on W. For w ∈ W, both N f w and N f w₀ equal the total weight ∑ x ∈ xs, m x (N_eq_fibreMult ∘ fibreMult_eq_sum_weights), hence agree.

lemma N_eq_of_mem_W (h : MultiplicityPatchingData f w₀)
    {w : RiemannSphere} (hw : w ∈ h.W) :
    N f w = N f w₀

isLocallyConstant_N_of_pointwiseMultiplicityPatching

Local constancy of N f from a pointwise multiplicity-patching supply.

If for *every* w₀ : ℂℙ¹ we are given a MultiplicityPatchingData f w₀, then N f is locally constant on ℂℙ¹. The witness h w₀ supplies the open neighbourhood (h w₀).W of w₀ on which N f is constantly N f w₀ (N_eq_of_mem_W).

This is the multiplicity analogue of Jacobians.Discharge.fibreCard_isLocallyConstant_of_pointwiseHurwitz, and the structure ⇒ local-constancy half of the conservation-of-number assembly.

theorem isLocallyConstant_N_of_pointwiseMultiplicityPatching
    (f : MeromorphicFunction X)
    (h : ∀ w₀ : RiemannSphere, MultiplicityPatchingData f w₀) :
    IsLocallyConstant (N f)

properMapDegreeData_of_pointwiseMultiplicityPatching

ProperMapDegreeData f from the multiplicity-patching supply.

def properMapDegreeData_of_pointwiseMultiplicityPatching
    (f : MeromorphicFunction X)
    (h : ∀ w₀ : RiemannSphere, MultiplicityPatchingData f w₀) :
    Jacobians.ProperMapDegree.ProperMapDegreeData f

exists_properMapDegree_of_pointwiseMultiplicityPatching

The proper-map-degree existential (the exact shape of Jacobians.exists_properMapDegree: a common d : ℕ with zerosCount f = d = polesCount f) from the multiplicity-patching supply.

theorem exists_properMapDegree_of_pointwiseMultiplicityPatching
    (f : MeromorphicFunction X)
    (h : ∀ w₀ : RiemannSphere, MultiplicityPatchingData f w₀) :
    ∃ d : ℕ, zerosCount f = (d : ℤ) ∧ polesCount f = (d : ℤ)