Differential topology

Smooth manifolds and smooth maps between them: immersions, submersions, transversality, Morse theory, neighbourhood theorems and smooth structures.

• Classification of one-manifolds
• Immersions
• Regular level sets
• Sard's theorem
• Morse theory
• Submersions
• Thom transversality theorem

TheoremA closed simply connected topological 4-manifold with no smooth structure#●ready to prove

There exists a compact, Hausdorff, simply connected topological space \(M\) that admits an atlas of charts modelled on \(\mathbb{R}^4\), such that no atlas of charts on \(M\) modelled on \(\mathbb{R}^4\) makes \(M\) a smooth (\(C^\infty\)) manifold.

public theorem_wanted four_manifold_not_smooth :
    ∃ (M : Type*) (_ : TopologicalSpace M) (_ : T2Space M) (_: CompactSpace M)
      (_ : SimplyConnectedSpace M) (_ : Nonempty (ChartedSpace 𝔼 M)),
      ∀ (_ : ChartedSpace 𝔼 M), ¬ IsManifold (𝓡 4) ∞ M

Sources

-. Problem four_manifold_not_smooth of the lean-eval benchmark.

TheoremCollar neighborhood theorem (topological form)#✓fully proved

Let \(n \ge 1\) and let \(M\) be a Hausdorff, second-countable smooth (\(C^\infty\)) manifold with boundary modeled on the closed half-space \(\{x \in \mathbb{R}^n : x_1 \ge 0\}\), and let \(\partial M\) be its boundary. Then there is an open embedding \(c : \partial M \times [0, 1) \to M\) such that \(c(b, 0) = b\) for every \(b \in \partial M\).

Proof: Local chart collars are glued by Brown's external-collar construction, following Hatcher, Algebraic Topology, Proposition 3.42, and the locally finite extension of Connelly (1971).

theorem topological_collar_neighborhood_of_smooth_manifold_with_boundary
    {n : ℕ} [NeZero n]
    {M : Type*} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace n) M]
    [IsManifold (𝓡∂ n) (⊤ : ℕ∞) M] [T2Space M] [SecondCountableTopology M] :
    ∃ (c : (↥(ModelWithCorners.boundary (I := 𝓡∂ n) M) × ↥(Set.Ico (0 : ℝ) 1)) → M),
      Topology.IsOpenEmbedding c ∧
        ∀ (b : ↥(ModelWithCorners.boundary (I := 𝓡∂ n) M)),
          c (b, ⟨(0 : ℝ), by simp [Set.mem_Ico]⟩) = b.val

Sources

• M. Hirsch, Differential Topology, GTM 33; J. Lee, Introduction to Smooth Manifolds, 2nd ed.; Kosinski, Differential Manifolds; Lean states topological collar IsOpenEmbedding corollary for EuclideanHalfSpace model.

TheoremHadamard–Caccioppoli global inverse theorem#✓fully proved

Let \(n \in \mathbb{N}\) and let \(f : \mathbb{R}^n \to \mathbb{R}^n\) be a proper map that is a \(C^\infty\) local diffeomorphism. Then \(f\) is a global \(C^\infty\) diffeomorphism: there is a \(C^\infty\) diffeomorphism \(\Phi : \mathbb{R}^n \to \mathbb{R}^n\) whose underlying map is \(f\).

theorem hadamard_caccioppoli_global_inverse
    {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf_proper : IsProperMap f)
    (hf_local : IsLocalDiffeomorph (𝓘(ℝ, EuclideanSpace ℝ (Fin n)))
      (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) f) :
    ∃ (Φ : EuclideanSpace ℝ (Fin n) ≃ₘ⟮𝓘(ℝ, EuclideanSpace ℝ (Fin n)),
      𝓘(ℝ, EuclideanSpace ℝ (Fin n))⟯ EuclideanSpace ℝ (Fin n)), ⇑Φ = f

Sources

• J. Hadamard, Bull. Soc. Math. France 34 (1906) 71–84; R. Caccioppoli, Rend. Sem. Mat. Univ. Padova 3 (1932); F.-C. Plastock, Trans. Amer. Math. Soc. 200 (1974) extension to Banach spaces; J. Lee, Riemannian Manifolds? Lean states Euclidean ℝⁿ = EuclideanSpace ℝ (Fin n) specialization with IsProperMap and IsLocalDiffeomorph hypotheses.

TheoremHairy ball theorem#✓fully proved

Let \(k \in \mathbb{N}\) and let \(E\) be a real inner product space of dimension \(2k + 1\), with unit sphere \(S = \{x \in E : \|x\| = 1\}\). If \(f : S \to E\) is continuous and \(\langle f(x), x \rangle = 0\) for every \(x \in S\), then \(f(x) = 0\) for some \(x \in S\).

theorem hairyBall_even_sphere_ambient
    {k : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (hDim : Module.finrank ℝ E = 2 * k + 1)
    (f : sphere (0 : E) 1 → E)
    (hf : Continuous f)
    (hortho : ∀ x : sphere (0 : E) 1, @inner ℝ E _ (f x) (x : E) = 0) :
    ∃ x : sphere (0 : E) 1, f x = 0

Sources

• H. Poincaré proved the 2-sphere case in 1885 and L. E. J. Brouwer extended it to higher even-dimensional spheres in 1912; J. Milnor, Topology from the Differentiable Viewpoint hairy ball; Guillemin-Pollack, Differential Topology; Lean states even-sphere ambient finite-dimensional inner-product specialization via inner = 0.

TheoremSmooth retraction onto a closed embedded manifold in \(\mathbb{R}^n\)#✓fully proved

Let \(M\) be a Hausdorff, second-countable smooth (\(C^\infty\)) manifold without boundary, modelled on a finite-dimensional real normed space, and let \(e \colon M \to \mathbb{R}^n\) be a smooth embedding (a \(C^\infty\) immersion that is a topological embedding) whose image \(e(M)\) is closed in \(\mathbb{R}^n\). Then there exist an open set \(U \subseteq \mathbb{R}^n\) containing \(e(M)\) and a \(C^\infty\) map \(r \colon U \to M\) such that \(r(e(x)) = x\) for every \(x \in M\).

theorem tubular_smoothRetraction
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (⊤ : ℕ∞) M]
    [T2Space M] [SecondCountableTopology M]
    {n : ℕ}
    (e : M → EuclideanSpace ℝ (Fin n))
    (he : IsSmoothEmbedding I (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) e)
    (hclosed : IsClosed (Set.range e)) :
    ∃ (U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n)))
      (hU_sup : Set.range e ⊆ (U : Set (EuclideanSpace ℝ (Fin n)))),
      ∃ (r : ↥U → M),
        ContMDiff (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) I (⊤ : ℕ∞) r ∧
          ∀ (x : M), r ⟨e x, hU_sup ⟨x, rfl⟩⟩ = x

Sources

• Tubular neighborhood theorem; M. Hirsch, Differential Topology; J. Lee, Introduction to Smooth Manifolds; Lean states smooth-retraction corollary for closed embedding into EuclideanSpace ℝ (Fin n) via Opens.

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.