Smooth embeddings

In this file, we define C^n embeddings between C^n manifolds. This will be useful to define embedded submanifolds.

Main definitions and results

• IsSmoothEmbedding I J n f means f : M → N is a C^n embedding: it is both a C^n immersion and a topological embedding
• IsSmoothEmbedding.prodMap: the product of two smooth embeddings is a smooth embedding
• IsSmoothEmbedding.id: the identity map is a smooth embedding
• IsSmoothEmbedding.of_opens: the inclusion of an open subset s → M of a smooth manifold is a smooth embedding
• ModelWithCorners.isSmoothEmbedding: every model with corners is itself a smooth embedding
• IsSmoothEmbedding.sumInl and IsSmoothEmbedding.sumInr: given C^n manifolds M and N, Sum.inl : M → M ⊕ N and Sum.inr : N → M ⊕ N are C^n embeddings
• IsSmoothEmbedding.contMDiff: if f is a C^n embedding, it is automatically C^n in the sense of ContMDiff.

Implementation notes

• Unlike immersions, being an embedding is a global notion: this is why we have no definition IsSmoothEmbeddingAt. (Besides, it would be equivalent to being an immersion at x.)
• Note that being a smooth embedding is a stronger condition than being a smooth map which is a topological embedding. Even being a homeomorphism and a smooth map is not sufficient. See e.g. https://math.stackexchange.com/a/2583667 and https://math.stackexchange.com/a/3769328 for counterexamples.

TODO

• IsSmoothEmbedding.comp: the composition of smooth embeddings (between Banach manifolds) is a smooth embedding
• IsLocalDiffeomorph.isSmoothEmbedding, Diffeomorph.isSmoothEmbedding: a local diffeomorphism (and in particular, a diffeomorphism) is a smooth embedding

structure Manifold.IsSmoothEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8} [TopologicalSpace H] [TopologicalSpace G] (I : ModelWithCorners 𝕜 E₁ H) (J : ModelWithCorners 𝕜 E₃ G) {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) : Prop

A C^n map f : M → M' is a smooth C^n embedding if it is a topological embedding and a C^n immersion.

• isImmersion : IsImmersion I J n f
• isEmbedding : Topology.IsEmbedding f

theorem Manifold.isSmoothEmbedding_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8} [TopologicalSpace H] [TopologicalSpace G] (I : ModelWithCorners 𝕜 E₁ H) (J : ModelWithCorners 𝕜 E₃ G) {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N) : IsSmoothEmbedding I J n f ↔ IsImmersion I J n f ∧ Topology.IsEmbedding f

theorem Manifold.IsSmoothEmbedding.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] : IsSmoothEmbedding I I n id

theorem Manifold.IsSmoothEmbedding.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} {E₄ : Type u_5} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] [NormedAddCommGroup E₄] [NormedSpace 𝕜 E₄] {H : Type u_6} {H' : Type u_7} {G : Type u_8} {G' : Type u_9} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E₁ H} {I' : ModelWithCorners 𝕜 E₂ H'} {J : ModelWithCorners 𝕜 E₃ G} {J' : ModelWithCorners 𝕜 E₄ G'} {M : Type u_10} {M' : Type u_11} {N : Type u_12} {N' : Type u_13} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'] (hf : IsSmoothEmbedding I J n f) (hg : IsSmoothEmbedding I' J' n g) : IsSmoothEmbedding (I.prod I') (J.prod J') n (Prod.map f g)

If f: M → N and g: M' × N' are smooth embeddings, respectively, then so is f × g: M × M' → N × N'.

theorem Manifold.IsSmoothEmbedding.of_opens {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] (s : TopologicalSpace.Opens M) : IsSmoothEmbedding I I n Subtype.val

theorem ModelWithCorners.isSmoothEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {n : ℕ} : Manifold.IsSmoothEmbedding I (modelWithCornersSelf 𝕜 E₁) ↑n ↑I

Every ModelWithCorners 𝕜 E H is a smooth embedding when viewed as a map H → E.

theorem Manifold.IsSmoothEmbedding.sumInl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_14} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'] : IsSmoothEmbedding I I n Sum.inl

Given C^n manifolds M and N, Sum.inl : M → M ⊕ N is a C^n embedding.

theorem Manifold.IsSmoothEmbedding.sumInr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_14} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'] : IsSmoothEmbedding I I n Sum.inr

Given C^n manifolds M and N, Sum.inr : N → M ⊕ N is a C^n embedding.

theorem Manifold.IsSmoothEmbedding.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H} {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (hf : IsSmoothEmbedding I J n f) : ContMDiff I J n f

A smooth embedding is automatically smooth.