Nondegenerate critical points of separated sums

A separated sum φ ∘ Prod.fst + ψ ∘ Prod.snd on a product E × F has block-diagonal second derivative, so its Hessian quadratic form at (a, b) is the orthogonal product of the Hessians of φ at a and of ψ at b. Consequently (a, b) is a nondegenerate critical point of the sum exactly when a and b are nondegenerate critical points of the summands, and the Morse index is additive. This is the calculus behind the product of two Morse functions on a product manifold, whose critical points are the pairs of critical points, graded by the sum of the indices.

Main declarations

• TauCeti.hessianQuadraticForm_comp_fst_add_comp_snd: the Hessian of a separated sum is the product of the Hessians of the summands.
• TauCeti.isNondegenerateCriticalPoint_comp_fst_add_comp_snd_iff and TauCeti.IsNondegenerateCriticalPoint.comp_fst_add_comp_snd: nondegenerate critical points of a separated sum are the pairs of nondegenerate critical points of the summands.
• TauCeti.morseIndex_comp_fst_add_comp_snd: the Morse index of a separated sum is the sum of the Morse indices of the summands.

References

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

@[simp]

theorem TauCeti.hessianQuadraticForm_comp_fst_add_comp_snd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {ψ : F → ℝ} {a : E} {b : F} (hφ : ContDiffAt ℝ 2 φ a) (hψ : ContDiffAt ℝ 2 ψ b) : hessianQuadraticForm (φ ∘ Prod.fst + ψ ∘ Prod.snd) (a, b) = QuadraticMap.prod (hessianQuadraticForm φ a) (hessianQuadraticForm ψ b)

The Hessian quadratic form of a separated sum at (a, b) is the orthogonal product of the Hessians of the summands at a and b.

@[simp]

theorem TauCeti.isNondegenerateCriticalPoint_comp_fst_add_comp_snd_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {ψ : F → ℝ} {a : E} {b : F} (hφ : ContDiffAt ℝ 2 φ a) (hψ : ContDiffAt ℝ 2 ψ b) : IsNondegenerateCriticalPoint (φ ∘ Prod.fst + ψ ∘ Prod.snd) (a, b) ↔ IsNondegenerateCriticalPoint φ a ∧ IsNondegenerateCriticalPoint ψ b

Nondegenerate critical points of a separated sum. For φ twice continuously differentiable at a and ψ twice continuously differentiable at b, the separated sum φ ∘ Prod.fst + ψ ∘ Prod.snd has a nondegenerate critical point at (a, b) exactly when φ has one at a and ψ has one at b.

theorem TauCeti.IsNondegenerateCriticalPoint.comp_fst_add_comp_snd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {ψ : F → ℝ} {a : E} {b : F} (hφ : IsNondegenerateCriticalPoint φ a) (hψ : IsNondegenerateCriticalPoint ψ b) : IsNondegenerateCriticalPoint (φ ∘ Prod.fst + ψ ∘ Prod.snd) (a, b)

A pair of nondegenerate critical points of φ and ψ is a nondegenerate critical point of the separated sum φ ∘ Prod.fst + ψ ∘ Prod.snd.

@[simp]

theorem TauCeti.morseIndex_comp_fst_add_comp_snd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} {ψ : F → ℝ} {a : E} {b : F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hφ : ContDiffAt ℝ 2 φ a) (hψ : ContDiffAt ℝ 2 ψ b) : morseIndex (φ ∘ Prod.fst + ψ ∘ Prod.snd) (a, b) = morseIndex φ a + morseIndex ψ b

The Morse index of a separated sum is additive: for φ twice continuously differentiable at a and ψ twice continuously differentiable at b, the index of φ ∘ Prod.fst + ψ ∘ Prod.snd at (a, b) is the sum of the indices of φ at a and of ψ at b.