Transporting filled covers along isomorphisms of covers

Let h : E ≃ₜ F be an isomorphism of covers of ℂ ∖ {0, 1}, a homeomorphism with p' ∘ h = p. It transports the added points of the filled cover of p to those of p' by its bijection FilledPoint.congr h hh on the components over the three punctures, preserving the local degree at each added point (TauCeti.FilledCover.degree_congr). The local-degree comparison needs neither finiteness nor the covering property.

When p is a covering map with finite fibres, h extends to a homeomorphism of filled covers TauCeti.FilledCover.congr, which is h on E and is the transport of added points on the added points, and which commutes with the extended projections to the Riemann sphere (TauCeti.FilledCover.fillMap_congr_apply). The extension exists because the end of a filling chart is intrinsic to the cover (TauCeti.FilledCover.map_chart_comap_nhds_zero): it is the filter of points of the component going to infinity in ℂ ∖ {0, 1}, which h carries to the corresponding filter for p'. Thus the filled cover is functorial in isomorphisms of covers: the extension respects identities and composition (TauCeti.FilledCover.congr_refl, TauCeti.FilledCover.congr_trans).

Main declarations

• TauCeti.FilledCover.degree_congr: isomorphic covers have the same local degree at corresponding added points.
• TauCeti.FilledCover.range_chart_congr: an isomorphism of covers carries each component over a puncture onto the corresponding component.
• TauCeti.FilledCover.congr: the homeomorphism of filled covers extending an isomorphism of covers.
• TauCeti.FilledCover.fillMap_congr_apply: it commutes with the extended projections.
• TauCeti.FilledCover.congr_refl, TauCeti.FilledCover.congr_trans: the extension respects identities and composition.

References

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

@[simp]

theorem TauCeti.FilledCover.degree_congr {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p) : degree p' ((FilledPoint.congr h hh) i) = degree p i

Isomorphic covers have the same local degree at corresponding added points.

theorem TauCeti.FilledCover.range_chart_congr {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p) : Set.range (chart p' ((FilledPoint.congr h hh) i)) = ⇑h '' Set.range (chart p i)

An isomorphism of covers carries components onto components. The image under h of the component of p ⁻¹' D_q* giving the added point i is the component of p' ⁻¹' D_q* giving the transported added point.

noncomputable def TauCeti.FilledCover.congr {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) : FilledCover p ≃ₜ FilledCover p'

Functoriality of the filled cover in isomorphisms of covers. An isomorphism h : E ≃ₜ F over ℂ ∖ {0, 1} from a covering map p with finite fibres to p' extends to a homeomorphism of their filled covers. It is h on E (TauCeti.FilledCover.congr_apply_incl), sends the added point of a component to the added point of its image component (TauCeti.FilledCover.congr_apply_center), and commutes with the extended projections to the Riemann sphere (TauCeti.FilledCover.fillMap_congr_apply).

@[simp]

theorem TauCeti.FilledCover.congr_apply_incl {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (x : E) : (congr hp hfin h hh) (PunctureFilling.incl (chart p) x) = PunctureFilling.incl (chart p') (h x)

@[simp]

theorem TauCeti.FilledCover.congr_apply_center {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p) : (congr hp hfin h hh) (PunctureFilling.center (chart p) i) = PunctureFilling.center (chart p') ((FilledPoint.congr h hh) i)

@[simp]

theorem TauCeti.FilledCover.congr_symm_apply_incl {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (x : F) : (congr hp hfin h hh).symm (PunctureFilling.incl (chart p') x) = PunctureFilling.incl (chart p) (h.symm x)

@[simp]

theorem TauCeti.FilledCover.congr_symm_apply_center {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (i : FilledPoint p') : (congr hp hfin h hh).symm (PunctureFilling.center (chart p') i) = PunctureFilling.center (chart p) ((FilledPoint.congr h hh).symm i)

@[simp]

theorem TauCeti.FilledCover.fillMap_congr_apply {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (y : FilledCover p) : fillMap p' ((congr hp hfin h hh) y) = fillMap p y

The extended homeomorphism lies over the Riemann sphere: it commutes with the extended projections fillMap p and fillMap p'.

@[simp]

theorem TauCeti.FilledCover.congr_refl {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) : congr hp hfin (Homeomorph.refl E) ⋯ = Homeomorph.refl (FilledCover p)

The identity isomorphism of covers extends to the identity of the filled cover.

theorem TauCeti.FilledCover.congr_trans {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {p : E → ThricePuncturedSphere} {p' : F → ThricePuncturedSphere} {G : Type u_3} [TopologicalSpace G] {p'' : G → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (hp' : IsCoveringMap p') {z₁ : ThricePuncturedSphere} (hfin' : Finite ↑(p' ⁻¹' {z₁})) (h : E ≃ₜ F) (hh : p' ∘ ⇑h = p) (k : F ≃ₜ G) (hk : p'' ∘ ⇑k = p') : congr hp hfin (h.trans k) ⋯ = (congr hp hfin h hh).trans (congr hp' hfin' k hk)

The extension of a composite of isomorphisms of covers is the composite of the extensions.