26.12. ProperDegree.ProperMapDegreeSheets🔗

Jacobians.ProperDegree.ProperMapDegreeSheets — source

meromorphicAt_toFun_chartPullback

The chart pullback f.toFun ∘ (chartAt x).symm is meromorphic at any target point z. At y₀ := (chartAt x).symm z the function is meromorphic at the centre of its own chart (f.meromorphic y₀); the chart transition (chartAt y₀) ∘ (chartAt x).symm is analytic at z (maximal-atlas coordinate change, ω), and MeromorphicAt.comp_analyticAt transports the order across the (locally invertible) transition.

theorem meromorphicAt_toFun_chartPullback {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) (x : X)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) x).target) :
    MeromorphicAt (f.toFun ∘ (chartAt (H := ℂ) x).symm) z

analyticAt_holoRepr_chartPullback_target

The chart pullback holoRepr ∘ (chartAt x).symm is analytic at a target point of a non-pole. The analytic analogue of meromorphicAt_toFun_chartPullback: at y₀ := (chartAt x).symm z, where f has nonnegative order, holoRepr ∘ (chartAt y₀).symm is analytic at its own chart centre (analyticAt_holoRepr_chartPullback_of_orderNonneg); the chart transition (chartAt y₀) ∘ (chartAt x).symm is analytic at z (maximal-atlas coordinate change, ω), so AnalyticAt.comp transports the analyticity across. This supplies the AnalyticAt ℂ G z hypothesis the reciprocal keystone meromorphicOrderAt_inv_sub_eq consumes at each fibre point.

theorem analyticAt_holoRepr_chartPullback_target {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (x : X)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) x).target)
    (hnp : 0 ≤ f.orderAtPoint ((chartAt (H := ℂ) x).symm z)) :
    AnalyticAt ℂ (fun w => f.holoRepr ((chartAt (H := ℂ) x).symm w)) z

holoRepr_pullback_eventuallyEq_toFun

Off-center, holoRepr ∘ (chartAt x).symm agrees with f.toFun ∘ (chartAt x).symm. At any target point z, the raw pullback is analytic on the *punctured* neighbourhood (it is meromorphic there, meromorphicAt_toFun_chartPullback), so f.toFun carries no junk and its punctured limit holoRepr equals the analytic value. This generalises holoRepr_chartPullback_eventuallyEq_NFAt from the chart centre to any target point.

theorem holoRepr_pullback_eventuallyEq_toFun {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) (x : X)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) x).target) :
    f.holoRepr ∘ (chartAt (H := ℂ) x).symm =ᶠ[𝓝[≠] z]
      f.toFun ∘ (chartAt (H := ℂ) x).symm

meromorphicOrderAt_holoRepr_sub_eq

The chart-pullback order of localDeg can be read with holoRepr instead of f.toFun. Since holoRepr ∘ chart.symm and f.toFun ∘ chart.symm agree on 𝓝[≠] z (holoRepr_pullback_eventuallyEq_toFun) and meromorphicOrderAt is 𝓝[≠]-determined.

theorem meromorphicOrderAt_holoRepr_sub_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) (x : X) (c : ℂ)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) x).target) :
    meromorphicOrderAt (fun w => f.holoRepr ((chartAt (H := ℂ) x).symm w) - c) z =
      meromorphicOrderAt (fun w => f.toFun ((chartAt (H := ℂ) x).symm w) - c) z

toRiemannSphere_not_isConstant_of_div_ne_zero

Non-constancy bridge. A meromorphic f with nontrivial divisor (f.div ≠ 0) has toRiemannSphere non-constant: f.div ≠ 0 means some point has nonzero order, and a function with a nonzero order somewhere is non-constant on the sphere (toRiemannSphere_not_isConstant, the compact-Liouville corollary).

