Normalized Morse charts #
A TauCeti.MorseChart writes a function near a nondegenerate critical point as
f y = f x + (1/2) Σᵢ wᵢ (L (ψ y))ᵢ² with unordered weights wᵢ = ±1. This file reorders
the coordinates so that the negative weights come first, divides by √2, and takes Euclidean
coordinates. The result is a partial diffeomorphism ψ onto an open subset of
EuclideanSpace ℝ (Fin m), m = dim M, centred at the critical point, in which
f y = f x - Σ_{i < λ} (ψ y)ᵢ² + Σ_{i ≥ λ} (ψ y)ᵢ²
on the whole source, where λ is the manifold Morse index. Through the boundaryless model
transport this holds for every boundaryless model, not only for self-modelled manifolds. This is
the coordinate form in which handles are attached to sublevel sets.
As a first application, a nondegenerate critical point of index 0 is a strict local minimum,
and one of index dim M is a strict local maximum. For every other index, there are curves
through the critical point, smooth near the parameter 0, along which f takes values below and
above the critical value; in dimension two this is the index-one saddle model
f = f x - u² + v².
Main declarations #
TauCeti.MorseChart.normalizedCoord: the reordered, rescaled Euclidean coordinates of a Morse chart.TauCeti.MorseChart.normalizedChart: a Morse chart as a partial diffeomorphism into Euclidean space, withTauCeti.MorseChart.eq_quadratic_normalizedChartits sum-of-squares equation.TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart: the normalized Morse lemma on a manifold with an arbitrary boundaryless model.TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart_subset: a normalized Morse chart with source inside a prescribed neighbourhood of the critical point.TauCeti.exists_pairwise_disjoint_normalized_morseCharts: normalized Morse charts with pairwise disjoint sources at finitely many nondegenerate critical points of a Hausdorff manifold.TauCeti.IsManifoldNondegenerateCriticalPoint.exists_twoDimensional_saddleChart: the index-one normal form in dimension two.TauCeti.IsManifoldNondegenerateCriticalPoint.exists_saddleCurves: curves through a critical point of index strictly between0anddim M, smooth near it, along which the function is below and above its critical value.TauCeti.IsManifoldNondegenerateCriticalPoint.eventually_lt_of_manifoldMorseIndex_eq_zeroandTauCeti.IsManifoldNondegenerateCriticalPoint.eventually_lt_of_manifoldMorseIndex_eq_finrank: strict local extrema at critical points of extreme index.
References #
- J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Lemma 2.2 and Corollary 2.3.
Sorting the coordinates of a Morse chart by weight puts the λ negative weights first,
where λ is the Morse index.
The normalized linear coordinates of a Morse chart: the coordinates L of the chart, sorted
so that the negative weights come first, divided by √2, and read in Euclidean space.
Instances For
The i-th normalized coordinate is the σ i-th chart coordinate divided by √2, where σ
sorts the weights increasingly.
In normalized coordinates the quadratic form (1/2) Σᵢ wᵢ (L v)ᵢ² of a Morse chart is the
signed sum of squares of its Morse index.
A Morse chart in normalized coordinates, as a partial diffeomorphism onto an open subset of
Euclidean space. In these coordinates f is f x plus the signed sum of squares of its Morse
index (TauCeti.MorseChart.eq_quadratic_normalizedChart).
Instances For
The normalized chart has the same source as the Morse chart.
The target of the normalized chart is the target of the Morse chart in normalized coordinates.
The normalized chart is the Morse chart followed by the normalized linear coordinates.
The inverse of the normalized chart undoes the normalized coordinates, then the chart.
The normalized chart is centred at the critical point.
The critical point is the only point of the source with normalized coordinates 0.
The normalized Morse lemma. On the whole source of a Morse chart,
f y = f x - Σ_{i < λ} (ψ y)ᵢ² + Σ_{i ≥ λ} (ψ y)ᵢ² in the normalized chart ψ, where λ is the
Morse index.
The normalized Morse lemma on a manifold. At a nondegenerate critical point x of a
function f which is smooth near x, on a manifold with a boundaryless model, there is a partial
diffeomorphism ψ onto an open subset of EuclideanSpace ℝ (Fin m), m = dim M, with
ψ x = 0 and
f y = f x - Σ_{i < λ} (ψ y)ᵢ² + Σ_{i ≥ λ} (ψ y)ᵢ²
on its whole source, where λ is the manifold Morse index of f at x.
The normalized Morse lemma in a prescribed neighbourhood. At a nondegenerate critical
point x of a function f which is smooth near x, every neighbourhood U of x contains the
source of a normalized Morse chart: a partial diffeomorphism ψ onto an open subset of
EuclideanSpace ℝ (Fin m), m = dim M, with ψ x = 0 and
f y = f x - Σ_{i < λ} (ψ y)ᵢ² + Σ_{i ≥ λ} (ψ y)ᵢ²
on its whole source, where λ is the manifold Morse index of f at x.
Disjoint normalized Morse charts. At finitely many nondegenerate critical points of a
function on a Hausdorff manifold, smooth near each of them, there are normalized Morse charts with
pairwise disjoint sources, each inside a prescribed neighbourhood of its centre. The charts are
indexed by the points of the finite set S.
The two-dimensional saddle normal form. At a nondegenerate critical point of index one
on a two-dimensional manifold, there are smooth Euclidean coordinates (u, v) centred at the
point in which f = f x - u² + v² on the whole chart source.
At a nondegenerate critical point whose Morse index is neither 0 nor dim M, there are two
curves through the critical point, smooth near the parameter 0, along which the function is
strictly below, respectively strictly above, its critical value at every sufficiently small nonzero
parameter. The curves are defined on all of ℝ.
At a nondegenerate critical point of Morse index 0 of a function smooth near it, on a
manifold with a boundaryless model, the function has a strict local minimum.
At a nondegenerate critical point of Morse index dim M of a function smooth near it, on a
manifold with a boundaryless model, the function has a strict local maximum.