26.9. ProperDegree.MultiplicityPatchingConstruct🔗

Jacobians.ProperDegree.MultiplicityPatchingConstruct — source

shiftMero

The shift f − c as a meromorphic function (built directly, independent of the Sub (MeromorphicFunction X) instance).

noncomputable def shiftMero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (c : ℂ) : MeromorphicFunction X

localDeg_coe_eq_orderAtPoint_sub

localDeg at a finite value as an orderAtPoint of the shift f − c.

localDeg f (coe c) y = orderAtPoint (shiftMero f c) y. Both are (meromorphicOrderAt (z ↦ f(chart_y.symm z) − c) (chart_y y)).untop₀ — the order of vanishing of f − c at y, read in the chart at y. This is *definitional* (shiftMero plugs the constant c into the subtraction).

lemma localDeg_coe_eq_orderAtPoint_sub {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (c : ℂ) (y : X) :
    localDeg f ((c : ℂ) : RiemannSphere) y
      = MeromorphicFunction.orderAtPoint (shiftMero f c) y

localDeg_coe_eq_chartPullback_order

Chart-invariant reading of localDeg at a finite value.

For y in the source of *any* atlas chart e, the local degree of F over coe c at y is the order of z ↦ f(e.symm z) − c at e y. This is the proven chart-invariance orderAtPoint_chart_invariant applied to the shift shiftMero f c; it is what lets the chart-at-x order sum of the planar normal form be matched, preimage by preimage, against the intrinsic localDeg.

lemma localDeg_coe_eq_chartPullback_order {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (c : ℂ) {y : X}
    (e : OpenPartialHomeomorph X ℂ) (he : e ∈ atlas ℂ X) (hy : y ∈ e.source) :
    localDeg f ((c : ℂ) : RiemannSphere) y
      = (meromorphicOrderAt (fun z => f.toFun (e.symm z) - c) (e y)).untop₀

fibreMult_infty_eq_polesCount

Special-fibre identity at ∞: the genuine local-degree sum over the pole fibre F⁻¹(∞) equals polesCount f.

F⁻¹(∞) = {x | order x < 0} (the poles) and localDeg f ∞ x = −order x, so the sum is ∑_{x : order x < 0} (−order x). Reindexing this finite-set sum onto the divisor support (where the extra points all have order = 0, hence are excluded by the order < 0 filter) gives polesCount f verbatim.

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

fibreMult_zero_eq_zerosCount

Special-fibre identity at coe 0: the genuine local-degree sum over the zero fibre F⁻¹(coe 0) equals zerosCount f.

localDeg f (coe 0) x = orderAtPoint f x (localDeg_zero_eq_order), and the order function vanishes off {x | order x ≠ 0}. A point of the fibre F⁻¹(coe 0) is a non-pole (it maps to coe 0 ≠ ∞, so order ≥ 0), so on the support {order ≠ 0} membership in the fibre is equivalent to being a genuine zero {0 < order} (forward: order ≥ 0 and order ≠ 0; backward: zeros_subset_toRiemannSphere_preimage_zero). The finsum therefore collapses onto the zeros, reindexing to zerosCount f.

Note this needs *no* fibre-finiteness hypothesis: the summand's support is finite (⊆ {order ≠ 0}, finite on compact X), which is all finsum needs.

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

N_eq_fibreMult_everywhere

N f is the genuine fibre-multiplicity function everywhere.

N f differs from fibreMult f only at the two special values coe 0, ∞, where it plugs in zerosCount f, polesCount f respectively; the special-fibre identities (fibreMult_zero_eq_zerosCount, fibreMult_infty_eq_polesCount) prove those plugs *equal* the genuine multiplicity sums there. Hence N f w = fibreMult f w for every w.

lemma N_eq_fibreMult_everywhere {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (w : RiemannSphere) :
    N f w = fibreMult f w

MultiplicityPatchingData.ofGeometricData

Streamlined builder for MultiplicityPatchingData. Identical to the raw structure *except* the N_eq_fibreMult field is supplied automatically by the proven global identity N f = fibreMult f. The caller provides only the geometric conservation-of-number data (sheets, weights, per-sheet conservation, finite fibres, no-escape).

def MultiplicityPatchingData.ofGeometricData {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (w₀ : RiemannSphere)
    (xs : Finset X)
    (xs_coe : (xs : Set X) = f.toRiemannSphere ⁻¹' {w₀})
    (U : X → Set X)
    (U_open : ∀ x ∈ xs, IsOpen (U x))
    (mem_U_self : ∀ x ∈ xs, x ∈ U x)
    (U_pairwiseDisjoint : ∀ x ∈ xs, ∀ x' ∈ xs, x ≠ x' → Disjoint (U x) (U x'))
    (m : X → ℤ)
    (W : Set RiemannSphere)
    (W_open : IsOpen W)
    (w₀_mem_W : w₀ ∈ W)
    (sheetMult_eq : ∀ x ∈ xs, ∀ w ∈ W,
      (∑ᶠ y ∈ U x ∩ f.toRiemannSphere ⁻¹' {w}, localDeg f w y) = m x)
    (fibre_finite : ∀ w ∈ W, (f.toRiemannSphere ⁻¹' {w}).Finite)
    (preimage_W_subset : f.toRiemannSphere ⁻¹' W ⊆ ⋃ x ∈ xs, U x) :
    MultiplicityPatchingData f w₀ where

MultiplicityPatchingData.ofDisjointSheets

No-escape skeleton for MultiplicityPatchingData.

From pairwise-disjoint open sheets U x (one per fibre point x ∈ xs, where ↑xs = F⁻¹{w₀}), each carrying an open value-neighbourhood Wsheet x ∋ w₀ on which the per-sheet multiplicity conservation holds, together with an open value-neighbourhood Wfin ∋ w₀ over which every fibre is finite, this builds a MultiplicityPatchingData f w₀.

The no-escape (preimage_W_subset) and the shrinking of the value-neighbourhood to a common W := (f '' K)ᶜ ∩ ⋂ Wsheet x ∩ Wfin are discharged via the proper-map compactness argument; the N_eq_fibreMult field is the global identity N = fibreMult. Conservation persists from Wsheet x to the smaller W by monotonicity (the sheets U x are *not* shrunk, so no preimage is lost); fibre finiteness persists from Wfin. Supplying Wfin *separately* (rather than deriving it as ⋂ Wsheet x) keeps the empty-fibre case sound (xs = ∅ makes ⋂ Wsheet x = univ, but Wfin can be a genuine finiteness neighbourhood).

def MultiplicityPatchingData.ofDisjointSheets {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (w₀ : RiemannSphere)
    (xs : Finset X)
    (xs_coe : (xs : Set X) = f.toRiemannSphere ⁻¹' {w₀})
    (U : X → Set X)
    (U_open : ∀ x ∈ xs, IsOpen (U x))
    (mem_U_self : ∀ x ∈ xs, x ∈ U x)
    (U_pairwiseDisjoint : ∀ x ∈ xs, ∀ x' ∈ xs, x ≠ x' → Disjoint (U x) (U x'))
    (m : X → ℤ)
    (Wsheet : X → Set RiemannSphere)
    (Wsheet_open : ∀ x ∈ xs, IsOpen (Wsheet x))
    (w₀_mem_Wsheet : ∀ x ∈ xs, w₀ ∈ Wsheet x)
    (sheetMult_eq : ∀ x ∈ xs, ∀ w ∈ Wsheet x,
      (∑ᶠ y ∈ U x ∩ f.toRiemannSphere ⁻¹' {w}, localDeg f w y) = m x)
    (Wfin : Set RiemannSphere) (Wfin_open : IsOpen Wfin) (w₀_mem_Wfin : w₀ ∈ Wfin)
    (fibre_finite_Wfin : ∀ w ∈ Wfin, (f.toRiemannSphere ⁻¹' {w}).Finite) :
    MultiplicityPatchingData f w₀

LocalMultiplicitySheets

The irreducible local conservation data at a value w₀ : ℂℙ¹: the geometric inputs to MultiplicityPatchingData.ofDisjointSheets. Bundles the finite fibre enumeration, the pairwise-disjoint sheets, the per-sheet weights and value-neighbourhoods, the per-sheet multiplicity conservation, and fibre finiteness over the common value-neighbourhood.

structure LocalMultiplicitySheets {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (w₀ : RiemannSphere) where

LocalMultiplicitySheets.toPatchingData

From the local data to the patching datum.

def LocalMultiplicitySheets.toPatchingData {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {f : MeromorphicFunction X}
    {w₀ : RiemannSphere} (s : LocalMultiplicitySheets f w₀) :
    MultiplicityPatchingData f w₀

LocalMultiplicitySheets.ofNotMemRange

Empty-fibre witness. At w₀ ∉ range F, the empty local-sheet datum satisfies LocalMultiplicitySheets f w₀: the fibre over w₀ is empty, and on the open neighbourhood Wfin := (range F)ᶜ every fibre is empty (hence finite). Since F is proper its range is closed, so (range F)ᶜ is open and contains w₀. Hence the structure's obligations are satisfiable, not a disguised False.

def LocalMultiplicitySheets.ofNotMemRange {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    {w₀ : RiemannSphere} (h_notmem : w₀ ∉ Set.range f.toRiemannSphere) :
    LocalMultiplicitySheets f w₀ where

exists_properMapDegree_of_localSheets

The proper-map-degree existential (a common d : ℕ with zerosCount f = d = polesCount f) from a pointwise local-conservation supply.

theorem exists_properMapDegree_of_localSheets {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (h : ∀ w₀ : RiemannSphere, LocalMultiplicitySheets f w₀) :
    ∃ d : ℕ, zerosCount f = (d : ℤ) ∧ polesCount f = (d : ℤ)