Characteristic and attaching maps of Morse cells

Let ψ be a chart of M with values in ℝⁿ in which a function f has the normal form

f = c - Σ_{j < k} yⱼ² + Σ_{j ≥ k} yⱼ²,

and suppose the target of ψ contains the closed ball of radius √ε about 0, for some 0 < ε. When the centre of ψ is the only critical point of f in the compact region f⁻¹[c - ε, c + ε] and ε is small, Milnor's Morse Theory, Theorem 3.2, shows that passing the level c attaches, up to homotopy, the cell {‖y‖² ≤ ε, yⱼ = 0 for j ≥ k} of the negative coordinates, read in M through ψ. The constructions here use only the chart hypotheses. This file parametrizes that cell by the unit disc D^k ⊆ ℝᵏ:

χ(w) = ψ⁻¹(√ε • (w, 0)),

where (w, 0) ∈ ℝⁿ extends w by zero onto the first k coordinates. Then f (χ w) = c - ε ‖w‖², so χ maps the disc into the sublevel M_c = {f ≤ c} and its boundary sphere into the level f⁻¹(c - ε); a point of the disc is sent into the lower sublevel M_{c-ε} = {f ≤ c - ε} exactly when it lies on the boundary sphere. The map χ is injective on the disc, its image there is the cell, and it is a closed embedding of the disc into a Hausdorff M.

Bundled as morphisms of topological spaces, χ is the characteristic map (D^k, ∂D^k) → (M_{c+ε}, M_{c-ε}) of the cell and its restriction to the boundary sphere is the attaching map ∂D^k → M_{c-ε}. These are the maps out of which the comparison between M_{c-ε} with cells attached along the attaching maps and the sublevel M_{c+ε} is built, as the map induced on the pushout by the inclusion of M_{c-ε} and the characteristic maps.

