Squared distance from almost every point is Morse along an immersion

Let F : E → V be a C² map from an open subset U of a finite-dimensional real normed space into a finite-dimensional real inner product space, whose differential is injective at every point of U. For almost every point a of V, with respect to any Haar measure, every critical point in U of the squared distance u ↦ ‖F u - a‖² is nondegenerate (TauCeti.ae_hasNondegenerateCriticalPointsOn_norm_sq_sub_comp). This is the genericity that makes the squared distance from a point a Morse function on an immersed or embedded submanifold of Euclidean space; combined with properness along closed embeddings, it gives the Morse exhaustions used to build CW models of affine varieties and Stein manifolds.

The proof is local. Near a point u₀, let R be the image of the differential of F at u₀. The orthogonal projection of F to R is a local diffeomorphism, so in its coordinate w ∈ R the map becomes the graph F = w + h(w) with h(w) ∈ Rᗮ (ContDiffOn.exists_openPartialHomeomorph_starProjection). Writing a = b + c with b ∈ R and c ∈ Rᗮ, Pythagoras (Submodule.norm_sub_add_sq_of_mem_of_mem_orthogonal) gives

‖F - a‖² = (‖w‖² + ‖h(w) - c‖²) - 2⟪b, w⟫ + ‖b‖².

This is a family of functions of w, depending smoothly on the parameter c, perturbed by the linear form 2⟪b, ·⟫; the joint genericity of such perturbations, TauCeti.ae_hasNondegenerateCriticalPointsOn_sub_prod, shows that almost every (b, c) gives only nondegenerate critical points. Countably many such neighbourhoods cover U.

Main results

• TauCeti.ae_hasNondegenerateCriticalPointsOn_norm_sq_sub_comp: for almost every a, the squared distance from a along a C² immersion has only nondegenerate critical points.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, §6, Theorem 6.6, which proves the same genericity through the focal points of the normal bundle.
• V. Guillemin and A. Pollack, Differential Topology, Prentice-Hall, 1974, Chapter 1, §7, for the reduction to linear perturbations in graph coordinates.

theorem TauCeti.ae_hasNondegenerateCriticalPointsOn_norm_sq_sub_comp {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {F : E → V} {U : Set E} [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] (hU : IsOpen U) (hF : ContDiffOn ℝ 2 F U) (hinj : ∀ u ∈ U, Function.Injective ⇑(fderiv ℝ F u)) : ∀ᵐ (a : V) ∂μ, HasNondegenerateCriticalPointsOn (fun (u : E) => ‖F u - a‖ ^ 2) U

The squared distance from almost every point is Morse along an immersion. If F is C² on the open set U and its differential is injective at every point of U, then for almost every a ∈ V, with respect to any Haar measure μ, every critical point in U of u ↦ ‖F u - a‖² is nondegenerate.