Maps that are locally the power map w ↦ w ^ e

A map f : X → Y is locally the e-th power map at x (TauCeti.IsLocalPowerAt f x e) if, in some chart φ : X → ℂ centred at x and some chart ψ : Y → ℂ centred at f x, it reads as w ↦ w ^ e. This is the local model of a topological branched covering of surfaces at a point of local degree e: unbranched points are those with e = 1, and a branch point of a branched covering of the sphere has some e > 1 there.

The charts are only homeomorphisms onto open subsets of ℂ, with no compatibility between them, so the exponent cannot be read off as an order of vanishing. It is nevertheless a topological invariant of f at x, because it counts preimages: on every small enough neighbourhood V of x, every point y ≠ f x close enough to f x has exactly e preimages in V (TauCeti.IsLocalPowerAt.exists_ncard_inter_preimage_eq). Two pairs of charts exhibiting f as a power map at x therefore exhibit the same power (TauCeti.IsLocalPowerAt.unique). The same count is what adds up the local degrees over a fibre of a finite branched covering.

Main definitions

• TauCeti.IsLocalPowerAt f x e: f is w ↦ w ^ e near x, in charts centred at x and f x.

Main results

• TauCeti.IsLocalPowerAt.ne_zero: the exponent is positive.
• TauCeti.IsLocalPowerAt.continuousAt: a local power map is continuous at the modelled point.
• TauCeti.IsLocalPowerAt.eventually_ne: x is isolated in its fibre.
• TauCeti.IsLocalPowerAt.exists_ncard_inter_preimage_eq: the exponent counts the preimages near x of the points near f x.
• TauCeti.IsLocalPowerAt.unique: the exponent is determined by f and x.
• TauCeti.IsLocalPowerAt.comp_homeomorph: invariance under a homeomorphism of the source.
• IsLocalHomeomorphOn.isLocalPowerAt_one: a local homeomorphism is locally the first power map wherever the target has a chart.
• TauCeti.isLocalPowerAt_id: the identity is locally the first power map wherever there is a chart.

References

• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, Theorem 2.1 (the local model z ↦ z ^ k) and §4 (its exponent as a local preimage count).

def TauCeti.IsLocalPowerAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (x : X) (e : ℕ) : Prop

The map f is locally the e-th power map at x: there are a chart φ of X centred at x and a chart ψ of Y centred at f x such that f maps the source of φ into the source of ψ and ψ (f (φ.symm w)) = w ^ e for every w in the image of φ. The exponent is positive (TauCeti.IsLocalPowerAt.ne_zero) and unique (TauCeti.IsLocalPowerAt.unique).

theorem TauCeti.isLocalPowerAt_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} : IsLocalPowerAt f x e ↔ ∃ (φ : OpenPartialHomeomorph X ℂ) (ψ : OpenPartialHomeomorph Y ℂ), x ∈ φ.source ∧ Set.MapsTo f φ.source ψ.source ∧ ↑φ x = 0 ∧ ↑ψ (f x) = 0 ∧ ∀ w ∈ φ.target, ↑ψ (f (↑φ.symm w)) = w ^ e

Unfolding TauCeti.IsLocalPowerAt.

theorem TauCeti.IsLocalPowerAt.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} (h : IsLocalPowerAt f x e) : ContinuousAt f x

A map that is locally a power map at x is continuous at x.

theorem TauCeti.IsLocalPowerAt.ne_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} (h : IsLocalPowerAt f x e) : e ≠ 0

The exponent of a local power map is positive: w ↦ w ^ 0 does not vanish at 0.

theorem TauCeti.IsLocalPowerAt.nhdsNE_neBot {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} (h : IsLocalPowerAt f x e) : (nhdsWithin (f x) {f x}ᶜ).NeBot

The value f x is not isolated in the target of a local power map.

theorem TauCeti.IsLocalPowerAt.eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} (h : IsLocalPowerAt f x e) : ∀ᶠ (x' : X) in nhdsWithin x {x}ᶜ, f x' ≠ f x

A point at which f is locally a power map is isolated in its fibre.

theorem TauCeti.IsLocalPowerAt.exists_ncard_inter_preimage_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e : ℕ} (h : IsLocalPowerAt f x e) {N : Set X} (hN : N ∈ nhds x) : ∃ V ⊆ N, IsOpen V ∧ x ∈ V ∧ ∀ᶠ (y : Y) in nhdsWithin (f x) {f x}ᶜ, (V ∩ f ⁻¹' {y}).ncard = e

The exponent counts preimages. If f is locally the e-th power map at x, then inside any neighbourhood N of x there is an open neighbourhood V of x such that every point y ≠ f x close enough to f x has exactly e preimages in V.

theorem TauCeti.IsLocalPowerAt.unique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {e e' : ℕ} (h : IsLocalPowerAt f x e) (h' : IsLocalPowerAt f x e') : e = e'

The exponent of a local power map is unique: two pairs of charts exhibiting f near x as w ↦ w ^ e and as w ↦ w ^ e' have e = e'.

theorem TauCeti.IsLocalPowerAt.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {e : ℕ} {X' : Type u_3} [TopologicalSpace X'] (g : X' ≃ₜ X) {x' : X'} (h : IsLocalPowerAt f (g x') e) : IsLocalPowerAt (f ∘ ⇑g) x' e

Being locally a power map is invariant under a homeomorphism of the source.

theorem IsLocalHomeomorphOn.isLocalPowerAt_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} (hf : IsLocalHomeomorphOn f s) (hx : x ∈ s) {ψ : OpenPartialHomeomorph Y ℂ} (hψ : f x ∈ ψ.source) : TauCeti.IsLocalPowerAt f x 1

A local homeomorphism is locally the first power map at every point of s whose image lies in the source of some chart ψ of the target.

theorem TauCeti.isLocalPowerAt_id {X : Type u_1} [TopologicalSpace X] {x : X} {ψ : OpenPartialHomeomorph X ℂ} (hx : x ∈ ψ.source) : IsLocalPowerAt id x 1

The identity is locally the first power map at every point in the source of some chart.