theorem toRiemannSphere_not_isConstant_of_div_ne_zero {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (hnc : (f.div : Divisor X) ≠ 0) :
    ¬ Jacobians.Discharge.IsConstantMap f.toRiemannSphere

fibre_finite_of_div_ne_zero

All fibres of F = toRiemannSphere are finite for a non-constant f (f.div ≠ 0). Direct from the unconditional finite-fibres theorem (fibres_finite) applied to the ContMDiff sphere map (contMDiff_toRiemannSphere), using the non-constancy bridge.

theorem fibre_finite_of_div_ne_zero {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (hnc : (f.div : Divisor X) ≠ 0) (w : RiemannSphere) :
    (f.toRiemannSphere ⁻¹' {w}).Finite

orderSum_eq_of_analyticOrder_radiusBounded

Radius-bounded planar conservation of number. Identical to Planar.orderSum_eq_of_analyticOrder but with the counting radius ε bounded by a prescribed R_ext > 0 — the freedom we need to fit each sheet inside a pre-chosen disjoint neighbourhood.

theorem orderSum_eq_of_analyticOrder_radiusBounded
    {g : ℂ → ℂ} {x₀ w₀ : ℂ} {m : ℕ} {R_ext : ℝ} (hR_ext : 0 < R_ext)
    (hm : 1 ≤ m)
    (hg : AnalyticAt ℂ g x₀) (h_w₀ : g x₀ = w₀)
    (hord : analyticOrderAt (fun z => g z - w₀) x₀ = (m : ℕ∞)) :
    ∃ ε > (0 : ℝ), ε ≤ R_ext ∧ ∃ δ > (0 : ℝ),
      ∀ w ∈ ball w₀ δ, w ≠ w₀ →
        (∑ᶠ z ∈ {z ∈ ball x₀ ε | g z = w}, (meromorphicOrderAt (fun ζ => g ζ - w) z).untop₀)
          = (m : ℤ)

SheetDatum

Per-sheet local-conservation output at a fibre point, parametrised by the ambient value w₀ and a containing open set V (a disjoint-separating neighbourhood). Bundles the open sheet U ⊆ V containing x, an open value-neighbourhood W ∋ w₀, the integer weight m, and the per-sheet multiplicity conservation ∑_{y ∈ U ∩ F⁻¹(w)} localDeg = m for w ∈ W.

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

exists_sheetDatum_coe

The per-point construction at a finite value coe c. At a fibre point x of F⁻¹(coe c) (so holoRepr x = c, x a non-pole), with a clean separating neighbourhood V (open, containing x, inside the chart source and the non-pole locus), the radius-bounded planar normal form applied to g = holoRepr ∘ chart.symm produces a sheet U ⊆ V and a value-disc W = coe '' ball c δ on which the per-sheet multiplicity sum is the local order m = localDeg f (coe c) x. The generic rows (w = coe c', c' ≠ c) come from the engine; the central row (w = coe c) holds because the c-fibre in U is the single isolated point x.

theorem exists_sheetDatum_coe {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (hnc : (f.div : Divisor X) ≠ 0)
    (c : ℂ) {x : X} (hx_fib : f.toRiemannSphere x = ((c : ℂ) : RiemannSphere))
    {V : Set X} (hV_open : IsOpen V) (hxV : x ∈ V)
    (hV_np : V ⊆ {y | 0 ≤ f.orderAtPoint y}) :
    Nonempty (SheetDatum f ((c : ℂ) : RiemannSphere) x V)

meromorphicOrderAt_inv_sub_eq

The reciprocal order-matching identity (the keystone for the ∞ case). At a point z where G is analytic with finite nonzero value G z = c', the order of 1/G − 1/c' equals the order of G − c': writing 1/G − 1/c' = −(c'·G)⁻¹ · (G − c') with −(c'·G)⁻¹ analytic and nonzero at z (meromorphicOrderAt_mul_of_ne_zero). This is what lets the planar engine applied to the reciprocal 1/G (a zero of order = the pole order at the pole) re-deliver the finite-value local degrees localDeg f (coe c') in the pole fibre's ∞-neighbourhood.

theorem meromorphicOrderAt_inv_sub_eq (G : ℂ → ℂ) {z c' : ℂ} (hc' : c' ≠ 0) (hGz : G z = c')
    (hGanal : AnalyticAt ℂ G z) :
    meromorphicOrderAt (fun ζ => (G ζ)⁻¹ - c'⁻¹) z = meromorphicOrderAt (fun ζ => G ζ - c') z

meromorphicOrderAt_chartPullback_eq_orderAtPoint

The chart-pullback order of f.toFun at the chart centre equals orderAtPoint (as a WithTop ℤ, *finite*). At a pole (orderAtPoint x < 0) the order is not ⊤ (else orderAtPoint would be the junk 0), so meromorphicOrderAt (f.toFun ∘ e.symm) (e x) = (orderAtPoint x : ℤ). This pins the negative order −m of the pullback G, whose reciprocal 1/G then has the positive order m that drives the reciprocal normal form.

theorem meromorphicOrderAt_chartPullback_eq_orderAtPoint {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) {x : X}
    (hx_pole : f.orderAtPoint x < 0) :
    meromorphicOrderAt (fun z => f.toFun ((chartAt (H := ℂ) x).symm z)) ((chartAt (H := ℂ) x) x)
      = (f.orderAtPoint x : WithTop ℤ)

exists_reciprocal_NF

The repaired reciprocal at a pole. At a pole x (orderAtPoint x < 0), with g = f.holoRepr ∘ (chartAt x).symm the *junk-free* chart pullback (meromorphic, order −m; equal to f.toFun ∘ (chartAt x).symm off the centre, so it cuts the geometric value fibre F⁻¹(coe ·)), the normal-form representative h := toMeromorphicNFAt g⁻¹ (e x) of the reciprocal 1/g is analytic at e x, agrees with (g ·)⁻¹ on the punctured neighbourhood 𝓝[≠] (e x), vanishes at e x (h (e x) = 0), and has analytic order exactly m = (orderAtPoint x).natAbs ≥ 1 (meromorphicOrderAt g⁻¹ = −meromorphicOrderAt g = m, transported through the normal form, with AnalyticAt.meromorphicOrderAt_eq converting the meromorphic order to the analytic order). This is the analytic input the planar engine consumes at w₀ = 0.

theorem exists_reciprocal_NF {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) {x : X} (hx_pole : f.orderAtPoint x < 0) :
    ∃ (h : ℂ → ℂ) (m : ℕ), 1 ≤ m ∧ (m : ℤ) = -f.orderAtPoint x ∧
      AnalyticAt ℂ h ((chartAt (H := ℂ) x) x) ∧
      ((fun z => (f.holoRepr ((chartAt (H := ℂ) x).symm z))⁻¹)
        =ᶠ[𝓝[≠] ((chartAt (H := ℂ) x) x)] h) ∧
      h ((chartAt (H := ℂ) x) x) = 0 ∧
      analyticOrderAt h ((chartAt (H := ℂ) x) x) = (m : ℕ∞)

exists_sheetDatum_infty

The per-point construction at ∞ (the pole fibre). At a pole x (orderAtPoint x < 0, so F x = ∞), with a clean separating neighbourhood V, the same conservation-of-number content holds via the reciprocal normal form 1/g (a zero of order = the pole order at e x): a sheet U ⊆ V and an ∞-neighbourhood W on which the per-sheet multiplicity sum is the pole order m = localDeg f ∞ x = −orderAtPoint x.

theorem exists_sheetDatum_infty {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (_hnc : (f.div : Divisor X) ≠ 0)
    {x : X} (hx_pole : f.orderAtPoint x < 0)
    {V : Set X} (hV_open : IsOpen V) (hxV : x ∈ V)
    (_hV_src : V ⊆ (chartAt (H := ℂ) x).source) :
    Nonempty (SheetDatum f OnePoint.infty x V)

ofSheetData

Assembling LocalMultiplicitySheets from the per-sheet data. Given the finite fibre xs, pairwise-disjoint separating neighbourhoods V0 ⊇ V, and a per-point SheetDatum at each fibre point (in its sheet V x), this packages the full local conservation structure. The total per-point fields are read off as ⋃ (h : x ∈ xs), (D x h).U (= the datum on the fibre, ∅ off it), and disjointness descends from U ⊆ V ⊆ V0 with V0 pairwise disjoint.

def ofSheetData {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X)
    (w₀ : RiemannSphere) (xs : Finset X)
    (hxs_coe : (xs : Set X) = f.toRiemannSphere ⁻¹' {w₀})
    (V0 : X → Set X) (hV0disj : (f.toRiemannSphere ⁻¹' {w₀}).PairwiseDisjoint V0)
    (V : X → Set X) (hV_sub : ∀ x, V x ⊆ V0 x)
    (hfin : ∀ w : RiemannSphere, (f.toRiemannSphere ⁻¹' {w}).Finite)
    (hdatum : ∀ x ∈ xs, Nonempty (SheetDatum f w₀ x (V x))) :
    LocalMultiplicitySheets f w₀

localMultiplicitySheets_of_mem_range

The local conservation data at a value in the range (w₀ ∈ range F), for a *non-constant* f (f.div ≠ 0, ensuring finite fibres): the genuine §17.9 content, built per fibre point from the planar normal form. The finite fibre is enumerated by xs; pairwise-disjoint clean sheets are chosen by T2 separation (Set.Finite.t2_separation) intersected with the chart source and the non-pole locus, then the per-point datum (exists_sheetDatum_coe at a finite value, exists_sheetDatum_infty at ∞) supplies each sheet's conservation.

def localMultiplicitySheets_of_mem_range {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (hnc : (f.div : Divisor X) ≠ 0)
    {w₀ : RiemannSphere} (hmem : w₀ ∈ Set.range f.toRiemannSphere) :
    LocalMultiplicitySheets f w₀

localMultiplicitySheets_of_nonconstant

Pointwise local-conservation supply for non-constant f. For every value w₀ : ℂℙ¹ there is a LocalMultiplicitySheets f w₀: the empty-fibre witness off the range, and the §17.9 construction on it. (Needs f.div ≠ 0: for a constant f the fibre over the constant value is all of X, which is infinite, so no finite xs enumerates it — that case is handled separately by exists_properMapDegree_of_div_eq_zero.)

def localMultiplicitySheets_of_nonconstant {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X)
    (hnc : (f.div : Divisor X) ≠ 0) (w₀ : RiemannSphere) :
    LocalMultiplicitySheets f w₀

exists_properMapDegree_proven

The proper-map-degree existential — ∃ d : ℕ with zerosCount f = d = polesCount f. For the trivial divisor (f.div = 0, the constant/germ-zero case) both counts vanish; otherwise it follows from the pointwise local-conservation supply via the connectedness globalization.

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