Two normal-form charts of the same index may parametrize the cell differently. Suppose the characteristic map χ₁ of one is homotopic as a map of pairs to χ₀ ∘ g for the characteristic map χ₀ of the other and an orthogonal map g (in Milnor's comparison of two charts, the polar factor of the negative block of the transition). Then the attaching map α₁ is homotopic to α₀ ∘ g. If det g = 1, then g can be removed: it is joined to the identity in the special orthogonal group, so χ₁ is homotopic to χ₀ as a map of pairs, and the two attaching maps are homotopic. If the cell has index 1 and det g = -1, then g = -1, and α₁ is homotopic to α₀ composed with the swap of the two points of ∂D¹ = {-1, 1}. In every index, det g = -1 changes the sign of the attaching map in reduced homology (TauCeti.reducedSingularHomologyFunctor_map_morseAttachingMap_of_det_eq_neg_one).

Main definitions

• OpenPartialHomeomorph.morseCellMap: the parametrization w ↦ ψ⁻¹(√ε • (w, 0)) of the cell of a normal-form chart.
• OpenPartialHomeomorph.morseCharacteristicMap: the characteristic map D^k ⟶ M_{c+ε} of the cell.
• OpenPartialHomeomorph.morseAttachingMap: the attaching map ∂D^k ⟶ M_{c-ε} of the cell.

Main results

• OpenPartialHomeomorph.morseCellMap_image_closedBall: the image of the unit disc is the cell {‖ψ x‖² ≤ ε, (ψ x)ⱼ = 0 for j ≥ k}.
• OpenPartialHomeomorph.closedBall_inter_preimage_morseCellMap_sublevel: a point of the disc lands in M_{c-ε} exactly when it lies on the boundary sphere.
• OpenPartialHomeomorph.preimage_morseCharacteristicMap_sublevel: the characteristic map is a map of pairs (D^k, ∂D^k) → (M_{c+ε}, M_{c-ε}).
• OpenPartialHomeomorph.isClosedEmbedding_morseCharacteristicMap: the characteristic map is a closed embedding.
• OpenPartialHomeomorph.disjoint_range_morseCharacteristicMap: the cells of two charts with disjoint sources are disjoint.
• OpenPartialHomeomorph.morseAttachingMap_comp_sublevelInclusion: the attaching map is the restriction of the characteristic map to the boundary sphere.
• TauCeti.mapsTo_range_diskBoundaryInclusion_of_morseCharacteristicMap_le, TauCeti.mapsTo_range_diskBoundaryInclusion_of_homotopy_morseCharacteristicMap: for 0 < ε, a self-map h of the disc such that χ ∘ h sends the boundary sphere into the lower sublevel, for instance the end of a homotopy of maps of pairs, preserves the boundary sphere.
• TauCeti.homotopic_morseAttachingMap_diskBoundaryMap_comp: a homotopy of pairs from χ₁ to χ₀ ∘ g gives a homotopy from α₁ to α₀ ∘ g.
• TauCeti.exists_homotopy_morseCharacteristicMap_of_det_eq_one, TauCeti.homotopic_morseAttachingMap_of_det_eq_one: an orthogonal change of parametrization of determinant 1 is removed from a homotopy of characteristic maps, and the attaching maps are then homotopic.
• TauCeti.homotopic_morseAttachingMap_diskBoundaryNeg_comp_of_det_eq_neg_one: for a cell of index 1, an orthogonal change of parametrization of determinant -1 swaps the two attaching points.

References

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

noncomputable def OpenPartialHomeomorph.morseCellMap {M : Type u} [TopologicalSpace M] {n k : ℕ} (ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hk : k ≤ n) (ε : ℝ) (w : EuclideanSpace ℝ (Fin k)) : M

The parametrization w ↦ ψ⁻¹(√ε • (w, 0)) of the cell {‖y‖² ≤ ε, yⱼ = 0 for j ≥ k} of a chart ψ, where (w, 0) extends w ∈ ℝᵏ by zero onto the first k coordinates of ℝⁿ. On the unit disc it is the characteristic map of the cell; see OpenPartialHomeomorph.morseCellMap_image_closedBall.

theorem OpenPartialHomeomorph.morseCellMap_def {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hk : k ≤ n) (w : EuclideanSpace ℝ (Fin k)) : ψ.morseCellMap hk ε w = ↑ψ.symm (√ε • (LinearIsometry.piLpExtendByZero 2 ℝ ℝ (Fin.castLEEmb hk)) w)

OpenPartialHomeomorph.morseCellMap ψ hk ε w is ψ⁻¹(√ε • (w, 0)).

@[simp]

theorem OpenPartialHomeomorph.morseCellMap_zero {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hk : k ≤ n) : ψ.morseCellMap hk ε 0 = ↑ψ.symm 0

The centre of the cell is the centre ψ⁻¹ 0 of the chart.

theorem OpenPartialHomeomorph.morseCellMap_smul {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hk : k ≤ n) {a : ℝ} (ha : 0 ≤ a) (w : EuclideanSpace ℝ (Fin k)) : ψ.morseCellMap hk ε (a • w) = ψ.morseCellMap hk (ε * a ^ 2) w

Scaling the parameter of a characteristic disc rescales its width quadratically.

theorem OpenPartialHomeomorph.morseCellMap_mem_source {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hw : ‖w‖ ≤ 1) : ψ.morseCellMap hk ε w ∈ ψ.source

A point of the unit disc is sent into the source of the chart.

theorem OpenPartialHomeomorph.apply_morseCellMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hw : ‖w‖ ≤ 1) : ↑ψ (ψ.morseCellMap hk ε w) = √ε • (LinearIsometry.piLpExtendByZero 2 ℝ ℝ (Fin.castLEEmb hk)) w

In the chart, a point of the unit disc is sent to √ε • (w, 0).

theorem OpenPartialHomeomorph.apply_morseCellMap_apply_eq_zero {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hw : ‖w‖ ≤ 1) {j : Fin n} (hj : k ≤ ↑j) : (↑ψ (ψ.morseCellMap hk ε w)).ofLp j = 0

