Whitney embedding theorem (strong form, dimension 2n)
whitney_embedding
Submitter: Kim Morrison.
Notes: Every smooth n-manifold (n ≥ 1, Hausdorff, second-countable) admits a smooth embedding into ℝ^(2n). The smooth-embedding triple — smooth, topological embedding (mathlib's `IsEmbedding`), and immersion (`mfderiv` injective at every point) — follows the same pattern as mathlib's compact-finite-dimensional embedding theorem `SmoothBumpCovering.exists_embedding_euclidean_of_compact`, which uses the stronger `IsClosedEmbedding` because the source is compact and produces an embedding into some `ℝ^k` with no dimension bound. The sharp 2n bound here is the *strong* Whitney theorem. The n = 0 case is excluded because the 2n bound fails there (a two-point discrete 0-manifold embeds in `ℝ¹` but not in `ℝ⁰`). §112 of Knill's *Some Fundamental Theorems in Mathematics*.
Source: H. Whitney, 'The self-intersections of a smooth n-manifold in 2n-space', Ann. of Math. (2) 45 (1944) 220–246. Earlier 2n+1 form: H. Whitney, 'Differentiable manifolds', Ann. of Math. (2) 37 (1936) 645–680. Listed as §112 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).
Informal solution: The classical proof has three steps. (1) **Weak 2n+1 embedding** (Whitney 1936): start from any immersion M → ℝ^N with N large, then use a Sard-style transversality / generic-projection argument to drop dimension to 2n+1 — at each step, the bad locus of projection directions causing immersion or injection failures has measure zero in S^(N−1). (2) **Whitney trick**: in dimension 2n with n ≥ 3, pairs of opposite-sign transverse self-intersections of a generic 2n-immersion M^n → ℝ^(2n) can be cancelled by an isotopy supported in a Whitney disk pairing the two intersection points. (3) **Low dimensions** (n = 1, 2): handled separately by direct classical arguments (1-manifolds embed by classification of curves; 2-manifolds — compact orientable, compact non-orientable, and open — each via a separate construction, since the Whitney trick requires n ≥ 3). Mathlib has `SmoothBumpCovering.exists_embedding_euclidean_of_compact` (compact-finite-dimensional Whitney with no dimension bound) but no Sard's theorem (the `Mathlib/Geometry/Manifold/WhitneyEmbedding.lean` file's own `## TODO` flags this gap explicitly), no generic-projection argument, and no Whitney trick.
theorem declaration uses `sorry`whitney_embedding (n : ℕ) (_hn : 1 ≤ n)
{M : Type*} [TopologicalSpace M]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
[T2Space M] [SecondCountableTopology M] :
∃ e : M → EuclideanSpace ℝ (Fin (2 * n)),
ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e ∧
IsEmbedding e ∧
∀ x : M, Function.Injective (mfderiv (𝓡 n) (𝓡 (2 * n)) e x) := n:ℕ_hn:1 ≤ nM:Type u_1inst✝⁴:TopologicalSpace Minst✝³:ChartedSpace (EuclideanSpace ℝ (Fin n)) Minst✝²:IsManifold (𝓡 n) ∞ Minst✝¹:T2Space Minst✝:SecondCountableTopology M⊢ ∃ e, ContMDiff (𝓡 n) (𝓡 2 * n) ∞ e ∧ IsEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)
All goals completed! 🐙Solved by
Not yet solved.