The field of meromorphic functions on a connected Riemann surface

A meromorphic function on a Riemann surface X is a holomorphic map f : X → OnePoint ℂ to the Riemann sphere which is not the constant map ∞ (TauCeti.RiemannSurface.MeromorphicFunction X). This file makes these functions a field when X is connected, and a ℂ-algebra through the constant functions.

The operations are not defined pointwise, since a sum or product of two maps to the sphere has no meaning at the common poles. Instead, f is read in the affine chart of the sphere as a function f.finitePart : X → ℂ, which agrees with f away from the poles and is meromorphic in the sense of TauCeti.RiemannSurface.MeromorphicAt at every point (TauCeti.RiemannSurface.MeromorphicFunction.meromorphicAt_finitePart). The pointwise sum of two finite parts is again meromorphic, and TauCeti.RiemannSurface.sphereMap turns it back into a holomorphic map to the sphere, filling in the removable singularities and poles. This defines f + g, and likewise f * g, -f, f - g and f⁻¹.

Each operation is characterized by its values off the poles: for instance f + g is the unique meromorphic function whose value at every point where f and g are finite is the sum of their values (TauCeti.RiemannSurface.MeromorphicFunction.eq_add_iff). By continuity, a meromorphic function is determined by its values on the punctured neighbourhoods of the points (TauCeti.RiemannSurface.MeromorphicFunction.eq_of_eventually_apply_eq), and by the identity theorem the poles of a meromorphic function on a connected Riemann surface are isolated (TauCeti.RiemannSurface.MeromorphicFunction.eventually_ne_infty), so the points where f and g are finite fill a punctured neighbourhood of every point. In the same way a meromorphic function on a connected Riemann surface is determined by the germs of its finite part on these punctured neighbourhoods. The meromorphic functions therefore embed into a commutative ring compatibly with the operations, which gives the commutative ring structure. The zeros of a nonzero meromorphic function are isolated as well, so its finite part is eventually nonzero on every punctured neighbourhood and its inverse is a multiplicative inverse.

Main definitions

• TauCeti.RiemannSurface.MeromorphicFunction X: the meromorphic functions on X, as holomorphic maps to the Riemann sphere which are not identically ∞.
• TauCeti.RiemannSurface.MeromorphicFunction.finitePart: a meromorphic function read in the affine chart of the sphere, with value 0 at the poles.
• TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic: the meromorphic function defined by a function X → ℂ meromorphic at every point.
• TauCeti.RiemannSurface.MeromorphicFunction.instField and TauCeti.RiemannSurface.MeromorphicFunction.instAlgebra: the field and ℂ-algebra structures on a connected Riemann surface.

Main results

• TauCeti.RiemannSurface.MeromorphicFunction.sphereMap_finitePart: a meromorphic function is recovered from its finite part by TauCeti.RiemannSurface.sphereMap.
• TauCeti.RiemannSurface.MeromorphicFunction.eq_add_iff, TauCeti.RiemannSurface.MeromorphicFunction.eq_mul_iff, TauCeti.RiemannSurface.MeromorphicFunction.eq_neg_iff and TauCeti.RiemannSurface.MeromorphicFunction.eq_inv_iff: the defining properties of the operations.
• TauCeti.RiemannSurface.MeromorphicFunction.inv_apply_of_eq_infty: the inverse of a meromorphic function vanishes at its poles.
• TauCeti.RiemannSurface.MeromorphicFunction.finite_setOf_eq_infty: on a compact preconnected Riemann surface, a meromorphic function has finitely many poles.
• TauCeti.RiemannSurface.MeromorphicFunction.finite_setOf_eq_zero: on a compact connected Riemann surface, a nonzero meromorphic function has finitely many zeros.
• TauCeti.RiemannSurface.MeromorphicFunction.exists_algebraMap_eq_of_forall_ne_infty: the maximum principle, a meromorphic function without poles on a compact connected Riemann surface is constant.
• MeromorphicFunction.exists_algebraMap_eq_of_forall_ne_ne_infty_of_forall_ne_ne_zero: a meromorphic function with neither zeros nor poles off one point of a compact connected Riemann surface is constant.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §1, 1.12 to 1.16.
• Ernesto Girondo and Gabino González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press, 2012, Proposition 1.23.

