The quotient of a disc by a finite rotation group

The group rootsOfUnity m ℂ of the m-th roots of unity acts on ℂ by rotations. This file proves that u ↦ u ^ m is the orbit map of that action, topologically: for every invariant set s ⊆ ℂ, the orbit space of s is homeomorphic to the image of s under u ↦ u ^ m. For the open disc of radius r about 0 the image is the disc of radius r ^ m, so the quotient of a disc by a cyclic rotation group of order m is again a disc, with coordinate u ^ m.

This is the local model of a quotient Riemann surface at a point whose stabilizer is cyclic of order m: in a coordinate centred at the fixed point in which a generator acts by a primitive m-th root of unity, the orbit space near the point is a disc, and the quotient map is u ↦ u ^ m. For m ≥ 2, the only point of the disc with a nontrivial stabilizer is its centre (TauCeti.freeLocus_rootsOfUnity); on the complementary free locus the orbit projection is a covering map by TauCeti.isCoveringMap_quotientMk_freeLocus, and u ↦ u ^ m itself is a covering map of the punctured plane with nonvanishing derivative (Mathlib's isCoveringMapOn_npow). At the centre, u ↦ u ^ m vanishes to order exactly m (Mathlib's analyticOrderAt_centeredMonomial).

The homeomorphism is built from Mathlib's theorem that u ↦ u ^ m is an open quotient map of ℂ (Complex.isOpenQuotientMap_pow, a consequence of the open mapping theorem), restricted to the saturated set s, together with the identification of its fibres with the orbits of the roots of unity (TauCeti.orbitRel_rootsOfUnity_apply). Both steps are Mathlib's generic quotient API: Homeomorph.Quotient.congrRight replaces the orbit relation by the fibre relation, and Topology.IsQuotientMap.homeomorph identifies the quotient by the fibres of the restricted power map with its image.

Main declarations

• SubMulAction.rootsOfUnityQuotientHomeomorph: the orbit space of an invariant set s is homeomorphic to (· ^ m) '' s, sending the class of u to u ^ m.
• TauCeti.rootsOfUnityBall: the open disc of radius r about 0, as an invariant set.
• TauCeti.image_pow_ball: u ↦ u ^ m maps the disc of radius r onto the disc of radius r ^ m.
• TauCeti.rootsOfUnityBallQuotientHomeomorph: the orbit space of the disc of radius r is homeomorphic to the disc of radius r ^ m.
• TauCeti.freeLocus_rootsOfUnity: for m ≥ 2, the action is free exactly off 0.

References

• Hershel M. Farkas and Irwin Kra, Riemann Surfaces, second edition, Chapter I §4.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Chapter III §3.

noncomputable def SubMulAction.rootsOfUnityQuotientHomeomorph {m : ℕ} [NeZero m] (s : SubMulAction ↥(rootsOfUnity m ℂ) ℂ) : MulAction.orbitRel.Quotient ↥(rootsOfUnity m ℂ) ↥s ≃ₜ ↑((fun (x : ℂ) => x ^ m) '' ↑s)

The orbit space of a set s ⊆ ℂ invariant under the m-th roots of unity is homeomorphic to the image of s under u ↦ u ^ m, by sending the orbit of u to u ^ m.

Equations

• s.rootsOfUnityQuotientHomeomorph = (Homeomorph.Quotient.congrRight ⋯).trans ⋯.homeomorph

@[simp]

theorem SubMulAction.coe_rootsOfUnityQuotientHomeomorph_mk {m : ℕ} [NeZero m] (s : SubMulAction ↥(rootsOfUnity m ℂ) ℂ) (u : ↥s) : ↑(s.rootsOfUnityQuotientHomeomorph ⟦u⟧) = ↑u ^ m

theorem TauCeti.eventually_rootsOfUnity_invariant_nhds_of_nhdsNE {m : ℕ} {E : Type u_1} {f : ℂ → E} (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : ∀ᶠ (u : ℂ) in nhds 0, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u

Invariance under the m-th roots of unity on a punctured neighbourhood of 0 extends to a neighbourhood of 0, since every rotation fixes 0.

def TauCeti.rootsOfUnityBall (m : ℕ) [NeZero m] (r : ℝ) : SubMulAction ↥(rootsOfUnity m ℂ) ℂ

The open disc of radius r about 0, as a set invariant under the m-th roots of unity.

Equations

• TauCeti.rootsOfUnityBall m r = { carrier := Metric.ball 0 r, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.coe_rootsOfUnityBall {m : ℕ} [NeZero m] (r : ℝ) : ↑(rootsOfUnityBall m r) = Metric.ball 0 r

@[simp]

theorem TauCeti.mem_rootsOfUnityBall {m : ℕ} [NeZero m] {r : ℝ} {u : ℂ} : u ∈ rootsOfUnityBall m r ↔ ‖u‖ < r

theorem TauCeti.image_pow_ball {m : ℕ} [NeZero m] {r : ℝ} (hr : 0 ≤ r) : (fun (x : ℂ) => x ^ m) '' Metric.ball 0 r = Metric.ball 0 (r ^ m)

For 0 ≤ r, the map u ↦ u ^ m sends the disc of radius r about 0 onto the disc of radius r ^ m.

noncomputable def TauCeti.rootsOfUnityBallQuotientHomeomorph {m : ℕ} [NeZero m] {r : ℝ} (hr : 0 ≤ r) : MulAction.orbitRel.Quotient ↥(rootsOfUnity m ℂ) ↥(rootsOfUnityBall m r) ≃ₜ ↑(Metric.ball 0 (r ^ m))

For 0 ≤ r, the orbit space of the disc of radius r about 0 under the m-th roots of unity is homeomorphic to the disc of radius r ^ m, by sending the orbit of u to u ^ m.

Equations

• TauCeti.rootsOfUnityBallQuotientHomeomorph hr = (TauCeti.rootsOfUnityBall m r).rootsOfUnityQuotientHomeomorph.trans (Homeomorph.setCongr ⋯)

@[simp]

theorem TauCeti.coe_rootsOfUnityBallQuotientHomeomorph_mk {m : ℕ} [NeZero m] {r : ℝ} (hr : 0 ≤ r) (u : ↥(rootsOfUnityBall m r)) : ↑((rootsOfUnityBallQuotientHomeomorph hr) ⟦u⟧) = ↑u ^ m

theorem TauCeti.freeLocus_rootsOfUnity {m : ℕ} (hm : 1 < m) : ↑(freeLocus ↥(rootsOfUnity m ℂ) ℂ) = {0}ᶜ

For m ≥ 2, the m-th roots of unity act freely exactly on the nonzero complex numbers: the centre 0 is the only point with a nontrivial stabilizer.