In the chart, the coordinates of a point of the cell vanish beyond the first k.

theorem OpenPartialHomeomorph.norm_apply_morseCellMap_sq {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hε : 0 ≤ ε) (hw : ‖w‖ ≤ 1) : ‖↑ψ (ψ.morseCellMap hk ε w)‖ ^ 2 = ε * ‖w‖ ^ 2

In the chart, the squared norm of the image of a point w of the unit disc is ε ‖w‖².

theorem OpenPartialHomeomorph.continuousOn_morseCellMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) : ContinuousOn (ψ.morseCellMap hk ε) (Metric.closedBall 0 1)

The parametrization of the cell is continuous on the unit disc.

theorem OpenPartialHomeomorph.injOn_morseCellMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hε : 0 < ε) : Set.InjOn (ψ.morseCellMap hk ε) (Metric.closedBall 0 1)

The parametrization of the cell is injective on the unit disc.

theorem OpenPartialHomeomorph.isClosedEmbedding_domRestrict_morseCellMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) [T2Space M] (hk : k ≤ n) (hε : 0 < ε) : Topology.IsClosedEmbedding ((Metric.closedBall 0 1).domRestrict (ψ.morseCellMap hk ε))

The parametrization of the cell is a closed embedding of the unit disc into a Hausdorff space.

theorem OpenPartialHomeomorph.morseCellMap_image_closedBall {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hk : k ≤ n) (hε : 0 < ε) : ψ.morseCellMap hk ε '' Metric.closedBall 0 1 = ψ.source ∩ ↑ψ ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k ≤ ↑j → y.ofLp j = 0}

The image of the unit disc is the cell {‖ψ x‖² ≤ ε, (ψ x)ⱼ = 0 for j ≥ k} of the chart.

