The filled cover as a topological branched cover of the sphere

Let p : E → ℂ ∖ {0, 1} be a covering map with finite fibres, and let TauCeti.FilledCover.fillMap p : FilledCover p → OnePoint ℂ be its extension to the filled cover, sending the added point of each component of p ⁻¹' D_q* to its puncture q. Over the complement of the three marked points fillMap p is a covering map, whose fibre over a point z of ℂ ∖ {0, 1} is the fibre of p over z (TauCeti.FilledCover.isCoveringMapOn_fillMap, TauCeti.FilledCover.fillMap_preimage_toOnePoint). This file proves the remaining local property that makes it a branched cover with branch values in {0, 1, ∞}: at the added point of a component i, it is w ↦ w ^ e for e = FilledCover.degree p i, in the chart of the filled cover centred at that point and the inverse of the standard sphere coordinate TauCeti.ThricePuncturedSphere.Puncture.sphereCoordInv at the puncture.

Consequently every connected degree-n cover C of ℂ ∖ {0, 1} fills to a topological branched cover of degree n (TauCeti.ConnectedCover.toTopBranchedCover), whose local degree at the added point of a component is the local degree of that component. Isomorphic covers fill to isomorphic branched covers (TauCeti.ConnectedCover.toTopBranchedCoverIso), so filling is defined on isomorphism classes (TauCeti.ConnectedCoverClass.toTopBranchedCover). Deleting the marked fibres again recovers C up to isomorphism (TauCeti.ConnectedCover.connectedCoverIso), so filling is a right inverse of the restriction map from isomorphism classes of topological branched covers of degree n to isomorphism classes of connected degree-n covers of ℂ ∖ {0, 1} (TauCeti.ConnectedCoverClass.restrict_toTopBranchedCover), which is therefore surjective (TauCeti.TopBranchedCover.IsoClass.restrict_surjective). Since a branched cover is determined by its unbranched part (TauCeti.TopBranchedCover.IsoClass.restrict_injective), every topological branched cover is isomorphic to the filled cover of its unbranched part (TauCeti.TopBranchedCover.isoFilledCover), and restriction is a bijection on isomorphism classes (TauCeti.TopBranchedCover.IsoClass.restrict_bijective).

Through this isomorphism the ramification of a topological branched cover is read off its monodromy: over 0, 1 and ∞ the ramification partition, formed by the local degrees at the points of the fibre, is the full cycle type of σ0, σ1 and σinf in the monodromy triple of the unbranched part (TauCeti.TopBranchedCover.parts_ramificationPartition_zero), since the points over a puncture of a filled cover are the added points over it, whose local degrees are the cycle lengths (TauCeti.FilledCover.map_degree_overZero).

Main results

• TauCeti.FilledCover.isLocalPowerAt_fillMap_center: at the added point of a component, fillMap p is locally the power map of exponent the local degree of the component.
• TauCeti.ConnectedCover.toTopBranchedCover: the filled cover of a connected degree-n cover, as a topological branched cover of degree n.
• TauCeti.ConnectedCover.localDegree_toTopBranchedCover_center: its local degrees at the added points.
• TauCeti.ConnectedCover.toTopBranchedCoverIso: an isomorphism of covers extends to an isomorphism of their filled branched covers.
• TauCeti.ConnectedCoverClass.toTopBranchedCover: the filled branched cover of an isomorphism class of covers.
• TauCeti.ConnectedCover.connectedCoverIso: deleting the marked fibres of the filled cover gives back the original cover.
• TauCeti.ConnectedCoverClass.restrict_toTopBranchedCover: on isomorphism classes, restriction undoes filling.
• TauCeti.TopBranchedCover.IsoClass.restrict_surjective: every connected degree-n cover of ℂ ∖ {0, 1} is the restriction of a topological branched cover of degree n.
• TauCeti.TopBranchedCover.isoFilledCover: every topological branched cover is isomorphic to the filled cover of its unbranched part.
• TauCeti.TopBranchedCover.IsoClass.restrict_bijective: topological branched covers of degree n and connected degree-n covers of ℂ ∖ {0, 1} have the same isomorphism classes.
• TauCeti.TopBranchedCover.parts_ramificationPartition_zero, TauCeti.TopBranchedCover.parts_ramificationPartition_one, TauCeti.TopBranchedCover.parts_ramificationPartition_inf: the ramification partitions over 0, 1 and ∞ are the full cycle types of σ0, σ1 and σinf.

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 (Lemma 1.80: a finite unramified cover of a punctured surface extends to a branched cover of the compact surface).
• O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §8, Theorem 8.4.

