Meromorphic functions as holomorphic maps to the Riemann sphere

A meromorphic function f : X → ℂ on a Riemann surface X is the same thing as a holomorphic map X → OnePoint ℂ to the Riemann sphere which is not identically ∞. This file constructs the forward direction. The map TauCeti.RiemannSurface.sphereMap f sends x to the limit of f y in OnePoint ℂ as y tends to x with y ≠ x. Thus it agrees with f at every point where f is continuous (TauCeti.RiemannSurface.sphereMap_of_continuousAt). For a meromorphic f it is ∞ exactly at the poles (TauCeti.RiemannSurface.sphereMap_eq_infty_iff). At a removable singularity it takes the limiting value, whatever value f itself was given there (TauCeti.RiemannSurface.sphereMap_eq_coe_iff).

Holomorphy is checked in the two charts of the sphere (TauCeti.RiemannSurface.mdifferentiableAt_sphereMap). Away from the poles, the map read in the affine chart is the normal form of f, which is holomorphic by the removable singularity theorem. At a pole, it is read in the inverted chart as the normal form of the reciprocal 1 / f. That function vanishes at the pole and is again holomorphic there.

On a compact connected Riemann surface, a meromorphic function which is not constant near some point therefore gives a finite holomorphic map to the sphere (TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMeromorphic), with finite fibres. This is the route from the existence of nonconstant meromorphic functions, as produced by the Riemann–Roch theorem, to the degree theory of finite holomorphic maps.

Main declarations

• TauCeti.RiemannSurface.sphereMap: the map to the Riemann sphere defined by f : X → ℂ.
• TauCeti.RiemannSurface.sphereMap_of_continuousAt, TauCeti.RiemannSurface.eventually_sphereMap_eq, TauCeti.RiemannSurface.sphereMap_eq_coe_iff and TauCeti.RiemannSurface.sphereMap_eq_infty_iff: its values.
• TauCeti.RiemannSurface.mdifferentiableAt_sphereMap and TauCeti.RiemannSurface.mdifferentiable_sphereMap: it is holomorphic when f is meromorphic.
• TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMeromorphic: the finite holomorphic map to the sphere defined by a meromorphic function which is not constant near some point, on a compact connected Riemann surface.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §1, Theorem 1.15.

@[simp]

theorem OnePoint.meromorphicOrderAt_affineChart_infty : TauCeti.RiemannSurface.meromorphicOrderAt (↑affineChart) infty = ↑(-1)

The affine coordinate has a simple pole at infinity.

noncomputable def TauCeti.RiemannSurface.sphereMap {X : Type u_1} [TopologicalSpace X] (f : X → ℂ) (x : X) : OnePoint ℂ

The map to the Riemann sphere OnePoint ℂ defined by a function f : X → ℂ, typically on a Riemann surface: its value at x is the limit of f y in OnePoint ℂ as y tends to x with y ≠ x. It agrees with f wherever f is continuous (TauCeti.RiemannSurface.sphereMap_of_continuousAt). When f is meromorphic it is ∞ exactly at the poles of f (TauCeti.RiemannSurface.sphereMap_eq_infty_iff), and it is holomorphic (TauCeti.RiemannSurface.mdifferentiable_sphereMap). Where the limit does not exist, the value is junk.

theorem TauCeti.RiemannSurface.sphereMap_def {X : Type u_1} [TopologicalSpace X] (f : X → ℂ) (x : X) : sphereMap f x = (nhdsWithin x {x}ᶜ).limUnder fun (y : X) => ↑(f y)

Values

theorem TauCeti.RiemannSurface.sphereMap_eq_of_tendsto {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] {c : OnePoint ℂ} (h : Filter.Tendsto (fun (y : X) => ↑(f y)) (nhdsWithin x {x}ᶜ) (nhds c)) : sphereMap f x = c

The value of sphereMap f at x is any limit of f at x in the Riemann sphere.

