The finite connected covers of the punctured disc

Let 𝔻* = ball 0 1 \ {0} be the punctured unit disc in ℂ. For e ≠ 0 the power map z ↦ z ^ e sends 𝔻* onto itself, and it is a covering map with e sheets: the fibre over w is the set of e-th roots of w. This is the local model of a branched cover near a point of ramification index e.

Conversely, every connected cover of 𝔻* with e ≠ 0 sheets is isomorphic over 𝔻* to this model. The fundamental group of 𝔻* is infinite cyclic, so a connected cover of 𝔻* is determined up to isomorphism by its number of sheets (IsCoveringMap.exists_homeomorph_comp_eq_of_card_fiber_eq). The isomorphism can moreover be chosen to carry any given point over w to any given e-th root of w; it is therefore not unique, but only unique up to the rotations of 𝔻* by e-th roots of unity.

Main declarations

• TauCeti.pow_mem_ball_zero_one_diff_singleton_iff: for e ≠ 0, z ^ e lies in the punctured unit ball exactly when z does.
• TauCeti.puncturedDiscPow: the map z ↦ z ^ e from 𝔻* to itself, for e ≠ 0.
• TauCeti.puncturedDiscPow_mul: the power maps compose, z ^ (e * f) = (z ^ f) ^ e.
• TauCeti.isCoveringMap_puncturedDiscPow: it is a covering map.
• TauCeti.isQuotientCoveringMap_puncturedDiscPow: it is the quotient covering by the rotations through the e-th roots of unity.
• TauCeti.card_puncturedDiscPow_preimage_singleton: each of its fibres has e points.
• TauCeti.puncturedDiscCircle: the canonical counterclockwise generator based at 1/2.
• TauCeti.isCycleOn_monodromyPerm_puncturedDiscCircle: monodromy of the power map around this generator is one cycle on its e-element fibre.
• TauCeti.puncturedDiscPowDeckMulEquiv: its deck group is the group of e-th roots of unity, acting by rotations.
• IsCoveringMap.exists_homeomorph_puncturedDiscPow_comp_eq: a connected cover of 𝔻* with e ≠ 0 sheets is isomorphic over 𝔻* to z ↦ z ^ e, by an isomorphism matching any given points of the two fibres over a point.
• IsCoveringMap.exists_homeomorph_puncturedDiscPow_comp_eq_iff: a connected cover of 𝔻* is isomorphic over 𝔻* to z ↦ z ^ e exactly when it has e sheets.
• IsCoveringMap.exists_homeomorph_connectedComponent_puncturedDiscPow_comp_eq_iff: for a cover of 𝔻* with finite fibres that need not be connected, the same holds for the restriction to each connected component, with e the number of points of the component over a point.
• TauCeti.existsUnique_rootsOfUnity_smul_homeomorph: any two such isomorphisms differ by rotation through a unique e-th root of unity.
• IsCoveringMap.existsUnique_homeomorph_puncturedDiscPow_comp_eq: prescribing the image of one point makes the isomorphism with the power-map model unique.

References

• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §5, Theorem 5.10 (a finite cover of the punctured disc with k sheets is z ↦ z ^ k).
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (the classification of covering spaces).

noncomputable def TauCeti.puncturedDiscBasepoint : ↑(Metric.ball 0 1 \ {0})

The basepoint 1/2 in the punctured unit disc.

@[simp]

theorem TauCeti.coe_puncturedDiscBasepoint : ↑puncturedDiscBasepoint = 1 / 2

The punctured-disc basepoint is the positive real point 1/2.

noncomputable def TauCeti.puncturedDiscCircle : Path puncturedDiscBasepoint puncturedDiscBasepoint

The counterclockwise circle of radius 1/2 about zero, regarded as a loop in the punctured unit disc based at puncturedDiscBasepoint.

@[simp]

theorem TauCeti.coe_puncturedDiscCircle_apply (t : ↑unitInterval) : ↑(puncturedDiscCircle t) = circleMap 0 (1 / 2) (2 * Real.pi * ↑t)

