Local power coordinates for holomorphic maps of Riemann surfaces

A map holomorphic and nonconstant near a point has the local expression u ↦ u ^ m, where m is its local multiplicity. Given any target chart at the image, we construct a source chart in the maximal holomorphic atlas, centered at the source point. Subtracting the coordinate of the image centers the target chart. The power identity holds on the entire source chart domain, and that domain maps into the given target chart. It can be chosen inside any prescribed neighbourhood of the source point.

This supplies actual biholomorphic coordinates at ramification points, rather than just a count of nearby fibres. They are the local models used to remove and replace branch discs in the branched-cover Euler-characteristic argument. The theorem TauCeti.RiemannSurface.isLocalPowerAt_localMultiplicity packages the same coordinates in the topological TauCeti.IsLocalPowerAt vocabulary used by branched covers. In particular, on a connected Riemann surface every fibre of a nonconstant holomorphic map is discrete (TauCeti.RiemannSurface.eventually_apply_ne_of_ne_const).

References

• Otto Forster, Lectures on Riemann Surfaces, §2, the local normal form theorem.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Chapter II, §4.

theorem TauCeti.RiemannSurface.exists_chart_eq_pow_localMultiplicity {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {f : X → Y} {x : X} (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) (hne : ¬Filter.EventuallyConst f (nhds x)) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 Y) (hfx : f x ∈ e'.source) {W : Set X} (hW : W ∈ nhds x) : ∃ e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X, x ∈ e.source ∧ ↑e x = 0 ∧ e.source ⊆ W ∧ ∀ y ∈ e.source, f y ∈ e'.source ∧ ↑e' (f y) - ↑e' (f x) = ↑e y ^ localMultiplicity f x

The local power-map normal form. For any target chart at the image of a point where a holomorphic map is not locally constant, there is a centered source chart in which the map is the power with exponent its local multiplicity. The identity holds on the whole source chart and its image lies in the target chart domain. The source chart can be chosen inside any prescribed neighbourhood.

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

A holomorphic map that is nonconstant near x is locally the power map whose exponent is its local multiplicity. This is the topological local-power formulation of exists_chart_eq_pow_localMultiplicity.

theorem TauCeti.RiemannSurface.eventually_apply_ne_of_ne_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {f : X → Y} [PreconnectedSpace X] (hf : MDiff f) {y₀ : Y} (h : f ≠ fun (x : X) => y₀) (x : X) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, f y ≠ y₀

Discreteness of the fibres. On a connected Riemann surface, a holomorphic map other than the constant map with value y₀ takes the value y₀ at no point of a punctured neighbourhood of any point.