The square of the mod-two Morse boundary counts broken trajectories

For critical points p and r whose Morse indices differ by two, a broken trajectory from p to r is a pair of trajectories, from p to a critical point q of the intermediate index and from q to r. Representing each component by its point on the middle level between its endpoints, the broken trajectories form the set TauCeti.morseBrokenTrajectorySet of triples (q, z₁, z₂).

Under the compact-sublevel and Morse--Smale hypotheses of the mod-two Morse boundary ∂, this set is finite, and the r-coefficient of ∂ (∂ p) is its cardinality modulo two. Consequently ∂ ∘ ∂ = 0 holds exactly when every set of broken index-two trajectories has even cardinality. This isolates the algebraic half of ∂² = 0; the geometric half, that broken trajectories are the boundary of a compact one-dimensional manifold of trajectories and therefore come in pairs, requires the compactification and gluing of index-two trajectory spaces and is not proved here.

Main declarations

• TauCeti.morseBoundaryCoeff_eq_ncard: for consecutive indices, the boundary coefficient is the parity of the middle-level trajectory slice, with no condition on the critical values.
• TauCeti.morseBrokenTrajectorySet: the broken index-two trajectories from p to r.
• TauCeti.finite_morseBrokenTrajectorySet_of_isCompact_sublevel: there are finitely many.
• TauCeti.morseBoundary_morseBoundaryOnGenerator_apply: the coefficients of ∂ (∂ p) count broken trajectories modulo two.
• TauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff: ∂ ∘ ∂ = 0 exactly when every set of broken trajectories has even cardinality.

Reference

M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 4 (the Morse complex): the proof that ∂ ∘ ∂ = 0 counts the coefficient of r in ∂ (∂ p) as the number of broken trajectories from p to r.

noncomputable def TauCeti.morseBrokenTrajectorySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (p r : E) : Set (MorseCriticalPoint f × E × E)

The broken index-two trajectories from p to r: triples (q, z₁, z₂) of a critical point q whose Morse index lies one below that of p and one above that of r, a point z₁ on the middle-level slice of trajectories from p to q, and a point z₂ on the middle-level slice of trajectories from q to r.

@[simp]

theorem TauCeti.mem_morseBrokenTrajectorySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} {p r : E} {x : MorseCriticalPoint f × E × E} : x ∈ morseBrokenTrajectorySet hf p r ↔ morseIndex f p = morseIndex f ↑x.1 + 1 ∧ morseIndex f ↑x.1 = morseIndex f r + 1 ∧ x.2.1 ∈ morseTrajectorySlice hf p ↑x.1 ∧ x.2.2 ∈ morseTrajectorySlice hf (↑x.1) r

Membership in the set of broken index-two trajectories.

theorem TauCeti.value_lt_of_mem_morseTrajectorySlice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfd : Differentiable ℝ f) {hf : LipschitzWith K (gradient f)} {p q z : E} (hpq : p ≠ q) (hz : z ∈ morseTrajectorySlice hf p q) : f q < f p

A point of the middle-level slice between distinct endpoints forces the critical value to drop strictly.

theorem TauCeti.value_lt_of_mem_morseBrokenTrajectorySet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfd : Differentiable ℝ f) {hf : LipschitzWith K (gradient f)} {p r : E} {x : MorseCriticalPoint f × E × E} (hx : x ∈ morseBrokenTrajectorySet hf p r) : f ↑x.1 < f p

The intermediate critical point of a broken trajectory has strictly smaller critical value than its source.

theorem TauCeti.finite_morseBrokenTrajectorySet_of_isCompact_sublevel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hM : HasNondegenerateCriticalPointsOn f Set.univ) (hcompact : ∀ (c : ℝ), IsCompact {z : E | f z ≤ c}) (htr : IsMorseSmale f hf) (p r : MorseCriticalPoint f) : (morseBrokenTrajectorySet hf ↑p ↑r).Finite

There are finitely many broken index-two trajectories between two critical points, under the compact-sublevel and Morse--Smale hypotheses of the Morse boundary.

theorem TauCeti.morseBoundaryCoeff_eq_ncard {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hM : HasNondegenerateCriticalPointsOn f Set.univ) (hcompact : ∀ (c : ℝ), IsCompact {z : E | f z ≤ c}) (htr : IsMorseSmale f hf) {p q : MorseCriticalPoint f} (hind : morseIndex f ↑p = morseIndex f ↑q + 1) : morseBoundaryCoeff hfs hf hM hcompact htr p q = ↑(morseTrajectorySlice hf ↑p ↑q).ncard

For critical points of consecutive index, the boundary coefficient is the cardinality of the middle-level trajectory slice modulo two. No comparison of critical values is needed: when the value does not drop, the slice is empty.

theorem TauCeti.morseBoundary_morseBoundaryOnGenerator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hM : HasNondegenerateCriticalPointsOn f Set.univ) (hcompact : ∀ (c : ℝ), IsCompact {z : E | f z ≤ c}) (htr : IsMorseSmale f hf) (p r : MorseCriticalPoint f) : ((morseBoundary hfs hf hM hcompact htr) (morseBoundaryOnGenerator hfs hf hM hcompact htr p)) r = ↑(morseBrokenTrajectorySet hf ↑p ↑r).ncard

The r-coefficient of the boundary of the boundary of p is the number of broken index-two trajectories from p to r, modulo two.

theorem TauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hM : HasNondegenerateCriticalPointsOn f Set.univ) (hcompact : ∀ (c : ℝ), IsCompact {z : E | f z ≤ c}) (htr : IsMorseSmale f hf) : morseBoundary hfs hf hM hcompact htr ∘ₗ morseBoundary hfs hf hM hcompact htr = 0 ↔ ∀ (p r : MorseCriticalPoint f), Even (morseBrokenTrajectorySet hf ↑p ↑r).ncard

The mod-two Morse boundary squares to zero exactly when, between any two critical points, the number of broken index-two trajectories is even.