The mod-two Morse boundary

This file defines the algebraic boundary obtained by counting isolated negative-gradient trajectories between critical points of consecutive Morse index. A trajectory is represented by its unique intersection with the middle level between its endpoints. Under compact-sublevel and Morse--Smale hypotheses, this slice is finite, so its cardinality modulo two is well-defined.

The boundary of one critical point is a finitely supported sum: every endpoint with nonzero coefficient is a critical point in the compact sublevel of the source. Extending this assignment linearly gives an endomorphism of the free ZMod 2-module on the critical points. Proving that this endomorphism squares to zero requires the compactification and gluing of index-two trajectory spaces and is not asserted here.

Main declarations

• TauCeti.MorseCriticalPoint: the type of nondegenerate critical points of a real-valued function.
• TauCeti.morseTrajectorySlice: the middle-level representatives of trajectories from p to q.
• TauCeti.morseTrajectoryCount: the cardinality modulo two of a finite trajectory slice.
• TauCeti.morseBoundaryOnGenerator: the finitely supported boundary of a critical point.
• TauCeti.morseBoundary: the linear extension to mod-two Morse chains.

Reference

M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 4 (the Morse complex).

@[reducible, inline]

abbrev TauCeti.MorseCriticalPoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) : Type u_1

A nondegenerate critical point of a real-valued function. These are the generators of the Morse chain module.

@[simp]

theorem TauCeti.MorseCriticalPoint.fderiv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (p : MorseCriticalPoint f) : fderiv ℝ f ↑p = 0

The differential vanishes at a Morse critical point.

theorem TauCeti.MorseCriticalPoint.isNondegenerate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (p : MorseCriticalPoint f) : IsNondegenerateCriticalPoint f ↑p

A Morse critical point is nondegenerate.

theorem TauCeti.finite_setOf_value_le_of_isCompact_sublevel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (hfs : ContDiff ℝ 2 f) (hM : HasNondegenerateCriticalPointsOn f Set.univ) (hcompact : ∀ (c : ℝ), IsCompact {z : E | f z ≤ c}) (c : ℝ) : {q : MorseCriticalPoint f | f ↑q ≤ c}.Finite

Under compact sublevels, only finitely many critical points have critical value at most c.

@[reducible, inline]

abbrev TauCeti.MorseChain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) : Type u_1

Mod-two Morse chains are finitely supported functions on the critical points.

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

The middle-level slice representing unparametrized negative-gradient trajectories from p to q. Every nonconstant trajectory crosses this level exactly once.

@[simp]

theorem TauCeti.mem_morseTrajectorySlice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} {p q z : E} : z ∈ morseTrajectorySlice hf p q ↔ z ∈ (negativeGradientFlow f hf).unstableSet p ∧ z ∈ (negativeGradientFlow f hf).stableSet q ∧ f z = (f p + f q) / 2

Membership in the middle-level trajectory slice.

theorem TauCeti.finite_morseTrajectorySlice_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}) {p q : E} (hp : IsNondegenerateCriticalPoint f p) (hq : IsNondegenerateCriticalPoint f q) (hind : morseIndex f p = morseIndex f q + 1) (hqp : f q < f p) (htr : IsMorseSmale f hf) : (morseTrajectorySlice hf p q).Finite

The canonical middle-level trajectory slice is finite for critical points of consecutive index under compact-sublevel and Morse--Smale hypotheses.

