Whitney embedding theorem (strong form, dimension 2n)

whitney_embedding — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Whitney embedding theorem** (Whitney 1944). Every smooth
`n`-manifold (`n ≥ 1`, Hausdorff, second-countable) admits a smooth
embedding into `ℝ^{2n}`. -/
theorem 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) := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: whitney_embedding
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.