structure TauCeti.RiemannSurface.MeromorphicFunction (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_1

A meromorphic function on a Riemann surface X: a holomorphic map X → OnePoint ℂ to the Riemann sphere which is not the constant map ∞. On a connected X these form a field (TauCeti.RiemannSurface.MeromorphicFunction.instField).

• toFun : X → OnePoint ℂ

  The underlying map to the Riemann sphere.

• mdifferentiable' : MDiff self.toFun
• ne_infty' : self.toFun ≠ fun (x : X) => OnePoint.infty

@[instance_reducible]

instance TauCeti.RiemannSurface.MeromorphicFunction.instFunLikeOnePointComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : FunLike (MeromorphicFunction X) X (OnePoint ℂ)

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → OnePoint ℂ) (hf : MDiff f) (h : f ≠ fun (x : X) => OnePoint.infty) : ⇑{ toFun := f, mdifferentiable' := hf, ne_infty' := h } = f

theorem TauCeti.RiemannSurface.MeromorphicFunction.ext {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} (h : ∀ (x : X), f x = g x) : f = g

theorem TauCeti.RiemannSurface.MeromorphicFunction.ext_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} : f = g ↔ ∀ (x : X), f x = g x

theorem TauCeti.RiemannSurface.MeromorphicFunction.mdifferentiable {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) : MDiff ⇑f

A meromorphic function is a holomorphic map to the Riemann sphere.

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_ne_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) : ⇑f ≠ fun (x : X) => OnePoint.infty

A meromorphic function is not the constant map ∞.

theorem TauCeti.RiemannSurface.MeromorphicFunction.continuous {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) : Continuous ⇑f

The finite part

noncomputable def TauCeti.RiemannSurface.MeromorphicFunction.finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) (x : X) : ℂ

A meromorphic function read in the affine chart of the Riemann sphere: its value at x is f x when this is finite, and 0 at a pole of f.

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_def {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : MeromorphicFunction X) (x : X) : f.finitePart x = ↑OnePoint.affineChart (f x)

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} {z : ℂ} (h : f x = ↑z) : f.finitePart x = z

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_of_eq_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} (h : f x = OnePoint.infty) : f.finitePart x = 0

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} (h : f x ≠ OnePoint.infty) : ↑(f.finitePart x) = f x

Away from the poles, a meromorphic function is its finite part.

theorem TauCeti.RiemannSurface.MeromorphicFunction.continuousAt_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} (h : f x ≠ OnePoint.infty) : ContinuousAt f.finitePart x

theorem TauCeti.RiemannSurface.MeromorphicFunction.mdifferentiableAt_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} (h : f x ≠ OnePoint.infty) : MDiffAt f.finitePart x

Away from the poles, the finite part of a meromorphic function is holomorphic: it is the meromorphic function read in the affine chart of the sphere.

theorem TauCeti.RiemannSurface.MeromorphicFunction.contMDiffAt_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (h : f x ≠ OnePoint.infty) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f.finitePart x

Away from the poles, the finite part of a meromorphic function is complex analytic.

theorem TauCeti.RiemannSurface.MeromorphicFunction.apply_eq_of_tendsto {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} {φ : X → OnePoint ℂ} {c : OnePoint ℂ} (hφ : Filter.Tendsto φ (nhdsWithin x {x}ᶜ) (nhds c)) (h : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, f y = φ y) : f x = c

The value of a meromorphic function at x is the limit at x, along the punctured neighbourhoods of x, of any map to the sphere that agrees with it near x.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_of_eventually_apply_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} (h : ∀ (x : X), ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, f y = g y) : f = g

Uniqueness of meromorphic functions. Two meromorphic functions which agree on a punctured neighbourhood of every point are equal.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_of_forall_apply_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {p : X → Prop} (hp : ∀ (x : X), ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y) (h : ∀ (x : X), p x → f x = g x) : f = g

To show that f equals g, it suffices to compare their values at the points satisfying a property p which holds on a punctured neighbourhood of every point, such as being a pole of neither of two given meromorphic functions.

theorem TauCeti.RiemannSurface.MeromorphicFunction.meromorphicAt_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (f : MeromorphicFunction X) (x : X) : MeromorphicAt f.finitePart x

The finite part of a meromorphic function is meromorphic at every point. Away from the poles it is holomorphic; near a pole it is the reciprocal of the holomorphic function reading f in the inverted chart of the sphere.

