The charted-space structure on a puncture filling #
Let E be a space charted over ℂ and let φ i : 𝔻* → E be open embeddings of the punctured
unit disc 𝔻* = ball 0 1 \ {0}. Their puncture filling TauCeti.PunctureFilling φ adds the
centre of each punctured disc. It is again locally homeomorphic to ℂ
(TauCeti.PunctureFilling.chartedSpace): at a point of E the chart is the chart of E there,
and at an added point center φ i it is the inverse of the filled disc disc φ i, which sends
center φ i to 0.
Away from the added points, the chart at center φ i is the inverse of φ i read as a chart of
E, TauCeti.PunctureFilling.puncturedDiscChart. When every such chart is compatible with the
charts of E for a structure groupoid closed under restriction, the charts of the filling are
compatible for that groupoid too (TauCeti.PunctureFilling.hasGroupoid); in particular, filling
the punctures of a C^n manifold along punctured discs which are C^n diffeomorphisms onto
their images gives a C^n manifold (TauCeti.PunctureFilling.isManifold). No removable
singularity theorem is needed: the only chart containing center φ i is the chart at that
point, so every other transition map lives inside E.
This is how the compactification of a finite cover of a punctured Riemann surface receives its
charts: E carries the charts pulled back along the covering map, and the punctured discs are the
components of the preimages of punctured discs about the punctures. The charts are holomorphically
compatible once these components are biholomorphic to 𝔻*.
Main declarations #
TauCeti.PunctureFilling.chartedSpace: the charted spacePunctureFilling φoverℂ, with preferred chartsTauCeti.PunctureFilling.chartAt_inclandTauCeti.PunctureFilling.chartAt_center.TauCeti.PunctureFilling.puncturedDiscChart: the inverse of a punctured disc, as a chart ofE.TauCeti.PunctureFilling.hasGroupoid,TauCeti.PunctureFilling.isManifold: compatibility of the charts of the filling.
Implementation notes #
The charts are assembled by hand, as Mathlib assembles those of a disjoint union
(ChartedSpace.sum), rather than through TauCeti.chartedSpaceOfIsOpenEmbedding: that
construction picks the piece containing a point by choice, so the chart at a point of E could be
a filled disc rather than the chart of E, and its gluing condition asks for maps defined on all
of the unit disc, which φ i is not.
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: the charts at the added points).
- O. Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer 1981, §8, Theorem 8.4.
The inverse of an open embedding φ i : 𝔻* → E of the punctured unit disc, as a chart of E
with values in ℂ: its source is the image of φ i and its target is 𝔻*.
Instances For
The charts #
The puncture filling is locally homeomorphic to ℂ. If E is charted over ℂ and the
punctured discs φ i are open embeddings, the chart at a point of E is the chart of E there,
and the chart at the added point center φ i is the inverse of the filled disc disc φ i.
Instances For
The chart of the puncture filling at a point of E is the chart of E at that point.
The chart of the puncture filling at the added point center φ i is the inverse of the
i-th filled disc.
The atlas of the puncture filling consists of the charts of E and the inverses of the filled
discs.
Compatibility of the charts #
The charts of a puncture filling are compatible for a structure groupoid G closed under
restriction, as soon as the charts of E are and the inverse of every punctured disc φ i is
compatible with them.
Filling the punctures of a C^n manifold gives a C^n manifold, as soon as the punctured
discs φ i are C^n diffeomorphisms onto their images, that is, their inverses belong to the
maximal atlas of E.