theorem OpenPartialHomeomorph.apply_morseCellMap_eq_sub_mul_norm_sq {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (hw : ‖w‖ ≤ 1) : f (ψ.morseCellMap hk ε w) = c - ε * ‖w‖ ^ 2

Where f has the normal form c - Σ_{j < k} yⱼ² + Σ_{j ≥ k} yⱼ² in the chart, f takes the value c - ε ‖w‖² at the image of a point w of the unit disc.

theorem OpenPartialHomeomorph.apply_morseCellMap_le {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (hw : ‖w‖ ≤ 1) : f (ψ.morseCellMap hk ε w) ≤ c

The unit disc is sent into the sublevel {f ≤ c}.

theorem OpenPartialHomeomorph.apply_morseCellMap_of_norm_eq_one {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} {w : EuclideanSpace ℝ (Fin k)} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (hw : ‖w‖ = 1) : f (ψ.morseCellMap hk ε w) = c - ε

The boundary sphere of the unit disc is sent into the level f⁻¹(c - ε).

theorem OpenPartialHomeomorph.closedBall_inter_preimage_morseCellMap_sublevel {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 < ε) : Metric.closedBall 0 1 ∩ ψ.morseCellMap hk ε ⁻¹' {x : M | f x ≤ c - ε} = Metric.sphere 0 1

A point of the unit disc is sent into the lower sublevel {f ≤ c - ε} exactly when it lies on the boundary sphere.

noncomputable def OpenPartialHomeomorph.morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {f : M → ℝ} {c ε : ℝ} (ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hk : k ≤ n) (hε : 0 ≤ ε) (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) : TopCat.disk k ⟶ ↧↑{x : M | f x ≤ c + ε}

The characteristic map (D^k, ∂D^k) → (M_{c+ε}, M_{c-ε}) of the cell of a chart ψ in which f = c - Σ_{j < k} yⱼ² + Σ_{j ≥ k} yⱼ² and whose target contains the closed ball of radius √ε: the map w ↦ ψ⁻¹(√ε • (w, 0)) from the unit disc into the sublevel {f ≤ c + ε}.

noncomputable def OpenPartialHomeomorph.morseAttachingMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {f : M → ℝ} {c ε : ℝ} (ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hk : k ≤ n) (hε : 0 ≤ ε) (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) : TopCat.diskBoundary k ⟶ ↧↑{x : M | f x ≤ c - ε}

The attaching map ∂D^k → M_{c-ε} of the cell of a chart ψ in which f = c - Σ_{j < k} yⱼ² + Σ_{j ≥ k} yⱼ² and whose target contains the closed ball of radius √ε: the restriction of w ↦ ψ⁻¹(√ε • (w, 0)) to the unit sphere, which it maps into the level f⁻¹(c - ε).

@[simp]

theorem OpenPartialHomeomorph.coe_morseCharacteristicMap_apply {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (w : ↑(TopCat.disk k)) : ↑((CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk hε hball hf)) w) = ψ.morseCellMap hk ε ↑w.down

@[simp]

theorem OpenPartialHomeomorph.coe_morseAttachingMap_apply {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (w : ↑(TopCat.diskBoundary k)) : ↑((CategoryTheory.ConcreteCategory.hom (ψ.morseAttachingMap hk hε hball hf)) w) = ψ.morseCellMap hk ε ↑w.down

theorem OpenPartialHomeomorph.coe_morseCharacteristicMap_diskBoundaryInclusion {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) (s : ↑(TopCat.diskBoundary k)) : ↑((CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk hε hball hf)) ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) = ↑((CategoryTheory.ConcreteCategory.hom (ψ.morseAttachingMap hk hε hball hf)) s)

On the boundary sphere, the characteristic map of the cell is its attaching map. This is the pointwise form of OpenPartialHomeomorph.morseAttachingMap_comp_sublevelInclusion.

theorem OpenPartialHomeomorph.morseAttachingMap_comp_sublevelInclusion {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) : CategoryTheory.CategoryStruct.comp (ψ.morseAttachingMap hk hε hball hf) (TopCat.ofHom (TauCeti.sublevelInclusion f (c - ε) (c + ε) ⋯)) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion k) (ψ.morseCharacteristicMap hk hε hball hf)

The attaching map is the restriction of the characteristic map to the boundary sphere: the square formed with the inclusions ∂D^k ⊆ D^k and M_{c-ε} ⊆ M_{c+ε} commutes. This is the compatibility needed to glue the inclusion of M_{c-ε} and the characteristic map into a map out of M_{c-ε} with the cell attached.

theorem OpenPartialHomeomorph.morseAttachingMap_comp_sublevelInclusion_assoc {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 ≤ ε) {Z : TopCat} (h : ↧↑{x : M | f x ≤ c + ε} ⟶ Z) : CategoryTheory.CategoryStruct.comp (ψ.morseAttachingMap hk hε hball hf) (CategoryTheory.CategoryStruct.comp (TopCat.ofHom (TauCeti.sublevelInclusion f (c - ε) (c + ε) ⋯)) h) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion k) (CategoryTheory.CategoryStruct.comp (ψ.morseCharacteristicMap hk hε hball hf) h)

The attaching map is the restriction of the characteristic map to the boundary sphere: the square formed with the inclusions ∂D^k ⊆ D^k and M_{c-ε} ⊆ M_{c+ε} commutes. This is the compatibility needed to glue the inclusion of M_{c-ε} and the characteristic map into a map out of M_{c-ε} with the cell attached.

theorem OpenPartialHomeomorph.morseCharacteristicMap_injective {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 < ε) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf))

The characteristic map of the cell is injective.

theorem OpenPartialHomeomorph.isClosedEmbedding_morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) [T2Space M] (hk : k ≤ n) (hε : 0 < ε) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf))

The characteristic map of the cell is a closed embedding of the unit disc into the sublevel M_{c+ε}, when M is Hausdorff.

