Meromorphic predicates and orders on a Riemann surface (CC3, chart layer)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.1).

• MeromorphicAtX f x / MeromorphicOnX f U: CC3's frozen chart-composite predicate, MeromorphicAt (f ∘ (chartAt ℂ x).symm) (chartAt ℂ x x). Junk-robust: junk in the chart composite off the chart source never affects the germ at chartAt x x.
• ordAtX f x : WithTop ℤ: CC3's frozen chart-composite order. Chart-invariant (ordAtX_eq_of_mem_source), and ordAtX_congr needs no meromorphy hypothesis — it holds for arbitrary f =ᶠ[𝓝[≠] x] g, which is exactly what lets ord descend to germ classes later.
• The workhorse eventually_nhdsNE_iff_comp_chart transports any eventual/punctured-neighborhood statement about f near x to a statement about the chart composite near chartAt ℂ x x (and back); every other transport lemma in this file is a one-line specialization of it.

def RS.MeromorphicAtX {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (x : X) : Prop

CC3 (frozen): meromorphy of the standard-chart composite. Junk-robust.

Equations

• RS.MeromorphicAtX f x = MeromorphicAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

def RS.MeromorphicOnX {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (U : Set X) : Prop

Relative CC3 predicate; the frozen global one is MeromorphicOnX f Set.univ.

Equations

• RS.MeromorphicOnX f U = ∀ x ∈ U, RS.MeromorphicAtX f x

theorem RS.meromorphicOnX_univ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} : MeromorphicOnX f Set.univ ↔ ∀ (x : X), MeromorphicAtX f x

noncomputable def RS.ordAtX {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (x : X) : WithTop ℤ

CC3 (frozen): the order at x, WithTop ℤ-valued, junk 0 off meromorphy.

Equations

• RS.ordAtX f x = meromorphicOrderAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

theorem RS.ordAtX_def {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (x : X) : ordAtX f x = meromorphicOrderAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

The chart-transport workhorse

theorem RS.eventually_nhdsNE_iff_comp_chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {p : X → Prop} {x : X} : (∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y) ↔ ∀ᶠ (z : ℂ) in nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ, p (↑(chartAt ℂ x).symm z)

Transport an eventual (punctured-neighborhood) property of f near x through the standard chart at x, and back. Every 𝓝[≠]-transport proof in this unit reduces to this one lemma.

theorem RS.eventually_nhdsNE_comp_chart_apply_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {q : ℂ → Prop} {x : X} : (∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, q (↑(chartAt ℂ x) y)) ↔ ∀ᶠ (z : ℂ) in nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ, q z

Simpler companion transport (no correction needed): a property q of the chart-image c y transports directly by pulling back along c.

theorem RS.frequently_nhdsNE_iff_comp_chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {p : X → Prop} {x : X} : (∃ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y) ↔ ∃ᶠ (z : ℂ) in nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ, p (↑(chartAt ℂ x).symm z)

Frequently version of eventually_nhdsNE_iff_comp_chart.

theorem RS.eventuallyEq_nhdsNE_comp_chart_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} : f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f ∘ ↑(chartAt ℂ x).symm =ᶠ[nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ] g ∘ ↑(chartAt ℂ x).symm

Specialization of eventually_nhdsNE_iff_comp_chart to EventuallyEq: agreement of f, g near x transports to agreement of their chart composites near chartAt ℂ x x.

theorem RS.tendsto_nhdsNE_comp_chart_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} {l : Filter ℂ} : Filter.Tendsto f (nhdsWithin x {x}ᶜ) l ↔ Filter.Tendsto (f ∘ ↑(chartAt ℂ x).symm) (nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ) l

Tendsto version of the chart-transport workhorse.

MeromorphicAtX: congruence and arithmetic

theorem RS.MeromorphicAtX.congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAtX g x

theorem RS.ordAtX_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : ordAtX f x = ordAtX g x

Meromorphy-free: ordAtX respects 𝓝[≠]-agreement of arbitrary functions.

theorem RS.meromorphicAtX_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} (c : ℂ) : MeromorphicAtX (fun (x : X) => c) x

theorem RS.MeromorphicAtX.add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) : MeromorphicAtX (f + g) x

theorem RS.MeromorphicAtX.mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) : MeromorphicAtX (f * g) x

theorem RS.MeromorphicAtX.neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : MeromorphicAtX (-f) x

theorem RS.MeromorphicAtX.sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) : MeromorphicAtX (f - g) x

theorem RS.MeromorphicAtX.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (c : ℂ) (hf : MeromorphicAtX f x) : MeromorphicAtX (c • f) x

theorem RS.MeromorphicAtX.inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : MeromorphicAtX f⁻¹ x

