The map from a filled cover to the sphere

Extend a finite cover of the thrice-punctured sphere over its filled points by sending each added centre to its puncture. In a filled disc the extension is the power map followed by the inverse standard coordinate on the sphere. This formula proves continuity at the centres; compactness of the filled cover then gives properness. For a nonempty cover the extension is surjective.

Exactly the original cover lies over the unpunctured sphere, and the extension there is the original projection. In particular the fibre of the extension over a point of ℂ ∖ {0, 1} is the fibre of the original cover, the fibre over a puncture q consists of the added points over q, and off the marked points the extension is a covering map. Continuity and density also characterize the extension uniquely.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, §1.2.7, Lemma 1.80.
• O. Forster, Lectures on Riemann Surfaces, Theorem 8.4.

The construction uses PunctureFilling.extend and its final-topology universal property.

noncomputable def TauCeti.FilledCover.fillMap {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : FilledCover p → OnePoint ℂ

The extension of the covering projection to the filled cover, taking each added centre to its puncture in the Riemann sphere.

@[simp]

theorem TauCeti.FilledCover.fillMap_incl {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (x : E) : fillMap p (PunctureFilling.incl (chart p) x) = (p x).toOnePoint

@[simp]

theorem TauCeti.FilledCover.fillMap_center {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (i : FilledPoint p) : fillMap p (PunctureFilling.center (chart p) i) = ((FilledPoint.sigmaEquiv p) i).fst.toOnePoint

@[simp]

theorem TauCeti.FilledCover.preimage_range_toOnePoint {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) : fillMap p ⁻¹' Set.range ThricePuncturedSphere.toOnePoint = Set.range (PunctureFilling.incl (chart p))

The original cover is exactly the part of the filled cover lying over the unpunctured sphere.

theorem TauCeti.FilledCover.fillMap_preimage_puncture {E : Type u_1} [TopologicalSpace E] (p : E → ThricePuncturedSphere) (q : ThricePuncturedSphere.Puncture) : fillMap p ⁻¹' {q.toOnePoint} = Set.range fun (c : ConnectedComponents ↑(p ⁻¹' q.neighborhood)) => PunctureFilling.center (chart p) ((FilledPoint.sigmaEquiv p).symm ⟨q, c⟩)

The fibre of the extended projection over a puncture q consists of the added points, one for each connected component of p ⁻¹' D_q*.

theorem TauCeti.FilledCover.toOnePoint_comp_chart {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) (w : ↑(Metric.ball 0 1 \ {0})) : (p (chart p i w)).toOnePoint = ((FilledPoint.sigmaEquiv p) i).fst.sphereCoordInv (↑w ^ degree p i)

On a punctured filling chart, the projection is the power map followed by the inverse sphere coordinate at the corresponding puncture.

theorem TauCeti.FilledCover.fillMap_disc {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) (w : ↑(Metric.ball 0 1)) : fillMap p (PunctureFilling.disc (chart p) i w) = ((FilledPoint.sigmaEquiv p) i).fst.sphereCoordInv (↑w ^ degree p i)

The extension has the same power-map formula on the whole filled disc, including zero.

theorem TauCeti.FilledCover.continuous_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : Continuous (fillMap p)

The extended covering projection is continuous, including at the filled points.

theorem TauCeti.FilledCover.isProperMap_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : IsProperMap (fillMap p)

Compactness of the filled finite cover makes the extended projection proper.

theorem TauCeti.FilledCover.surjective_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : Function.Surjective p) : Function.Surjective (fillMap p)

The extension of a surjective map hits every point of the sphere.

noncomputable def TauCeti.FilledCover.unpuncturedHomeomorph {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : E ≃ₜ ↑(fillMap p ⁻¹' Set.range ThricePuncturedSphere.toOnePoint)

The unpunctured part of the filled cover is canonically the original covering space.

@[simp]

theorem TauCeti.FilledCover.coe_unpuncturedHomeomorph {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (x : E) : ↑((unpuncturedHomeomorph hp hfin) x) = PunctureFilling.incl (chart p) x

theorem TauCeti.FilledCover.isCoveringMap_restrictPreimage_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : IsCoveringMap ((Set.range ThricePuncturedSphere.toOnePoint).restrictPreimage (fillMap p))

Over the unpunctured sphere, the extension is a covering map: under the canonical identifications of source and target it is the original cover.

theorem TauCeti.FilledCover.fillMap_preimage_toOnePoint {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (z : ThricePuncturedSphere) : fillMap p ⁻¹' {z.toOnePoint} = PunctureFilling.incl (chart p) '' p ⁻¹' {z}

The fibre of the extended projection over a point z of ℂ ∖ {0, 1} is the fibre of p over z: no added point lies over z.

theorem TauCeti.FilledCover.natCard_fillMap_preimage_toOnePoint {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (z : ThricePuncturedSphere) : Nat.card ↑(fillMap p ⁻¹' {z.toOnePoint}) = Nat.card ↑(p ⁻¹' {z})

The fibre of the extended projection over a point z of ℂ ∖ {0, 1} has as many points as the fibre of p over z.

theorem TauCeti.FilledCover.isCoveringMapOn_fillMap {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : IsCoveringMapOn (fillMap p) ThricePuncturedSphere.markedᶜ

Off the marked points, the extended projection is a covering map.

theorem TauCeti.FilledCover.fillMap_unique {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) {f : FilledCover p → OnePoint ℂ} (hf : Continuous f) (hext : ∀ (x : E), f (PunctureFilling.incl (chart p) x) = (p x).toOnePoint) : f = fillMap p

A continuous extension of the projection to the filled cover is unique.