Squared distance from almost every point is a Morse function on an immersed manifold

Let i : M → V be an immersion of a second-countable boundaryless finite-dimensional manifold into a finite-dimensional real inner product space. For almost every point a ∈ V, with respect to any Haar measure, the squared distance x ↦ ‖i x - a‖² has only nondegenerate critical points: for a C² immersion every critical point is nondegenerate (TauCeti.ae_forall_isManifoldNondegenerateCriticalPoint_norm_sq_sub_comp), and for a smooth immersion the squared distance is a Morse function (TauCeti.ae_isMorse_norm_sq_sub_comp).

No closedness or properness of i is needed for genericity. When i is a closed embedding the squared distance is moreover proper (TauCeti.isProperMap_norm_sq_sub_comp), and together these give a proper Morse exhaustion of M bounded below. For a holomorphic immersion of a complex manifold its critical points also have real Morse index at most the complex dimension (TauCeti.manifoldMorseIndex_norm_sq_sub_comp_le), which is Milnor's route to the homotopy type of affine varieties and Stein manifolds.

The proof reads i in countably many charts, where TauCeti.ae_hasNondegenerateCriticalPointsOn_norm_sq_sub_comp applies, and transfers criticality and nondegeneracy between those charts and the preferred charts of the manifold.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, §6, Theorem 6.6, and §7.

theorem TauCeti.ae_forall_isManifoldNondegenerateCriticalPoint_norm_sq_sub_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [SecondCountableTopology M] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {i : M → V} (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] (hi : ContMDiff I (modelWithCornersSelf ℝ V) 2 i) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% i x)) : ∀ᵐ (a : V) ∂μ, ∀ x ∈ criticalPoints I fun (y : M) => ‖i y - a‖ ^ 2, IsManifoldNondegenerateCriticalPoint I (fun (y : M) => ‖i y - a‖ ^ 2) x

The squared distance from almost every point has nondegenerate critical points along a C² immersion. If i : M → V is C² with injective differential everywhere, then for almost every a ∈ V, with respect to any Haar measure μ, every critical point of x ↦ ‖i x - a‖² is nondegenerate.

theorem TauCeti.ae_isMorse_norm_sq_sub_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [SecondCountableTopology M] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {i : M → V} (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] (hi : ContMDiff I (modelWithCornersSelf ℝ V) (↑⊤) i) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% i x)) : ∀ᵐ (a : V) ∂μ, IsMorse I fun (y : M) => ‖i y - a‖ ^ 2

The squared distance from almost every point is a Morse function on a smoothly immersed manifold. If i : M → V is smooth with injective differential everywhere, then for almost every a ∈ V, with respect to any Haar measure μ, the function x ↦ ‖i x - a‖² is Morse.