The cells of a critical level form a relative CW complex

Milnor's cell attachment theorem (TauCeti.IsMorse.exists_sublevel_union_cells_deformation) says that, for small ε > 0, the sublevel M_{c+ε} = {f ≤ c + ε} of a Morse function strong deformation retracts onto the lower sublevel M_{c-ε} = {f ≤ c - ε} together with one disc at each critical point of the level c: in a normalized Morse chart φ of index λ, in which f = c - Σ_{j < λ} yⱼ² + Σ_{j ≥ λ} yⱼ², the disc is {‖y‖² ≤ ε, yⱼ = 0 for j ≥ λ}. This file shows that these discs are the cells of a relative CW complex over M_{c-ε}, so that M_{c+ε} has the homotopy type of M_{c-ε} with one λ-cell attached at each critical point of index λ.

The characteristic map of the cell of a chart φ is OpenPartialHomeomorph.morseCellMap: on the Euclidean unit disc of ℝ^λ it sends w to the point of chart coordinates (√ε • w, 0), with w in the first λ coordinates. On the boundary sphere f = c - ε, so the attaching map lands in M_{c-ε}, while f > c - ε on the open disc, which is therefore disjoint from M_{c-ε}. Mathlib's classical Topology.RelCWComplex takes characteristic maps on the closed unit ball of the sup norm, which is carried onto the Euclidean disc by the radial homeomorphism ContinuousLinearEquiv.unitBallHomeomorph; read back on the Euclidean disc 𝔻 λ through TauCeti.cellDiskHom, the characteristic map is again OpenPartialHomeomorph.morseCellMap (TauCeti.coe_cellDiskHom_morseRelCWComplex).

The construction is purely topological: it uses only charts φ i that are open partial homeomorphisms to ℝⁿ with pairwise disjoint sources, the normal form of a continuous f in them, and the containment of the closed ball of radius √ε in their targets.

Main definitions

• TauCeti.morseRelCWComplex: the finite relative CW complex M_{c-ε} ∪ ⋃ cells over M_{c-ε}, with one k i-cell for each chart φ i.

Main results

• TauCeti.finite_morseRelCWComplex: the relative CW complex TauCeti.morseRelCWComplex is finite.
• TauCeti.cellFrontier_morseRelCWComplex_subset: each of its cells is attached along the base M_{c-ε}.
• TauCeti.IsMorse.exists_relCWComplex_sublevel_deformation: Milnor's cell attachment theorem in CW form. Across a value c of a Morse function with a compact band around it, the sublevel M_{c+ε} strong deformation retracts onto a finite CW complex relative to M_{c-ε} whose m-cells correspond to the critical points of index m on the level c, each attached along M_{c-ε}.

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Theorem 3.2 and Remark 3.3.

@[instance_reducible]

noncomputable def TauCeti.morseRelCWComplex {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) : Topology.RelCWComplex ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}) {x : M | f x ≤ c - ε}

The cells of a critical level form a relative CW complex. Let φ i be charts of M into ℝⁿ with pairwise disjoint sources, each containing the closed ball of radius √ε in its target, in which a continuous f has the normal form c - Σ_{j < k i} yⱼ² + Σ_{j ≥ k i} yⱼ². Then the lower sublevel {f ≤ c - ε} with the discs {‖y‖² ≤ ε, yⱼ = 0 for j ≥ k i} of the charts attached is a finite CW complex relative to {f ≤ c - ε}, with one k i-cell for each i (TauCeti.morseRelCWComplexCellEquiv), whose characteristic map is OpenPartialHomeomorph.morseCellMap (TauCeti.coe_map_morseRelCWComplex).

noncomputable def TauCeti.morseRelCWComplexCellEquiv {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) (m : ℕ) : Topology.RelCWComplex.cell ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}) m ≃ { i : ι // k i = m }

The m-cells of TauCeti.morseRelCWComplex are the charts φ i with k i = m.

instance TauCeti.finite_morseRelCWComplex {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) : Topology.RelCWComplex.Finite ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0})

TauCeti.morseRelCWComplex is a finite relative CW complex: its cells have dimension at most n and there are finitely many charts.

@[simp]

