Thom transversality theorem

TheoremApproximation by maps having zero as a regular value#✓fully proved

Let \(M\) be a Hausdorff, second-countable smooth manifold without boundary modelled on a finite-dimensional real normed space, let \(f : M \to \mathbb{R}^n\) be \(C^\infty\), and let \(\varepsilon > 0\). Then there is a \(C^\infty\) map \(g : M \to \mathbb{R}^n\) such that \(\lVert f(x) - g(x) \rVert < \varepsilon\) for every \(x \in M\) (Euclidean norm) and \(0\) is a regular value of \(g\), that is, the manifold derivative of \(g\) at \(x\) is surjective for every \(x \in M\) with \(g(x) = 0\).

No compactness is needed.

theorem thom_transversality_uniform_approx_regular_value_zero
    {n : ℕ}
    (f : M → EuclideanSpace ℝ (Fin n))
    (hf : ContMDiff I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) f)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (g : M → EuclideanSpace ℝ (Fin n)),
      ContMDiff I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) g ∧
        (∀ x : M, ‖f x - g x‖ < ε) ∧
        (∀ x : M, g x = 0 →
          Function.Surjective (mfderiv I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) g x))

Uses 2 · Used by 1

Proof usesCritical values of a map to Euclidean space · Sard's theorem for maps into Euclidean space

Used byApproximation by maps having zero as a regular value, compact case

TheoremApproximation by maps having zero as a regular value, compact case#✓fully proved

Let \(M\) be a compact, Hausdorff, second-countable smooth manifold without boundary modelled on a finite-dimensional real normed space, let \(f : M \to \mathbb{R}^n\) be \(C^\infty\), and let \(\varepsilon > 0\). Then there is a \(C^\infty\) map \(g : M \to \mathbb{R}^n\) such that \(\lVert f(x) - g(x) \rVert < \varepsilon\) for every \(x \in M\) (Euclidean norm) and \(0\) is a regular value of \(g\), that is, the manifold derivative of \(g\) at \(x\) is surjective for every \(x \in M\) with \(g(x) = 0\).

theorem thom_transversality_compact_source_uniform_approx_regular_value_zero
    {n : ℕ}
    (f : M → EuclideanSpace ℝ (Fin n))
    (hf : ContMDiff I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) f)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (g : M → EuclideanSpace ℝ (Fin n)),
      ContMDiff I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) g ∧
        (∀ x : M, ‖f x - g x‖ < ε) ∧
        (∀ x : M, g x = 0 →
          Function.Surjective (mfderiv I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) g x))

Sources

• R. Thom, Comment. Math. Helv. 28 (1954) 17–86 transversality; M. Hirsch, Differential Topology; Guillemin-Pollack, Differential Topology; J. Lee, ISMs; Lean states compact-source uniform-approx regular-value-zero corollary.

Uses 1

Proof usesApproximation by maps having zero as a regular value

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.