Squared distance on complex manifolds

For a holomorphic map i from a complex manifold to a complex inner product space, the Levi form of x ↦ ‖i x - a‖² is the pullback of the ambient Hermitian metric by the actual complex manifold derivative of i. In particular, it is positive definite at every immersion point, independently of the center a.

At a critical point the resulting intrinsic real Hessian identity bounds the real Morse index by the complex dimension. Combining this index bound with Haar genericity of squared-distance Morse functions along smooth immersions (TauCeti.ae_isMorse_norm_sq_sub_comp) shows that for a smooth holomorphic immersion of a second-countable complex manifold into a finite-dimensional complex inner product space and almost every center a, y ↦ ‖i y - a‖² is a real Morse function whose critical points all have index at most finrank ℂ E (TauCeti.ae_isMorse_and_manifoldMorseIndex_norm_sq_sub_comp_le, TauCeti.exists_isMorse_and_manifoldMorseIndex_norm_sq_sub_comp_le).

Along the inclusion of an open subset, squared distance is strictly plurisubharmonic at every point (TauCeti.isManifoldStrictlyPlurisubharmonicAt_norm_sq_sub_subtypeVal).

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.

The calculation uses TauCeti.manifoldLeviForm_comp_apply and TauCeti.leviForm_norm_sq.

@[simp]

theorem TauCeti.manifoldLeviForm_norm_sq_sub_comp_apply {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) (v w : E) : ((manifoldLeviForm E (fun (y : M) => ‖i y - a‖ ^ 2) x) v) w = inner ℂ ((d% i x) v) ((d% i x) w)

The Levi form of squared distance along a holomorphic map is the pullback of the ambient Hermitian metric.

theorem TauCeti.re_manifoldLeviForm_norm_sq_sub_comp_apply_self {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) (v : E) : (((manifoldLeviForm E (fun (y : M) => ‖i y - a‖ ^ 2) x) v) v).re = ‖(d% i x) v‖ ^ 2

The Levi diagonal of squared distance is the squared norm of the complex tangent map.

@[simp]

theorem TauCeti.isManifoldStrictlyPlurisubharmonicAt_norm_sq_sub_comp_iff {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) : IsManifoldStrictlyPlurisubharmonicAt E (fun (y : M) => ‖i y - a‖ ^ 2) x ↔ Function.Injective ⇑(d% i x)

Squared distance along a holomorphic map is strictly plurisubharmonic exactly at its immersion points.

theorem TauCeti.contMDiffAt_norm_sq_sub_comp {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) : ContMDiffAt (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) 2 (fun (y : M) => ‖i y - a‖ ^ 2) x

Squared distance along a complex C² map is real C².

theorem TauCeti.criticalHessian_norm_sq_sub_comp_add_I_smul {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) (v : E) : ((criticalHessian (modelWithCornersSelf ℝ E) (fun (y : M) => ‖i y - a‖ ^ 2) x) v) v + ((criticalHessian (modelWithCornersSelf ℝ E) (fun (y : M) => ‖i y - a‖ ^ 2) x) (Complex.I • v)) (Complex.I • v) = 4 * ‖(d% i x) v‖ ^ 2

The sum of the real Hessian on a complex tangent vector and its rotation by I is four times the squared norm of the tangent map. The Hessian here is computed in the preferred chart; at a critical point it is intrinsic.

theorem TauCeti.hessianQuadraticForm_norm_sq_sub_comp_add_I_smul_of_mem_maximalAtlas {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) 2 M) (hx : x ∈ e.source) (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) (hcrit : (d% fun (y : M) => ‖i y - a‖ ^ 2) x = 0) (v : E) : (hessianQuadraticForm ((fun (y : M) => ‖i y - a‖ ^ 2) ∘ ↑e.symm) (↑e x)) ((d% ↑e x) v) + (hessianQuadraticForm ((fun (y : M) => ‖i y - a‖ ^ 2) ∘ ↑e.symm) (↑e x)) ((d% ↑e x) (Complex.I • v)) = 4 * ‖(d% i x) v‖ ^ 2

At a critical point, the squared-distance Hessian identity can be computed in any real C² chart, including charts which are not holomorphic. The two tangent vectors in that chart are transported by its actual real manifold derivative.

theorem TauCeti.manifoldMorseIndex_norm_sq_sub_comp_le {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} {x : M} {a : F} [FiniteDimensional ℂ E] [IsManifold (modelWithCornersSelf ℂ E) 2 M] (hi : ContMDiffAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) 2 i x) (hinj : Function.Injective ⇑(d% i x)) (hcrit : (d% fun (y : M) => ‖i y - a‖ ^ 2) x = 0) : manifoldMorseIndex (modelWithCornersSelf ℝ E) (fun (y : M) => ‖i y - a‖ ^ 2) x ≤ Module.finrank ℂ E

At a critical point of squared distance along a holomorphic immersion, the real Morse index is at most the complex dimension of the source.

theorem TauCeti.isManifoldStrictlyPlurisubharmonicAt_norm_sq_sub_subtypeVal {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (U : TopologicalSpace.Opens F) (a : F) (x : ↥U) : IsManifoldStrictlyPlurisubharmonicAt F (fun (y : ↥U) => ‖↑y - a‖ ^ 2) x

Along the inclusion of an open subset of a complex inner product space, the squared distance from any point is strictly plurisubharmonic at every point.

theorem TauCeti.ae_isMorse_and_manifoldMorseIndex_norm_sq_sub_comp_le {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} [FiniteDimensional ℂ E] [FiniteDimensional ℂ F] [IsManifold (modelWithCornersSelf ℂ E) (↑⊤) M] [SecondCountableTopology M] [MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] (hi : ContMDiff (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) (↑⊤) i) (hinj : ∀ (x : M), Function.Injective ⇑(d% i x)) : ∀ᵐ (a : F) ∂μ, (IsMorse (modelWithCornersSelf ℝ E) fun (y : M) => ‖i y - a‖ ^ 2) ∧ ∀ x ∈ criticalPoints (modelWithCornersSelf ℝ E) fun (y : M) => ‖i y - a‖ ^ 2, manifoldMorseIndex (modelWithCornersSelf ℝ E) (fun (y : M) => ‖i y - a‖ ^ 2) x ≤ Module.finrank ℂ E

Generic low-index squared-distance Morse functions on a holomorphically immersed manifold. For a smooth holomorphic immersion i : M → F of a second-countable complex manifold into a finite-dimensional complex inner product space and almost every a ∈ F (with respect to any Haar measure μ), y ↦ ‖i y - a‖ ^ 2 is a real Morse function on M whose critical points all have Morse index at most finrank ℂ E.

theorem TauCeti.exists_isMorse_and_manifoldMorseIndex_norm_sq_sub_comp_le {E : Type u_1} {F : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] {i : M → F} [FiniteDimensional ℂ E] [FiniteDimensional ℂ F] [IsManifold (modelWithCornersSelf ℂ E) (↑⊤) M] [SecondCountableTopology M] (hi : ContMDiff (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) (↑⊤) i) (hinj : ∀ (x : M), Function.Injective ⇑(d% i x)) : ∃ (a : F), (IsMorse (modelWithCornersSelf ℝ E) fun (y : M) => ‖i y - a‖ ^ 2) ∧ ∀ x ∈ criticalPoints (modelWithCornersSelf ℝ E) fun (y : M) => ‖i y - a‖ ^ 2, manifoldMorseIndex (modelWithCornersSelf ℝ E) (fun (y : M) => ‖i y - a‖ ^ 2) x ≤ Module.finrank ℂ E

Existence of a low-index squared-distance Morse function on a holomorphically immersed manifold.