The power maps of the Riemann sphere

For n ≠ 0, the power map z ↦ z ^ n of ℂ extends to the Riemann sphere OnePoint ℂ by sending ∞ to ∞; this extension is Mathlib's OnePoint.map. In the affine chart it is z ↦ z ^ n, and in the inverted chart at ∞ it is again w ↦ w ^ n, because (w⁻¹ ^ n)⁻¹ = w ^ n. So it is holomorphic, it has local multiplicity n at 0 and at ∞, and local multiplicity 1 everywhere else, where its derivative n z ^ (n - 1) does not vanish.

Its fibre over 0 is the single point 0, so its degree is n, and its only possible branch values are 0 and ∞. Together with the identity (n = 1), these are the simplest finite holomorphic maps of the sphere, and the basic examples of branched covers of the sphere with few branch values: z ↦ z ^ n is the local model of every branched cover near a ramification point of index n.

The power map is the polynomial map of X ^ n, so holomorphy, the local multiplicities away from 0, the degree and the branch values are read off from the general polynomial maps of the sphere, using that 0 is the only critical point of X ^ n when n ≥ 2, while X has no critical points.

Main declarations

• TauCeti.RiemannSurface.mdifferentiable_onePointMap_pow: the extension of z ↦ z ^ n to the Riemann sphere is holomorphic.
• TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_zero, TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_infty, TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_coe_of_ne_zero: its local multiplicities are n at 0 and ∞, and 1 elsewhere.
• TauCeti.RiemannSurface.FiniteHolomorphicMap.spherePow: the power map as a finite holomorphic map of the Riemann sphere.
• TauCeti.RiemannSurface.degree_onePointMap_pow: it has degree n.
• TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues_spherePow_subset: its branch values lie in {0, ∞}.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §1.5 (c) (the charts of the Riemann sphere) and §2 (the local behaviour of holomorphic maps, z ↦ z ^ k).

theorem TauCeti.RiemannSurface.mdifferentiable_onePointMap_pow {n : ℕ} (hn : n ≠ 0) : MDiff (OnePoint.map fun (z : ℂ) => z ^ n)

The power maps of the Riemann sphere are holomorphic. For n ≠ 0, the extension of z ↦ z ^ n to OnePoint ℂ, sending ∞ to ∞, is holomorphic.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_zero {n : ℕ} : localMultiplicity (OnePoint.map fun (z : ℂ) => z ^ n) ↑0 = n

The extension of z ↦ z ^ n to the Riemann sphere has local multiplicity n at 0.

@[simp]

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_infty {n : ℕ} (hn : n ≠ 0) : localMultiplicity (OnePoint.map fun (z : ℂ) => z ^ n) OnePoint.infty = n

The extension of z ↦ z ^ n to the Riemann sphere has local multiplicity n at ∞, where it is w ↦ w ^ n in the inverted chart.

theorem TauCeti.RiemannSurface.localMultiplicity_onePointMap_pow_coe_of_ne_zero {n : ℕ} (hn : n ≠ 0) {z : ℂ} (hz : z ≠ 0) : localMultiplicity (OnePoint.map fun (z : ℂ) => z ^ n) ↑z = 1

Away from 0 and ∞, the extension of z ↦ z ^ n to the Riemann sphere has local multiplicity 1: there the derivative n z ^ (n - 1) does not vanish.

noncomputable def TauCeti.RiemannSurface.FiniteHolomorphicMap.spherePow {n : ℕ} (hn : n ≠ 0) : FiniteHolomorphicMap (OnePoint ℂ) (OnePoint ℂ)

The power map z ↦ z ^ n of the Riemann sphere, for n ≠ 0, sending ∞ to ∞, as a finite holomorphic map: the polynomial map of X ^ n.

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.coe_spherePow {n : ℕ} (hn : n ≠ 0) : ↑(spherePow hn) = OnePoint.map fun (z : ℂ) => z ^ n

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues_spherePow_subset {n : ℕ} (hn : n ≠ 0) : (spherePow hn).branchValues ⊆ {↑0, OnePoint.infty}

The branch values of the power map z ↦ z ^ n of the Riemann sphere lie in {0, ∞}.

@[simp]

theorem TauCeti.RiemannSurface.degree_onePointMap_pow {n : ℕ} (hn : n ≠ 0) : degree (OnePoint.map fun (z : ℂ) => z ^ n) = n

The power map z ↦ z ^ n of the Riemann sphere has degree n, the degree of X ^ n.