Filling the punctures of a finite cover of the thrice-punctured sphere #
Let p : E → ℂ ∖ {0, 1} be a covering map with finite fibres. Over the standard punctured
neighbourhood D_q* of each puncture q ∈ {0, 1, ∞}, every connected component C of
p ⁻¹' D_q* is a finite connected cover of a punctured disc, hence isomorphic over D_q* to the
power map w ↦ w ^ e on the punctured unit disc 𝔻*, where e ≠ 0 is the local degree
FilledCover.degree p i of the component. The filled cover
FilledCover p adds one point to E for each such component (these are the points
TauCeti.FilledPoint p), the centre of the disc parametrising it: it is the puncture filling
TauCeti.PunctureFilling of E along the parametrisations FilledCover.chart p i : 𝔻* → E
of the components i, one of which is chosen for each component. Different choices differ by a
rotation by an e-th root of unity (TauCeti.existsUnique_rootsOfUnity_smul_homeomorph).
The filled cover is a compact Hausdorff space containing E as an open dense subspace
(TauCeti.PunctureFilling.isOpenEmbedding_incl, TauCeti.PunctureFilling.denseRange_incl); it is
connected when E is (TauCeti.PunctureFilling.connectedSpace). When the fibre over 1/2 is
numbered, the added points are the cycles of the three permutations of the monodromy triple, so
there are c(σ0) + c(σ1) + c(σinf) of them, counting fixed points as cycles, and the local degree
of each component is the length of its cycle. This is the
topological space underlying the branched cover of the Riemann sphere attached to p.
Main declarations #
TauCeti.FilledPoint.sigmaEquiv p: the added pointsTauCeti.FilledPoint p, the components ofp ⁻¹' D_q*, as pairs of a punctureqand a component over it.TauCeti.FilledCover.degree p i: the local degree of the componenti.TauCeti.FilledCover.chart p i: the chosen parametrisation of the componentiby𝔻*, under whichpisw ↦ w ^ degree p iin the standard coordinate ofD_q*(TauCeti.FilledCover.exists_homeomorph_chart_eq).TauCeti.FilledCover p: the coverEwith the punctures of its components filled in.TauCeti.FilledCover.t2Space,TauCeti.FilledCover.compactSpace,TauCeti.FilledCover.secondCountableTopology: the filled cover is Hausdorff and compact, and second countable whenEis.TauCeti.FilledCover.finite_filledPoint: a finite cover has finitely many added points.TauCeti.FilledCover.indexEquiv: the added points are the cycles ofσ0,σ1andσinf.TauCeti.FilledCover.degree_overZero_mk_monodromy,TauCeti.FilledCover.degree_overOne_mk_monodromy,TauCeti.FilledCover.degree_overInf_mk_monodromy: the local degree of the component of a cycle is its length.TauCeti.FilledCover.natCard_range_center: there arec(σ0) + c(σ1) + c(σinf)added points.
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: filling the punctures of a finite unramified cover).
- O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §8, Theorem 8.4.
The connected component of p ⁻¹' D_q* giving the added point i, as a subset of
p ⁻¹' D_q*, where q is the puncture of i.
Instances For
The local degree of the component i of p ⁻¹' D_q*: the number of its points over the
basepoint of 𝔻* in the standard coordinate of D_q*. When p is a covering map with finite
fibres, it is nonzero (FilledCover.degree_ne_zero), p is w ↦ w ^ degree p i along the
filling chart (FilledCover.exists_homeomorph_chart_eq), and it is the length of the cycle of the
monodromy labelling i (FilledCover.degree_overZero_mk_monodromy and its analogues).
Instances For
The local degree is the cardinality of the component fibre over the standard basepoint of the punctured disc.
The filling chart of the component i of p ⁻¹' D_q*: a parametrisation 𝔻* → E of
that component under which p is w ↦ w ^ degree p i in the standard coordinate of D_q*. One
is chosen for each component. Such a parametrisation exists when p is a covering map with finite
fibres (FilledCover.exists_homeomorph_chart_eq); otherwise the chart is an unspecified map.
Instances For
The filled cover of a cover p : E → ℂ ∖ {0, 1}: the space E with one point added for
each connected component of the preimage p ⁻¹' D_q* of the standard punctured neighbourhood of
each puncture q ∈ {0, 1, ∞}, filling the puncture of that component along its filling chart
FilledCover.chart p. When p is a covering map with finite fibres, this is a compact Hausdorff
space containing E as an open dense subspace.
Instances For
The local degree of each component of the preimage of a standard punctured neighbourhood is nonzero.
The filling charts. The filling chart of the component i of p ⁻¹' D_q* is the inverse
of a homeomorphism h from that component onto 𝔻* under which p becomes the power map
w ↦ w ^ degree p i in the standard coordinate q.coord of D_q*.
In the standard coordinate of D_q*, the cover p is the power map w ↦ w ^ degree p i
along the filling chart of each component i over q.
The filling chart of the component i of p ⁻¹' D_q* parametrises exactly the points of
that component.
The filling charts are open embeddings.
The end of a filling chart. Approaching the puncture of 𝔻* along the filling chart of
the component i of p ⁻¹' D_q* is the same as going to infinity in ℂ ∖ {0, 1} within that
component: the image of the end of 𝔻* is the filter of points of the component whose images
under p eventually leave every compact subset of ℂ ∖ {0, 1}. In particular, the end does not
depend on the chosen chart.
The filled cover is Hausdorff.
The local degree over 0 is the cycle length. The component of p ⁻¹' D₀* containing the
endpoint of the lift of αZero from the sheet ν.symm j has local degree the length of the cycle
of j under σ0. This is the component that FilledCover.indexEquiv labels by that cycle, so
simp rewrites degree p ((indexEquiv hp ν).symm (.inl (Quotient.mk _ j))) to the cycle length.
The local degree over 1 is the cycle length. The component of p ⁻¹' D₁* containing the
endpoint of the lift of αOne from the sheet ν.symm j has local degree the length of the cycle of
j under σ1. This is the component that FilledCover.indexEquiv labels by that cycle, so simp
rewrites degree p ((indexEquiv hp ν).symm (.inr (.inl (Quotient.mk _ j)))) to the cycle length.
The local degree over ∞ is the cycle length. The component of p ⁻¹' D∞* containing the
endpoint of the lift of αPlus from the sheet ν.symm j has local degree the length of the cycle
of j under σinf. This is the component that FilledCover.indexEquiv labels by that cycle, so
simp rewrites degree p ((indexEquiv hp ν).symm (.inr (.inr (Quotient.mk _ j)))) to the cycle
length.
The filled cover is compact: outside the images of the discs of radius 1 / 2 under the
filling charts, a finite cover lies over a compact core of ℂ ∖ {0, 1}.
The filled cover of a second-countable cover is second countable.
The number of added points. For a cover whose fibre over 1/2 is numbered by ν, the
filled cover has c(σ0) + c(σ1) + c(σinf) added points, where c(σ) is the number of cycles of
σ, fixed points included (FilledPoint.natCard_eq_cycleCounts).