The local multiplicity of a holomorphic map between Riemann surfaces

Let f : X → Y be a map between Riemann surfaces, that is, complex manifolds modelled on ℂ, and let x : X. Reading f in a chart e at x and a chart e' at f x gives the function e' ∘ f ∘ e.symm of one complex variable, and the local multiplicity of f at x is the order of vanishing of e' ∘ f ∘ e.symm - e' (f x) at e x, computed with Mathlib's analyticOrderNatAt. This file defines TauCeti.RiemannSurface.localMultiplicity using the preferred charts chartAt ℂ x and chartAt ℂ (f x), and proves that any two charts of the maximal atlases give the same value when f is holomorphic near x (TauCeti.RiemannSurface.localMultiplicity_eq_analyticOrderNatAt). Chart independence makes the local multiplicity an invariant of the map rather than of the coordinates used to read it, so it may be computed in whichever charts are convenient; every result below is obtained by choosing suitable charts.

For a map holomorphic near x, the local multiplicity vanishes exactly when f is constant near x, and otherwise it is positive; it multiplies under composition; and it equals 1 exactly when f is injective on a neighbourhood of x, so that a holomorphic map is a local biholomorphism precisely at its points of multiplicity one. On the model space ℂ the local multiplicity is the order of vanishing of f - f z at z, and the power map z ↦ z ^ m has local multiplicity m at the origin.

For a map holomorphic and nonconstant near x, the local multiplicity m ≥ 1 is the ramification index of the map at x: near such a point the map is z ↦ z ^ m in suitable coordinates, and the degree of a nonconstant holomorphic map between compact connected Riemann surfaces is the sum of the local multiplicities over any fibre. Neither the local normal form nor the degree is part of this file.

Main declarations

• TauCeti.RiemannSurface.localMultiplicity: the local multiplicity of f : X → Y at x.
• TauCeti.RiemannSurface.localMultiplicity_eq_analyticOrderNatAt: it may be computed in any charts of the maximal atlases at x and f x.
• TauCeti.RiemannSurface.localMultiplicity_eq_zero_iff and TauCeti.RiemannSurface.localMultiplicity_pos_iff: it vanishes exactly at points near which f is constant; in particular a constant map has local multiplicity 0 (TauCeti.RiemannSurface.localMultiplicity_const).
• TauCeti.RiemannSurface.localMultiplicity_comp_of_eventually_mdifferentiableAt: it multiplies under composition.
• TauCeti.RiemannSurface.localMultiplicity_eq_one_iff: it is 1 exactly when f is injective near x.
• TauCeti.RiemannSurface.eventually_localMultiplicity_eq_one: near a point where f is not locally constant, it is 1 at every other point, so ramification points are isolated.
• TauCeti.RiemannSurface.localMultiplicity_pow_zero: the power map z ↦ z ^ m has local multiplicity m at 0.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §2 and §4.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter II §4.

The local multiplicity

noncomputable def TauCeti.RiemannSurface.localMultiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (x : X) : ℕ

The local multiplicity of a map f : X → Y between Riemann surfaces at x: the order of vanishing at chartAt ℂ x x of f read in the charts at x and f x, recentred at f x.

For f holomorphic near x this does not depend on the charts (TauCeti.RiemannSurface.localMultiplicity_eq_analyticOrderNatAt) and vanishes exactly when f is constant near x (TauCeti.RiemannSurface.localMultiplicity_eq_zero_iff). If f is not holomorphic near x, the value is junk, as for analyticOrderNatAt.

Equations

• TauCeti.RiemannSurface.localMultiplicity f x = analyticOrderNatAt (fun (z : ℂ) => ↑(chartAt ℂ (f x)) (f (↑(chartAt ℂ x).symm z)) - ↑(chartAt ℂ (f x)) (f x)) (↑(chartAt ℂ x) x)

theorem TauCeti.RiemannSurface.localMultiplicity_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (x : X) : localMultiplicity f x = analyticOrderNatAt (fun (z : ℂ) => ↑(chartAt ℂ (f x)) (f (↑(chartAt ℂ x).symm z)) - ↑(chartAt ℂ (f x)) (f x)) (↑(chartAt ℂ x) x)

theorem TauCeti.RiemannSurface.localMultiplicity_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} {g : X → Y} (h : f =ᶠ[nhds x] g) : localMultiplicity f x = localMultiplicity g x

Two maps that agree near x have the same local multiplicity at x.

theorem TauCeti.RiemannSurface.localMultiplicity_eq_zero_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)) : localMultiplicity f x = 0

A map that is constant near x has local multiplicity 0 at x.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (y : Y) (x : X) : localMultiplicity (fun (x : X) => y) x = 0

