26.13. ProperDegree.ToSphereGeneral🔗

Jacobians.ProperDegree.ToSphereGeneral — source

MeromorphicFunction.toRiemannSphere

The holomorphic map X → ℂℙ¹ associated with a meromorphic function f: send a genuine pole (orderAtPoint x < 0) to ∞, and every other point to the limit-repair value coe (holoRepr x) (the junk-free meromorphic value, see Jacobians.MeromorphicLiouville).

Generalizes MeromorphicFunction.toSphere, which fixed a single pole P and sent only P to ∞.

def MeromorphicFunction.toRiemannSphere {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) :
    X → RiemannSphere

MeromorphicFunction.toRiemannSphere_of_pole

lemma MeromorphicFunction.toRiemannSphere_of_pole {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) {x : X}
    (hx : f.orderAtPoint x < 0) : f.toRiemannSphere x = OnePoint.infty

MeromorphicFunction.toRiemannSphere_of_nonneg

lemma MeromorphicFunction.toRiemannSphere_of_nonneg {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) {x : X}
    (hx : 0 ≤ f.orderAtPoint x) :
    f.toRiemannSphere x = ((f.holoRepr x : ℂ) : RiemannSphere)

MeromorphicFunction.toRiemannSphere_preimage_infty

Preimage of ∞ is exactly the set of poles {x | orderAtPoint x < 0} (the finite value coe _ never equals ∞, and we send a point to ∞ iff it is a pole).

lemma MeromorphicFunction.toRiemannSphere_preimage_infty {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) :
    f.toRiemannSphere ⁻¹' {OnePoint.infty} = {x | f.orderAtPoint x < 0}

MeromorphicFunction.toRiemannSphere_chartPullback_eventuallyEq_coe

Punctured chart pullback of toRiemannSphere is coe ∘ holoRepr. For ANY point P (in particular a pole), every point in a punctured neighborhood of P is a non-pole (poles are isolated, orderAtPoint_isolated_at), so reading through the chart φ = chartAt P, the pullback toRiemannSphere ∘ φ.symm agrees with coe ∘ holoRepr ∘ φ.symm off the center φ P. This is the punctured-neighborhood input the pole analysis consumes (the analogue, for toRiemannSphere, of holoRepr_chartPullback_eventuallyEq_NFAt).

