The Morse index on a smooth manifold

This file defines the preferred-extended-chart Morse index by applying TauCeti.morseIndex to a function's coordinate expression in the preferred extended chart.

Following TauCeti.IsManifoldNondegenerateCriticalPoint, the definition itself assumes no smoothness and no boundarylessness. The results below prove that it depends only on the germ of the function, and that it is unchanged when the model space is transported through a continuous linear equivalence. The model-space comparison theorem makes the construction reduce exactly to the existing calculus definition. This file does not compare the preferred chart with arbitrary manifold charts.

When the preferred-chart Hessian is nondegenerate, the indices of a function and its negation add to the dimension of the model space. At a local minimum of a C² function on a boundaryless manifold, the index vanishes without a nondegeneracy assumption.

Main declarations

• TauCeti.manifoldMorseIndex: the Morse index in the preferred manifold chart.
• TauCeti.manifoldMorseIndex_congr_of_eventuallyEq: the index depends only on the germ of the function.
• TauCeti.manifoldMorseIndex_modelSpace: comparison with TauCeti.morseIndex on a normed vector space.
• TauCeti.manifoldMorseIndex_eq_zero_of_isLocalMin: the index vanishes at a local minimum of a C² function on a boundaryless manifold.
• TauCeti.manifoldMorseIndex_transContinuousLinearEquiv: invariance under an equivalent choice of model space.
• TauCeti.manifoldMorseIndex_neg_add_manifoldMorseIndex_eq_finrank: the complementary-index formula under nondegeneracy of the preferred-chart Hessian.
• IsManifoldNondegenerateCriticalPoint.manifoldMorseIndex_neg_add_manifoldMorseIndex_eq_finrank: the critical-point specialization.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.
• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 2.

noncomputable def TauCeti.manifoldMorseIndex {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) : ℕ

The Morse index of a real-valued function at a point of a smooth manifold: the negative index of inertia of the Hessian of its expression in the preferred extended chart.

As with TauCeti.morseIndex and TauCeti.IsManifoldNondegenerateCriticalPoint, the definition carries no smoothness or boundary hypotheses and is available at every point. It is specifically the index computed in the preferred extended chart; the results below prove germ locality and invariance under transport of the model by a continuous linear equivalence. For a model with boundary or corners the unconstrained Hessian can depend on the behaviour of the chart inverse off range I, and it is not the boundary Morse condition, which is a different theory.

theorem TauCeti.manifoldMorseIndex_def {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} : manifoldMorseIndex I f x = morseIndex (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

The manifold Morse index is the Morse index of the preferred coordinate expression.

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

The manifold Morse index depends only on the germ of the function at the point.

@[simp]

theorem TauCeti.manifoldMorseIndex_modelSpace {V : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] {g : V → ℝ} {v : V} : manifoldMorseIndex (modelWithCornersSelf ℝ V) g v = morseIndex g v

On a normed vector space with its self-model manifold structure, the manifold Morse index is the ordinary Morse index.

theorem TauCeti.manifoldMorseIndex_le_finrank {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} : manifoldMorseIndex I f x ≤ Module.finrank ℝ E

The manifold Morse index is at most the dimension of the model space.

theorem TauCeti.manifoldMorseIndex_eq_zero_of_isLocalMin {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [I.Boundaryless] (hf : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 f x) (hmin : IsLocalMin f x) : manifoldMorseIndex I f x = 0

At a local minimum of a C² function on a boundaryless manifold, the preferred-chart Morse index is zero. No nondegeneracy assumption is needed.

theorem TauCeti.manifoldMorseIndex_transContinuousLinearEquiv {E : Type u_1} {E' : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} (e : E ≃L[ℝ] E') : manifoldMorseIndex (I.transContinuousLinearEquiv e) f x = manifoldMorseIndex I f x

The manifold Morse index is unchanged when the manifold model is transported through a continuous linear equivalence.

theorem TauCeti.manifoldMorseIndex_neg_add_manifoldMorseIndex_eq_finrank {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} (h : QuadraticMap.Nondegenerate) : manifoldMorseIndex I (-f) x + manifoldMorseIndex I f x = Module.finrank ℝ E

If the preferred-chart Hessian is nondegenerate, the manifold Morse indices of a function and its negation add to the dimension of the model space.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.manifoldMorseIndex_neg_add_manifoldMorseIndex_eq_finrank {E : Type u_1} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} (h : IsManifoldNondegenerateCriticalPoint I f x) : manifoldMorseIndex I (-f) x + manifoldMorseIndex I f x = Module.finrank ℝ E

At a nondegenerate critical point, the Morse indices of a function and its negation add to the dimension of the manifold.