Deformation retractions

Two successive strong deformation retractions compose: first deform onto the intermediate space, then run its deformation after the first retraction. The resulting homotopy fixes the image of the final inclusion throughout. Inclusions are expressed as continuous maps, so the result also applies to subspaces represented by different but homeomorphic types; for subsets of one space, ContinuousMap.HomotopicRel.exists_inter_deformation_trans states it with set inclusions. A strong deformation retraction also determines every retraction onto the same subspace up to homotopy relative to that subspace (ContinuousMap.HomotopicRel.of_leftInverse). The inclusion of a retract whose retraction, followed by the inclusion, is homotopic to the identity, as for a strong deformation retraction, is a homotopy equivalence (ContinuousMap.HomotopyEquiv.ofRetraction). Strong deformation retractions of subsets also transport along homeomorphisms (Homeomorph.exists_deformation_of_image_eq).

A homotopy from the identity that fixes a subset S at all times and ends in S gives a strong deformation retraction onto S (TauCeti.exists_strong_deformation_retraction_of_homotopy).

A deformation retraction in the weak sense of B onto A ⊆ B is a deformation of B within itself, starting at the identity, ending inside A, and keeping A inside A at all times. The inclusion of A is then a homotopy equivalence (ContinuousMap.HomotopyEquiv.ofWeakDeformationRetraction). Unlike a strong deformation retraction, the deformation need not fix A, which allows straight-line deformations that slide points of A within A.

Deformations of an open piece extend by the identity. Let j : Y → X be an open embedding. A continuous family of self-maps of Y which fixes the points of j ⁻¹' V, for an open neighbourhood V of the complement of the range of j, extends by the identity to a continuous family of self-maps of X (Topology.IsOpenEmbedding.exists_continuousMap_extend_id). Hence a strong deformation retraction of j ⁻¹' S onto j ⁻¹' T extends to one of S onto T, provided the points of S outside the range of j have an open neighbourhood V with S ∩ V ⊆ T (Topology.IsOpenEmbedding.exists_deformation_of_preimage). This is how deformations of the smooth part X \ A of a space, built for instance from the flow of a function F that is small near the closed set A, are turned into deformations of X fixing A.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 0, Exercise 4 (deformation retractions in the weak sense).