Isolated poles and finiteness of poles

theorem TauCeti.RiemannSurface.MeromorphicFunction.eventually_ne_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [PreconnectedSpace X] (f : MeromorphicFunction X) (x : X) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, f y ≠ OnePoint.infty

The poles of a meromorphic function are isolated. On a connected Riemann surface, a meromorphic function is finite at every point of a punctured neighbourhood of any point.

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.sphereMap_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [PreconnectedSpace X] (f : MeromorphicFunction X) : sphereMap f.finitePart = ⇑f

On a connected Riemann surface, a meromorphic function is recovered from its finite part by taking limits on punctured neighbourhoods.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_of_eventuallyEq_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [PreconnectedSpace X] (h : ∀ (x : X), f.finitePart =ᶠ[nhdsWithin x {x}ᶜ] g.finitePart) : f = g

On a connected Riemann surface, two meromorphic functions whose finite parts agree on a punctured neighbourhood of every point are equal.

theorem TauCeti.RiemannSurface.MeromorphicFunction.finite_setOf_eq_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [PreconnectedSpace X] [CompactSpace X] (f : MeromorphicFunction X) : {x : X | f x = OnePoint.infty}.Finite

A meromorphic function on a compact preconnected Riemann surface has finitely many poles.

Meromorphic functions from functions X → ℂ

noncomputable def TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) : MeromorphicFunction X

The meromorphic function on a nonempty Riemann surface defined by a function h : X → ℂ meromorphic at every point: the holomorphic map TauCeti.RiemannSurface.sphereMap h to the Riemann sphere, which agrees with h on a punctured neighbourhood of every point.

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_ofMeromorphic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) : ⇑(ofMeromorphic hh) = sphereMap h

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_ofMeromorphic_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (x : X) : (ofMeromorphic hh).finitePart =ᶠ[nhdsWithin x {x}ᶜ] h

The finite part of TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic hh agrees with h on a punctured neighbourhood of every point.

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_apply_of_continuousAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (hc : ContinuousAt h x) : (ofMeromorphic hh) x = ↑(h x)

At a point where h is continuous, TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic hh takes the value of h.

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) {k : X → ℂ} (hk : ∀ (x : X), MeromorphicAt k x) (hhk : ∀ (x : X), h =ᶠ[nhdsWithin x {x}ᶜ] k) : ofMeromorphic hh = ofMeromorphic hk

TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic hh depends only on the values of h on a punctured neighbourhood of every point.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_ofMeromorphic_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) {p : X → Prop} (hp : ∀ (x : X), ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y) (hc : ∀ (x : X), p x → ContinuousAt h x) {k : MeromorphicFunction X} : k = ofMeromorphic hh ↔ ∀ (x : X), p x → k x = ↑(h x)

A meromorphic function k equals TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic hh if and only if it agrees with h at the points satisfying a property p which holds on a punctured neighbourhood of every point and at which h is continuous.

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_finitePart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [Nonempty X] [PreconnectedSpace X] (f : MeromorphicFunction X) : ofMeromorphic ⋯ = f

On a connected Riemann surface, a meromorphic function is the one defined by its finite part.