The punctured-disc circle is the usual positive parametrization t ↦ (1/2) * exp (2πit).

theorem TauCeti.zpowers_puncturedDiscCircle_eq_top : Subgroup.zpowers (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk puncturedDiscCircle)) = ⊤

The counterclockwise circle generates the fundamental group of the punctured disc.

@[instance_reducible]

noncomputable instance TauCeti.puncturedDiscSMul {e : ℕ} [NeZero e] : SMul ↥(rootsOfUnity e ℂ) ↑(Metric.ball 0 1 \ {0})

The scalar action of the e-th roots of unity on the punctured disc is rotation.

@[instance_reducible]

noncomputable instance TauCeti.puncturedDiscMulAction {e : ℕ} [NeZero e] : MulAction ↥(rootsOfUnity e ℂ) ↑(Metric.ball 0 1 \ {0})

The action of the e-th roots of unity on the punctured disc is rotation.

@[simp]

theorem TauCeti.coe_rootsOfUnity_smul_puncturedDisc {e : ℕ} [NeZero e] (ζ : ↥(rootsOfUnity e ℂ)) (z : ↑(Metric.ball 0 1 \ {0})) : ↑(ζ • z) = ζ • ↑z

instance TauCeti.puncturedDiscContinuousConstSMul {e : ℕ} [NeZero e] : ContinuousConstSMul ↥(rootsOfUnity e ℂ) ↑(Metric.ball 0 1 \ {0})

Rotation by a root of unity is continuous on the punctured disc.

instance TauCeti.puncturedDiscIsCancelSMul {e : ℕ} [NeZero e] : IsCancelSMul ↥(rootsOfUnity e ℂ) ↑(Metric.ball 0 1 \ {0})

Rotation by a root of unity acts cancellatively on the punctured disc.

theorem TauCeti.pow_mem_ball_zero_one_diff_singleton_iff {e : ℕ} {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (he : e ≠ 0) {z : 𝕜} : z ^ e ∈ Metric.ball 0 1 \ {0} ↔ z ∈ Metric.ball 0 1 \ {0}

For e ≠ 0, z ^ e lies in the punctured unit ball exactly when z does.

def TauCeti.puncturedDiscPow {e : ℕ} (he : e ≠ 0) : C(↑(Metric.ball 0 1 \ {0}), ↑(Metric.ball 0 1 \ {0}))

The power map z ↦ z ^ e from the punctured unit disc ball 0 1 \ {0} to itself, for e ≠ 0.

@[simp]

theorem TauCeti.coe_puncturedDiscPow_apply {e : ℕ} (he : e ≠ 0) (z : ↑(Metric.ball 0 1 \ {0})) : ↑((puncturedDiscPow he) z) = ↑z ^ e

@[simp]

theorem TauCeti.puncturedDiscPow_one : puncturedDiscPow ⋯ = ContinuousMap.id ↑(Metric.ball 0 1 \ {0})

The first power map of the punctured disc is the identity.

theorem TauCeti.puncturedDiscPow_mul {e f : ℕ} (he : e ≠ 0) (hf : f ≠ 0) : puncturedDiscPow ⋯ = (puncturedDiscPow he).comp (puncturedDiscPow hf)

The power maps of the punctured disc compose: z ↦ z ^ (e * f) is z ↦ z ^ e after z ↦ z ^ f.

theorem TauCeti.isCoveringMap_puncturedDiscPow {e : ℕ} (he : e ≠ 0) : IsCoveringMap ⇑(puncturedDiscPow he)

The power map of the punctured disc is a covering map. It is the restriction of the covering map z ↦ z ^ e of ℂ \ {0} to the preimage of the punctured disc, which is the punctured disc itself.

theorem TauCeti.isCycleOn_monodromyPerm_puncturedDiscCircle {e : ℕ} (he : e ≠ 0) : ((⋯.monodromyPerm puncturedDiscBasepoint) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk puncturedDiscCircle))).IsCycleOn Set.univ