noncomputable def TauCeti.morseTrajectoryCount {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (p q : E) (hfinite : (morseTrajectorySlice hf p q).Finite) : ZMod 2

The mod-two count of a finite middle-level trajectory slice. The finiteness witness is an explicit argument so the definition cannot silently assign zero to an infinite slice.

theorem TauCeti.morseTrajectoryCount_eq_ncard {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (p q : E) (hfinite : (morseTrajectorySlice hf p q).Finite) : morseTrajectoryCount hf p q hfinite = ↑(morseTrajectorySlice hf p q).ncard

The trajectory count is the natural-number cardinality of the slice, reduced modulo two.

noncomputable def TauCeti.morseBoundaryCoeff {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) : ZMod 2

The coefficient of q in the mod-two boundary of p. It is zero unless the Morse index drops by one and the critical value strictly decreases; otherwise it counts the canonical middle-level trajectory slice modulo two.

theorem TauCeti.morseBoundaryCoeff_eq_trajectoryCount {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) (hqp : f ↑q < f ↑p) : morseBoundaryCoeff hfs hf hM hcompact htr p q = morseTrajectoryCount hf ↑p ↑q ⋯

When the endpoints have consecutive index and decreasing critical value, the boundary coefficient is the parity of the middle-level trajectory slice.

@[simp]

theorem TauCeti.morseBoundaryCoeff_eq_zero_of_morseIndex_ne_add_one {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 = 0

The boundary coefficient vanishes when the endpoint indices do not differ by one.

@[simp]

theorem TauCeti.morseBoundaryCoeff_eq_zero_of_value_le {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) (hqp : f ↑p ≤ f ↑q) : morseBoundaryCoeff hfs hf hM hcompact htr p q = 0

The boundary coefficient vanishes unless the critical value decreases.

theorem TauCeti.morseIndex_eq_add_one_of_morseBoundaryCoeff_ne_zero {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} (hcoeff : morseBoundaryCoeff hfs hf hM hcompact htr p q ≠ 0) : morseIndex f ↑p = morseIndex f ↑q + 1

A nonzero boundary coefficient can only join critical points whose indices differ by one.

theorem TauCeti.value_lt_of_morseBoundaryCoeff_ne_zero {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} (hcoeff : morseBoundaryCoeff hfs hf hM hcompact htr p q ≠ 0) : f ↑q < f ↑p

A nonzero boundary coefficient strictly decreases the critical value.

noncomputable def TauCeti.morseBoundaryOnGenerator {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 : MorseCriticalPoint f) : MorseChain f

The mod-two Morse boundary of one critical point, as a finitely supported sum of critical points.

@[simp]

theorem TauCeti.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 q : MorseCriticalPoint f) : (morseBoundaryOnGenerator hfs hf hM hcompact htr p) q = morseBoundaryCoeff hfs hf hM hcompact htr p q

The coefficient of a generator in the boundary is its mod-two trajectory count.

theorem TauCeti.morseIndex_eq_add_one_of_mem_support_morseBoundaryOnGenerator {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} (hq : q ∈ (morseBoundaryOnGenerator hfs hf hM hcompact htr p).support) : morseIndex f ↑p = morseIndex f ↑q + 1

Every generator in the support of a boundary has Morse index one below the source.

theorem TauCeti.value_lt_of_mem_support_morseBoundaryOnGenerator {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} (hq : q ∈ (morseBoundaryOnGenerator hfs hf hM hcompact htr p).support) : f ↑q < f ↑p

Every generator in the support of a boundary has smaller critical value than the source.

noncomputable def TauCeti.morseBoundary {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) : MorseChain f →ₗ[ZMod 2] MorseChain f

The mod-two Morse boundary, obtained by linearly extending the trajectory count on critical points.

@[simp]

theorem TauCeti.morseBoundary_single {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 : MorseCriticalPoint f) (a : ZMod 2) : (morseBoundary hfs hf hM hcompact htr) (Finsupp.single p a) = a • morseBoundaryOnGenerator hfs hf hM hcompact htr p

The Morse boundary sends a basis generator to its trajectory-counting boundary.

theorem TauCeti.morseBoundary_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) (c : MorseChain f) (q : MorseCriticalPoint f) : ((morseBoundary hfs hf hM hcompact htr) c) q = Finsupp.sum c fun (p : MorseCriticalPoint f) (a : ZMod 2) => a * morseBoundaryCoeff hfs hf hM hcompact htr p q

The q coefficient of a Morse boundary is the finite sum of the input coefficients times the trajectory counts from their generators to q.