theorem OpenPartialHomeomorph.preimage_morseCharacteristicMap_sublevel {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 < ε) : ⇑(CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf)) ⁻¹' {x : ↑↧↑{x : M | f x ≤ c + ε} | f ↑x ≤ c - ε} = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k))

A point of the disc is sent by the characteristic map into the lower sublevel M_{c-ε} exactly when it lies on the boundary sphere: the characteristic map is a map of pairs (D^k, ∂D^k) → (M_{c+ε}, M_{c-ε}).

theorem OpenPartialHomeomorph.mem_range_diskBoundaryInclusion_of_morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 < ε) (v : ↑(TopCat.disk k)) (hv : (CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf)) v ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.ofHom (TauCeti.sublevelInclusion f (c - ε) (c + ε) ⋯)))) : v ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k))

A point of the disc carried by the characteristic map into the lower sublevel M_{c-ε}, viewed inside M_{c+ε}, lies on the boundary sphere.

theorem OpenPartialHomeomorph.disjoint_range_morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) {k' : ℕ} {ψ' : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} (hψ : Disjoint ψ.source ψ'.source) (hball' : Metric.closedBall 0 √ε ⊆ ψ'.target) (hf' : ∀ y ∈ ψ'.source, f y = c + ∑ j : Fin n, (if ↑j < k' then -1 else 1) * (↑ψ' y).ofLp j ^ 2) (hk : k ≤ n) (hk' : k' ≤ n) (hε : 0 ≤ ε) : Disjoint (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk hε hball hf))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (ψ'.morseCharacteristicMap hk' hε hball' hf')))

The cells of two charts with disjoint sources are disjoint.

theorem OpenPartialHomeomorph.range_morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n k : ℕ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {f : M → ℝ} {c ε : ℝ} (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) (hk : k ≤ n) (hε : 0 < ε) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf)) = {x : ↑{x : M | f x ≤ c + ε} | ↑x ∈ ψ.source ∩ ↑ψ ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k ≤ ↑j → y.ofLp j = 0}}

The image of the characteristic map is the cell {‖ψ x‖² ≤ ε, (ψ x)ⱼ = 0 for j ≥ k} of the chart, viewed in the sublevel M_{c+ε}.

theorem TauCeti.mapsTo_range_diskBoundaryInclusion_of_morseCharacteristicMap_le {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {k : ℕ} (hk : k ≤ n) (hε : 0 < ε) (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) {h : TopCat.disk k ⟶ TopCat.disk k} (hh : ∀ (s : ↑(TopCat.diskBoundary k)), f ↑((CategoryTheory.ConcreteCategory.hom (ψ.morseCharacteristicMap hk ⋯ hball hf)) ((CategoryTheory.ConcreteCategory.hom h) ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s))) ≤ c - ε) : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom h)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)))

A self-map of the disc whose composite with a characteristic map sends the boundary sphere into the lower sublevel preserves the boundary sphere. Let χ be the characteristic map of the cell of a normal-form chart, with 0 < ε. If h is a self-map of the disc such that χ ∘ h sends the boundary sphere into the lower sublevel M_{c-ε}, then h sends the boundary sphere into itself, so h is a self-map of the pair (D^k, ∂D^k).

theorem TauCeti.mapsTo_range_diskBoundaryInclusion_of_homotopy_morseCharacteristicMap {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {k : ℕ} (hk : k ≤ n) (hε : 0 < ε) (hball : Metric.closedBall 0 √ε ⊆ ψ.target) (hf : ∀ y ∈ ψ.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ y).ofLp j ^ 2) {h : TopCat.disk k ⟶ TopCat.disk k} {g : TopCat.disk k ⟶ ↧↑{x : M | f x ≤ c + ε}} (K : (TopCat.Hom.hom g).Homotopy (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp h (ψ.morseCharacteristicMap hk ⋯ hball hf)))) (hK : ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary k)), f ↑(K (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) ≤ c - ε) : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom h)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)))