Monodromy of the power map around the puncture is one cycle. For the positive generator puncturedDiscCircle of the fundamental group, monodromy acts transitively by the powers of a single permutation on the entire fibre over puncturedDiscBasepoint.

theorem TauCeti.isQuotientCoveringMap_puncturedDiscPow {e : ℕ} [NeZero e] : IsQuotientCoveringMap ⇑(puncturedDiscPow ⋯) ↥(rootsOfUnity e ℂ)

The power map is the quotient covering by rotations through the e-th roots of unity. Its fibres are exactly the rotation orbits.

noncomputable def TauCeti.puncturedDiscPowDeckMulEquiv {e : ℕ} (he : e ≠ 0) : ↥(rootsOfUnity e ℂ) ≃* ↥(deck ⇑(puncturedDiscPow he))

The deck group of the punctured-disc power map is the group of e-th roots of unity. Under this isomorphism a root of unity acts by rotation (puncturedDiscPowDeckMulEquiv_apply).

@[simp]

theorem TauCeti.puncturedDiscPowDeckMulEquiv_apply {e : ℕ} (he : e ≠ 0) (ζ : ↥(rootsOfUnity e ℂ)) (z : ↑(Metric.ball 0 1 \ {0})) : ↑(↑((puncturedDiscPowDeckMulEquiv he) ζ) z) = ζ • ↑z

A root of unity acts through puncturedDiscPowDeckMulEquiv by multiplying points of the punctured disc.

@[simp]

theorem TauCeti.puncturedDiscPowDeckMulEquiv_symm_apply {e : ℕ} (he : e ≠ 0) (φ : ↥(deck ⇑(puncturedDiscPow he))) (z : ↑(Metric.ball 0 1 \ {0})) : ↑↑((puncturedDiscPowDeckMulEquiv he).symm φ) * ↑z = ↑(↑φ z)

Every deck transformation of the punctured-disc power map is rotation by the corresponding root of unity under puncturedDiscPowDeckMulEquiv.

theorem TauCeti.card_deck_puncturedDiscPow {e : ℕ} (he : e ≠ 0) : Nat.card ↥(deck ⇑(puncturedDiscPow he)) = e

The deck group of z ↦ z ^ e has order e.