theorem TauCeti.FilledCover.isLocalPowerAt_fillMap_center {E : Type u_1} [TopologicalSpace E] {p : E → ThricePuncturedSphere} (hp : IsCoveringMap p) {z₀ : ThricePuncturedSphere} (hfin : Finite ↑(p ⁻¹' {z₀})) (i : FilledPoint p) : IsLocalPowerAt (fillMap p) (PunctureFilling.center (chart p) i) (degree p i)

The local model at a filled point. At the added point of the component i over the puncture q, the extended projection is w ↦ w ^ degree p i, in the chart of the filled cover centred at that point and the inverse of the extended coordinate q.sphereCoordInv of the sphere at q.

noncomputable def TauCeti.ConnectedCover.toTopBranchedCover {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : TopBranchedCover n

The filled cover as a topological branched cover. Filling the punctures of a connected degree-n cover C of ℂ ∖ {0, 1}, and extending its projection to the added points, gives a topological branched cover of the sphere of degree n with branch values in {0, 1, ∞}. Its total space is FilledCover C.cover.proj and its projection is FilledCover.fillMap (TauCeti.ConnectedCover.toTopBranchedCover_π_apply).

@[simp]

theorem TauCeti.ConnectedCover.toTopBranchedCover_π_apply {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) (y : FilledCover ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) : C.toTopBranchedCover.π y = FilledCover.fillMap (⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) y

The projection of the filled branched cover is the extension of the projection of C.

@[simp]

theorem TauCeti.ConnectedCover.localDegree_toTopBranchedCover_center {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) (i : FilledPoint ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) : C.toTopBranchedCover.localDegree (PunctureFilling.center (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) i) = FilledCover.degree (⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) i

The local degree of the filled branched cover at the added point of a component is the local degree FilledCover.degree of that component.

noncomputable def TauCeti.ConnectedCover.connectedCoverHomeomorph {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : ↑C.cover.obj.left ≃ₜ ↑C.toTopBranchedCover.connectedCover.cover.obj.left

The total space of C is homeomorphic to the total space of the cover obtained by deleting the marked fibres from its filled branched cover, by the inclusion E ↪ FilledCover.

@[simp]

theorem TauCeti.ConnectedCover.coe_connectedCoverHomeomorph_apply {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) (x : ↑C.cover.obj.left) : ↑(C.toTopBranchedCover.connectedCoverHomeomorph (C.connectedCoverHomeomorph x)) = PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) x

The homeomorphism TauCeti.ConnectedCover.connectedCoverHomeomorph is the inclusion of the total space of C into its filled cover.

noncomputable def TauCeti.ConnectedCover.connectedCoverIso {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : C.cover ≅ C.toTopBranchedCover.connectedCover.cover

Deleting the marked fibres of the filled cover recovers the cover. The connected cover of ℂ ∖ {0, 1} underlying the filled branched cover of C is isomorphic to C, by the inclusion of the total space of C into its filled cover.

@[simp]

theorem TauCeti.ConnectedCover.connectedCoverIso_hom_hom_left {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : CategoryTheory.Over.Hom.left C.connectedCoverIso.hom.hom = (TopCat.isoOfHomeo C.connectedCoverHomeomorph).hom

The map of total spaces underlying TauCeti.ConnectedCover.connectedCoverIso.

@[simp]

theorem TauCeti.ConnectedCover.connectedCoverIso_inv_hom_left {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : CategoryTheory.Over.Hom.left C.connectedCoverIso.inv.hom = (TopCat.isoOfHomeo C.connectedCoverHomeomorph).inv

The inverse map of total spaces underlying TauCeti.ConnectedCover.connectedCoverIso.

noncomputable def TauCeti.ConnectedCover.toTopBranchedCoverIso {n : ℕ} {C D : ConnectedCover ThricePuncturedSphere.basePt n} (f : C.cover ≅ D.cover) : C.toTopBranchedCover.Iso D.toTopBranchedCover

Isomorphic covers have isomorphic filled branched covers. An isomorphism f of connected covers of ℂ ∖ {0, 1} extends to an isomorphism of their filled branched covers, which is f on the total space of C (TauCeti.ConnectedCover.toTopBranchedCoverIso_apply_incl).

@[simp]

theorem TauCeti.ConnectedCover.toTopBranchedCoverIso_apply_incl {n : ℕ} {C D : ConnectedCover ThricePuncturedSphere.basePt n} (f : C.cover ≅ D.cover) (x : ↑C.cover.obj.left) : (toTopBranchedCoverIso f).toHomeomorph (PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj C.cover))) x) = PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj D.cover))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom.hom)) x)

The isomorphism TauCeti.ConnectedCover.toTopBranchedCoverIso f is f on the total space of C.

noncomputable def TauCeti.ConnectedCoverClass.toTopBranchedCover {n : ℕ} : ConnectedCoverClass ThricePuncturedSphere.basePt n → TopBranchedCover.IsoClass n

