Morse functions on smooth manifolds

This file lifts nondegenerate critical points and Morse functions from normed spaces to smooth manifolds without boundary. A critical point is nondegenerate when the coordinate expression of the function in the preferred extended chart has a nondegenerate critical point in the sense of TauCeti.IsNondegenerateCriticalPoint. The latter notion is invariant under smooth changes of coordinates, so this is the usual intrinsic definition.

IsMorseOn I f s additionally requires f to be smooth on s and every critical point in s to be nondegenerate. The smoothness condition is what distinguishes a Morse function from the weaker normed-space predicate HasNondegenerateCriticalPointsOn, which deliberately imposes no regularity away from critical points. On a normed vector space, the manifold definitions reduce exactly to the existing calculus definitions.

This is the manifold-level starting point for Morse homology: stable and unstable manifolds, Morse--Smale trajectory spaces, and the Morse differential are attached to a Morse function on a manifold, rather than to a function on one global coordinate space.

Main declarations

• TauCeti.IsManifoldNondegenerateCriticalPoint: a nondegenerate critical point of a real-valued function on a smooth manifold.
• TauCeti.IsManifoldNondegenerateCriticalPoint.contMDiffAt: such a function is C² at the point.
• TauCeti.IsMorseOn: a smooth function whose critical points in a set are nondegenerate.
• TauCeti.IsMorse: a Morse function on the whole manifold.
• TauCeti.isManifoldNondegenerateCriticalPoint_modelSpace_iff and TauCeti.isMorseOn_modelSpace_iff: comparison with the normed-space definitions.

The definition follows Audin--Damian, Morse Theory and Floer Homology, Chapter 1.

def TauCeti.IsManifoldNondegenerateCriticalPoint {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) : Prop

A point x is a nondegenerate critical point of f when, in the preferred extended chart at x, the coordinate expression of f has a nondegenerate critical point. As with mfderiv and ContMDiff, the definition carries no smoothness or boundary hypotheses; it is the intended chart-independent notion when I.Boundaryless and IsManifold I ∞ M hold, and results relying on intrinsic meaning assume these. For models with boundary the unconstrained Hessian is not the boundary Morse condition, which is a different theory.

theorem TauCeti.isManifoldNondegenerateCriticalPoint_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} (I : ModelWithCorners ℝ E H) : IsManifoldNondegenerateCriticalPoint I f x ↔ IsNondegenerateCriticalPoint (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

The coordinate characterization of a nondegenerate critical point.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.contMDiffAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} {I : ModelWithCorners ℝ E H} (h : IsManifoldNondegenerateCriticalPoint I f x) : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 f x

A function with a nondegenerate critical point is C² there.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} {I : ModelWithCorners ℝ E H} (h : IsManifoldNondegenerateCriticalPoint I f x) : IsManifoldNondegenerateCriticalPoint I (-f) x

Negating a function preserves its nondegenerate critical points.

@[simp]

theorem TauCeti.isManifoldNondegenerateCriticalPoint_neg_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} {I : ModelWithCorners ℝ E H} : IsManifoldNondegenerateCriticalPoint I (-f) x ↔ IsManifoldNondegenerateCriticalPoint I f x

Being a nondegenerate critical point is invariant under negating the function.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.congr_of_eventuallyEq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f g : M → ℝ} {x : M} {I : ModelWithCorners ℝ E H} (h : IsManifoldNondegenerateCriticalPoint I f x) (hfg : f =ᶠ[nhds x] g) : IsManifoldNondegenerateCriticalPoint I g x

Nondegeneracy of a critical point depends only on the germ of the function there.

@[simp]

theorem TauCeti.isManifoldNondegenerateCriticalPoint_modelSpace_iff {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : V → ℝ} {v : V} : IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ V) h v ↔ IsNondegenerateCriticalPoint h v

On a normed vector space with its self-model manifold structure, a manifold nondegenerate critical point is exactly a nondegenerate critical point in the existing calculus sense.

def TauCeti.IsMorseOn {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → ℝ) (s : Set M) : Prop

A function is Morse on s when it is smooth there and every critical point in s is a nondegenerate critical point. Criticality is tested in the same preferred coordinates used by IsManifoldNondegenerateCriticalPoint; on a vector space this is exactly fderiv ℝ f x = 0.

theorem TauCeti.isMorseOn_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} : IsMorseOn I f s ↔ ContMDiffOn I (modelWithCornersSelf ℝ ℝ) (↑⊤) f s ∧ ∀ x ∈ s, fderiv ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0 → IsManifoldNondegenerateCriticalPoint I f x

The introduction and elimination rule for a function being Morse on a set.

theorem TauCeti.IsMorseOn.contMDiffOn {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f s) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) (↑⊤) f s

A function which is Morse on a set is smooth there.

