The complex charts of the filled cover

Let p : E → ℂ ∖ {0, 1} be a covering map with finite fibres. Its filled cover TauCeti.FilledCover p adds to E one point for each component of p ⁻¹' D_q* over each puncture q ∈ {0, 1, ∞}. This file makes it a space charted over ℂ, and shows that the charts are holomorphically compatible, so that the filled cover is a one-dimensional complex manifold. Together with TauCeti.FilledCover.t2Space and TauCeti.FilledCover.compactSpace it is a compact Riemann surface, connected when E is (TauCeti.PunctureFilling.connectedSpace).

The charts (TauCeti.FilledCover.chartedSpace) are those of the puncture filling TauCeti.PunctureFilling.chartedSpace:

• at a point x of E, the chart is p itself, read in ℂ, near x (TauCeti.FilledCover.chartAt_incl_apply_incl); these are the charts of ℂ pulled back along the local homeomorphism E → ℂ;
• at the added point of a component i over q, the chart is the inverse of the filled disc of the filling chart TauCeti.FilledCover.chart p i, sending that point to 0.

These charts are holomorphically compatible (TauCeti.FilledCover.isManifold). The only transitions to check are between a filling chart and the charts of E, away from the added points: along the filling chart of i, the cover p is w ↦ w ^ e followed by the inverse of the standard coordinate of D_q* (w ↦ w / 2, w ↦ 1 - w / 2 or w ↦ 2 / w), which is holomorphic. A homeomorphism with holomorphic inverse is a holomorphic chart (OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn_symm).

Main declarations

• TauCeti.FilledCover.chartedSpace: the charts of the filled cover.
• TauCeti.FilledCover.chartAt_incl_apply_incl: the chart at a point of E reads every point of E as its image under p.
• TauCeti.FilledCover.chartAt_incl_source, TauCeti.FilledCover.chartAt_incl_target, TauCeti.FilledCover.chartAt_incl_symm_apply: the inverse of the chart at a point x of E is the local inverse of p at x.
• TauCeti.FilledCover.chartAt_center_source, TauCeti.FilledCover.chartAt_center_apply_disc, TauCeti.FilledCover.chartAt_center_symm_apply: the chart at an added point is the inverse of the filled disc of its component.
• TauCeti.FilledCover.isManifold: the filled cover is a complex manifold.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press, 2012, §1.2.7 (the charts added at the filled points are declared holomorphic, and the transition functions are checked).
• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §8, Theorem 8.4.

@[irreducible]

noncomputable def TauCeti.FilledCover.chartedSpace {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : ChartedSpace ℂ (FilledCover p)

The charts of the filled cover. The filled cover of a covering map p : E → ℂ ∖ {0, 1} with finite fibres is charted over ℂ as a puncture filling: E carries the charts of ℂ pulled back along p, and the added point of each component i the inverse of the filled disc of its filling chart FilledCover.chart p i.

It is irreducible, so that its characteristic chart lemmas below (chartAt_incl_*, chartAt_center_*) can be simp lemmas: otherwise simp would unfold it and prove them from the generic PunctureFilling ones.

@[simp]

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

The chart of the filled cover at a point x of E reads every point y of E as its image p y in ℂ.

@[simp]

theorem TauCeti.FilledCover.chartAt_incl_source {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (x : E) : (chartAt ℂ (PunctureFilling.incl (chart p) x)).source = PunctureFilling.incl (chart p) '' (⋯.localInverseAt x).target

The chart of the filled cover at a point x of E is defined on the image in the filled cover of the neighbourhood of x on which p is inverted by its local inverse at x.

@[simp]

theorem TauCeti.FilledCover.chartAt_incl_target {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (x : E) : (chartAt ℂ (PunctureFilling.incl (chart p) x)).target = (⋯.localInverseAt x).source

The chart of the filled cover at a point x of E takes values in the domain of the local inverse of p at x.

@[simp]

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

The inverse of the chart of the filled cover at a point x of E is the local inverse of p at x, followed by the inclusion of E.

@[simp]

theorem TauCeti.FilledCover.chartAt_center_source {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) : (chartAt ℂ (PunctureFilling.center (chart p) i)).source = Set.range (PunctureFilling.disc (chart p) i)

The chart of the filled cover at the added point of the component i is defined on the filled disc of i.

@[simp]

theorem TauCeti.FilledCover.chartAt_center_target {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) : (chartAt ℂ (PunctureFilling.center (chart p) i)).target = Metric.ball 0 1

The chart of the filled cover at the added point of a component takes values in the unit disc.

@[simp]

theorem TauCeti.FilledCover.chartAt_center_apply_disc {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) (z : ↑(Metric.ball 0 1)) : ↑(chartAt ℂ (PunctureFilling.center (chart p) i)) (PunctureFilling.disc (chart p) i z) = ↑z

The chart of the filled cover at the added point of the component i reads the point disc (chart p) i z of the filled disc of i as z.

@[simp]

theorem TauCeti.FilledCover.chartAt_center_apply_center {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) : ↑(chartAt ℂ (PunctureFilling.center (chart p) i)) (PunctureFilling.center (chart p) i) = 0

The chart of the filled cover at the added point of a component sends that point to 0.

@[simp]

theorem TauCeti.FilledCover.chartAt_center_symm_apply {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) (z : ↑(Metric.ball 0 1)) : ↑(chartAt ℂ (PunctureFilling.center (chart p) i)).symm ↑z = PunctureFilling.disc (chart p) i z

The inverse of the chart of the filled cover at the added point of the component i is the filled disc of i.

theorem TauCeti.FilledCover.isManifold {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) {n : WithTop ℕ∞} : IsManifold (modelWithCornersSelf ℂ ℂ) n (FilledCover p)

The filled cover is a complex manifold. The charts of the filled cover of a covering map p : E → ℂ ∖ {0, 1} with finite fibres are holomorphically compatible.