The components of a cover over the punctured neighborhood of infinity

Let p : E → ℂ ∖ {0, 1} be a covering map whose fibre over the basepoint 1/2 is numbered by ν, with monodromy triple (σ0, σ1, σinf). This file proves that the connected components of the preimage p ⁻¹' D∞* of the standard punctured neighborhood D∞* = {z | 2 < ‖z‖} of infinity are in bijection with the cycles of σinf.

These components are the points to be added over ∞ when a finite cover of the thrice-punctured sphere is compactified to a branched cover of the Riemann sphere. The bijection is not with the fibre, nor with the orbits of the whole monodromy group: it is with the orbits of the single permutation σinf.

The proof has three steps.

• The fundamental group of D∞* at p₊ = 1/2 + (√35/2)·i is generated by the large clockwise circle δInf (zpowers_δInf), and D∞* is path connected. So the components of p ⁻¹' D∞* are the cycles of the monodromy of δInf on the fibre over p₊ (IsCoveringMap.sameCycleQuotientEquivZerothHomotopy).
• Transported to the basepoint 1/2 along the vertical segment αPlus, the class of δInf is periphInf (transport_δInf_eq_periphInf). So monodromy along αPlus carries the cycles of periphInf on the fibre over 1/2 to those of δInf on the fibre over p₊.
• The numbering ν carries the monodromy of periphInf to σinf.

Explicitly, the cycle of a sheet i corresponds to the component containing the endpoint of the lift of αPlus that starts at the point numbered i.

Main declarations

• IsCoveringMap.sameCycle_monodromyTriple_σinf_iff: two sheets lie in the same cycle of σinf exactly when the endpoints of their lifts of αPlus lie in the same cycle of the local monodromy at infinity.
• IsCoveringMap.sameCycle_monodromyTriple_σinf_iff_joinedIn: equivalently, exactly when those endpoints are joined by a path inside p ⁻¹' D∞*.
• IsCoveringMap.sameCycleQuotientσinfEquivConnectedComponents: the cycles of σinf are the connected components of p ⁻¹' D∞*, with value sameCycleQuotientσinfEquivConnectedComponents_mk on the cycle of a sheet.

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 components of the preimage of a punctured disc, one added point for each) and §2.7 (their correspondence with the cycles of the monodromy).

theorem IsCoveringMap.sameCycle_monodromyTriple_σinf_iff {n : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (i j : Fin n) : (hp.monodromyTriple ν).σinf.SameCycle i j ↔ ((hp.monodromyPerm TauCeti.ThricePuncturedSphere.pPlus) ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } TauCeti.ThricePuncturedSphere.infBasePt) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.δInf)))).SameCycle (hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) (ν.symm i)) (hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) (ν.symm j))

σinf is the local monodromy at infinity. Two sheets lie in the same cycle of the third permutation σinf of the monodromy triple exactly when the endpoints of their lifts of αPlus lie in the same cycle of the monodromy of the clockwise large circle δInf, a generator of the fundamental group of the punctured neighborhood of infinity.

theorem IsCoveringMap.sameCycle_monodromyTriple_σinf_iff_joinedIn {n : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (i j : Fin n) : (hp.monodromyTriple ν).σinf.SameCycle i j ↔ JoinedIn (p ⁻¹' TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInf) ↑(hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) (ν.symm i)) ↑(hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) (ν.symm j))

Cycles of σinf are the components over infinity, pointwise. Two sheets lie in the same cycle of σinf exactly when the endpoints of their lifts of αPlus are joined by a path inside the preimage of the punctured neighborhood of infinity.

theorem IsCoveringMap.monodromy_αPlus_mem_preimage {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt})) : ↑(hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) e) ∈ p ⁻¹' TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInf

The endpoint of a lift of αPlus lies over the punctured neighborhood of infinity.

noncomputable def IsCoveringMap.sameCycleQuotientσinfEquivConnectedComponents {n : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) : Quotient (Equiv.Perm.SameCycle.setoid (hp.monodromyTriple ν).σinf) ≃ ConnectedComponents ↑(p ⁻¹' TauCeti.ThricePuncturedSphere.puncturedNeighborhoodInf)

The points over infinity. The cycles of the third permutation σinf of the monodromy triple are in bijection with the connected components of the preimage of the punctured neighborhood {z | 2 < ‖z‖} of infinity. The cycle of a sheet i goes to the component of the endpoint of the lift of αPlus starting at the point numbered i (IsCoveringMap.sameCycleQuotientσinfEquivConnectedComponents_mk).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsCoveringMap.sameCycleQuotientσinfEquivConnectedComponents_mk {n : ℕ} {E : Type u_1} [TopologicalSpace E] {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) (i : Fin n) : (hp.sameCycleQuotientσinfEquivConnectedComponents ν) ⟦i⟧ = ConnectedComponents.mk ⟨↑(hp.monodromy (Path.Homotopic.Quotient.mk TauCeti.ThricePuncturedSphere.αPlus) (ν.symm i)), ⋯⟩

The cycle of the sheet i goes to the connected component of the endpoint of the lift of αPlus starting at the point numbered i.