theorem TauCeti.card_puncturedDiscPow_preimage_singleton {e : ℕ} (he : e ≠ 0) (w : ↑(Metric.ball 0 1 \ {0})) : Nat.card ↑(⇑(puncturedDiscPow he) ⁻¹' {w}) = e

The power map of the punctured disc has e sheets: the fibre over any point w consists of the e distinct e-th roots of w.

theorem IsCoveringMap.exists_homeomorph_puncturedDiscPow_comp_eq {e : ℕ} {E : Type u_1} [TopologicalSpace E] [ConnectedSpace E] {p : E → ↑(Metric.ball 0 1 \ {0})} (hp : IsCoveringMap p) (he : e ≠ 0) {w : ↑(Metric.ball 0 1 \ {0})} (hcard : Nat.card ↑(p ⁻¹' {w}) = e) (y₀ : ↑(p ⁻¹' {w})) (z₀ : ↑(⇑(TauCeti.puncturedDiscPow he) ⁻¹' {w})) : ∃ (h : E ≃ₜ ↑(Metric.ball 0 1 \ {0})), h ↑y₀ = ↑z₀ ∧ ⇑(TauCeti.puncturedDiscPow he) ∘ ⇑h = p

Every finite connected cover of the punctured disc is a power map. Let p : E → 𝔻* be a covering map from a connected space whose fibre over w has e ≠ 0 points. Then p is isomorphic over 𝔻* to z ↦ z ^ e, by a homeomorphism E ≃ₜ 𝔻* carrying any given point y₀ over w to any given e-th root z₀ of w.

theorem IsCoveringMap.exists_homeomorph_puncturedDiscPow_comp_eq_iff {e : ℕ} {E : Type u_1} [TopologicalSpace E] [ConnectedSpace E] {p : E → ↑(Metric.ball 0 1 \ {0})} (hp : IsCoveringMap p) (he : e ≠ 0) (w : ↑(Metric.ball 0 1 \ {0})) : (∃ (h : E ≃ₜ ↑(Metric.ball 0 1 \ {0})), ⇑(TauCeti.puncturedDiscPow he) ∘ ⇑h = p) ↔ Nat.card ↑(p ⁻¹' {w}) = e

The finite connected covers of the punctured disc are classified by their degree. A covering map p : E → 𝔻* from a connected space is isomorphic over 𝔻* to z ↦ z ^ e, for e ≠ 0, exactly when its fibre over some (equivalently, every) point w has e points.

theorem IsCoveringMap.exists_homeomorph_connectedComponent_puncturedDiscPow_comp_eq_iff {e : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → ↑(Metric.ball 0 1 \ {0})} (hp : IsCoveringMap p) (hfin : ∀ (w : ↑(Metric.ball 0 1 \ {0})), (p ⁻¹' {w}).Finite) (x : E) (he : e ≠ 0) (w : ↑(Metric.ball 0 1 \ {0})) : (∃ (h : ↑(connectedComponent x) ≃ₜ ↑(Metric.ball 0 1 \ {0})), ⇑(TauCeti.puncturedDiscPow he) ∘ ⇑h = (connectedComponent x).domRestrict p) ↔ {y : E | y ∈ connectedComponent x ∧ p y = w}.ncard = e

Each component of a finite cover of the punctured disc is a power map. Let p : E → 𝔻* be a covering map with finite fibres, with E not necessarily connected. The restriction of p to the connected component of x is isomorphic over 𝔻* to z ↦ z ^ e, for e ≠ 0, exactly when that component has e points over some (equivalently, every) point w.

theorem TauCeti.existsUnique_rootsOfUnity_smul_homeomorph {e : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → ↑(Metric.ball 0 1 \ {0})} (he : e ≠ 0) (h k : E ≃ₜ ↑(Metric.ball 0 1 \ {0})) (hh : ⇑(puncturedDiscPow he) ∘ ⇑h = p) (hk : ⇑(puncturedDiscPow he) ∘ ⇑k = p) : ∃! ζ : ↥(rootsOfUnity e ℂ), ∀ (y : E), ↑(k y) = ↑↑ζ * ↑(h y)

Two identifications of a cover with the punctured-disc power map differ by a unique rotation. More precisely, if h and k are homeomorphisms from the same space to the punctured disc and both identify a map p with z ↦ z ^ e, then there is a unique e-th root of unity ζ such that, after coercion to ℂ, k y = ζ · h y for every y.

No covering or connectedness hypothesis is needed: the difference k ∘ h⁻¹ is a deck transformation of the power map, whose deck group is the group of e-th roots of unity.

theorem IsCoveringMap.existsUnique_homeomorph_puncturedDiscPow_comp_eq {e : ℕ} {E : Type u_1} [TopologicalSpace E] [ConnectedSpace E] {p : E → ↑(Metric.ball 0 1 \ {0})} (hp : IsCoveringMap p) (he : e ≠ 0) {w : ↑(Metric.ball 0 1 \ {0})} (hcard : Nat.card ↑(p ⁻¹' {w}) = e) (y₀ : ↑(p ⁻¹' {w})) (z₀ : ↑(⇑(TauCeti.puncturedDiscPow he) ⁻¹' {w})) : ∃! h : E ≃ₜ ↑(Metric.ball 0 1 \ {0}), h ↑y₀ = ↑z₀ ∧ ⇑(TauCeti.puncturedDiscPow he) ∘ ⇑h = p

A point-rigidified finite connected cover of the punctured disc has a unique power-map model. Given points y₀ and z₀ in corresponding fibres, there is exactly one homeomorphism over the punctured disc carrying y₀ to z₀. Without the point condition, the homeomorphism is unique only up to the rotations described by existsUnique_rootsOfUnity_smul_homeomorph.