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 smooth m-dimensional manifold can be embedded into ℝ^(2m+1). This requires a version of Sard's theorem: for a locally Lipschitz continuous map f : ℝ^m → ℝ^n, m < n, the range has Hausdorff dimension at most m, 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 × ℝ) ^ ι.

Equations

• SmoothBumpCovering.embeddingPiTangent f = { val := fun (x : M) (i : ι) => (↑(f.toFun i) x • ↑(extChartAt I (f.c i)) x, ↑(f.toFun i) x), property := ⋯ }

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 : M) (i : ι) => (↑(f.toFun i) x • ↑(extChartAt I (f.c i)) x, ↑(f.toFun 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) : Set.InjOn (⇑(SmoothBumpCovering.embeddingPiTangent f)) 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) : Function.Injective ⇑(SmoothBumpCovering.embeddingPiTangent f)

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 (f.c (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) : ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), 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 : M → EuclideanSpace ℝ (Fin n)), 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.