Reattaching Morse cells along a homotopy of characteristic maps #
Passing a critical level c of a Morse function attaches one cell at each critical point on the
level (TauCeti.morseCellAttachment), but the attaching maps depend on the chosen normal-form
charts. This file compares the attachments built from two chart families φ₀ and φ₁ with the
same indices, following Milnor's Lemma 3.6.
Write M_a = {f ≤ a}, χⱼ i : (D^{k i}, ∂D^{k i}) → (M_{c+ε}, M_{c-ε}) for the characteristic
maps of the cells and αⱼ i for their attaching maps. Suppose given, for each chart index i, a
self-map h i of the pair (D^{k i}, ∂D^{k i}) and a homotopy of maps of pairs
K i : χ₁ i ≃ χ₀ i ∘ h i, that is, a homotopy whose restriction H i to the boundary sphere stays
in the lower sublevel M_{c-ε}. Then H i is a homotopy from α₁ i to α₀ i ∘ h i, and the
reattachment map
E : M_{c-ε} ∪_{α₁} ⨆ᵢ D^{k i} → M_{c-ε} ∪_{α₀} ⨆ᵢ D^{k i}
(TauCeti.morseCellReattachment) is the identity on M_{c-ε}, sends a point x of the disc of
i with ‖x‖ ≤ 1/2 to the point h i (2x) of the disc of i, and sends a point with
1/2 ≤ ‖x‖ to the point H i (2 - 2‖x‖, x/‖x‖) of M_{c-ε}. These pieces agree on the seam
‖x‖ = 1/2, because H i (1, ·) = α₀ i ∘ h i and h i preserves the boundary sphere, and on the
attaching sphere ‖x‖ = 1, because H i (0, ·) = α₁ i. It is the fiberwise reattachment map
TauCeti.fiberwiseCellReattachment over a point. When 0 < ε, any self-map h i of the
disc admitting such a homotopy K i preserves the boundary sphere: at the end of K i the sphere
is sent by χ₀ i ∘ h i into M_{c-ε}, which χ₀ i meets exactly on the sphere.
Composed with the handle-to-cell comparison Φ₀ : M_{c-ε} ∪_{α₀} ⨆ᵢ D^{k i} → M_{c+ε}
(TauCeti.morseCellComparison), the map E reads K i along the map
x ↦ (τ x, ρ x) from the disc to the cylinder I × D^{k i}, where τ x = 1 and ρ x = 2x for
‖x‖ ≤ 1/2 and τ x = 2 - 2‖x‖ and ρ x = x/‖x‖ for 1/2 ≤ ‖x‖. On the boundary sphere this
map is x ↦ (0, x), so the straight-line homotopy to x ↦ (0, x) in the convex cylinder fixes
the boundary sphere. Through K i, it gives a homotopy from Φ₀ ∘ E to Φ₁ relative to the
lower sublevel (TauCeti.homotopicRel_morseCellReattachment_comp_morseCellComparison), which is
the homotopy TauCeti.fiberwiseCellReattachmentHomotopy over a point.
Consequently, if g₀ is a left inverse of Φ₀, then E is homotopic to g₀ ∘ Φ₁ relative to the
lower sublevel. Milnor's cell attachment theorem supplies such left inverses for admissible charts
(TauCeti.exists_morseCellAttachment_deformation), with Φⱼ ∘ gⱼ homotopic to the identity
relative to the image of Φⱼ. From this:
Eis a homotopy equivalence whose homotopy inverse and both homotopies fix the lower sublevel;- the relative homotopy class of
Edoes not depend on the homotopiesK i; - for three chart families the reattachment maps compose up to homotopy relative to the lower sublevel.
Main definitions #
TauCeti.morseCellReattachment: the reattachment mapM_{c-ε} ∪_{α₁} ⨆ᵢ D^{k i} → M_{c-ε} ∪_{α₀} ⨆ᵢ D^{k i}of a family of homotopies of pairsχ₁ i ≃ χ₀ i ∘ h i.
Main results #
TauCeti.homotopicRel_morseCellReattachment_comp_morseCellComparison:Φ₀ ∘ Eis homotopic toΦ₁relative to the lower sublevel.TauCeti.homotopicRel_morseCellReattachment_of_leftInverse: for a left inverseg₀ofΦ₀,Eis homotopic tog₀ ∘ Φ₁relative to the lower sublevel.TauCeti.homotopicRel_morseCellReattachment_morseCellReattachment: two reattachment maps between the same attachments are homotopic relative to the lower sublevel, providedΦ₀has a left inverse.TauCeti.homotopicRel_morseCellReattachment_comp_morseCellReattachment: reattachment maps compose up to homotopy relative to the lower sublevel, providedΦ₀has a left inverse.TauCeti.exists_homotopicRel_morseCellReattachment_comp: Milnor's Lemma 3.6 for Morse cells. For admissible chart families, the reattachment map is a homotopy equivalence relative to the lower sublevel.
References #
- J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Lemma 3.6 and Remark 3.3.
The cell attachment of a chart family is the fiberwise cell attachment over a point, with the
lower sublevel M_{c-ε} viewed inside the upper sublevel M_{c+ε}.
noncomputable def
TauCeti.morseCellReattachment
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
:
The reattachment map E : M_{c-ε} ∪_{α₁} ⨆ᵢ D^{k i} → M_{c-ε} ∪_{α₀} ⨆ᵢ D^{k i} of a
family of self-maps h i of the disc pairs (D^{k i}, ∂D^{k i}) and of homotopies of maps of pairs
K i : χ₁ i ≃ χ₀ i ∘ h i between the characteristic maps of the cells of the chart families φ₁
and φ₀. It is the identity on the lower sublevel M_{c-ε}; on the disc of i it sends x to
the point h i (2x) of the disc of i when ‖x‖ ≤ 1/2, and to the point
K i (2 - 2‖x‖, x/‖x‖) of M_{c-ε} when 1/2 ≤ ‖x‖. It is the fiberwise reattachment map
TauCeti.fiberwiseCellReattachment over a point.
Instances For
@[simp]
theorem
TauCeti.morseCellReattachment_morseCellAttachmentIncl
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(x : ↑{x : M | f x ≤ c - ε})
:
(CategoryTheory.ConcreteCategory.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK))
((CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)) x) = (CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀)) x
The reattachment map sends a point of the lower sublevel to itself.
@[simp]
theorem
TauCeti.morseCellAttachmentIncl_comp_morseCellReattachment
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
:
CategoryTheory.CategoryStruct.comp (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)
(morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK) = morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀
The reattachment map is the identity on the lower sublevel.
@[simp]
theorem
TauCeti.morseCellAttachmentIncl_comp_morseCellReattachment_assoc
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
{Z : TopCat}
(h✝ : morseCellAttachment φ₀ k hk hε hball₀ hf₀ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)
(CategoryTheory.CategoryStruct.comp (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK) h✝) = CategoryTheory.CategoryStruct.comp (morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀) h✝
The reattachment map is the identity on the lower sublevel.
theorem
TauCeti.morseCellReattachment_morseCellAttachmentCell_of_norm_le
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(i : ι)
{w v : ↑(TopCat.disk (k i))}
(hw : ‖↑w.down‖ ≤ 1 / 2)
(hv : ↑v.down = 2 • ↑w.down)
:
(CategoryTheory.ConcreteCategory.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK))
((CategoryTheory.ConcreteCategory.hom (morseCellAttachmentCell φ₁ k hk hε hball₁ hf₁ i)) w) = (CategoryTheory.ConcreteCategory.hom (morseCellAttachmentCell φ₀ k hk hε hball₀ hf₀ i))
((CategoryTheory.ConcreteCategory.hom (h i)) v)
On the disc of radius 1/2 of the cell of i, the reattachment map is x ↦ h i (2x), read in
the cell of i.
theorem
TauCeti.morseCellReattachment_morseCellAttachmentCell_of_le_norm
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(i : ι)
{w : ↑(TopCat.disk (k i))}
(hw : 1 / 2 ≤ ‖↑w.down‖)
{t : ↑unitInterval}
(ht : ↑t = 2 - 2 * ‖↑w.down‖)
{s : ↑(TopCat.diskBoundary (k i))}
(hs : ↑s.down = ‖↑w.down‖⁻¹ • ↑w.down)
:
(CategoryTheory.ConcreteCategory.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK))
((CategoryTheory.ConcreteCategory.hom (morseCellAttachmentCell φ₁ k hk hε hball₁ hf₁ i)) w) = (CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀))
⟨↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)), ⋯⟩
Outside the disc of radius 1/2 of the cell of i, the reattachment map is
x ↦ K i (2 - 2‖x‖, x/‖x‖), read in the lower sublevel.
theorem
TauCeti.homotopicRel_morseCellReattachment_comp_morseCellComparison
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
:
(TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK)
(morseCellComparison φ₀ k hk hε hball₀ hf₀))).HomotopicRel
(TopCat.Hom.hom (morseCellComparison φ₁ k hk hε hball₁ hf₁))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)))
Φ₀ ∘ E is homotopic to Φ₁ relative to the lower sublevel. The reattachment map followed
by the handle-to-cell comparison Φ₀ is homotopic to the handle-to-cell comparison Φ₁, by a
homotopy fixing the lower sublevel M_{c-ε}: the homotopy
TauCeti.fiberwiseCellReattachmentHomotopy over a point.
theorem
TauCeti.homotopicRel_morseCellReattachment_of_leftInverse
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(g₀ : C(↑↧↑{x : M | f x ≤ c + ε}, ↑(morseCellAttachment φ₀ k hk hε hball₀ hf₀)))
(hg₀ : Function.LeftInverse ⇑g₀ ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₀ k hk hε hball₀ hf₀)))
:
(TopCat.Hom.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK)).HomotopicRel
(g₀.comp (TopCat.Hom.hom (morseCellComparison φ₁ k hk hε hball₁ hf₁)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)))
For a left inverse g₀ of the handle-to-cell comparison Φ₀, the reattachment map is
homotopic to g₀ ∘ Φ₁ relative to the lower sublevel.
theorem
TauCeti.homotopicRel_morseCellReattachment_morseCellReattachment
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(h' : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh' :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h' i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K' :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h' i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK' :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K' i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(g₀ : C(↑↧↑{x : M | f x ≤ c + ε}, ↑(morseCellAttachment φ₀ k hk hε hball₀ hf₀)))
(hg₀ : Function.LeftInverse ⇑g₀ ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₀ k hk hε hball₀ hf₀)))
:
(TopCat.Hom.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK)).HomotopicRel
(TopCat.Hom.hom (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h' hh' K' hK'))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁)))
The reattachment map does not depend on the homotopy of characteristic maps. Two
reattachment maps between the same attachments, built from any self-maps of the disc pairs and any
homotopies of maps of pairs, are homotopic relative to the lower sublevel, provided the target
handle-to-cell comparison Φ₀ has a left inverse.
theorem
TauCeti.homotopicRel_morseCellReattachment_comp_morseCellReattachment
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(φ₂ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(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)
(h₀₁ : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh₀₁ :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h₀₁ i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K₀₁ :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h₀₁ i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK₀₁ :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K₀₁ i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(h₁₂ : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh₁₂ :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h₁₂ i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K₁₂ :
(i : ι) →
(TopCat.Hom.hom ((φ₂ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h₁₂ i) ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK₁₂ :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K₁₂ i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(h₀₂ : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh₀₂ :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h₀₂ i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K₀₂ :
(i : ι) →
(TopCat.Hom.hom ((φ₂ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h₀₂ i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK₀₂ :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K₀₂ i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(g₀ : C(↑↧↑{x : M | f x ≤ c + ε}, ↑(morseCellAttachment φ₀ k hk hε hball₀ hf₀)))
(hg₀ : Function.LeftInverse ⇑g₀ ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₀ k hk hε hball₀ hf₀)))
:
(TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp (morseCellReattachment φ₁ φ₂ k hk hε hball₁ hball₂ hf₁ hf₂ h₁₂ hh₁₂ K₁₂ hK₁₂)
(morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h₀₁ hh₀₁ K₀₁ hK₀₁))).HomotopicRel
(TopCat.Hom.hom (morseCellReattachment φ₀ φ₂ k hk hε hball₀ hball₂ hf₀ hf₂ h₀₂ hh₀₂ K₀₂ hK₀₂))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₂ k hk hε hball₂ hf₂)))
Reattachment maps compose up to homotopy. For three chart families φ₀, φ₁, φ₂ and
reattachment maps E₀₁, E₁₂, E₀₂ between their attachments, E₀₁ ∘ E₁₂ is homotopic to E₀₂
relative to the lower sublevel, provided Φ₀ has a left inverse.
theorem
TauCeti.exists_homotopicRel_morseCellReattachment_comp_of_leftInverse
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
(φ₀ φ₁ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 ≤ ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √ε ⊆ (φ₀ i).target)
(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)
(hf₁ : ∀ (i : ι), ∀ y ∈ (φ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(φ₁ i) y).ofLp j ^ 2)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(hh :
∀ (i : ι),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (h i)))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i)))))
(K :
(i : ι) →
(TopCat.Hom.hom ((φ₁ i).morseCharacteristicMap ⋯ hε ⋯ ⋯)).Homotopy
(TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp (h i) ((φ₀ i).morseCharacteristicMap ⋯ hε ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
(g₀ : C(↑↧↑{x : M | f x ≤ c + ε}, ↑(morseCellAttachment φ₀ k hk hε hball₀ hf₀)))
(hg₀ : Function.LeftInverse ⇑g₀ ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₀ k hk hε hball₀ hf₀)))
(g₁ : C(↑↧↑{x : M | f x ≤ c + ε}, ↑(morseCellAttachment φ₁ k hk hε hball₁ hf₁)))
(hg₁ : Function.LeftInverse ⇑g₁ ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₁ k hk hε hball₁ hf₁)))
(hΦ₁ :
(ContinuousMap.id ↑↧↑{x : M | f x ≤ c + ε}).HomotopicRel
((TopCat.Hom.hom (morseCellComparison φ₁ k hk hε hball₁ hf₁)).comp g₁)
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellComparison φ₁ k hk hε hball₁ hf₁))))
:
∃ (E' : morseCellAttachment φ₀ k hk hε hball₀ hf₀ ⟶ morseCellAttachment φ₁ k hk hε hball₁ hf₁),
CategoryTheory.CategoryStruct.comp (morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀) E' = morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁ ∧ (TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp (morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK)
E')).HomotopicRel
(ContinuousMap.id ↑(morseCellAttachment φ₁ k hk hε hball₁ hf₁))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₁ k hk hε hball₁ hf₁))) ∧ (TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp E'
(morseCellReattachment φ₀ φ₁ k hk hε hball₀ hball₁ hf₀ hf₁ h hh K hK))).HomotopicRel
(ContinuousMap.id ↑(morseCellAttachment φ₀ k hk hε hball₀ hf₀))
(Set.range ⇑(CategoryTheory.ConcreteCategory.hom (morseCellAttachmentIncl φ₀ k hk hε hball₀ hf₀)))
The reattachment map is a homotopy equivalence relative to the lower sublevel. If both
handle-to-cell comparisons Φⱼ have left inverses gⱼ, and Φ₁ ∘ g₁ is homotopic to the
identity relative to the image of Φ₁, then the reattachment map E has a homotopy inverse E'
which is the identity on the lower sublevel, with E' ∘ E and E ∘ E' homotopic to the identities
relative to the lower sublevel. The inverse is g₁ ∘ Φ₀.
theorem
TauCeti.exists_homotopicRel_morseCellReattachment_comp
{M : Type u}
[TopologicalSpace M]
{n : ℕ}
{ι : Type u}
{f : M → ℝ}
{c ε : ℝ}
{E : Type u_1}
{H : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[I.Boundaryless]
[IsManifold I (↑⊤) M]
[T2Space M]
[Finite ι]
(hfs : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(ψ₀ ψ₁ : ι → PartialDiffeomorph I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) M (EuclideanSpace ℝ (Fin n)) ↑⊤)
(hψ₀ : Pairwise (Function.onFun Disjoint fun (i : ι) => (ψ₀ i).source))
(hψ₁ : Pairwise (Function.onFun Disjoint fun (i : ι) => (ψ₁ i).source))
(k : ι → ℕ)
(hk : ∀ (i : ι), k i ≤ n)
(hε : 0 < ε)
(hball₀ : ∀ (i : ι), Metric.closedBall 0 √(2 * ε) ⊆ (ψ₀ i).target)
(hball₁ : ∀ (i : ι), Metric.closedBall 0 √(2 * ε) ⊆ (ψ₁ i).target)
(hf₀ :
∀ (i : ι),
∀ y ∈ (ψ₀ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(ψ₀ i).toPartialEquiv y).ofLp j ^ 2)
(hf₁ :
∀ (i : ι),
∀ y ∈ (ψ₁ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(ψ₁ i).toPartialEquiv y).ofLp j ^ 2)
(hcompact : IsCompact (f ⁻¹' Set.Icc (c - ε) (c + ε)))
(hcrit₀ : criticalPoints I f ∩ f ⁻¹' Set.Icc (c - ε) (c + ε) ⊆ ⋃ (i : ι), (ψ₀ i).source)
(hcrit₁ : criticalPoints I f ∩ f ⁻¹' Set.Icc (c - ε) (c + ε) ⊆ ⋃ (i : ι), (ψ₁ i).source)
(h : (i : ι) → TopCat.disk (k i) ⟶ TopCat.disk (k i))
(K :
(i : ι) →
(TopCat.Hom.hom ((ψ₁ i).toOpenPartialHomeomorph.morseCharacteristicMap ⋯ ⋯ ⋯ ⋯)).Homotopy
(TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp (h i) ((ψ₀ i).toOpenPartialHomeomorph.morseCharacteristicMap ⋯ ⋯ ⋯ ⋯))))
(hK :
∀ (i : ι) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary (k i))),
f ↑((K i) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion (k i))) s)) ≤ c - ε)
:
∃ (E' :
morseCellAttachment (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₀ ⟶ morseCellAttachment (fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₁),
CategoryTheory.CategoryStruct.comp
(morseCellAttachmentIncl (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₀) E' = morseCellAttachmentIncl (fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₁ ∧ (TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp
(morseCellReattachment (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph)
(fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ ⋯ hf₀ hf₁ h ⋯ K hK)
E')).HomotopicRel
(ContinuousMap.id ↑(morseCellAttachment (fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₁))
(Set.range
⇑(CategoryTheory.ConcreteCategory.hom
(morseCellAttachmentIncl (fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₁))) ∧ (TopCat.Hom.hom
(CategoryTheory.CategoryStruct.comp E'
(morseCellReattachment (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph)
(fun (i : ι) => (ψ₁ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ ⋯ hf₀ hf₁ h ⋯ K hK))).HomotopicRel
(ContinuousMap.id ↑(morseCellAttachment (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₀))
(Set.range
⇑(CategoryTheory.ConcreteCategory.hom
(morseCellAttachmentIncl (fun (i : ι) => (ψ₀ i).toOpenPartialHomeomorph) k hk ⋯ ⋯ hf₀)))
Milnor's Lemma 3.6 for Morse cells. Let f be smooth and let ψ₀, ψ₁ be two families of
normal-form charts with the same indices k i, each with pairwise disjoint sources, targets
containing the closed ball of radius √(2ε), and sources covering the critical points of the
compact band f⁻¹[c - ε, c + ε]. Given self-maps h i of the discs and homotopies of maps of
pairs K i : χ₁ i ≃ χ₀ i ∘ h i between the characteristic maps of the cells, the reattachment map
E : M_{c-ε} ∪_{α₁} ⨆ᵢ D^{k i} → M_{c-ε} ∪_{α₀} ⨆ᵢ D^{k i} is a homotopy equivalence relative to
the lower sublevel: it has a homotopy inverse which is the identity on M_{c-ε}, and both
composites are homotopic to the identities relative to M_{c-ε}. The maps h i need not be given
as maps of pairs: since 0 < ε, the homotopies K i force them to preserve the boundary spheres
(TauCeti.mapsTo_range_diskBoundaryInclusion_of_homotopy_morseCharacteristicMap).