The field operations

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instZero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Zero (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instOne {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : One (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instAdd {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Add (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instMul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Mul (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instNeg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Neg (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instSub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Sub (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instInv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Inv (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instSMulNat {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : SMul ℕ (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instSMulInt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : SMul ℤ (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instPowNat {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Pow (MeromorphicFunction X) ℕ

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instNatCast {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : NatCast (MeromorphicFunction X)

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instIntCast {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : IntCast (MeromorphicFunction X)

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : ⇑0 = fun (x : X) => ↑0

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : ⇑1 = fun (x : X) => ↑1

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : finitePart 0 = 0

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : finitePart 1 = 1

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_add_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (f g : MeromorphicFunction X) (x : X) : (f + g).finitePart =ᶠ[nhdsWithin x {x}ᶜ] f.finitePart + g.finitePart

The finite part of f + g agrees with the sum of the finite parts of f and g on a punctured neighbourhood of every point.

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_mul_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (f g : MeromorphicFunction X) (x : X) : (f * g).finitePart =ᶠ[nhdsWithin x {x}ᶜ] f.finitePart * g.finitePart

The finite part of f * g agrees with the product of the finite parts of f and g on a punctured neighbourhood of every point.

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_neg_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (f : MeromorphicFunction X) (x : X) : (-f).finitePart =ᶠ[nhdsWithin x {x}ᶜ] -f.finitePart

The finite part of -f agrees with the negative of the finite part of f on a punctured neighbourhood of every point.

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_inv_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (f : MeromorphicFunction X) (x : X) : f⁻¹.finitePart =ᶠ[nhdsWithin x {x}ᶜ] f.finitePart⁻¹

The finite part of f⁻¹ agrees with the inverse of the finite part of f on a punctured neighbourhood of every point.

The commutative ring structure

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instCommRing {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : CommRing (MeromorphicFunction X)

The meromorphic functions on a connected Riemann surface form a commutative ring.

The field structure

theorem TauCeti.RiemannSurface.MeromorphicFunction.eventually_finitePart_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f ≠ 0) (x : X) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, f.finitePart y ≠ 0

The zeros of a nonzero meromorphic function on a connected Riemann surface are isolated, as are its poles, so its finite part vanishes at no point of a punctured neighbourhood of any point.

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instField {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Field (MeromorphicFunction X)

The meromorphic functions on a connected Riemann surface form a field.

The defining properties of the operations

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_add_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {k : MeromorphicFunction X} : k = f + g ↔ ∀ (x : X), f x ≠ OnePoint.infty → g x ≠ OnePoint.infty → k x = ↑(f.finitePart x + g.finitePart x)

The defining property of addition. On a connected Riemann surface, f + g is the unique meromorphic function whose value at every point where f and g are both finite is the sum of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_mul_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {k : MeromorphicFunction X} : k = f * g ↔ ∀ (x : X), f x ≠ OnePoint.infty → g x ≠ OnePoint.infty → k x = ↑(f.finitePart x * g.finitePart x)

The defining property of multiplication. On a connected Riemann surface, f * g is the unique meromorphic function whose value at every point where f and g are both finite is the product of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_neg_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {k : MeromorphicFunction X} : k = -f ↔ ∀ (x : X), f x ≠ OnePoint.infty → k x = ↑(-f.finitePart x)

The defining property of negation. On a connected Riemann surface, -f is the unique meromorphic function whose value at every point where f is finite is the negative of the value of f.

theorem TauCeti.RiemannSurface.MeromorphicFunction.eq_inv_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f ≠ 0) {k : MeromorphicFunction X} : k = f⁻¹ ↔ ∀ (x : X), f x ≠ OnePoint.infty → f x ≠ ↑0 → k x = ↑(f.finitePart x)⁻¹

The defining property of the inverse. On a connected Riemann surface, the inverse of a nonzero meromorphic function f is the unique meromorphic function whose value at every point where f is finite and nonzero is the inverse of the value of f.

The ℂ-algebra structure

@[instance_reducible]

noncomputable instance TauCeti.RiemannSurface.MeromorphicFunction.instAlgebra {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] : Algebra ℂ (MeromorphicFunction X)

The meromorphic functions on a connected Riemann surface form a ℂ-algebra, ℂ acting through the constant functions.

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.coe_algebraMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (c : ℂ) : ⇑((algebraMap ℂ (MeromorphicFunction X)) c) = fun (x : X) => ↑c

theorem TauCeti.RiemannSurface.MeromorphicFunction.exists_apply_ne_of_notMem_range_algebraMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f ∉ Set.range ⇑(algebraMap ℂ (MeromorphicFunction X))) : ∃ (x : X) (y : X), f x ≠ f y

A meromorphic function outside the range of the constant functions takes two distinct values on the Riemann sphere.

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.finitePart_algebraMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (c : ℂ) : ((algebraMap ℂ (MeromorphicFunction X)) c).finitePart = fun (x : X) => c

ofMeromorphic and the operations

On a connected Riemann surface, TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic sends constants, sums, products, negatives, differences, inverses and powers of functions X → ℂ to the corresponding operations on meromorphic functions. Apart from the constants, these lemmas are not simp lemmas: their left-hand sides do not determine the meromorphy proofs of the operands, so simp could not discharge them. Instantiate them instead, as in simp [ofMeromorphic_add hh hk].

@[simp]

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (c : ℂ) : ofMeromorphic ⋯ = (algebraMap ℂ (MeromorphicFunction X)) c

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h k : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (hk : ∀ (x : X), MeromorphicAt k x) : ofMeromorphic ⋯ = ofMeromorphic hh + ofMeromorphic hk

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h k : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (hk : ∀ (x : X), MeromorphicAt k x) : ofMeromorphic ⋯ = ofMeromorphic hh * ofMeromorphic hk

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) : ofMeromorphic ⋯ = -ofMeromorphic hh

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h k : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (hk : ∀ (x : X), MeromorphicAt k x) : ofMeromorphic ⋯ = ofMeromorphic hh - ofMeromorphic hk

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) : ofMeromorphic ⋯ = (ofMeromorphic hh)⁻¹

theorem TauCeti.RiemannSurface.MeromorphicFunction.ofMeromorphic_pow {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {h : X → ℂ} (hh : ∀ (x : X), MeromorphicAt h x) (n : ℕ) : ofMeromorphic ⋯ = ofMeromorphic hh ^ n

Values of the operations

At a point where the operands are finite, the operations on meromorphic functions are computed pointwise. Each operation has two forms: one for operands known to be finite, in terms of their finite parts, and one (_of_eq_coe) for operands with known finite values. At a pole of f, its inverse vanishes.

theorem TauCeti.RiemannSurface.MeromorphicFunction.add_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (hg : g x ≠ OnePoint.infty) : (f + g) x = ↑(f.finitePart x + g.finitePart x)

At a point where f and g are finite, f + g takes the sum of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.add_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a b : ℂ} (hf : f x = ↑a) (hg : g x = ↑b) : (f + g) x = ↑(a + b)

If f and g take the values a and b at x, then f + g takes the value a + b.

theorem TauCeti.RiemannSurface.MeromorphicFunction.mul_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (hg : g x ≠ OnePoint.infty) : (f * g) x = ↑(f.finitePart x * g.finitePart x)

At a point where f and g are finite, f * g takes the product of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.mul_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a b : ℂ} (hf : f x = ↑a) (hg : g x = ↑b) : (f * g) x = ↑(a * b)

If f and g take the values a and b at x, then f * g takes the value a * b.

theorem TauCeti.RiemannSurface.MeromorphicFunction.neg_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) : (-f) x = ↑(-f.finitePart x)

At a point where f is finite, -f takes the negative of its value.

theorem TauCeti.RiemannSurface.MeromorphicFunction.neg_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a : ℂ} (hf : f x = ↑a) : (-f) x = ↑(-a)

If f takes the value a at x, then -f takes the value -a.

theorem TauCeti.RiemannSurface.MeromorphicFunction.sub_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a b : ℂ} (hf : f x = ↑a) (hg : g x = ↑b) : (f - g) x = ↑(a - b)

If f and g take the values a and b at x, then f - g takes the value a - b.

theorem TauCeti.RiemannSurface.MeromorphicFunction.sub_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (hg : g x ≠ OnePoint.infty) : (f - g) x = ↑(f.finitePart x - g.finitePart x)

At a point where f and g are finite, f - g takes the difference of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.inv_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (hf0 : f x ≠ ↑0) : f⁻¹ x = ↑(f.finitePart x)⁻¹

At a point where f is finite and nonzero, f⁻¹ takes the inverse of its value.

theorem TauCeti.RiemannSurface.MeromorphicFunction.inv_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a : ℂ} (hf : f x = ↑a) (ha : a ≠ 0) : f⁻¹ x = ↑a⁻¹

If f takes a nonzero value a at x, then f⁻¹ takes the value a⁻¹.

theorem TauCeti.RiemannSurface.MeromorphicFunction.pow_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a : ℂ} (hf : f x = ↑a) (n : ℕ) : (f ^ n) x = ↑(a ^ n)

If f takes the value a at x, then f ^ n takes the value a ^ n.

theorem TauCeti.RiemannSurface.MeromorphicFunction.pow_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (n : ℕ) : (f ^ n) x = ↑(f.finitePart x ^ n)

At a point where f is finite, f ^ n takes the n-th power of its value.

theorem TauCeti.RiemannSurface.MeromorphicFunction.zpow_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a : ℂ} (hf : f x = ↑a) (ha : a ≠ 0) (n : ℤ) : (f ^ n) x = ↑(a ^ n)

If f takes a nonzero value a at x, then f ^ n takes the value a ^ n, for every integer n.

theorem TauCeti.RiemannSurface.MeromorphicFunction.zpow_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (hf0 : f x ≠ ↑0) (n : ℤ) : (f ^ n) x = ↑(f.finitePart x ^ n)

At a point where f is finite and nonzero, f ^ n takes the n-th power of its value, for every integer n.

theorem TauCeti.RiemannSurface.MeromorphicFunction.prod_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {ι : Type u_2} {s : Finset ι} {f : ι → MeromorphicFunction X} {a : ι → ℂ} (hf : ∀ i ∈ s, (f i) x = ↑(a i)) : (∏ i ∈ s, f i) x = ↑(∏ i ∈ s, a i)

If each f i takes the value a i at x, then the product of the f i takes the product of the a i.

theorem TauCeti.RiemannSurface.MeromorphicFunction.prod_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {ι : Type u_2} {s : Finset ι} {f : ι → MeromorphicFunction X} (hf : ∀ i ∈ s, (f i) x ≠ OnePoint.infty) : (∏ i ∈ s, f i) x = ↑(∏ i ∈ s, (f i).finitePart x)

At a point where each f i is finite, the product of the f i takes the product of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.sum_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {ι : Type u_2} {s : Finset ι} {f : ι → MeromorphicFunction X} {a : ι → ℂ} (hf : ∀ i ∈ s, (f i) x = ↑(a i)) : (∑ i ∈ s, f i) x = ↑(∑ i ∈ s, a i)

If each f i takes the value a i at x, then the sum of the f i takes the sum of the a i.

theorem TauCeti.RiemannSurface.MeromorphicFunction.sum_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {ι : Type u_2} {s : Finset ι} {f : ι → MeromorphicFunction X} (hf : ∀ i ∈ s, (f i) x ≠ OnePoint.infty) : (∑ i ∈ s, f i) x = ↑(∑ i ∈ s, (f i).finitePart x)

At a point where each f i is finite, the sum of the f i takes the sum of their values.

theorem TauCeti.RiemannSurface.MeromorphicFunction.aeval_apply_of_eq_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] {a : ℂ} (hf : f x = ↑a) (p : Polynomial ℂ) : ((Polynomial.aeval f) p) x = ↑(Polynomial.eval a p)

If f takes the value a at x, then the polynomial p evaluated at f takes the value p(a) at x.

theorem TauCeti.RiemannSurface.MeromorphicFunction.aeval_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x ≠ OnePoint.infty) (p : Polynomial ℂ) : ((Polynomial.aeval f) p) x = ↑(Polynomial.eval (f.finitePart x) p)

At a point where f is finite, a polynomial evaluated at f takes the value of the polynomial at f.finitePart x.

theorem TauCeti.RiemannSurface.MeromorphicFunction.inv_apply_of_eq_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] (hf : f x = OnePoint.infty) : f⁻¹ x = ↑0

The inverse vanishes at the poles. At a pole of f, the meromorphic function f⁻¹ takes the value 0.

Finiteness of zeros, and the maximum principle

theorem TauCeti.RiemannSurface.MeromorphicFunction.finite_setOf_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] [CompactSpace X] (hf : f ≠ 0) : {x : X | f x = ↑0}.Finite

A nonzero meromorphic function on a compact connected Riemann surface has finitely many zeros.

theorem TauCeti.RiemannSurface.MeromorphicFunction.exists_algebraMap_eq_of_forall_ne_infty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] [CompactSpace X] (h : ∀ (x : X), f x ≠ OnePoint.infty) : ∃ (c : ℂ), (algebraMap ℂ (MeromorphicFunction X)) c = f

The maximum principle. A meromorphic function without poles on a compact connected Riemann surface is constant.

theorem TauCeti.RiemannSurface.MeromorphicFunction.exists_algebraMap_eq_of_forall_ne_ne_infty_of_forall_ne_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : MeromorphicFunction X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [ConnectedSpace X] [CompactSpace X] (x₀ : X) (hinf : ∀ (x : X), x ≠ x₀ → f x ≠ OnePoint.infty) (h0 : ∀ (x : X), x ≠ x₀ → f x ≠ ↑0) : ∃ (c : ℂ), (algebraMap ℂ (MeromorphicFunction X)) c = f

A meromorphic function with neither zeros nor poles off one point is constant on a compact connected Riemann surface.