Local multiplicity of a holomorphic map (CC4)

• RS.multiplicityENat F x : ℕ∞ — the vanishing order of inChartAt F x at chartAt ℂ x x. ⊤ iff F is holomorphic and locally constant at x; junk 0 if not holomorphic.
• RS.multiplicity F x : ℕ — toNat of the above; junk 0 for locally-constant or non-holomorphic F. RS.IsRamifiedAt F x means 2 ≤ multiplicity F x.
• Junk API: multiplicityENat_eq_top_of_eventuallyConst, multiplicity_of_eventuallyConst.
• Honest API (guarded by holomorphy/nonconstancy): multiplicityENat_ne_zero, multiplicityENat_eq_top_iff, natCast_multiplicity, one_le_multiplicity.
• RS.analyticOrderAt_charts_eq_multiplicityENat — chart invariance in any maximal-atlas pair.
• Isolated fibres: RS.eventually_ne, RS.exists_nhds_fiber_eq_singleton.
• CC3 compatibility: RS.meromorphicOrderAt_chart_sub, RS.meromorphicOrderAt_chart_of_eq_zero.

noncomputable def RS.multiplicityENat {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : ℕ∞

ℕ∞-valued local multiplicity (CC4). ⊤ iff F is holomorphic and locally constant at x; 0 iff inChartAt F x is not analytic (junk). Honest value: the vanishing order k ≥ 1.

Equations

• RS.multiplicityENat F x = analyticOrderAt (RS.inChartAt F x) (↑(chartAt ℂ x) x)

noncomputable def RS.multiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : ℕ

CC4's multiplicity F x : ℕ: the order when finite; junk 0 when F is locally constant at x (order ⊤) or not holomorphic at x (order junk 0).

Equations

• RS.multiplicity F x = (RS.multiplicityENat F x).toNat

def RS.IsRamifiedAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : Prop

F is ramified at x iff its local multiplicity is at least 2.

Equations

• RS.IsRamifiedAt F x = (2 ≤ RS.multiplicity F x)

theorem RS.multiplicityENat_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : multiplicityENat F x = analyticOrderAt (inChartAt F x) (↑(chartAt ℂ x) x)

theorem RS.multiplicity_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (x : X) : multiplicity F x = (multiplicityENat F x).toNat

@[simp]

theorem RS.multiplicityENat_planar (f : ℂ → ℂ) (z₀ : ℂ) : multiplicityENat f z₀ = analyticOrderAt (fun (x : ℂ) => f x - f z₀) z₀

Planar specialization: on ℂ the charts are refl, so the multiplicity is the recentered vanishing order itself.

theorem RS.multiplicityENat_eq_top_of_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (h : Filter.EventuallyConst F (nhds x)) : multiplicityENat F x = ⊤

@[simp]

theorem RS.multiplicity_of_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (h : Filter.EventuallyConst F (nhds x)) : multiplicity F x = 0

theorem RS.multiplicityENat_ne_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) : multiplicityENat F x ≠ 0

theorem RS.multiplicityENat_eq_top_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) : multiplicityENat F x = ⊤ ↔ Filter.EventuallyConst F (nhds x)

theorem RS.multiplicityENat_ne_top {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : multiplicityENat F x ≠ ⊤

theorem RS.natCast_multiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : ↑(multiplicity F x) = multiplicityENat F x

theorem RS.one_le_multiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : 1 ≤ multiplicity F x

theorem RS.analyticOrderAt_charts_eq_multiplicityENat {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) {e : OpenPartialHomeomorph X ℂ} {e' : OpenPartialHomeomorph Y ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hxe : x ∈ e.source) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hxe' : F x ∈ e'.source) : analyticOrderAt (fun (z : ℂ) => ↑e' (F (↑e.symm z)) - ↑e' (F x)) (↑e x) = multiplicityENat F x

CHART INVARIANCE: the defining order is the same in any admissible chart pair.

theorem RS.eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, F y ≠ F x

Isolated points of the fibre: near x (but off x), F avoids the value F x.

theorem RS.exists_nhds_fiber_eq_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hnc : ¬Filter.EventuallyConst F (nhds x)) : ∃ U ∈ nhds x, ∀ y ∈ U, F y = F x → y = x

The fibre of F x meets a suitable neighborhood of x only in x.

theorem RS.meromorphicOrderAt_chart_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) : meromorphicOrderAt (fun (z : ℂ) => f (↑(chartAt ℂ x).symm z) - f x) (↑(chartAt ℂ x) x) = ENat.map Nat.cast (multiplicityENat f x)

CC3 COMPATIBILITY: our multiplicity vs meromorphicOrderAt in the chart at x (for target ℂ the target chart is refl).

theorem RS.meromorphicOrderAt_chart_of_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) (h0 : f x = 0) : meromorphicOrderAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x) = ENat.map Nat.cast (multiplicityENat f x)

CC3 compatibility for functions vanishing at x: meromorphic-and-divisors reads the LHS as ordAtX f x.