A constant map has local multiplicity 0 everywhere.

theorem TauCeti.RiemannSurface.localMultiplicity_eq_analyticOrderNatAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {e : OpenPartialHomeomorph X ℂ} {e' : OpenPartialHomeomorph Y ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 Y) (hx : x ∈ e.source) (hfx : f x ∈ e'.source) (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : localMultiplicity f x = analyticOrderNatAt (fun (z : ℂ) => ↑e' (f (↑e.symm z)) - ↑e' (f x)) (↑e x)

Chart independence of the local multiplicity. For a map holomorphic near x, the local multiplicity is the order of vanishing of the recentred chart representative of f in any charts of the maximal atlases at x and f x.

Vanishing and positivity

theorem TauCeti.RiemannSurface.localMultiplicity_eq_zero_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : localMultiplicity f x = 0 ↔ Filter.EventuallyConst f (nhds x)

For a map holomorphic near x, the local multiplicity at x vanishes exactly when the map is constant near x.

theorem TauCeti.RiemannSurface.localMultiplicity_pos_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : 0 < localMultiplicity f x ↔ ¬Filter.EventuallyConst f (nhds x)

For a map holomorphic near x, the local multiplicity at x is positive exactly when the map is not constant near x.

theorem TauCeti.RiemannSurface.natCast_localMultiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) (hne : ¬Filter.EventuallyConst f (nhds x)) : ↑(localMultiplicity f x) = analyticOrderAt (fun (z : ℂ) => ↑(chartAt ℂ (f x)) (f (↑(chartAt ℂ x).symm z)) - ↑(chartAt ℂ (f x)) (f x)) (↑(chartAt ℂ x) x)

For a map holomorphic and nonconstant near x, the local multiplicity is the order of vanishing, in ℕ∞, of the recentred chart representative in the charts at x and f x.

Composition

theorem TauCeti.RiemannSurface.localMultiplicity_comp_of_eventually_mdifferentiableAt {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] {g : Y → Z} (hg : ∀ᶠ (y : Y) in nhds (f x), MDiffAt g y) (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : localMultiplicity (g ∘ f) x = localMultiplicity g (f x) * localMultiplicity f x

Multiplicativity of the local multiplicity. The local multiplicity of a composition of maps holomorphic near the relevant points is the product of the local multiplicities.

Multiplicity one

theorem TauCeti.RiemannSurface.localMultiplicity_eq_one_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : localMultiplicity f x = 1 ↔ ∃ U ∈ nhds x, Set.InjOn f U

Multiplicity one means local injectivity. A map holomorphic near x has local multiplicity 1 at x exactly when it is injective on a neighbourhood of x; by the inverse function theorem, these are the points at which it is a local biholomorphism.

theorem TauCeti.RiemannSurface.eventually_localMultiplicity_eq_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) (hne : ¬Filter.EventuallyConst f (nhds x)) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, localMultiplicity f y = 1

Ramification points are isolated. A map holomorphic and not constant near x has local multiplicity 1 at every point of a punctured neighbourhood of x.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (x : X) : localMultiplicity id x = 1

The identity has local multiplicity 1 everywhere.

theorem TauCeti.RiemannSurface.localMultiplicity_eq_one_of_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (hx : x ∈ e.source) : localMultiplicity (↑e) x = 1

A chart of the maximal atlas has local multiplicity 1 at every point of its domain.

The model space

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_eq_analyticOrderNatAt_sub (f : ℂ → ℂ) (z : ℂ) : localMultiplicity f z = analyticOrderNatAt (fun (w : ℂ) => f w - f z) z

On the model space ℂ, the local multiplicity of f at z is the order of vanishing of f - f z at z.

theorem TauCeti.RiemannSurface.localMultiplicity_pow_zero (m : ℕ) : localMultiplicity (fun (z : ℂ) => z ^ m) 0 = m

The power map z ↦ z ^ m has local multiplicity m at the origin.

theorem TauCeti.RiemannSurface.localMultiplicity_eq_of_coordinate_eventuallyEq_pow_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {e : OpenPartialHomeomorph X ℂ} {e' : OpenPartialHomeomorph Y ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 Y) (hx : x ∈ e.source) (hfx : f x ∈ e'.source) (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) {m : ℕ} (hm : 0 < m) (hex : ↑e x = 0) (hefx : ↑e' (f x) = 0) (hpow : (fun (z : ℂ) => ↑e' (f (↑e.symm z))) =ᶠ[nhds 0] fun (z : ℂ) => z ^ m) : localMultiplicity f x = m

If a holomorphic map has coordinate expression z ↦ z ^ m in charts that send the source point and its image to zero, then its local multiplicity is m.