theorem TauCeti.RiemannSurface.sphereMap_eq_of_eventuallyEq {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] {k : X → OnePoint ℂ} (h : (fun (y : X) => ↑(f y)) =ᶠ[nhdsWithin x {x}ᶜ] k) (hk : ContinuousAt k x) : sphereMap f x = k x

The value of sphereMap f at x is the value at x of any map continuous at x which agrees with f on a punctured neighbourhood of x.

theorem TauCeti.RiemannSurface.sphereMap_of_continuousAt {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] (hf : ContinuousAt f x) : sphereMap f x = ↑(f x)

sphereMap f agrees with f at every point where f is continuous.

@[simp]

theorem TauCeti.RiemannSurface.sphereMap_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (c : ℂ) : (sphereMap fun (x : X) => c) = fun (x : X) => ↑c

The map to the sphere defined by a constant function is that constant.

The local picture in one variable

Holomorphy

theorem TauCeti.RiemannSurface.mdifferentiableAt_sphereMap {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) : MDiffAt (sphereMap f) x

Meromorphic functions are holomorphic maps to the Riemann sphere. If f is meromorphic at x, then sphereMap f is holomorphic at x.

theorem TauCeti.RiemannSurface.mdifferentiable_sphereMap {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : ∀ (x : X), MeromorphicAt f x) : MDiff (sphereMap f)

Meromorphic functions are holomorphic maps to the Riemann sphere. If f is meromorphic at every point, then sphereMap f is holomorphic.

theorem TauCeti.RiemannSurface.eventually_sphereMap_eq {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, sphereMap f y = ↑(f y)

Near a point where f is meromorphic, sphereMap f agrees with f away from the point.

theorem TauCeti.RiemannSurface.sphereMap_eq_infty_iff {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) : sphereMap f x = OnePoint.infty ↔ meromorphicOrderAt f x < 0

At a point where f is meromorphic, sphereMap f is ∞ exactly when f has a pole.

theorem TauCeti.RiemannSurface.affineChart_sphereMap_eventuallyEq {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) : (fun (y : X) => ↑OnePoint.affineChart (sphereMap f y)) =ᶠ[nhdsWithin x {x}ᶜ] f

Filling removable singularities and reading in the affine chart preserves a meromorphic function on a punctured neighbourhood.

theorem TauCeti.RiemannSurface.contMDiffAt_affineChart_sphereMap {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) (h : 0 ≤ meromorphicOrderAt f x) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (fun (y : X) => ↑OnePoint.affineChart (sphereMap f y)) x

The filled affine representative of a meromorphic function is holomorphic at a point where its order is nonnegative.

theorem TauCeti.RiemannSurface.sphereMap_eq_coe_iff {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} {x : X} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (hf : MeromorphicAt f x) {c : ℂ} : sphereMap f x = ↑c ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)

At a point where f is meromorphic, sphereMap f takes a finite value c exactly when f tends to c on punctured neighbourhoods of the point.

Finite holomorphic maps to the sphere

noncomputable def TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMeromorphic {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [CompactSpace X] [PreconnectedSpace X] (hf : ∀ (x : X), MeromorphicAt f x) {x₀ : X} (hx₀ : ¬Filter.EventuallyConst f (nhdsWithin x₀ {x₀}ᶜ)) : FiniteHolomorphicMap X (OnePoint ℂ)

The finite holomorphic map defined by a meromorphic function. On a compact connected Riemann surface, a meromorphic function which is not constant near some point x₀ defines the finite holomorphic map TauCeti.RiemannSurface.sphereMap f to the Riemann sphere.

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.coe_ofMeromorphic {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [CompactSpace X] [PreconnectedSpace X] (hf : ∀ (x : X), MeromorphicAt f x) {x₀ : X} (hx₀ : ¬Filter.EventuallyConst f (nhdsWithin x₀ {x₀}ᶜ)) : ↑(ofMeromorphic hf hx₀) = sphereMap f