A homotopy of maps of pairs into χ ∘ h forces h to preserve the boundary sphere. Let χ be the characteristic map of the cell of a normal-form chart, with 0 < ε, and let h be a self-map of the disc. If K is a homotopy from some map g : D^k → M_{c+ε} to χ ∘ h keeping the boundary sphere in the lower sublevel M_{c-ε}, then h sends the boundary sphere into itself. This is the form of the hypotheses of TauCeti.morseCellReattachment.

theorem TauCeti.exists_homotopy_morseCharacteristicMap_of_det_eq_one {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ₀ ψ₁ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {k : ℕ} (hk : k ≤ n) (hε : 0 ≤ ε) (hball₀ : Metric.closedBall 0 √ε ⊆ ψ₀.target) (hball₁ : Metric.closedBall 0 √ε ⊆ ψ₁.target) (hf₀ : ∀ y ∈ ψ₀.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₀ y).ofLp j ^ 2) (hf₁ : ∀ y ∈ ψ₁.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₁ y).ofLp j ^ 2) {g : EuclideanSpace ℝ (Fin k) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin k)} (hg : LinearMap.det ↑g.toLinearEquiv = 1) (K : (TopCat.Hom.hom (ψ₁.morseCharacteristicMap hk hε hball₁ hf₁)).Homotopy (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g.diskMap (ψ₀.morseCharacteristicMap hk hε hball₀ hf₀)))) (hK : ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary k)), f ↑(K (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) ≤ c - ε) : ∃ (K' : (TopCat.Hom.hom (ψ₁.morseCharacteristicMap hk hε hball₁ hf₁)).Homotopy (TopCat.Hom.hom (ψ₀.morseCharacteristicMap hk hε hball₀ hf₀))), ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary k)), f ↑(K' (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) ≤ c - ε

An orientation-preserving change of parametrization of a Morse cell can be removed. Let χ₀ and χ₁ be the characteristic maps of the cells of two normal-form charts of the same index k, and let g be a linear isometry of ℝᵏ with det g = 1. A homotopy of maps of pairs from χ₁ to χ₀ ∘ g, keeping the boundary sphere in the lower sublevel M_{c-ε}, can be replaced by a homotopy of maps of pairs from χ₁ to χ₀ with the same property. Then TauCeti.morseCellReattachment applies with the identity of the disc.

theorem TauCeti.homotopic_morseAttachingMap_diskBoundaryMap_comp {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ₀ ψ₁ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {k : ℕ} (hk : k ≤ n) (hε : 0 ≤ ε) (hball₀ : Metric.closedBall 0 √ε ⊆ ψ₀.target) (hball₁ : Metric.closedBall 0 √ε ⊆ ψ₁.target) (hf₀ : ∀ y ∈ ψ₀.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₀ y).ofLp j ^ 2) (hf₁ : ∀ y ∈ ψ₁.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₁ y).ofLp j ^ 2) {g : EuclideanSpace ℝ (Fin k) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin k)} (K : (TopCat.Hom.hom (ψ₁.morseCharacteristicMap hk hε hball₁ hf₁)).Homotopy (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g.diskMap (ψ₀.morseCharacteristicMap hk hε hball₀ hf₀)))) (hK : ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary k)), f ↑(K (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) ≤ c - ε) : (TopCat.Hom.hom (ψ₁.morseAttachingMap hk hε hball₁ hf₁)).Homotopic (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g.diskBoundaryMap (ψ₀.morseAttachingMap hk hε hball₀ hf₀)))

A homotopy of characteristic maps restricts to the attaching maps. If the characteristic map χ₁ of one normal-form chart is homotopic, as a map of pairs into (M_{c+ε}, M_{c-ε}), to χ₀ ∘ g for the characteristic map χ₀ of another chart of the same index and a linear isometry g, then the attaching map α₁ : ∂D^k → M_{c-ε} is homotopic to α₀ ∘ g, where g acts on the boundary sphere by LinearIsometryEquiv.diskBoundaryMap.