lemma MeromorphicFunction.toRiemannSphere_chartPullback_eventuallyEq_coe {X : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (P : X) :
    (fun w => f.toRiemannSphere ((chartAt (H := ℂ) P).symm w))
      =ᶠ[𝓝[≠] ((chartAt (H := ℂ) P) P)]
      (fun w => ((f.holoRepr ((chartAt (H := ℂ) P).symm w) : ℂ) : RiemannSphere))

MeromorphicFunction.toRiemannSphere_eventuallyEq_coe_holoRepr

Near a non-pole, toRiemannSphere agrees with coe ∘ holoRepr. Since poles are isolated (orderAtPoint_isolated_at), there is a neighborhood of a non-pole x on which every point is also a non-pole (order 0 for y ≠ x, order ≥ 0 at x), so the if in toRiemannSphere always takes the coe-branch.

lemma MeromorphicFunction.toRiemannSphere_eventuallyEq_coe_holoRepr {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) {x : X} (hx : 0 ≤ f.orderAtPoint x) :
    f.toRiemannSphere =ᶠ[𝓝 x] (fun y => ((f.holoRepr y : ℂ) : RiemannSphere))

MeromorphicFunction.contMDiffAt_toRiemannSphere_of_nonneg

Off the poles, toRiemannSphere is ContMDiff … ω. Where the order of f is ≥ 0, near x the map is coe ∘ holoRepr (toRiemannSphere_eventuallyEq_coe_holoRepr), and holoRepr is analytic in the chart there (analyticAt_holoRepr_chartPullback_of_orderNonneg); reading in the affine chart chartCoe at the finite value coe (holoRepr x), the chart pullback is holoRepr ∘ (chartAt x).symm, which is analytic. Mirrors contMDiffAt_toSphere_of_ne.

theorem MeromorphicFunction.contMDiffAt_toRiemannSphere_of_nonneg {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    {x : X} (hx : 0 ≤ f.orderAtPoint x) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω (f.toRiemannSphere) x

MeromorphicFunction.meromorphicOrderAt_chartPullback_of_pole

The chart-level order is the negative integer n recorded by orderAtPoint. At a pole (orderAtPoint P < 0) the order of the pullback F = f.toFun ∘ φ.symm at φ P equals (orderAtPoint P : ℤ), which is < 0 (so in particular F has a genuine pole — not a removable singularity — at φ P).

lemma MeromorphicFunction.meromorphicOrderAt_chartPullback_of_pole {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) {P : X} (hP : f.orderAtPoint P < 0) :
    meromorphicOrderAt (f.toFun ∘ (chartAt (H := ℂ) P).symm) ((chartAt (H := ℂ) P) P)
      = (f.orderAtPoint P : ℤ)

MeromorphicFunction.contMDiffAt_toRiemannSphere_at_pole

At a pole P, toRiemannSphere is ContMDiffAt … ω. Reading in the ∞-chart chartInfty at toRiemannSphere P = ∞, the chart pullback G = chartInfty ∘ toRiemannSphere ∘ φ.symm (φ = chartAt P) equals, near φ P, the inverse of the normal-form representative Nw⁻¹ of the pullback F = f.toFun ∘ φ.symm. Since F has meromorphicOrderAt = n < 0 (the pole), its normal form N has order n, so N⁻¹ is in normal form of order -n ≥ 1 > 0, hence analytic at φ P with value 0. Mirrors contMDiffAt_toSphere_at_pole, dropping the orderAtPoint P = -1 restriction (any n < 0 works).

theorem MeromorphicFunction.contMDiffAt_toRiemannSphere_at_pole {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    {P : X} (hP : f.orderAtPoint P < 0) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω (f.toRiemannSphere) P

MeromorphicFunction.contMDiff_toRiemannSphere

Holomorphy of toRiemannSphere. Off the poles, toRiemannSphere = coe ∘ holoRepr is analytic where the order is ≥ 0 (contMDiffAt_toRiemannSphere_of_nonneg). At a pole, reading in chartInfty, toRiemannSphere is z ↦ 1/f, analytic with value 0 (contMDiffAt_toRiemannSphere_at_pole). Together: ContMDiff … ω everywhere — the general "meromorphic function = holomorphic map to ℂℙ¹".

theorem MeromorphicFunction.contMDiff_toRiemannSphere {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (f.toRiemannSphere)

MeromorphicFunction.continuous_toRiemannSphere

toRiemannSphere is continuous (it is holomorphic).

theorem MeromorphicFunction.continuous_toRiemannSphere {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    Continuous (f.toRiemannSphere)

MeromorphicFunction.isProperMap_toRiemannSphere

toRiemannSphere is a proper map. X is compact and RiemannSphere is Hausdorff, so the continuous map toRiemannSphere is automatically proper (preimages of compacts are closed subsets of the compact X, hence compact).

theorem MeromorphicFunction.isProperMap_toRiemannSphere {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    IsProperMap (f.toRiemannSphere)

MeromorphicFunction.meromorphicOrderAt_chartPullback_of_zero

The chart-level order at a zero is the positive integer orderAtPoint x. At a genuine zero (0 < orderAtPoint x), the order of the pullback F = f.toFun ∘ φ.symm at φ x equals (orderAtPoint x : ℤ) > 0 (it is not ⊤, since untop₀ ⊤ = 0).

lemma MeromorphicFunction.meromorphicOrderAt_chartPullback_of_zero {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) {x : X} (hx : 0 < f.orderAtPoint x) :
    meromorphicOrderAt (f.toFun ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)
      = (f.orderAtPoint x : ℤ)

MeromorphicFunction.holoRepr_eq_zero_of_orderPos

At a genuine zero (0 < orderAtPoint x), the limit-repair value is 0. The pullback F tends to 0 along the punctured chart neighborhood (tendsto_zero_of_meromorphicOrderAt_pos, since the chart order is positive); transferring through φ.symm gives f.toFun → 0 along 𝓝[≠] x, so holoRepr x = limUnder (𝓝[≠] x) f.toFun = 0.

lemma MeromorphicFunction.holoRepr_eq_zero_of_orderPos {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) {x : X} (hx : 0 < f.orderAtPoint x) :
    f.holoRepr x = 0

MeromorphicFunction.zeros_subset_toRiemannSphere_preimage_zero

The zeros of f lie in the 0-fibre. A genuine zero (0 < orderAtPoint x) is a non-pole, where toRiemannSphere x = coe (holoRepr x) = coe 0 = 0. (Inclusion, not equality: the affine value coe 0 could also be attained where the order is 0 but the value happens to vanish, e.g. for a junk-free removable point.)

lemma MeromorphicFunction.zeros_subset_toRiemannSphere_preimage_zero {X : Type*}
    [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) :
    {x | 0 < f.orderAtPoint x} ⊆ f.toRiemannSphere ⁻¹' {((0 : ℂ) : RiemannSphere)}

MeromorphicFunction.finite_poles

The set of poles {x | orderAtPoint x < 0} is finite: it is contained in the support {x | orderAtPoint x ≠ 0} of the locally-finite order function, which is finite on the compact X (orderLocallyFinsupp.finiteSupport).

lemma MeromorphicFunction.finite_poles {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) :
    {x | f.orderAtPoint x < 0}.Finite

MeromorphicFunction.toRiemannSphere_not_isConstant_of_exists_pole

toRiemannSphere is non-constant when f has a pole. At a pole P, toRiemannSphere P = ∞. Poles are finite (finite_poles) while X is infinite (a nonempty open subset of a complex 1-manifold, infinite_of_isOpen_nonempty), so there is a non-pole x₀, where toRiemannSphere x₀ = coe (holoRepr x₀) ≠ ∞. Uses the genuine IsConstantMap predicate.

theorem MeromorphicFunction.toRiemannSphere_not_isConstant_of_exists_pole {X : Type*}
    [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (hpole : ∃ P, f.orderAtPoint P < 0) :
    ¬ IsConstantMap (f.toRiemannSphere)

MeromorphicFunction.toRiemannSphere_not_isConstant

toRiemannSphere is non-constant for a non-constant meromorphic f. A meromorphic function with some nonzero order (∃ x, orderAtPoint x ≠ 0 — i.e. genuinely non-constant) has a pole on the compact connected X (exists_pole_of_nonconstant, the compact-Liouville corollary), so toRiemannSphere is non-constant (toRiemannSphere_not_isConstant_of_exists_pole).

theorem MeromorphicFunction.toRiemannSphere_not_isConstant {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    (hf : ∃ x, f.orderAtPoint x ≠ 0) :
    ¬ IsConstantMap (f.toRiemannSphere)