Manifolds glued from open pieces

Let M be a topological space covered by the images of open embeddings φ j : U j → M of charted spaces modelled on a common space H. Transporting the charts of each piece along its embedding gives a charted-space structure on M, TauCeti.chartedSpaceOfIsOpenEmbedding. This is how a space glued from manifolds along open subsets, such as TopCat.GlueData.glued, receives its atlas.

The atlas is a C^n manifold as soon as the pieces are C^n manifolds and are glued along C^n maps. The gluing condition is phrased without inverses: whenever φ j x = φ k y, some map T : U j → U k that is C^n at x satisfies φ k ∘ T = φ j near x (so T sends x to y, as φ k is injective). For a space glued along transition maps, T is the transition itself. Each embedding φ j is then a C^n diffeomorphism onto its open image.

Up to its maximal atlas, the glued structure is the only C^n manifold structure on M for which every φ j is a local diffeomorphism. A chart belongs to the maximal atlas of a C^n manifold structure on M for which every φ j is a local diffeomorphism exactly when its composites with the maps φ j are local diffeomorphisms, a condition that does not mention the structure on M. Hence any such structure has the same maximal atlas as the glued one: both define the same C^n structure on M. Dually, a map out of M is a local diffeomorphism exactly when its composites with the embeddings are, so a bijection onto another manifold with this property is a diffeomorphism (IsLocalDiffeomorph.diffeomorphOfBijective).

The gluing condition has the local-deck-transformation shape of IsLocalHomeomorph.isManifold_chartedSpaceOfRightInverse in TauCeti/Geometry/Manifold/Instances/Quotient.lean.

Main declarations

• TauCeti.chartedSpaceOfIsOpenEmbedding: the charts transported from the pieces.
• TauCeti.isManifold_chartedSpaceOfIsOpenEmbedding: pieces glued along C^n maps give a C^n manifold.
• TauCeti.partialDiffeomorphOfIsOpenEmbedding: each embedding of a piece is a C^n diffeomorphism onto its image.
• TauCeti.contMDiff_iff_chartedSpaceOfIsOpenEmbedding: a map out of M is C^n exactly when its composite with every embedding is.
• TauCeti.isLocalDiffeomorph_iff_forall_comp: if every map of a jointly surjective family is a local diffeomorphism, a map out of M is a local diffeomorphism exactly when its composite with every map of the family is.
• TauCeti.isLocalDiffeomorph_iff_chartedSpaceOfIsOpenEmbedding: a map out of M is a C^n local diffeomorphism exactly when its composite with every embedding is.
• TauCeti.maximalAtlas_eq_of_forall_isLocalDiffeomorph: two C^n manifold structures making every map of a jointly surjective family a local diffeomorphism have the same maximal atlas.
• TauCeti.maximalAtlas_chartedSpaceOfIsOpenEmbedding_eq: uniqueness of the glued atlas.

Implementation notes

Pieces may be empty. The chart at a point is taken from a piece containing it, which is nonempty, so that its embedding is an open partial homeomorphism defined on the whole piece. Only the statements that invert the embedding of a given piece assume that piece is nonempty.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 1 (the smooth manifold chart lemma).
• IsLocalHomeomorph.isManifold_chartedSpaceOfRightInverse in TauCeti/Geometry/Manifold/Instances/Quotient.lean, whose construction is adapted here.

theorem TauCeti.exists_contMDiffAt_transition_of_isImmersion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) {E' : Type u_7} {H' : Type u_8} {N : Type u_9} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {g : M → N} (hg : ∀ (j : J), Manifold.IsImmersion I I' n (g ∘ φ j)) (j k : J) (x : U j) (y : U k) (hxy : φ j x = φ k y) : ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j

Open embeddings into a common topological space have smooth overlap transitions if their composites with a common map into an ambient manifold are smooth immersions.

@[instance_reducible]

noncomputable def TauCeti.chartedSpaceOfIsOpenEmbedding {H : Type u_3} [TopologicalSpace H] {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) : ChartedSpace H M

The charted-space structure on a space covered by open embeddings of charted spaces: the chart at a point is the inverse of the embedding of a piece containing it, followed by a chart of that piece.

theorem TauCeti.exists_chartAt_chartedSpaceOfIsOpenEmbedding_eq {H : Type u_3} [TopologicalSpace H] {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (x : M) : ∃ (j : J) (y : U j), φ j y = x ∧ chartAt H x = (Topology.IsOpenEmbedding.toOpenPartialHomeomorph (φ j) ⋯).symm.trans (chartAt H y)

Every chart of chartedSpaceOfIsOpenEmbedding is the inverse of the embedding of a piece followed by a chart of that piece.

theorem TauCeti.isManifold_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] : IsManifold I n M

Pieces that are C^n manifolds glued along C^n maps give a C^n manifold.

theorem TauCeti.contMDiffOn_symm_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) [Nonempty (U j)] : ContMDiffOn I I n (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph (φ j) ⋯).symm) (Set.range (φ j))

