Whitney embedding theorem #
In this file we prove a version of the Whitney embedding theorem: for any compact real manifold M,
for sufficiently large n there exists a smooth embedding M → ℝ^n.
TODO #
- Prove the weak Whitney embedding theorem: any
σ-compact smoothm-dimensional manifold can be embedded intoℝ^(2m+1). This requires a version of Sard's theorem: for a locally Lipschitz continuous mapf : ℝ^m → ℝ^n,m < n, the range has Hausdorff dimension at mostm, hence it has measure zero.
Tags #
partition of unity, smooth bump function, whitney theorem
Whitney embedding theorem #
In this section we prove a version of the Whitney embedding theorem: for any compact real manifold
M, for sufficiently large n there exists a smooth embedding M → ℝ^n.
def
SmoothBumpCovering.embeddingPiTangent
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
:
ContMDiffMap I (modelWithCornersSelf ℝ (ι → E × ℝ)) M (ι → E × ℝ) ⊤
Smooth embedding of M into (E × ℝ) ^ ι.
Instances For
theorem
SmoothBumpCovering.embeddingPiTangent_coe
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
:
↑(SmoothBumpCovering.embeddingPiTangent f) = fun x i =>
(↑(SmoothBumpCovering.toFun s f i) x • ↑(extChartAt I (SmoothBumpCovering.c s f i)) x,
↑(SmoothBumpCovering.toFun s f i) x)
theorem
SmoothBumpCovering.embeddingPiTangent_injOn
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
:
theorem
SmoothBumpCovering.embeddingPiTangent_injective
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
(f : SmoothBumpCovering ι I M Set.univ)
:
theorem
SmoothBumpCovering.comp_embeddingPiTangent_mfderiv
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
(x : M)
(hx : x ∈ s)
:
ContinuousLinearMap.comp
(ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ)
(ContinuousLinearMap.proj (SmoothBumpCovering.ind f x hx)))
(mfderiv I (modelWithCornersSelf ℝ (ι → E × ℝ)) (↑(SmoothBumpCovering.embeddingPiTangent f)) x) = mfderiv I I (↑(chartAt H (SmoothBumpCovering.c s f (SmoothBumpCovering.ind f x hx)))) x
theorem
SmoothBumpCovering.embeddingPiTangent_ker_mfderiv
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
(x : M)
(hx : x ∈ s)
:
LinearMap.ker (mfderiv I (modelWithCornersSelf ℝ (ι → E × ℝ)) (↑(SmoothBumpCovering.embeddingPiTangent f)) x) = ⊥
theorem
SmoothBumpCovering.embeddingPiTangent_injective_mfderiv
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[hi : Fintype ι]
{s : Set M}
(f : SmoothBumpCovering ι I M s)
(x : M)
(hx : x ∈ s)
:
Function.Injective ↑(mfderiv I (modelWithCornersSelf ℝ (ι → E × ℝ)) (↑(SmoothBumpCovering.embeddingPiTangent f)) x)
theorem
SmoothBumpCovering.exists_immersion_euclidean
{ι : Type uι}
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[Finite ι]
(f : SmoothBumpCovering ι I M Set.univ)
:
∃ n e,
Smooth I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e ∧ Function.Injective e ∧ ∀ (x : M), Function.Injective ↑(mfderiv I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e x)
Baby version of the Whitney weak embedding theorem: if M admits a finite covering by
supports of bump functions, then for some n it can be immersed into the n-dimensional
Euclidean space.
theorem
exists_embedding_euclidean_of_compact
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type uH}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type uM}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
[T2Space M]
[CompactSpace M]
:
∃ n e,
Smooth I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Function.Injective ↑(mfderiv I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) e x)
Baby version of the Whitney weak embedding theorem: if M admits a finite covering by
supports of bump functions, then for some n it can be embedded into the n-dimensional
Euclidean space.