theorem TauCeti.IsMorseOn.isManifoldNondegenerateCriticalPoint {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {x : M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f s) (hx : x ∈ s) (hcrit : fderiv ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0) : IsManifoldNondegenerateCriticalPoint I f x

Every critical point of a function which is Morse on s is a nondegenerate critical point.

theorem TauCeti.IsMorseOn.differentiableAt_comp_extChartAt_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {x : M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f s) (hx : x ∈ s) : DifferentiableAt ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

The coordinate expression of a function which is Morse on s is differentiable at the chart image of every point of s: either the point is not critical, so the derivative is nonzero, or it is a nondegenerate critical point, where the coordinate expression is twice continuously differentiable.

theorem TauCeti.IsMorseOn.mono {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s t : Set M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f t) (hst : s ⊆ t) : IsMorseOn I f s

The restriction of a Morse function to a smaller set is Morse there.

theorem TauCeti.isMorseOn_of_forall_exists_mem_nhds {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} (h : ∀ x ∈ s, ∃ t ∈ nhds x, IsMorseOn I f t) : IsMorseOn I f s

Being Morse is a local property: a function is Morse on s if each point of s has a neighbourhood on which it is Morse.

theorem TauCeti.IsMorseOn.congr {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f g : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f s) (hs : IsOpen s) (hfg : Set.EqOn g f s) : IsMorseOn I g s

A function which agrees on an open set with a function Morse there is Morse there.

theorem TauCeti.IsMorseOn.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} (h : IsMorseOn I f s) : IsMorseOn I (-f) s

Negating a function preserves the property of being Morse on a set.

@[simp]

theorem TauCeti.isMorseOn_neg_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {s : Set M} {I : ModelWithCorners ℝ E H} : IsMorseOn I (-f) s ↔ IsMorseOn I f s

Being Morse on a set is invariant under negating the function.

@[simp]

theorem TauCeti.isMorseOn_modelSpace_iff {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : V → ℝ} {u : Set V} : IsMorseOn (modelWithCornersSelf ℝ V) h u ↔ ContDiffOn ℝ (↑⊤) h u ∧ HasNondegenerateCriticalPointsOn h u

On a normed vector space, being Morse on s means being smooth on s and having nondegenerate critical points there in the existing calculus sense.

def TauCeti.IsMorse {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → ℝ) : Prop

A Morse function is a function which is Morse on the whole manifold.

@[simp]

theorem TauCeti.isMorseOn_univ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} : IsMorseOn I f Set.univ ↔ IsMorse I f

Being Morse on the whole manifold is being a Morse function.

@[simp]

theorem TauCeti.isMorseOn_empty {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} : IsMorseOn I f ∅

Every function is Morse on the empty set.

theorem TauCeti.isMorse_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} : IsMorse I f ↔ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f ∧ ∀ (x : M), fderiv ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0 → IsManifoldNondegenerateCriticalPoint I f x

A function is Morse exactly when it is smooth and all of its critical points are nondegenerate.

theorem TauCeti.IsMorse.contMDiff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} (h : IsMorse I f) : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f

A Morse function is smooth.

theorem TauCeti.IsMorse.isManifoldNondegenerateCriticalPoint {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} {I : ModelWithCorners ℝ E H} (h : IsMorse I f) (hcrit : fderiv ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = 0) : IsManifoldNondegenerateCriticalPoint I f x

Every critical point of a Morse function is a nondegenerate critical point.

theorem TauCeti.IsMorse.isManifoldNondegenerateCriticalPoint_of_mfderiv_eq_zero {E : Type u_1} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace M] {f : M → ℝ} [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (hf : IsMorse (modelWithCornersSelf ℝ E) f) {x : M} (hx : mfderiv% f x = 0) : IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ E) f x

A point where the derivative of a Morse function vanishes is a nondegenerate critical point.

theorem TauCeti.IsMorse.isMorseOn {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} (h : IsMorse I f) (s : Set M) : IsMorseOn I f s

A Morse function is Morse on every subset.

theorem TauCeti.IsMorse.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} (h : IsMorse I f) : IsMorse I (-f)

Negating a Morse function gives a Morse function.

@[simp]

theorem TauCeti.isMorse_neg_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {I : ModelWithCorners ℝ E H} : IsMorse I (-f) ↔ IsMorse I f

Being Morse is invariant under negating the function.

@[simp]

theorem TauCeti.isMorse_modelSpace_iff {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : V → ℝ} : IsMorse (modelWithCornersSelf ℝ V) h ↔ ContDiff ℝ (↑⊤) h ∧ HasNondegenerateCriticalPointsOn h Set.univ

On a normed vector space, a Morse function is exactly a smooth function all of whose critical points are nondegenerate in the existing calculus sense.