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 fmeansf : M → Nis aC^nembedding: it is both aC^nimmersion and a topological embeddingIsSmoothEmbedding.prodMap: the product of two smooth embeddings is a smooth embeddingIsSmoothEmbedding.id: the identity map is a smooth embeddingIsSmoothEmbedding.of_opens: the inclusion of an open subsets → Mof a smooth manifold is a smooth embeddingIsSmoothEmbedding.sumInlandIsSmoothEmbedding.sumInr: givenC^nmanifoldsMandN,Sum.inl : M → M ⊕ NandSum.inr : N → M ⊕ NareC^nembeddingsIsSmoothEmbedding.contMDiff: iffis aC^nembedding, it is automaticallyC^nin the sense ofContMDiff.
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 atx.) - 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 embeddingIsLocalDiffeomorph.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)
:
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
Instances For
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)
:
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
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.