Morse theory

DefinitionMorse quadratic form#✓fully proved

For natural numbers \(k\) and \(n\), the Morse quadratic form of index \(k\) on \(\mathbb{R}^n\), with coordinates \(v_0, \dots, v_{n-1}\), is the function \(Q_{k,n} \colon \mathbb{R}^n \to \mathbb{R}\) given by \(Q_{k,n}(v) = \sum_{i=0}^{n-1} \varepsilon_i v_i^2\), where \(\varepsilon_i = -1\) if \(i < k\) and \(\varepsilon_i = 1\) if \(i \ge k\). In particular, if \(k \ge n\) every coefficient is \(-1\).

def morseQuadratic (k n : ℕ) (v : EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ i : Fin n, (if (i : ℕ) < k then (-1 : ℝ) else 1) * (v i) ^ 2

Used by 7

Used bySmoothness of the Morse quadratic form · Morse function · Existence of Morse functions · Morse lemma · The Morse quadratic form when the index is at least the dimension · The Morse quadratic form vanishes at the origin · The Morse quadratic form of index zero

LemmaThe Morse quadratic form vanishes at the origin#✓fully proved

For all natural numbers \(k\) and \(n\), the Morse quadratic form \(Q_{k,n}\) of index \(k\) on \(\mathbb{R}^n\) satisfies \(Q_{k,n}(0) = 0\).

lemma morseQuadratic_zero (k n : ℕ) : morseQuadratic k n 0 = 0

Uses 1

Statement usesMorse quadratic form

LemmaSmoothness of the Morse quadratic form#✓fully proved

For all natural numbers \(k\) and \(n\), the Morse quadratic form \(Q_{k,n} \colon \mathbb{R}^n \to \mathbb{R}\) of index \(k\) is \(C^\infty\).

lemma contDiff_morseQuadratic (k n : ℕ) :
    ContDiff ℝ (⊤ : ℕ∞) (morseQuadratic k n)

Uses 1

Statement usesMorse quadratic form

LemmaThe Morse quadratic form of index zero#✓fully proved

For every natural number \(n\), the Morse quadratic form \(Q_{0,n}\) of index \(0\) on \(\mathbb{R}^n\) satisfies \(Q_{0,n}(v) = \|v\|^2\) for every \(v \in \mathbb{R}^n\), where \(\|v\|\) is the Euclidean norm of \(v\).

lemma morseQuadratic_zero_index (n : ℕ) (v : EuclideanSpace ℝ (Fin n)) :
    morseQuadratic 0 n v = ‖v‖ ^ 2

Uses 1

Statement usesMorse quadratic form

LemmaThe Morse quadratic form when the index is at least the dimension#✓fully proved

If \(n \le k\), then the Morse quadratic form \(Q_{k,n}\) of index \(k\) on \(\mathbb{R}^n\) satisfies \(Q_{k,n}(v) = -\|v\|^2\) for every \(v \in \mathbb{R}^n\), where \(\|v\|\) is the Euclidean norm of \(v\).

lemma morseQuadratic_of_le {k n : ℕ} (h : n ≤ k) (v : EuclideanSpace ℝ (Fin n)) :
    morseQuadratic k n v = -‖v‖ ^ 2

Uses 1

Statement usesMorse quadratic form

DefinitionMorse function#✓fully proved

Let \(M\) be a \(C^\infty\) manifold without boundary modelled on a real normed space of finite dimension \(d\). A function \(f \colon M \to \mathbb{R}\) is a Morse function if it is \(C^\infty\) and, for every critical point \(p\) of \(f\) (a point where the differential \(df_p\) is zero), there exist an integer \(0 \le k \le d\), a map \(\varphi \colon M \to \mathbb{R}^d\) that is a local \(C^\infty\) diffeomorphism at \(p\) with \(\varphi(p) = 0\), and an open set \(U\) containing \(p\) such that \(f(q) = f(p) + Q_k(\varphi(q))\) for all \(q \in U\). Here \(Q_k\) is the Morse quadratic form \(Q_k(y) = -y_1^2 - \dots - y_k^2 + y_{k+1}^2 + \dots + y_d^2\) on \(\mathbb{R}^d\).

def IsMorseFunction (f : M → ℝ) : Prop :=
  ContMDiff I (𝓘(ℝ, ℝ)) (⊤ : ℕ∞) f ∧
    ∀ p : M, mfderiv I (𝓘(ℝ, ℝ)) f p = 0 →
      ∃ (k : ℕ) (_ : k ≤ Module.finrank ℝ E)
        (φ : M → EuclideanSpace ℝ (Fin (Module.finrank ℝ E))),
        IsLocalDiffeomorphAt I (𝓘(ℝ, EuclideanSpace ℝ (Fin (Module.finrank ℝ E))))
            (⊤ : ℕ∞) φ p ∧
          φ p = 0 ∧
            ∃ (U : Set M) (_ : IsOpen U) (_ : p ∈ U),
              ∀ q ∈ U, f q = f p + morseQuadratic k (Module.finrank ℝ E) (φ q)

Uses 1 · Used by 1

Statement usesMorse quadratic form

Used byExistence of Morse functions

TheoremMorse lemma#✓fully proved

Let \(f \colon \mathbb{R}^n \to \mathbb{R}\) be a \(C^\infty\) function with \(Df(0) = 0\) whose Hessian at \(0\) is nondegenerate: if \(v \in \mathbb{R}^n\) satisfies \(D^2 f(0)(v, w) = 0\) for all \(w \in \mathbb{R}^n\), then \(v = 0\). Then there exist an integer \(0 \le k \le n\), a map \(\varphi \colon \mathbb{R}^n \to \mathbb{R}^n\) that is a local \(C^\infty\) diffeomorphism at \(0\) with \(\varphi(0) = 0\), and an open set \(U\) containing \(0\) such that \(f(x) = f(0) + Q_k(\varphi(x))\) for all \(x \in U\). Here \(Q_k\) is the Morse quadratic form \(Q_k(y) = -y_1^2 - \dots - y_k^2 + y_{k+1}^2 + \dots + y_n^2\) on \(\mathbb{R}^n\).

theorem morse_lemma
    {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (hcrit : fderiv ℝ f (0 : EuclideanSpace ℝ (Fin n)) = 0)
    (hHess : ∀ v : EuclideanSpace ℝ (Fin n),
      (∀ w : EuclideanSpace ℝ (Fin n),
        (fderiv ℝ (fderiv ℝ f) (0 : EuclideanSpace ℝ (Fin n)) v) w = 0) → v = 0) :
    ∃ (k : ℕ) (_hk : k ≤ n) (φ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)),
      IsLocalDiffeomorphAt (𝓘(ℝ, EuclideanSpace ℝ (Fin n)))
        (𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (⊤ : ℕ∞) φ (0 : EuclideanSpace ℝ (Fin n)) ∧
      φ (0 : EuclideanSpace ℝ (Fin n)) = 0 ∧
      ∃ (U : Set (EuclideanSpace ℝ (Fin n))) (_hU_open : IsOpen U)
        (_hU_mem : (0 : EuclideanSpace ℝ (Fin n)) ∈ U),
        ∀ x ∈ U, f x = f (0 : EuclideanSpace ℝ (Fin n)) + morseQuadratic k n (φ x)

Sources

• J. Milnor, Morse Theory, Ann. of Math. Studies 51 (1963) Lemma 2.2; M. Hirsch, Differential Topology; J. Lee, Intro to Smooth Manifolds, 2nd ed., Morse lemma; Lean states Euclidean origin finite-dimensional specialization with corrected nondegeneracy grouping (∀ w, (fderiv (fderiv f) 0 v) w = 0) → v = 0.

Uses 1 · Used by 1

Statement usesMorse quadratic form

Used byExistence of Morse functions

TheoremExistence of Morse functions#✓fully proved

Every Hausdorff, second-countable \(C^\infty\) manifold \(M\) without boundary, modelled on a finite-dimensional real normed space, admits a Morse function \(f \colon M \to \mathbb{R}\).

public theorem morse_function_exists
    {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]
    : ∃ f : M → ℝ, IsMorseFunction (I := I) f

Sources

• J. Milnor, Morse Theory, Ann. of Math. Studies 51 (1963); M. Hirsch, Differential Topology; J. Lee, Intro to Smooth Manifolds, 2nd ed.; Lean states boundaryless finite-dimensional second-countable specialization.

Uses 4

Statement usesMorse function

Proof usesMorse lemma · Morse quadratic form · Sard's theorem on open subsets of finite-dimensional spaces

DefinitionAlternating partial sum#✓fully proved

For a sequence \(a_0, a_1, a_2, \dots\) of natural numbers and \(k \in \mathbb{N}\), the alternating partial sum of \(a\) up to \(k\) is the integer \(\sum_{j=0}^{k} (-1)^{k-j} a_j\).

def alternatingPartialSum (a : ℕ → ℕ) (k : ℕ) : ℤ :=
  ∑ j ∈ Finset.range (k + 1), (-1 : ℤ) ^ (k - j) * (a j : ℤ)

Used by 1

Used byMorse inequalities

TheoremMorse inequalities#●ready to prove

Let \(M\) be a compact Hausdorff smooth manifold without boundary, modelled on a finite-dimensional real normed space, and let \(f : M \to \mathbb{R}\) be a Morse function: \(f\) is \(C^\infty\), has finitely many critical points, and the Hessian of \(f\) at each critical point, computed in the preferred chart, is a nondegenerate bilinear form. The Morse index of a critical point is the largest dimension of a subspace on which this Hessian is negative definite. For \(j \in \mathbb{N}\) let \(c_j\) be the number of critical points of \(f\) of Morse index \(j\), and let \(b_j\) be the dimension of the singular homology \(H_j(M; \mathbb{R})\) (taken to be \(0\) if infinite). Then for every \(k \in \mathbb{N}\),

\[\sum_{j=0}^{k} (-1)^{k-j} b_j \le \sum_{j=0}^{k} (-1)^{k-j} c_j.\]

public theorem_wanted morse_inequality
    {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]
    [CompactSpace M] [T2Space M] (f : M → ℝ) (_hf : IsMorseFunction I f) (k : ℕ) :
    alternatingPartialSum (bettiNumber M) k ≤
      alternatingPartialSum (morseCount I f) k

Sources

• M. Morse, The Calculus of Variations in the Large, AMS Colloq. Publ. 18 (1934). Listed as §40 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem morse_inequality of the lean-eval benchmark.

Uses 1

Statement usesAlternating partial sum

TheoremWeak Morse inequalities#●ready to prove

Let \(M\) be a compact Hausdorff smooth (\(C^\infty\)) manifold without boundary, modelled on a finite-dimensional real normed space, and let \(f \colon M \to \mathbb{R}\) be a Morse function, that is, a smooth function with finitely many critical points, all of them non-degenerate. Then for every \(k \in \mathbb{N}\) the \(k\)-th Betti number of \(M\), the real dimension of the singular homology \(H_k(M; \mathbb{R})\), is at most the number of critical points of \(f\) of Morse index \(k\).

public theorem_wanted weak_morse_inequality
    {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]
    [CompactSpace M] [T2Space M] (f : M → ℝ) (_hf : IsMorseFunction I f) (k : ℕ) :
    bettiNumber M k ≤ morseCount I f k

Sources

• M. Morse, The Calculus of Variations in the Large, AMS Colloq. Publ. 18 (1934). Listed as §40 additional statement in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem weak_morse_inequality of the lean-eval benchmark.

9 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.