theorem TauCeti.homotopic_morseAttachingMap_of_det_eq_one {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ₀ ψ₁ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} {k : ℕ} (hk : k ≤ n) (hε : 0 ≤ ε) (hball₀ : Metric.closedBall 0 √ε ⊆ ψ₀.target) (hball₁ : Metric.closedBall 0 √ε ⊆ ψ₁.target) (hf₀ : ∀ y ∈ ψ₀.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₀ y).ofLp j ^ 2) (hf₁ : ∀ y ∈ ψ₁.source, f y = c + ∑ j : Fin n, (if ↑j < k then -1 else 1) * (↑ψ₁ y).ofLp j ^ 2) {g : EuclideanSpace ℝ (Fin k) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin k)} (hg : LinearMap.det ↑g.toLinearEquiv = 1) (K : (TopCat.Hom.hom (ψ₁.morseCharacteristicMap hk hε hball₁ hf₁)).Homotopy (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g.diskMap (ψ₀.morseCharacteristicMap hk hε hball₀ hf₀)))) (hK : ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary k)), f ↑(K (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion k)) s)) ≤ c - ε) : (TopCat.Hom.hom (ψ₁.morseAttachingMap hk hε hball₁ hf₁)).Homotopic (TopCat.Hom.hom (ψ₀.morseAttachingMap hk hε hball₀ hf₀))

Orientation-preserving changes of chart give homotopic attaching maps. If the characteristic map χ₁ of one normal-form chart is homotopic, as a map of pairs into (M_{c+ε}, M_{c-ε}), to χ₀ ∘ g for the characteristic map χ₀ of another chart of the same index and a linear isometry g with det g = 1, then the two attaching maps ∂D^k → M_{c-ε} are homotopic.

theorem TauCeti.homotopic_morseAttachingMap_diskBoundaryNeg_comp_of_det_eq_neg_one {M : Type u} [TopologicalSpace M] {n : ℕ} {f : M → ℝ} {c ε : ℝ} {ψ₀ ψ₁ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))} (hk : 1 ≤ n) (hε : 0 ≤ ε) (hball₀ : Metric.closedBall 0 √ε ⊆ ψ₀.target) (hball₁ : Metric.closedBall 0 √ε ⊆ ψ₁.target) (hf₀ : ∀ y ∈ ψ₀.source, f y = c + ∑ j : Fin n, (if ↑j < 1 then -1 else 1) * (↑ψ₀ y).ofLp j ^ 2) (hf₁ : ∀ y ∈ ψ₁.source, f y = c + ∑ j : Fin n, (if ↑j < 1 then -1 else 1) * (↑ψ₁ y).ofLp j ^ 2) {g : EuclideanSpace ℝ (Fin 1) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 1)} (hg : LinearMap.det ↑g.toLinearEquiv = -1) (K : (TopCat.Hom.hom (ψ₁.morseCharacteristicMap hk hε hball₁ hf₁)).Homotopy (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g.diskMap (ψ₀.morseCharacteristicMap hk hε hball₀ hf₀)))) (hK : ∀ (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary 1)), f ↑(K (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion 1)) s)) ≤ c - ε) : (TopCat.Hom.hom (ψ₁.morseAttachingMap hk hε hball₁ hf₁)).Homotopic (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (diskBoundaryNeg 1) (ψ₀.morseAttachingMap hk hε hball₀ hf₀)))

An orientation-reversing change of chart swaps the attaching points of a cell of index 1. If the characteristic map χ₁ of one normal-form chart of index 1 is homotopic, as a map of pairs into (M_{c+ε}, M_{c-ε}), to χ₀ ∘ g for the characteristic map χ₀ of another and a linear isometry g of ℝ with det g = -1, then the attaching map α₁ is homotopic to α₀ composed with the antipodal map of ∂D¹ = {-1, 1}, which swaps the two points.