Whitney embedding theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
noncomputable
def
smooth_bump_covering.embedding_pi_tangent
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s) :
cont_mdiff_map I (model_with_corners_self ℝ (ι → E × ℝ)) M (ι → E × ℝ) ⊤
Smooth embedding of M into (E × ℝ) ^ ι.
theorem
smooth_bump_covering.embedding_pi_tangent_coe
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s) :
theorem
smooth_bump_covering.embedding_pi_tangent_inj_on
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s) :
theorem
smooth_bump_covering.embedding_pi_tangent_injective
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
(f : (smooth_bump_covering ι I M)) :
theorem
smooth_bump_covering.comp_embedding_pi_tangent_mfderiv
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s)
(x : M)
(hx : x ∈ s) :
((continuous_linear_map.fst ℝ E ℝ).comp (continuous_linear_map.proj (f.ind x hx))).comp (mfderiv I (model_with_corners_self ℝ (ι → E × ℝ)) ⇑(f.embedding_pi_tangent) x) = mfderiv I I ⇑(charted_space.chart_at H (f.c (f.ind x hx))) x
theorem
smooth_bump_covering.embedding_pi_tangent_ker_mfderiv
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s)
(x : M)
(hx : x ∈ s) :
linear_map.ker (mfderiv I (model_with_corners_self ℝ (ι → E × ℝ)) ⇑(f.embedding_pi_tangent) x) = ⊥
theorem
smooth_bump_covering.embedding_pi_tangent_injective_mfderiv
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[hi : fintype ι]
{s : set M}
(f : smooth_bump_covering ι I M s)
(x : M)
(hx : x ∈ s) :
function.injective ⇑(mfderiv I (model_with_corners_self ℝ (ι → E × ℝ)) ⇑(f.embedding_pi_tangent) x)
theorem
smooth_bump_covering.exists_immersion_euclidean
{ι : Type uι}
{E : Type uE}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[finite ι]
(f : (smooth_bump_covering ι I M)) :
∃ (n : ℕ) (e : M → euclidean_space ℝ (fin n)), smooth I (model_with_corners_self ℝ (euclidean_space ℝ (fin n))) e ∧ function.injective e ∧ ∀ (x : M), function.injective ⇑(mfderiv I (model_with_corners_self ℝ (euclidean_space ℝ (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}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type uH}
[topological_space H]
{I : model_with_corners ℝ E H}
{M : Type uM}
[topological_space M]
[charted_space H M]
[smooth_manifold_with_corners I M]
[t2_space M]
[compact_space M] :
∃ (n : ℕ) (e : M → euclidean_space ℝ (fin n)), smooth I (model_with_corners_self ℝ (euclidean_space ℝ (fin n))) e ∧ closed_embedding e ∧ ∀ (x : M), function.injective ⇑(mfderiv I (model_with_corners_self ℝ (euclidean_space ℝ (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.