theorem RS.MeromorphicAtX.pow {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (n : ℕ) : MeromorphicAtX (f ^ n) x

theorem RS.MeromorphicAtX.zpow {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (n : ℤ) : MeromorphicAtX (f ^ n) x

MeromorphicOnX: pointwise lifting

theorem RS.MeromorphicOnX.add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) (hg : MeromorphicOnX g U) : MeromorphicOnX (f + g) U

theorem RS.MeromorphicOnX.mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) (hg : MeromorphicOnX g U) : MeromorphicOnX (f * g) U

theorem RS.MeromorphicOnX.neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) : MeromorphicOnX (-f) U

theorem RS.MeromorphicOnX.sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) (hg : MeromorphicOnX g U) : MeromorphicOnX (f - g) U

theorem RS.MeromorphicOnX.smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {U : Set X} (c : ℂ) (hf : MeromorphicOnX f U) : MeromorphicOnX (c • f) U

theorem RS.MeromorphicOnX.inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {U : Set X} (hf : MeromorphicOnX f U) : MeromorphicOnX f⁻¹ U

theorem RS.meromorphicOnX_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (c : ℂ) (U : Set X) : MeromorphicOnX (fun (x : X) => c) U

Classification of the order (no chart invariance needed)

theorem RS.ordAtX_eq_top_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} : ordAtX f x = ⊤ ↔ f =ᶠ[nhdsWithin x {x}ᶜ] 0

theorem RS.ordAtX_ne_top_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : ordAtX f x ≠ ⊤ ↔ ∀ᶠ (z : X) in nhdsWithin x {x}ᶜ, f z ≠ 0

theorem RS.MeromorphicAtX.frequently_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : (∃ᶠ (z : X) in nhdsWithin x {x}ᶜ, f z = 0) ↔ f =ᶠ[nhdsWithin x {x}ᶜ] 0

theorem RS.tendsto_nhds_iff_ordAtX_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : (∃ (c : ℂ), Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)) ↔ 0 ≤ ordAtX f x

theorem RS.tendsto_cobounded_iff_ordAtX_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : MeromorphicAtX f x) : Filter.Tendsto f (nhdsWithin x {x}ᶜ) (Bornology.cobounded ℂ) ↔ ordAtX f x < 0

Order arithmetic (chart composites are literal +,*,⁻¹ of chart composites)

theorem RS.ordAtX_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) : min (ordAtX f x) (ordAtX g x) ≤ ordAtX (f + g) x

theorem RS.ordAtX_add_of_ne {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) (h : ordAtX f x ≠ ordAtX g x) : ordAtX (f + g) x = min (ordAtX f x) (ordAtX g x)

theorem RS.ordAtX_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {x : X} (hf : MeromorphicAtX f x) (hg : MeromorphicAtX g x) : ordAtX (f * g) x = ordAtX f x + ordAtX g x

theorem RS.ordAtX_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} : ordAtX f⁻¹ x = -ordAtX f x

theorem RS.ordAtX_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} : ordAtX (-f) x = ordAtX f x

theorem RS.ordAtX_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} {c : ℂ} (hc : c ≠ 0) : ordAtX (c • f) x = ordAtX f x

theorem RS.ordAtX_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} {c : ℂ} : ordAtX (fun (x : X) => c) x = if c = 0 then ⊤ else 0

theorem RS.ordAtX_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} : ordAtX 0 x = ⊤

theorem RS.ordAtX_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} : ordAtX 1 x = 0

theorem RS.eventually_ordAtX_eq_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [T1Space X] (h : ordAtX f x = ⊤) : ∀ᶠ (y : X) in nhds x, ordAtX f y = ⊤

No chart invariance needed: S = {x | ordAtX f x = ⊤} is open (the analogue of the identity theorem's "S open" step, specialized to a single point).

Chart invariance

theorem RS.meromorphicAtX_iff_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) : MeromorphicAtX f x ↔ MeromorphicAt (f ∘ ↑e.symm) (↑e x)

Meromorphy at x may be read in ANY maximal-atlas chart whose source contains x.

theorem RS.ordAtX_eq_of_mem_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) : ordAtX f x = meromorphicOrderAt (f ∘ ↑e.symm) (↑e x)

CC3 chart invariance: the order at x may be read in ANY maximal-atlas chart whose source contains x.

theorem RS.ContMDiffAt.meromorphicAtX {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) : MeromorphicAtX f x

theorem RS.ContMDiffAt.ordAtX_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) : 0 ≤ ordAtX f x

theorem RS.eventually_meromorphicAtX {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hf : MeromorphicAtX f x) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, MeromorphicAtX f y

MeromorphicAtX propagates to nearby points (read in the same chart, then converted by chart invariance).

theorem RS.eventually_ordAtX_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (hf : MeromorphicAtX f x) (h : ordAtX f x ≠ ⊤) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, ordAtX f y = 0

ordAtX is eventually 0 away from a point where it is finite (read in the same chart, then converted by chart invariance). Feeds the local finiteness of divisors.

CC4 compatibility

theorem RS.ordAtX_of_contMDiffAt_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) (h0 : f x = 0) : ordAtX f x = ENat.map Nat.cast (multiplicityENat f x)