11.7. Meromorphic.MeromorphicLiouville🔗

Jacobians.Meromorphic.MeromorphicLiouville — source

MeromorphicFunction.HasSingleSimplePole

f has a single simple pole at P: order -1 at P and order ≥ 0 elsewhere. (Defined here, rather than in DegreeOneSphere, so that both the sphere theorems and the Riemann–Roch reduction can refer to it without a cyclic import.)

def MeromorphicFunction.HasSingleSimplePole
    (f : MeromorphicFunction X) (P : X) : Prop

MeromorphicFunction.holoRepr

The limit repair of f: at each point, the limit of f along the punctured neighborhood. Where the order of f is ≥ 0 this is a genuine value (Mathlib tendsto_nhds_of_meromorphicOrderAt_nonneg), and it discards removable-singularity junk that f.toFun may carry.

noncomputable def MeromorphicFunction.holoRepr (f : MeromorphicFunction X) (x : X) : ℂ

MeromorphicFunction.exists_holoRepr_eq_NFOn

The local repair lemma. On a small open neighborhood V of φ x₀ (with φ = chartAt x₀), the limit-repair holoRepr, read back through the chart, coincides with the normal-form representative of the pullback F = f.toFun ∘ φ.symm. Concretely: for every w ∈ V, f.holoRepr (φ.symm w) = toMeromorphicNFOn F V w.

This needs the order of f to be ≥ 0 only at x₀ (the center); at the punctured points F is analytic, so its order is automatically ≥ 0.

theorem MeromorphicFunction.exists_holoRepr_eq_NFOn (f : MeromorphicFunction X) (x₀ : X)
    (h₀ : 0 ≤ f.orderAtPoint x₀) :
    ∃ V : Set ℂ, IsOpen V ∧ (chartAt (H := ℂ) x₀) x₀ ∈ V ∧
      ∃ (_hF : MeromorphicOn (f.toFun ∘ (chartAt (H := ℂ) x₀).symm) V),
        ∀ w ∈ V, f.holoRepr ((chartAt (H := ℂ) x₀).symm w) =
          toMeromorphicNFOn (f.toFun ∘ (chartAt (H := ℂ) x₀).symm) V w

MeromorphicFunction.holoRepr_chartPullback_eventuallyEq_NFAt

Off-center, the chart pullback of holoRepr equals the normal-form representative. With NO order hypothesis at the center x₀: on the *punctured* neighborhood 𝓝[≠] (φ x₀) (φ = chartAt x₀), the limit-repair holoRepr read back through the chart agrees with the normal-form representative toMeromorphicNFAt F (φ x₀) of the pullback F = f.toFun ∘ φ.symm.

Off the center, F is genuinely analytic (MeromorphicAt.eventually_analyticAt), so f.toFun carries no junk and its punctured limit there is the analytic value F w; this equals N w since the normal form agrees with F off the center. This is the punctured-neighborhood input that the simple-pole analysis at a pole (where the center order is < 0, so exists_holoRepr_eq_NFOn does not apply) consumes.

theorem MeromorphicFunction.holoRepr_chartPullback_eventuallyEq_NFAt
    (f : MeromorphicFunction X) (x₀ : X) :
    f.holoRepr ∘ (chartAt (H := ℂ) x₀).symm =ᶠ[𝓝[≠] ((chartAt (H := ℂ) x₀) x₀)]
      toMeromorphicNFAt (f.toFun ∘ (chartAt (H := ℂ) x₀).symm) ((chartAt (H := ℂ) x₀) x₀)

MeromorphicFunction.analyticAt_holoRepr_chartPullback_of_orderNonneg

The chart pullback of holoRepr is analytic at a point of nonnegative order. This is the local (pointwise) core of mdifferentiable_holoRepr, requiring 0 ≤ orderAtPoint *only at x₀* (not globally). Read back through the chart φ = chartAt x₀, the limit-repair holoRepr ∘ φ.symm agrees near φ x₀ with the analytic normal-form representative of the pullback (exists_holoRepr_eq_NFOn), hence is AnalyticAt ℂ.

theorem MeromorphicFunction.analyticAt_holoRepr_chartPullback_of_orderNonneg
    (f : MeromorphicFunction X) {x₀ : X} (h₀ : 0 ≤ f.orderAtPoint x₀) :
    AnalyticAt ℂ (f.holoRepr ∘ (chartAt (H := ℂ) x₀).symm) ((chartAt (H := ℂ) x₀) x₀)

MeromorphicFunction.mdifferentiable_holoRepr

The limit-repair is globally holomorphic. If f has no pole (∀ x, 0 ≤ orderAtPoint x), then f.holoRepr : X → ℂ is MDifferentiable. In each chart, holoRepr read back equals the analytic normal-form representative of the pullback (exists_holoRepr_eq_NFOn), hence is analytic; the chart bridge mdifferentiableWithinAt_of_comp_extChartAt_symm lifts this to the manifold.

theorem MeromorphicFunction.mdifferentiable_holoRepr [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    (hpos : ∀ x, 0 ≤ f.orderAtPoint x) :
    MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f.holoRepr

MeromorphicFunction.orderAtPoint_eq_zero_of_holoRepr_const

If the limit-repair holoRepr is constant (the conclusion of Liouville on a compact connected manifold), then the order of f is 0 at every point. In each chart the pullback f.toFun ∘ φ.symm agrees off the center with the normal-form representative, which equals the constant c; the order of a constant is 0 (⊤ ↦ 0 for c = 0, else 0).

theorem MeromorphicFunction.orderAtPoint_eq_zero_of_holoRepr_const (f : MeromorphicFunction X)
    (hpos : ∀ x, 0 ≤ f.orderAtPoint x) {c : ℂ} (hconst : ∀ y, f.holoRepr y = c) (x : X) :
    f.orderAtPoint x = 0

MeromorphicFunction.exists_pole_of_nonconstant

Compact Liouville for meromorphic functions. A non-constant meromorphic function on a compact connected Riemann surface has a pole. Contrapositive: with no pole every order is ≥ 0, so the limit-repair holoRepr is globally holomorphic (mdifferentiable_holoRepr); by holomorphic Liouville on the compact connected X (MDifferentiable.exists_eq_const_of_compactSpace) it is constant, forcing every order to be 0 (orderAtPoint_eq_zero_of_holoRepr_const) — contradicting non-constancy.

theorem MeromorphicFunction.exists_pole_of_nonconstant [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    (hf : ∃ x, f.orderAtPoint x ≠ 0) : ∃ x, f.orderAtPoint x < 0