Manifold atlases on spaces glued from open pieces #
Let D : TopCat.GlueData glue spaces D.U i along open subspaces D.V (i, j), and suppose all the
pieces and overlaps are charted spaces modelled on one space H. The canonical maps
D.toGlueData.ι i are open embeddings that jointly cover the glued space, so transporting charts
along them gives the glued space a charted-space structure, TopCat.GlueData.chartedSpace.
The overlap D.V (i, j) maps to its two adjacent pieces, by D.f i j into D.U i and by
D.f j i ∘ D.t i j into D.U j. The pieces and overlaps are compatible,
TopCat.GlueData.IsCompatible I n, when both maps are C^n local diffeomorphisms: the atlas of
the overlap is then compatible with the atlases of both pieces, and the second map records the
transition between the pieces. Equivalently, every inclusion D.f i j and every transition
D.t i j is a C^n local diffeomorphism (TopCat.GlueData.isCompatible_iff). If moreover
every piece is a C^n manifold, then the glued space is a C^n manifold, every canonical map is
a C^n local diffeomorphism, hence a C^n diffeomorphism onto its open image, and a map out of
the glued space is C^m, for m ≤ n, exactly when its restriction to every piece is.
For 𝕜 = ℂ this glues complex manifolds along holomorphic transitions.
The glued manifold structure is unique: any C^n manifold structure on the glued space for which
every canonical map is a C^n local diffeomorphism has the same maximal atlas, so both define the
same C^n structure. A map out of the glued space is a C^n local diffeomorphism exactly when its
composite with every canonical map is.
The relation identifying points of different pieces is consumed through D.ι_eq_iff_rel; it is
not copied into a new structure. Empty pieces need no special treatment.
Main declarations #
TopCat.GlueData.chartedSpace: the atlas on the glued space transported from the pieces.TopCat.GlueData.IsCompatible: the overlap compatibility condition.TopCat.GlueData.isCompatible_iff: compatibility means that the overlap inclusions and the transition maps are local diffeomorphisms.TopCat.GlueData.IsCompatible.isManifold: compatible pieces glue to aC^nmanifold.TopCat.GlueData.IsCompatible.isLocalDiffeomorph_ι: the canonical maps areC^nlocal diffeomorphisms.TopCat.GlueData.IsCompatible.partialDiffeomorphι: a canonical map as aC^ndiffeomorphism from a piece onto its image.TopCat.GlueData.IsCompatible.contMDiff_iff: smoothness of a map out of the glued manifold is tested on the pieces.TopCat.GlueData.IsCompatible.isLocalDiffeomorph_iff: local diffeomorphisms out of the glued space are detected on the pieces.TopCat.GlueData.IsCompatible.maximalAtlas_chartedSpace_eq: uniqueness of the glued manifold structure.
References #
- John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 1 (the smooth manifold chart lemma).
- Shoshichi Kobayashi and Katsumi Nomizu, Foundations of Differential Geometry, Volume I, Chapter I (atlases compatible with a pseudogroup).
The charted-space structure on the glued space of D: the chart at a point is the inverse of
the canonical map of a piece containing it, followed by a chart of that piece. Its body is exposed
so that the lemmas about TauCeti.chartedSpaceOfIsOpenEmbedding apply to it directly.
Instances For
Every chart of D.chartedSpace H is the inverse of the canonical map of a piece followed by a
chart of that piece.
The atlases of the pieces and overlaps of D are C^n compatible when both maps from an
overlap D.V (i, j) to its adjacent pieces, D.f i j to D.U i and D.f j i ∘ D.t i j to
D.U j, are C^n local diffeomorphisms.
- isLocalDiffeomorph_f (i j : D.J) : IsLocalDiffeomorph I I n ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j))
The inclusion of an overlap into the first adjacent piece is a local diffeomorphism.
- isLocalDiffeomorph_f_comp_t (i j : D.J) : IsLocalDiffeomorph I I n (⇑(CategoryTheory.ConcreteCategory.hom (D.f j i)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (D.t i j)))
The transition from an overlap into the second adjacent piece is a local diffeomorphism.
Instances For
If the inclusions D.f i j and the transitions D.t i j are C^n local diffeomorphisms,
then the pieces and overlaps of D are C^n compatible.
For compatible pieces and overlaps, every transition map D.t i j is a C^n local
diffeomorphism: it is the transition into the second piece followed by a local inverse of the
inclusion D.f j i.
The pieces and overlaps of D are C^n compatible exactly when every overlap inclusion
D.f i j and every transition map D.t i j is a C^n local diffeomorphism.
Transitions of a compatible gluing. If a point x of the piece D.U i and a point y of
the piece D.U j have the same image in the glued space, then near x the canonical map of D.U i
factors through that of D.U j along a map that is C^n at x.
Compatible open gluing. If the pieces of D are C^n manifolds whose atlases are
compatible with those of the overlaps, then the glued space is a C^n manifold.
The canonical map of a piece into a compatible gluing is C^n.
The inverse of the canonical map of a nonempty piece into a compatible gluing is C^n on the
image of that piece.
The canonical map of a nonempty piece into a compatible gluing, as a C^n diffeomorphism from
the piece onto its open image.
Instances For
The diffeomorphism of a piece onto its image in a compatible gluing is defined on the whole piece.
The diffeomorphism of a piece onto its image in a compatible gluing has the image of the canonical map as its target.
The diffeomorphism of a piece onto its image in a compatible gluing is the canonical map.
The canonical map of a piece into a compatible gluing is a C^n local diffeomorphism.
Smooth maps out of a compatible gluing. For m ≤ n, a map out of the glued space is C^m
exactly when its composite with the canonical map of every piece is C^m.
Local diffeomorphisms out of a compatible gluing. A map out of the glued space is a C^n
local diffeomorphism exactly when its composite with the canonical map of every piece is one. In
particular, a bijection onto another C^n manifold with this property is a diffeomorphism, by
IsLocalDiffeomorph.diffeomorphOfBijective.
Uniqueness of the glued manifold structure. A C^n manifold structure on the glued space
for which every canonical map is a C^n local diffeomorphism has the same maximal atlas as
D.chartedSpace H.