The Morse lemma on a smooth manifold #
At a nondegenerate critical point x of a smooth function f on a boundaryless smooth manifold
modelled on a finite-dimensional real normed space E, there is a chart of the maximal atlas,
centred at x, in which f is a nondegenerate quadratic form: after a linear change of
coordinates L : E ≃ (Fin n → ℝ),
f y = f x + (1/2) Σᵢ wᵢ (L (ψ y))ᵢ², with every wᵢ = ±1,
and the number of negative weights is the manifold Morse index of f at x. Such a chart is
recorded as a TauCeti.MorseChart. A Morse chart puts the function in quadratic form; it is
used to choose an adapted pseudo-gradient field that is linear near the critical point, whose
stable and unstable manifolds are then studied.
Main declarations #
TauCeti.MorseChart: a chart centred at a critical point in which the function is a diagonal nondegenerate quadratic form.TauCeti.MorseChart.restr: the restriction of a Morse chart to an open neighbourhood of its centre.TauCeti.MorseChart.splitCoord: the coordinates of a Morse chart, split by the sign of the weight.TauCeti.MorseChart.splitCoordL: the split coordinates as a continuous linear equivalence of the model.TauCeti.MorseChart.max_norm_fst_norm_snd_splitCoord: the sup norm of the coordinates is the larger of the norms of the two factors of the split coordinates.TauCeti.MorseChart.apply_toChart_symm_coord_symm_splitCoord_symm: the Morse normal form in split coordinates.TauCeti.MorseChart.lt_apply_of_norm_fst_eq,TauCeti.MorseChart.apply_lt_of_norm_snd_eq:fis abovef xwhere the contracting split coordinate dominates and belowf xwhere the expanding one dominates.TauCeti.MorseChart.finrank_snd_splitCoordandTauCeti.MorseChart.finrank_fst_splitCoord_add_manifoldMorseIndex: the expanding factor of the split coordinates has dimension the Morse index, and the contracting factor the complementary dimension.TauCeti.MorseChart.neg: a Morse chart forfis a Morse chart for-f, with the opposite weights.TauCeti.IsManifoldNondegenerateCriticalPoint.nonempty_morseChart: the Morse lemma on a manifold, for a function smooth near the critical point.TauCeti.IsMorse.nonempty_morseChart: every critical point of a Morse function has a Morse chart.
References #
- M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Theorem 1.3.1.
A Morse chart for f at x: a chart of the maximal atlas, centred at x, together with
a linear change of coordinates L : E ≃ (Fin n → ℝ) and weights wᵢ = ±1, such that on the source
of the chart f y = f x + (1/2) Σᵢ wᵢ (L (ψ y))ᵢ². The number of negative weights is the manifold
Morse index of f at x.
- toChart : OpenPartialHomeomorph M E
The chart.
The linear change of coordinates that diagonalizes the Hessian.
- weight : Fin (Module.finrank ℝ E) → ℝ
The diagonal weights of the Hessian.
- ncard_weight_neg : {i : Fin (Module.finrank ℝ E) | self.weight i < 0}.ncard = manifoldMorseIndex (modelWithCornersSelf ℝ E) f x
Instances For
The restriction of a Morse chart to an open neighbourhood s of its centre: the chart is
restricted to s, and the coordinates and weights are unchanged.
Instances For
The chart of a restricted Morse chart is the restricted chart.
Restricting a Morse chart does not change its coordinates.
Restricting a Morse chart does not change its weights.
The source of a restricted Morse chart.
A point of the chart is the point with its own coordinates.
The chart sends 0 back to the critical point.
The centre is the only point of the source sent to 0.
The critical point is the point with coordinates 0.
The chart of a Morse chart lies in the maximal atlas of class C¹.
The chart of a Morse chart is differentiable on its source.
A space with a Morse chart is finite-dimensional.
A coordinate of a Morse chart has weight different from 1 exactly when it has negative
weight.
A coordinate of a Morse chart has weight 1 exactly when it has positive weight.
The split coordinates of a Morse chart: the pair formed by the coordinates of positive
weight and the remaining coordinates, of weight -1. Each factor carries the sup norm.
Instances For
The first factor of the split coordinates consists of the coordinates of positive weight.
The second factor of the split coordinates consists of the coordinates of negative weight.
The coordinates of a point given in split coordinates.
The sup norm of the coordinates of a Morse chart is the larger of the norms of the two factors
of the split coordinates. So the coordinate cube ‖z‖ ≤ ε is the box ‖u‖ ≤ ε, ‖v‖ ≤ ε of the
split model.
The expanding factor of the split coordinates of a Morse chart has dimension the Morse index.
The contracting and expanding factors of the split coordinates of a Morse chart have complementary dimensions.
The Morse normal form in split coordinates. At the point with split coordinates (u, v),
f = f x + (Σᵢ uᵢ² - Σⱼ vⱼ²) / 2.
On the box, the split coordinates read a point of the chart.
The point with given split coordinates determines them.
Above the critical value on the entrance face. At a point of the chart whose contracting
split coordinate has norm ε and whose expanding one is small, f exceeds f x.
Below the critical value on the exit face. At a point of the chart whose expanding split
coordinate has norm ε and whose contracting one is small, f is less than f x.
A Morse chart for f at a nondegenerate critical point is a Morse chart for -f, with the
opposite weights.
Instances For
The negated Morse chart has the same chart.
The negated Morse chart has the same coordinates.
The negated Morse chart has the opposite weights.
The split coordinates of a Morse chart, as a continuous linear equivalence of the model.
Instances For
The continuous split coordinates of a point of the model are the split coordinates of its coordinates.
The point of the model with given continuous split coordinates.
The Morse lemma on a manifold. At a nondegenerate critical point x of a function f
that is smooth at every point of a neighbourhood of x, on a manifold modelled on a
finite-dimensional real normed space E, there is a Morse chart: a chart ψ of the maximal atlas,
centred at x, and a linear change of coordinates L : E ≃ (Fin n → ℝ) such that on the source
of ψ
f y = f x + (1/2) Σᵢ wᵢ (L (ψ y))ᵢ²,
where every weight wᵢ is -1 or 1 and the number of negative weights is the manifold Morse
index of f at x.
Every critical point of a Morse function has a Morse chart.