Filling punctured-disc ends of a space #
Let E be a topological space and let φ i : 𝔻* → E, for i : ι, be a family of maps from the
punctured unit disc 𝔻* = ball 0 1 \ {0} of ℂ. The puncture filling PunctureFilling φ adds
to E one new point center φ i for each i, and glues the unit disc 𝔻 = ball 0 1 onto
E ⊕ {center φ i} along φ i: the map disc φ i : 𝔻 → PunctureFilling φ sends 0 to
center φ i and every other point w to φ i w. The underlying type is the sum E ⊕ ι, and the
topology is the final topology of the inclusion of E and of the discs disc φ i, so that a map
out of the filling is continuous exactly when its restrictions to E and to every filled disc are
(PunctureFilling.continuous_iff). Concretely, the map PunctureFilling.extend g c which is
g : E → Y on E and c i at the added point center φ i is continuous exactly when g is
continuous, each g ∘ φ i is continuous, and converges to c i along the end of the corresponding
punctured disc, that is, at the points φ i w as w → 0
(PunctureFilling.continuous_extend_iff). This is how a map out of E is extended over the filled
punctures. In particular a continuous map f : E → E' with each f ∘ φ i continuous and carrying
the end of each punctured disc φ i into the end of φ' (σ i) induces a continuous map of
fillings (PunctureFilling.continuous_map), and when all the charts φ i and φ' j are
continuous, a homeomorphism of spaces matching up the ends of the punctured discs extends to a
homeomorphism of their fillings (PunctureFilling.congr).
This is how a finite cover of a punctured surface is compactified: each component of the preimage
of a punctured disc about a puncture is itself a punctured disc, and the filling adds its missing
centre. The general statements here need only the charts φ i. When they are open embeddings,
E and the filled discs are open subspaces of the filling, and the neighbourhoods of center φ i
are the images of the discs of radius r (PunctureFilling.hasBasis_nhds_center). Under the
hypotheses describing the ends of E the filling is Hausdorff, compact, connected and second
countable.
Main declarations #
TauCeti.PunctureFilling φ: the spaceEwith the punctures of the discsφ ifilled in, with the inclusionPunctureFilling.incl, the added pointsPunctureFilling.centerand the filled discsPunctureFilling.disc.TauCeti.PunctureFilling.isOpen_iff,TauCeti.PunctureFilling.continuous_iff: the final topology and its universal property.TauCeti.PunctureFilling.isOpenEmbedding_incl,TauCeti.PunctureFilling.isOpenEmbedding_disc:Eand the filled discs are open subspaces, andEis dense (TauCeti.PunctureFilling.denseRange_incl).TauCeti.PunctureFilling.nhds_center,TauCeti.PunctureFilling.hasBasis_nhds_center: the neighbourhoods of an added point.TauCeti.PunctureFilling.extend,TauCeti.PunctureFilling.continuous_extend_iff: maps out of the filling and their continuity.TauCeti.PunctureFilling.map,TauCeti.PunctureFilling.continuous_map,TauCeti.PunctureFilling.congr: the maps and homeomorphisms of fillings induced by maps carrying ends to ends.TauCeti.PunctureFilling.isDiscrete_range_center: the added points are isolated from one another.TauCeti.PunctureFilling.t2Space,TauCeti.PunctureFilling.compactSpace,TauCeti.PunctureFilling.connectedSpace,TauCeti.PunctureFilling.secondCountableTopology: the separation, compactness, connectedness and countability of the filling.
References #
- E. Girondo, 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 puncture filling of E along the punctured discs φ i : 𝔻* → E: the space E with
one point PunctureFilling.center φ i added for every i, which fills the puncture of φ i. Its
topology is the final topology of the inclusion PunctureFilling.incl of E and of the filled
discs PunctureFilling.disc φ i : 𝔻 → PunctureFilling φ.
Its points are those of the sum E ⊕ ι; the constructor is private, and points are built with
PunctureFilling.incl and PunctureFilling.center and taken apart with
PunctureFilling.induction.
A point of the puncture filling as a point of
E ⊕ ι: a point ofE, or the index of the puncture it fills.
Instances For
The inclusion of E into its puncture filling.
Instances For
The point of the puncture filling which fills the puncture of the i-th disc.
Instances For
The i-th filled disc: the unit disc mapped into the puncture filling, sending 0 to the
added point center φ i and every other point w to φ i w.
Instances For
The inclusion of E into its puncture filling is injective.
Distinct punctures are filled by distinct points.
Induction on the points of the puncture filling: each is a point of E or an added point.
Off its centre, the i-th filled disc is the punctured disc φ i.
A point of the i-th filled disc lies in E exactly when it is a point φ i w of the
punctured disc.
The i-th filled disc is injective when the punctured disc φ i is.
The points of the i-th filled disc which land in incl φ '' V are the points w of the
punctured disc with φ i w ∈ V.
The points of E on the image of W under the i-th filled disc are the images under φ i
of the points of W other than the centre.
Maps out of the puncture filling #
The map out of the puncture filling which is g on E and sends the added point
center φ i to c i. Every map out of the filling is of this form
(PunctureFilling.extend_comp_incl_center), and it is continuous exactly when g and each
g ∘ φ i are continuous and g converges to c i along the end of each punctured disc φ i
(PunctureFilling.continuous_extend_iff).
Instances For
Every map out of the puncture filling is the extension of its restriction to E by its values
at the added points.
The values of a map out of the puncture filling are those it takes on E and at the added
points.
The map of puncture fillings which is f : E → E' on E and sends the added point
center φ i to center φ' (σ i). It is continuous when f and every f ∘ φ i are continuous
and f carries the end of each punctured disc φ i into the end of φ' (σ i)
(PunctureFilling.continuous_map).
Instances For
The map of puncture fillings induced by identity maps is the identity.
The map of puncture fillings induced by composites is the composite of the induced maps.
The topology #
A subset of the puncture filling is open exactly when its preimages in E and in every filled
disc are open.
The universal property of the puncture filling. A map out of the filling is continuous
exactly when its restrictions to E and to every filled disc are.
The inclusion of E into its puncture filling is continuous.
Every filled disc is continuous.
E is an open subset of its puncture filling.
The added points form a closed subset of the puncture filling.
If the punctured discs φ i are continuous, E is an open subspace of its puncture
filling.
If the punctured discs φ j are continuous and φ i is an open embedding, the i-th filled
disc is an open subspace of the puncture filling.
E is dense in its puncture filling: every added point is a limit of points of E.
Neighbourhoods #
The punctured neighbourhoods of the centre of the i-th filled disc are carried onto the end
of the punctured disc φ i, the filter of points φ i w with w near 0.
The end of the i-th punctured disc converges to the added point center φ i.
If the punctured discs are continuous, the neighbourhoods of a point of E in the puncture
filling are its neighbourhoods in E.
The neighbourhoods of the added point center φ i are those of the point itself together with
the image of the end of φ i, the filter of points φ i w with w near 0.
The neighbourhoods of an added point. The images under disc φ i of the discs of radius
r > 0 form a basis of the neighbourhoods of center φ i.
The added points are isolated from one another: every set of added points is closed, as each filled disc meets it at most in its centre.
Continuity of maps out of the puncture filling #
Continuity of a map out of the puncture filling. The extension of g : E → Y by the values
c i at the added points is continuous exactly when g and each composite g ∘ φ i are
continuous, and g converges to c i along the end of each punctured disc φ i.
Functoriality of the puncture filling. The map of puncture fillings induced by a continuous
f : E → E' and a reindexing σ : ι → ι' is continuous if each f ∘ φ i is continuous and f
carries the end of each punctured disc φ i into the end of φ' (σ i).
Functoriality of the puncture filling in homeomorphisms. Suppose that all the charts
φ i and φ' j are continuous (hφ, hφ'). A homeomorphism e : E ≃ₜ E' and a bijection
σ : ι ≃ ι' such that e carries the end of each punctured disc φ i onto the end of
φ' (σ i) induce a homeomorphism of the puncture fillings, which is e on E and sends the added
point center φ i to center φ' (σ i).
Instances For
Separation, compactness, connectedness and countability #
The puncture filling is Hausdorff when E is, the punctured discs are open embeddings, no
point of E is a limit of the end of a punctured disc, and the ends of two different punctured
discs are disjoint.
The puncture filling of finitely many punctures is compact as soon as E minus the images
of the punctured discs of some radius r < 1 is compact.
The puncture filling of a connected space is connected, since E is dense in it.
The puncture filling of a second-countable space along countably many punctured discs is second countable.