Documentation

Mathlib.Geometry.Manifold.WhitneyEmbedding

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 #

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.

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),
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) :
    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] [SmoothManifoldWithCorners I M] [T2Space M] [hi : Fintype ι] {s : Set M} (f : SmoothBumpCovering ι I M s) :
    Set.InjOn (f.embeddingPiTangent) s
    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.fst E ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp (mfderiv I (modelWithCornersSelf (ιE × )) (f.embeddingPiTangent) x) = mfderiv I I ((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] [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 × )) (f.embeddingPiTangent) 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 × )) (f.embeddingPiTangent) 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.

    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.