theorem TauCeti.coe_map_morseRelCWComplex {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) (m : ℕ) (j : Topology.RelCWComplex.cell ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}) m) : ↑(Topology.RelCWComplex.map m j) = (φ ↑((morseRelCWComplexCellEquiv hfc φ hφ k hk hε hball hf m) j)).morseCellMap ⋯ ε ∘ ⇑(EuclideanSpace.equiv (Fin m) ℝ).unitBallHomeomorph.symm

The characteristic map of the m-cell of TauCeti.morseRelCWComplex at the chart φ i is OpenPartialHomeomorph.morseCellMap precomposed with the radial homeomorphism from the closed unit ball of the sup norm onto the Euclidean disc.

theorem TauCeti.coe_cellDiskHom_morseRelCWComplex {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) [T2Space M] (m : ℕ) (j : Topology.RelCWComplex.cell ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}) m) (z : ↑(TopCat.disk m)) : ↑((CategoryTheory.ConcreteCategory.hom (cellDiskHom j)) z) = (φ ↑((morseRelCWComplexCellEquiv hfc φ hφ k hk hε hball hf m) j)).morseCellMap ⋯ ε ↑z.down

Read on the Euclidean disc 𝔻 m through TauCeti.cellDiskHom, the characteristic map of the m-cell of TauCeti.morseRelCWComplex at the chart φ i is OpenPartialHomeomorph.morseCellMap: it sends w to the point of chart coordinates (√ε • w, 0).

theorem TauCeti.cellFrontier_morseRelCWComplex_subset {M : Type u} [TopologicalSpace M] {n : ℕ} {ι : Type u} [Finite ι] {f : M → ℝ} {c ε : ℝ} (hfc : Continuous f) (φ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hφ : Pairwise (Function.onFun Disjoint fun (i : ι) => (φ i).source)) (k : ι → ℕ) (hk : ∀ (i : ι), k i ≤ n) (hε : 0 < ε) (hball : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ i).target) (hf : ∀ (i : ι), ∀ y ∈ (φ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ i) y).ofLp j ^ 2) (m : ℕ) (j : Topology.RelCWComplex.cell ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (φ i).source ∩ ↑(φ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}) m) : Topology.RelCWComplex.cellFrontier m j ⊆ {x : M | f x ≤ c - ε}

Every cell of TauCeti.morseRelCWComplex is attached along the base: the boundary sphere of each cell lies on the level f = c - ε, in the lower sublevel {f ≤ c - ε}.

theorem TauCeti.IsMorse.exists_relCWComplex_sublevel_deformation {E : Type u_1} {H : Type u_2} {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {c δ : ℝ} (hf : IsMorse I f) (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) : ∃ (ε : ℝ), 0 < ε ∧ ε ≤ δ ∧ ∃ (C : Set M) (x : Topology.RelCWComplex C {x : M | f x ≤ c - ε}) (_ : Topology.RelCWComplex.Finite C) (hC : C ⊆ {x : M | f x ≤ c + ε}), (∀ (m : ℕ), Nonempty (Topology.RelCWComplex.cell C m ≃ { p : ↑(criticalPoints I f ∩ f ⁻¹' {c}) // manifoldMorseIndex I f ↑p = m })) ∧ (∀ (m : ℕ) (j : Topology.RelCWComplex.cell C m), Topology.RelCWComplex.cellFrontier m j ⊆ {x : M | f x ≤ c - ε}) ∧ ∃ (r : C(↑{x : M | f x ≤ c + ε}, ↑C)), (∀ (x : ↑C), r ((ContinuousMap.inclusion hC) x) = x) ∧ Nonempty (((ContinuousMap.inclusion hC).comp r).HomotopyRel (ContinuousMap.id ↑{x : M | f x ≤ c + ε}) {x : ↑{x : M | f x ≤ c + ε} | ↑x ∈ C})

Milnor's cell attachment theorem in CW form. Let f be a Morse function and c a value with a compact band f⁻¹[c - δ, c + δ]. Then for some 0 < ε ≤ δ the sublevel {f ≤ c + ε} strong deformation retracts onto a finite CW complex C ⊆ {f ≤ c + ε} relative to the lower sublevel {f ≤ c - ε}, whose m-cells correspond to the critical points of index m on the level c. The complex is TauCeti.morseRelCWComplex built from normalized Morse charts at these critical points.