Ambient charts for local Morse stable and unstable disks

The local stable and unstable sets of a negative-gradient equation are C¹ graphs over the positive and negative spectral subspaces of the Hessian. An explicit triangular change of ambient coordinates straightens each graph to its spectral subspace. The charts fix the critical displacement 0 and have identity derivative there, expressing tangency without a choice of basis.

The source and target are open cylinders over the parameter disk. The projection cutoff is strict inside these cylinders, so the statements describe the interiors of the local disks, not their boundaries. These are embedded local submanifold normal forms; transporting them along the flow, TauCeti.Analysis.Calculus.Morse.GlobalChart shows that the entire global stable and unstable sets are embedded. Displacements are centered at the critical point, as in IsNondegenerateCriticalPoint.localStableSet. The confinement radius is also chosen so that confined trajectories converge to the critical point, so the local disks lie in the global stable and unstable sets.

Main results

• IsNondegenerateCriticalPoint.exists_localStableSet_chart: a C¹ ambient chart whose stable-set slice is exactly the stable Hessian subspace.
• IsNondegenerateCriticalPoint.exists_localUnstableSet_chart: the backward-time counterpart.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localStableSet_chart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : ∃ r > 0, ∃ ρ > 0, ∃ (q : OpenPartialHomeomorph E E), q.source = ⇑h.stableProjection ⁻¹' Metric.ball 0 ρ ∧ q.target = ⇑h.stableProjection ⁻¹' Metric.ball 0 ρ ∧ ↑q 0 = 0 ∧ HasFDerivAt (↑q) (ContinuousLinearMap.id ℝ E) 0 ∧ (∀ z ∈ q.source, ContDiffAt ℝ 1 (↑q) z) ∧ (∀ z ∈ q.target, ContDiffAt ℝ 1 (↑q.symm) z) ∧ (∀ z ∈ q.source, z ∈ h.localStableSet r ρ ↔ ↑q z ∈ ⋯.stableLinearSubspace) ∧ ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Ici 0) → Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atTop (nhds 0)

The interior of a local stable disk admits a C¹ ambient straightening chart. The chart and its inverse are defined on the open cylinder over a positive-radius disk in the stable spectral subspace; the chart fixes zero and has identity derivative there. The confinement radius r is small enough that every forward trajectory confined to closedBall 0 r tends to the critical point, so the disk consists of points of the stable set.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localUnstableSet_chart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : ∃ r > 0, ∃ ρ > 0, ∃ (q : OpenPartialHomeomorph E E), q.source = ⇑h.unstableProjection ⁻¹' Metric.ball 0 ρ ∧ q.target = ⇑h.unstableProjection ⁻¹' Metric.ball 0 ρ ∧ ↑q 0 = 0 ∧ HasFDerivAt (↑q) (ContinuousLinearMap.id ℝ E) 0 ∧ (∀ z ∈ q.source, ContDiffAt ℝ 1 (↑q) z) ∧ (∀ z ∈ q.target, ContDiffAt ℝ 1 (↑q.symm) z) ∧ (∀ z ∈ q.source, z ∈ h.localUnstableSet r ρ ↔ ↑q z ∈ ⋯.unstableLinearSubspace) ∧ ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Iic 0) → Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atBot (nhds 0)

The interior of a local unstable disk admits a C¹ ambient straightening chart onto the unstable Hessian subspace, fixing zero with identity derivative. Its parameter dimension is the Morse index. Every backward trajectory confined to closedBall 0 r tends to the critical point in backward time.