The field of meromorphic germs at a point

Let 𝕜 be a nontrivially normed field and a : 𝕜. A function meromorphic at a is only determined, as such, on a punctured neighbourhood of a: Mathlib's MeromorphicAt ignores the value at a itself. This file collects the germs along the punctured neighbourhood filter 𝓝[≠] a of the functions 𝕜 → 𝕜 which are meromorphic at a into a subring TauCeti.meromorphicGerms 𝕜 a of Mathlib's ring of germs Filter.Germ (𝓝[≠] a) 𝕜, and shows that it is a field. Constant functions give its natural algebra structure over 𝕜.

The inverse of a germ is the pointwise inverse. It is a multiplicative inverse because, by the principle of isolated zeros (MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero), a meromorphic function whose punctured germ is nonzero vanishes at no point of some punctured neighbourhood (MeromorphicAt.germ_ne_zero_iff).

For 𝕜 = ℂ this is the local field of meromorphic functions in one variable; it is identified with the fraction field of the ring of holomorphic germs at a in TauCeti.Geometry.Manifold.Complex.StructureSheaf.MeromorphicGerm.

References

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

theorem MeromorphicAt.germ_ne_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : MeromorphicAt f a) : ↑f ≠ 0 ↔ ∀ᶠ (z : 𝕜) in nhdsWithin a {a}ᶜ, f z ≠ 0

A function meromorphic at a has a nonzero germ on the punctured neighbourhoods of a exactly when it vanishes at no point of some punctured neighbourhood of a.

def TauCeti.meromorphicGerms (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (a : 𝕜) : Subring ((nhdsWithin a {a}ᶜ).Germ 𝕜)

The germs on the punctured neighbourhoods of a of the functions meromorphic at a.

theorem TauCeti.mem_meromorphicGerms_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {φ : (nhdsWithin a {a}ᶜ).Germ 𝕜} : φ ∈ meromorphicGerms 𝕜 a ↔ ∃ (f : 𝕜 → 𝕜), MeromorphicAt f a ∧ ↑f = φ

A punctured germ is meromorphic at a when it is the germ of a function meromorphic at a.

@[simp]

theorem TauCeti.coe_mem_meromorphicGerms {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f : 𝕜 → 𝕜} : ↑f ∈ meromorphicGerms 𝕜 a ↔ MeromorphicAt f a

The germ of a function lies in meromorphicGerms 𝕜 a exactly when the function is meromorphic at a.

def TauCeti.meromorphicGerms.mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (f : 𝕜 → 𝕜) (hf : MeromorphicAt f a) : ↥(meromorphicGerms 𝕜 a)

The punctured germ of a function meromorphic at the centre.

@[simp]

theorem TauCeti.meromorphicGerms.coe_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (f : 𝕜 → 𝕜) (hf : MeromorphicAt f a) : ↑(mk f hf) = ↑f

@[simp]

theorem TauCeti.meromorphicGerms.mk_eq_mk_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f g : 𝕜 → 𝕜} {hf : MeromorphicAt f a} {hg : MeromorphicAt g a} : mk f hf = mk g hg ↔ f =ᶠ[nhdsWithin a {a}ᶜ] g

Two meromorphic representatives define the same germ exactly when they agree near the centre on punctured neighbourhoods.

theorem TauCeti.meromorphicGerms.exists_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ : ↥(meromorphicGerms 𝕜 a)) : ∃ (f : 𝕜 → 𝕜) (hf : MeromorphicAt f a), mk f hf = φ

Every meromorphic germ has a meromorphic function representative.

@[simp]

theorem TauCeti.meromorphicGerms.mk_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : mk (fun (x : 𝕜) => 0) ⋯ = 0

@[simp]

theorem TauCeti.meromorphicGerms.mk_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : mk (fun (x : 𝕜) => 1) ⋯ = 1

@[simp]

theorem TauCeti.meromorphicGerms.mk_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f a) (hg : MeromorphicAt g a) : mk (f + g) ⋯ = mk f hf + mk g hg

@[simp]

theorem TauCeti.meromorphicGerms.mk_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f a) (hg : MeromorphicAt g a) : mk (f * g) ⋯ = mk f hf * mk g hg

def TauCeti.meromorphicGerms.coordinate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (a : 𝕜) : ↥(meromorphicGerms 𝕜 a)

The local coordinate germ vanishing at the centre.

@[simp]

theorem TauCeti.meromorphicGerms.coe_coordinate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : ↑(coordinate a) = ↑fun (z : 𝕜) => z - a

@[instance_reducible]

instance TauCeti.meromorphicGerms.instAlgebraSubtypeGermNhdsWithinComplSetSingletonMemSubring {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : Algebra 𝕜 ↥(meromorphicGerms 𝕜 a)

Scalars act on meromorphic germs through constant functions.

@[simp]

theorem TauCeti.meromorphicGerms.coe_algebraMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (c : 𝕜) : ↑((algebraMap 𝕜 ↥(meromorphicGerms 𝕜 a)) c) = ↑c

@[simp]

theorem TauCeti.meromorphicGerms.mk_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (c : 𝕜) : mk (fun (x : 𝕜) => c) ⋯ = (algebraMap 𝕜 ↥(meromorphicGerms 𝕜 a)) c

@[simp]

theorem TauCeti.meromorphicGerms.coe_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (c : 𝕜) (φ : ↥(meromorphicGerms 𝕜 a)) : ↑(c • φ) = c • ↑φ

@[simp]

theorem TauCeti.meromorphicGerms.mk_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (c : 𝕜) {f : 𝕜 → 𝕜} (hf : MeromorphicAt f a) : mk (c • f) ⋯ = c • mk f hf

@[instance_reducible]

instance TauCeti.meromorphicGerms.instInvSubtypeGermNhdsWithinComplSetSingletonMemSubring {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : Inv ↥(meromorphicGerms 𝕜 a)

The inverse of a meromorphic germ is its pointwise inverse.

@[simp]

theorem TauCeti.meromorphicGerms.coe_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ : ↥(meromorphicGerms 𝕜 a)) : ↑φ⁻¹ = (↑φ)⁻¹

@[simp]

theorem TauCeti.meromorphicGerms.mk_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f a) : mk f⁻¹ ⋯ = (mk f hf)⁻¹

@[instance_reducible]

instance TauCeti.meromorphicGerms.instField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : Field ↥(meromorphicGerms 𝕜 a)

The germs of functions meromorphic at a, on punctured neighbourhoods of a, form a field.

@[simp]

theorem TauCeti.meromorphicGerms.coe_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ ψ : ↥(meromorphicGerms 𝕜 a)) : ↑(φ / ψ) = ↑φ / ↑ψ

@[simp]

theorem TauCeti.meromorphicGerms.coe_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ : ↥(meromorphicGerms 𝕜 a)) (n : ℤ) : ↑(φ ^ n) = ↑φ ^ n