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.

noncomputable 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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) : ContMDiffMap I (modelWithCornersSelf ℝ (ι → E × ℝ)) M (ι → E × ℝ) ↑⊤

Smooth embedding of M into (E × ℝ) ^ ι.

Equations

• f.embeddingPiTangent = ⟨fun (x : M) (i : ι) => (↑(f.toFun i) x • ↑(extChartAt I (f.c i)) x, ↑(f.toFun i) x), ⋯⟩

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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) : ⇑f.embeddingPiTangent = 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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) : Set.InjOn (⇑f.embeddingPiTangent) 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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] (f : SmoothBumpCovering ι I M) : Function.Injective ⇑f.embeddingPiTangent

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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : ((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp (mfderiv% ⇑f.embeddingPiTangent x) = mfderiv% ↑(chartAt H (f.c (f.ind 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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker = ⊥

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] [IsManifold I (↑⊤) M] [T2Space M] [Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : Function.Injective ⇑(mfderiv% ⇑f.embeddingPiTangent x)

theorem SmoothBumpCovering.exists_immersion_euclidean {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] [IsManifold I (↑⊤) M] [T2Space M] {ι : Type u_1} [Finite ι] (f : SmoothBumpCovering ι I M) : ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Function.Injective e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% 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] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] : ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% 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.