The filled branched cover of an isomorphism class of covers. Filling the punctures of a connected degree-n cover of ℂ ∖ {0, 1} is well defined on isomorphism classes, by TauCeti.ConnectedCover.toTopBranchedCoverIso.

@[simp]

theorem TauCeti.ConnectedCoverClass.toTopBranchedCover_mk {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : (mk C).toTopBranchedCover = TopBranchedCover.IsoClass.mk C.toTopBranchedCover

The filled branched cover of the class of C is the class of the filled branched cover of C.

@[simp]

theorem TauCeti.ConnectedCoverClass.mk_connectedCover_toTopBranchedCover {n : ℕ} (C : ConnectedCover ThricePuncturedSphere.basePt n) : mk C.toTopBranchedCover.connectedCover = mk C

Restricting the filled branched cover of C over ℂ ∖ {0, 1} gives back the isomorphism class of C.

@[simp]

theorem TauCeti.ConnectedCoverClass.restrict_toTopBranchedCover {n : ℕ} (c : ConnectedCoverClass ThricePuncturedSphere.basePt n) : c.toTopBranchedCover.restrict = c

Restriction undoes filling on isomorphism classes. Restricting the filled branched cover of a class of connected degree-n covers of ℂ ∖ {0, 1} over ℂ ∖ {0, 1} gives back that class.

theorem TauCeti.TopBranchedCover.IsoClass.restrict_surjective {n : ℕ} : Function.Surjective restrict

Every connected degree-n cover of ℂ ∖ {0, 1} extends to a topological branched cover of the sphere: restriction over ℂ ∖ {0, 1} is surjective on isomorphism classes, the filled cover TauCeti.ConnectedCoverClass.toTopBranchedCover providing a preimage of each class.

noncomputable def TauCeti.TopBranchedCover.isoFilledCover {n : ℕ} (X : TopBranchedCover n) : X.Iso X.connectedCover.toTopBranchedCover

A branched cover is the filling of its unbranched part. Every topological branched cover X of degree n is isomorphic to the filled cover of the connected cover of ℂ ∖ {0, 1} obtained by deleting its marked fibres, by an isomorphism which on the unbranched part is the inclusion into the filled cover (TauCeti.TopBranchedCover.toHomeomorph_isoFilledCover_connectedCoverHomeomorph). By TauCeti.TopBranchedCover.Iso.restrict_injective, it is the only such isomorphism.

@[simp]

theorem TauCeti.TopBranchedCover.toHomeomorph_isoFilledCover_connectedCoverHomeomorph {n : ℕ} (X : TopBranchedCover n) (x : ↑X.connectedCover.cover.obj.left) : X.isoFilledCover.toHomeomorph ↑(X.connectedCoverHomeomorph x) = PunctureFilling.incl (FilledCover.chart ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj X.connectedCover.cover))) x

On the unbranched part, TauCeti.TopBranchedCover.isoFilledCover is the inclusion of the total space of the connected cover into its filled cover.

theorem TauCeti.TopBranchedCover.IsoClass.restrict_bijective {n : ℕ} : Function.Bijective restrict

Topological branched covers are classified by their unbranched parts: restriction over ℂ ∖ {0, 1} is a bijection from isomorphism classes of topological branched covers of degree n to isomorphism classes of connected degree-n covers of ℂ ∖ {0, 1}.

Ramification partitions over the punctures

theorem TauCeti.TopBranchedCover.parts_ramificationPartition_zero {n : ℕ} (X : TopBranchedCover n) (ν : ↑(X.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (X.ramificationPartition ↑0).parts = (⋯.monodromyTriple ν).σ0.fullCycleType

The ramification partition over 0. The local degrees of a topological branched cover at the points over 0 are the cycle lengths of σ0 in its monodromy triple, fixed points included.

theorem TauCeti.TopBranchedCover.parts_ramificationPartition_one {n : ℕ} (X : TopBranchedCover n) (ν : ↑(X.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (X.ramificationPartition ↑1).parts = (⋯.monodromyTriple ν).σ1.fullCycleType

The ramification partition over 1. The local degrees of a topological branched cover at the points over 1 are the cycle lengths of σ1 in its monodromy triple, fixed points included.

theorem TauCeti.TopBranchedCover.parts_ramificationPartition_inf {n : ℕ} (X : TopBranchedCover n) (ν : ↑(X.restrict ⁻¹' {ThricePuncturedSphere.basePt}) ≃ Fin n) : (X.ramificationPartition OnePoint.infty).parts = (⋯.monodromyTriple ν).σinf.fullCycleType

The ramification partition over ∞. The local degrees of a topological branched cover at the points over ∞ are the cycle lengths of σinf in its monodromy triple, fixed points included.