The inverse of the embedding of a piece is C^n on its image.

theorem TauCeti.contMDiff_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) : ContMDiff I I n (φ j)

The embedding of a piece is C^n.

noncomputable def TauCeti.partialDiffeomorphOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) [Nonempty (U j)] : PartialDiffeomorph I I (U j) M n

The embedding of a piece, as a C^n diffeomorphism from the piece onto its open image.

@[simp]

theorem TauCeti.partialDiffeomorphOfIsOpenEmbedding_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) [Nonempty (U j)] : (partialDiffeomorphOfIsOpenEmbedding hφ hcover hdeck j).source = Set.univ

The diffeomorphism of a piece onto its image is defined on the whole piece.

@[simp]

theorem TauCeti.partialDiffeomorphOfIsOpenEmbedding_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) [Nonempty (U j)] : (partialDiffeomorphOfIsOpenEmbedding hφ hcover hdeck j).target = Set.range (φ j)

The diffeomorphism of a piece onto its image has the image of the embedding as its target.

@[simp]

theorem TauCeti.coe_partialDiffeomorphOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) [Nonempty (U j)] : ↑(partialDiffeomorphOfIsOpenEmbedding hφ hcover hdeck j).toPartialEquiv = φ j

The diffeomorphism of a piece onto its image is the embedding of the piece.

theorem TauCeti.isLocalDiffeomorph_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] (j : J) : IsLocalDiffeomorph I I n (φ j)

The embedding of a piece is a C^n local diffeomorphism.

theorem TauCeti.contMDiff_iff_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {g : M → N} : ContMDiff I I' n g ↔ ∀ (j : J), ContMDiff I I' n (g ∘ φ j)

Smooth maps out of a glued space. A map out of M is C^n exactly when its composite with the embedding of every piece is C^n.

theorem TauCeti.isLocalDiffeomorph_iff_forall_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) [ChartedSpace H M] (hφM : ∀ (j : J), IsLocalDiffeomorph I I n (φ j)) {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {g : M → N} : IsLocalDiffeomorph I I' n g ↔ ∀ (j : J), IsLocalDiffeomorph I I' n (g ∘ φ j)

Local diffeomorphisms out of a jointly surjective family. If every map φ j of a jointly surjective family is a C^n local diffeomorphism, then a map out of M is a C^n local diffeomorphism exactly when its composite with every φ j is one.

theorem TauCeti.isLocalDiffeomorph_iff_chartedSpaceOfIsOpenEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {g : M → N} : IsLocalDiffeomorph I I' n g ↔ ∀ (j : J), IsLocalDiffeomorph I I' n (g ∘ φ j)

Local diffeomorphisms out of a glued space. A map out of M is a C^n local diffeomorphism exactly when its composite with the embedding of every piece is one.

theorem TauCeti.maximalAtlas_eq_of_forall_isLocalDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) {c c' : ChartedSpace H M} (hc : IsManifold I n M) (hc' : IsManifold I n M) (hφc : ∀ (j : J), IsLocalDiffeomorph I I n (φ j)) (hφc' : ∀ (j : J), IsLocalDiffeomorph I I n (φ j)) : IsManifold.maximalAtlas I n M = IsManifold.maximalAtlas I n M

Uniqueness of glued atlases. Two C^n manifold structures on M for which every map φ j of a jointly surjective family is a C^n local diffeomorphism have the same maximal atlas. The maps φ j need not be embeddings.

theorem TauCeti.maximalAtlas_chartedSpaceOfIsOpenEmbedding_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {J : Type u_4} {U : J → Type u_5} [(j : J) → TopologicalSpace (U j)] [(j : J) → ChartedSpace H (U j)] {M : Type u_6} [TopologicalSpace M] {φ : (j : J) → U j → M} (hφ : ∀ (j : J), Topology.IsOpenEmbedding (φ j)) (hcover : ∀ (x : M), ∃ (j : J) (y : U j), φ j y = x) (hdeck : ∀ (j k : J) (x : U j) (y : U k), φ j x = φ k y → ∃ (T : U j → U k), ContMDiffAt I I n T x ∧ φ k ∘ T =ᶠ[nhds x] φ j) [∀ (j : J), IsManifold I n (U j)] {c : ChartedSpace H M} (hc : IsManifold I n M) (hφc : ∀ (j : J), IsLocalDiffeomorph I I n (φ j)) : IsManifold.maximalAtlas I n M = IsManifold.maximalAtlas I n M

Uniqueness of the glued atlas. A C^n manifold structure on M for which the embedding of every piece is a C^n local diffeomorphism has the same maximal atlas as chartedSpaceOfIsOpenEmbedding.