theorem ContinuousMap.HomotopicRel.comp_retractions {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {i : C(Y, X)} {j : C(Z, Y)} {r : C(X, Y)} {s : C(Y, Z)} (hX : (ContinuousMap.id X).HomotopicRel (i.comp r) (Set.range ⇑i)) (hY : (ContinuousMap.id Y).HomotopicRel (j.comp s) (Set.range ⇑j)) (hr : Function.LeftInverse ⇑r ⇑i) : (ContinuousMap.id X).HomotopicRel ((i.comp j).comp (s.comp r)) (Set.range ⇑(i.comp j))

Compose the relative homotopies of two strong deformation retractions. The first retraction must be a left inverse of its inclusion; no separation or closedness is needed.

theorem ContinuousMap.HomotopicRel.of_leftInverse {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {i : C(Y, X)} {r r' : C(X, Y)} {S : Set X} (h : (i.comp r').HomotopicRel (ContinuousMap.id X) S) (hr : Function.LeftInverse ⇑r ⇑i) : r'.HomotopicRel r S

Retractions onto a strong deformation retract are unique up to relative homotopy. If the composite of r' with i is homotopic to the identity relative to S, then every left inverse r of i is homotopic to r' relative to S. No condition relating S to the range of i is needed.

theorem ContinuousMap.HomotopicRel.exists_inter_deformation_trans {X : Type u_1} [TopologicalSpace X] {A B S : Set X} (hBA : B ⊆ A) (hSB : A ∩ S ⊆ B) (h₁ : ∃ (r : C(↑A, ↑B)), (∀ (b : ↑B), r ((inclusion hBA) b) = b) ∧ Nonempty (((inclusion hBA).comp r).HomotopyRel (ContinuousMap.id ↑A) {x : ↑A | ↑x ∈ B})) (h₂ : ∃ (r : C(↑B, ↑(B ∩ S))), (∀ (b : ↑(B ∩ S)), r ((inclusion ⋯) b) = b) ∧ Nonempty (((inclusion ⋯).comp r).HomotopyRel (ContinuousMap.id ↑B) {x : ↑B | ↑x ∈ S})) : ∃ (r : C(↑A, ↑(A ∩ S))), (∀ (a : ↑(A ∩ S)), r ((inclusion ⋯) a) = a) ∧ Nonempty (((inclusion ⋯).comp r).HomotopyRel (ContinuousMap.id ↑A) {x : ↑A | ↑x ∈ S})

Strong deformation retractions of subspaces compose. Let B ⊆ A be subspaces, and let S be a set with A ∩ S ⊆ B. If B is a strong deformation retract of A, and B ∩ S is one of B, then A ∩ S is a strong deformation retract of A.

theorem Homeomorph.exists_deformation_of_image_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) {A B : Set X} {A' B' : Set Y} (hBA : B ⊆ A) (hBA' : B' ⊆ A') (hA : ⇑e '' A = A') (hB : ⇑e '' B = B') (h : ∃ (r : C(↑A, ↑B)), (∀ (b : ↑B), r ((ContinuousMap.inclusion hBA) b) = b) ∧ Nonempty (((ContinuousMap.inclusion hBA).comp r).HomotopyRel (ContinuousMap.id ↑A) {x : ↑A | ↑x ∈ B})) : ∃ (r : C(↑A', ↑B')), (∀ (b : ↑B'), r ((ContinuousMap.inclusion hBA') b) = b) ∧ Nonempty (((ContinuousMap.inclusion hBA').comp r).HomotopyRel (ContinuousMap.id ↑A') {y : ↑A' | ↑y ∈ B'})

Strong deformation retractions transport along homeomorphisms. If B is a strong deformation retract of A ⊇ B and a homeomorphism e carries A onto A' and B onto B', then B' is a strong deformation retract of A'. The images are given as equations, so that A' and B' may be described independently of e.

def ContinuousMap.HomotopyEquiv.ofWeakDeformationRetraction {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (H : ↑unitInterval × ↑B → X) (hH : Continuous H) (hHB : ∀ (p : ↑unitInterval × ↑B), H p ∈ B) (h₀ : ∀ (x : ↑B), H (0, x) = ↑x) (h₁ : ∀ (x : ↑B), H (1, x) ∈ A) (hHA : ∀ (t : ↑unitInterval) (x : ↑B), ↑x ∈ A → H (t, x) ∈ A) : HomotopyEquiv ↑A ↑B

The inclusion of a weak deformation retract is a homotopy equivalence. Let A ⊆ B, and let H : I × B → X be a deformation of B within B which starts at the identity, ends inside A, and keeps A inside A at all times. Then the inclusion A → B is a homotopy equivalence, whose homotopy inverse is the end map of H.

@[simp]

theorem ContinuousMap.HomotopyEquiv.coe_ofWeakDeformationRetraction_apply {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (H : ↑unitInterval × ↑B → X) (hH : Continuous H) (hHB : ∀ (p : ↑unitInterval × ↑B), H p ∈ B) (h₀ : ∀ (x : ↑B), H (0, x) = ↑x) (h₁ : ∀ (x : ↑B), H (1, x) ∈ A) (hHA : ∀ (t : ↑unitInterval) (x : ↑B), ↑x ∈ A → H (t, x) ∈ A) (a : ↑A) : ↑((ofWeakDeformationRetraction hAB H hH hHB h₀ h₁ hHA).toFun a) = ↑a

The homotopy equivalence ContinuousMap.HomotopyEquiv.ofWeakDeformationRetraction is the inclusion.

@[simp]

theorem ContinuousMap.HomotopyEquiv.coe_ofWeakDeformationRetraction_symm_apply {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (H : ↑unitInterval × ↑B → X) (hH : Continuous H) (hHB : ∀ (p : ↑unitInterval × ↑B), H p ∈ B) (h₀ : ∀ (x : ↑B), H (0, x) = ↑x) (h₁ : ∀ (x : ↑B), H (1, x) ∈ A) (hHA : ∀ (t : ↑unitInterval) (x : ↑B), ↑x ∈ A → H (t, x) ∈ A) (x : ↑B) : ↑((ofWeakDeformationRetraction hAB H hH hHB h₀ h₁ hHA).symm.toFun x) = H (1, x)

The homotopy inverse of ContinuousMap.HomotopyEquiv.ofWeakDeformationRetraction is the end map of the deformation.

def ContinuousMap.HomotopyEquiv.ofRetraction {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (r : C(↑B, ↑A)) (hr : ∀ (a : ↑A), r ((inclusion hAB) a) = a) (G : ((inclusion hAB).comp r).Homotopy (ContinuousMap.id ↑B)) : HomotopyEquiv ↑A ↑B

The inclusion of a retract homotopic to the identity is a homotopy equivalence. Let A ⊆ B and let r : B → A be a retraction whose composite with the inclusion is homotopic to the identity of B, as for a strong deformation retraction. Then the inclusion A → B is a homotopy equivalence, whose homotopy inverse is r.

@[simp]

theorem ContinuousMap.HomotopyEquiv.coe_ofRetraction_apply {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (r : C(↑B, ↑A)) (hr : ∀ (a : ↑A), r ((inclusion hAB) a) = a) (G : ((inclusion hAB).comp r).Homotopy (ContinuousMap.id ↑B)) (a : ↑A) : ↑((ofRetraction hAB r hr G).toFun a) = ↑a

The homotopy equivalence ContinuousMap.HomotopyEquiv.ofRetraction is the inclusion.

@[simp]

theorem ContinuousMap.HomotopyEquiv.coe_ofRetraction_symm_apply {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hAB : A ⊆ B) (r : C(↑B, ↑A)) (hr : ∀ (a : ↑A), r ((inclusion hAB) a) = a) (G : ((inclusion hAB).comp r).Homotopy (ContinuousMap.id ↑B)) (b : ↑B) : (ofRetraction hAB r hr G).symm.toFun b = r b

The homotopy inverse of ContinuousMap.HomotopyEquiv.ofRetraction is the retraction.

theorem Topology.IsOpenEmbedding.exists_deformation_of_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {j : Y → X} (hj : IsOpenEmbedding j) {S T V : Set X} {s t : Set Y} (hTS : T ⊆ S) (hts : t ⊆ s) (hs : j ⁻¹' S = s) (ht : j ⁻¹' T = t) (hV : IsOpen V) (hSV : S \ Set.range j ⊆ V) (hVT : S ∩ V ⊆ T) (r : C(↑s, ↑t)) (H : ((ContinuousMap.inclusion hts).comp r).HomotopyRel (ContinuousMap.id ↑s) {y : ↑s | ↑y ∈ t}) : ∃ (r : C(↑S, ↑T)), (∀ (x : ↑T), r ((ContinuousMap.inclusion hTS) x) = x) ∧ Nonempty (((ContinuousMap.inclusion hTS).comp r).HomotopyRel (ContinuousMap.id ↑S) {x : ↑S | ↑x ∈ T})

A strong deformation retraction extends by the identity off an open embedding. Let j : Y → X be an open embedding and T ⊆ S subsets of X, with preimages t ⊆ s in Y. Suppose the points of S outside the range of j have an open neighbourhood V with S ∩ V ⊆ T. If H is a strong deformation retraction of s onto t, then T is a strong deformation retract of S: the deformation is H transported along j and extended by the identity, which it already is on j ⁻¹' V.

theorem TauCeti.exists_strong_deformation_retraction_of_homotopy {X : Type u_1} [TopologicalSpace X] {S : Set X} {F : ↑unitInterval × X → X} (hFc : Continuous F) (hzero : ∀ (x : X), F (0, x) = x) (hone : ∀ (x : X), F (1, x) ∈ S) (hfix : ∀ (t : ↑unitInterval), ∀ x ∈ S, F (t, x) = x) : ∃ (r : C(X, ↑S)), (∀ (x : ↑S), r ↑x = x) ∧ Nonempty ((ContinuousMap.id X).HomotopyRel ((ContinuousMap.subtypeVal S).comp r) S)

A homotopy from the identity that fixes a subset S at all times and ends in S gives a strong deformation retraction onto S: the retraction is the corestriction of the time-one map.