This file proves that if f : C(X, Y) is a weak homotopy equivalence, then the inclusion map MapCyl.domInclFromTop from X to the mapping cylinder of f is n-compressible for every natural number n, i.e., it is compressible with respect to TopCat.diskBoundaryIncl n : ∂𝔻 n ⟶ 𝔻 n for each n.

theorem HomotopyGroup.isIso_inducedPointedHom'_mapCyl_domIncl_of_isIso (n : ℕ) {X Y : TopCat} (f : X ⟶ Y) (x₀ : ↑X) (hf : CategoryTheory.IsIso (inducedPointedHom' n x₀ f)) : CategoryTheory.IsIso (inducedPointedHom' n x₀ (TopCat.MapCyl.domIncl f))

If the map πₙ(X, x₀) ⟶ πₙ(Y, f x₀) induced by f is an isomorphism, then the map πₙ(X, x₀) ⟶ πₙ(MapCyl f, ⋯) induced by inclusion into the mapping cylinder is an isomorphism.

theorem HomotopyGroup.isIso_inducedPointedHom_mapCyl_domInclFromTop_of_isIso (n : ℕ) {X Y : TopCat} (f : X ⟶ Y) (x₀ : ↑X) (hf : CategoryTheory.IsIso (inducedPointedHom' n x₀ f)) : CategoryTheory.IsIso (inducedPointedHom n ((TopCat.MapCyl.domInclToTop f) x₀) (TopCat.MapCyl.domInclFromTop f))

If the map πₙ(X, x₀) ⟶ πₙ(Y, f x₀) induced by f is an isomorphism, then the map πₙ(X, MapCyl.top f) ⟶ πₙ(MapCyl f, ⋯) induced by the inclusion domInclFromTop f : C(top f, MapCyl f) is an isomorphism.

theorem RelHomotopyGroup.inducedPointedHom_subtype_val_eq_iStar (n : ℕ) {X : Type u} [TopologicalSpace X] (A : Set X) (a : ↑A) : ⇑(CategoryTheory.ConcreteCategory.hom (HomotopyGroup.inducedPointedHom n a { toFun := Subtype.val, continuous_toFun := ⋯ })) = iStar n X A a

theorem RelHomotopyGroup.bijective_iStar_mapCyl_of_isIso (n : ℕ) {X Y : TopCat} (f : X ⟶ Y) (x₀ : ↑X) (hf : CategoryTheory.IsIso (HomotopyGroup.inducedPointedHom' n x₀ f)) : Function.Bijective (iStar n (↑(TopCat.MapCyl f)) (TopCat.MapCyl.top f) ((TopCat.MapCyl.domInclToTop f) x₀))

If the map πₙ(X, x₀) ⟶ πₙ(Y, f x₀) induced by f is an isomorphism, then the map iStar : πₙ(X, MapCyl.top f) → πₙ(MapCyl f, ⋯) is bijective.

theorem RelHomotopyGroup.unique_pi_mapCyl_of_isWeakHomotopyEquiv (n : ℕ) {X Y : TopCat} (f : X ⟶ Y) (x₀ : ↑X) (hf : IsWeakHomotopyEquiv (TopCat.Hom.hom f)) : Nonempty (Unique (RelHomotopyGroup (n + 1) (↑(TopCat.MapCyl f)) (TopCat.MapCyl.top f) ((TopCat.MapCyl.domInclToTop f) x₀)))

If f is a weak homotopy equivalence, then the relative homotopy group π_rel n (MapCyl f) (MapCyl.top f) (MapCyl.domInclToTop f x₀) is zero for all n ≥ 1 and x.

@[reducible, inline]

abbrev Cube.IsMapOfPairs {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(Fin n → ↑unitInterval, X)) : Prop

A continuous map from the n-dimensional cube to X is called a map of pairs to (X, A) if it sends the boundary ∂I^n into A.

Equations

• Cube.IsMapOfPairs X A f = ∀ y ∈ Cube.boundary (Fin n), f y ∈ A

theorem Cube.exists_relGenLoop_homotopicWith_isMapOfPairs {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(Fin (n + 1) → ↑unitInterval, X)) (hf : IsMapOfPairs X A f) : ∃ (a : ↑A) (g : ↑(RelGenLoop (n + 1) X A a)), f.HomotopicWith ↑g fun (h : C(Fin (n + 1) → ↑unitInterval, X)) => IsMapOfPairs X A h

For n ≥ 1, if f is a continuous map of pairs from (I^ Fin n, ∂I^n) to (X, A), then it is as a map of pairs homotopic to a RelGenLoop.

theorem Cube.homotopicWith_isMapOfPairs_of_relGenLoop_homotopic {n : ℕ} {X : Type u} [TopologicalSpace X] {A : Set X} {a : ↑A} {f g : ↑(RelGenLoop n X A a)} (fg : RelGenLoop.Homotopic f g) : (↑f).HomotopicWith ↑g fun (h : C(Fin n → ↑unitInterval, X)) => IsMapOfPairs X A h

theorem Cube.homotopicWith_const_isMapOfPairs_of_unique_pi {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(Fin (n + 1) → ↑unitInterval, X)) (hf : IsMapOfPairs X A f) (hpi : ∀ (a : ↑A), Nonempty (Unique (RelHomotopyGroup (n + 1) X A a))) : ∃ (a : ↑A), f.HomotopicWith (ContinuousMap.const (Fin (n + 1) → ↑unitInterval) ↑a) fun (h : C(Fin (n + 1) → ↑unitInterval, X)) => IsMapOfPairs X A h

Suppose n ≥ 1 and the relative homotopy group π_rel n X A a is zero for all a : A. If f is a continuous map of pairs from (I^ Fin n, ∂I^n) to (X, A), then it is as a map of pairs homotopic to a constant map.

@[reducible, inline]

abbrev TopCat.disk.IsMapOfPairs {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(↑(disk n), X)) : Prop

A continuous map from the n-dimensional disk to X is called a map of pairs to (X, A) if it sends the boundary ∂𝔻 n into A.

Equations

• TopCat.disk.IsMapOfPairs X A f = ∀ (y : ↑(TopCat.diskBoundary n)), f ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryIncl n)) y) ∈ A

theorem TopCat.disk.homotopicWith_const_isMapOfPairs_of_unique_pi {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(↑(disk (n + 1)), X)) (hf : IsMapOfPairs X A f) (hpi : ∀ (a : ↑A), Nonempty (Unique (RelHomotopyGroup (n + 1) X A a))) : ∃ (a : ↑A), f.HomotopicWith (ContinuousMap.const ↑(disk (n + 1)) ↑a) fun (h : C(↑(disk (n + 1)), X)) => IsMapOfPairs X A h

Suppose n ≥ 1 and the relative homotopy group π_rel n X A a is zero for all a : A. If f is a continuous map of pairs from (∂𝔻 n, 𝔻 n) to (X, A), then it is as a map of pairs homotopic to a constant map.

noncomputable def TopCat.Cyl.stretchToWall {n : ℕ} : C(↑unitInterval × ↑(disk (n + 1)), ↑unitInterval × ↑(disk (n + 1)))

stretchToWall

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Cyl.stretchToWall_fst_coe {n : ℕ} (t : ↑unitInterval) (x : EuclideanSpace ℝ (Fin (n + 1))) (hx : x ∈ Metric.closedBall 0 1) : ↑(stretchToWall (t, { down := ⟨x, hx⟩ })).1 = 2 - max (2 * ‖x‖) (2 - ↑t)

@[simp]

theorem TopCat.Cyl.stretchToWall_snd_down_val {n : ℕ} (t : ↑unitInterval) (x : EuclideanSpace ℝ (Fin (n + 1))) (hx : x ∈ Metric.closedBall 0 1) : ↑(stretchToWall (t, { down := ⟨x, hx⟩ })).2.down = (2 / max (2 * ‖x‖) (2 - ↑t)) • x

theorem TopCat.Cyl.stretchToWall_zero {n : ℕ} (x : ↑(disk (n + 1))) : stretchToWall (0, x) = (0, x)

theorem TopCat.Cyl.stretchToWall_eq_zero_of_norm_eq_one {n : ℕ} {t : ↑unitInterval} {x : EuclideanSpace ℝ (Fin (n + 1))} {hx : x ∈ Metric.closedBall 0 1} (hx1 : ‖x‖ = 1) : stretchToWall (t, { down := ⟨x, hx⟩ }) = (0, { down := ⟨x, hx⟩ })

theorem TopCat.disk.homotopicRel_boundary_of_homotopicWith_isMapOfPairs {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(↑(disk (n + 1)), X)) (H : ∃ (g : C(↑(disk (n + 1)), X)), Set.range ⇑g ⊆ A ∧ f.HomotopicWith g fun (h : C(↑(disk (n + 1)), X)) => IsMapOfPairs X A h) : ∃ (l : C(↑(disk (n + 1)), X)), Set.range ⇑l ⊆ A ∧ f.HomotopicRel l (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (diskBoundaryIncl (n + 1))))

Suppose n ≥ 1 and f is a continuous map of pairs from (∂𝔻 n, 𝔻 n) to (X, A). If f is as a map of pairs homotopic to a map into A, then f is relative to ∂𝔻 n homotopic to a map into A.

theorem TopCat.disk.homotopicRel_boundary_of_unique_pi {n : ℕ} (X : Type u) [TopologicalSpace X] (A : Set X) (f : C(↑(disk (n + 1)), X)) (hf : IsMapOfPairs X A f) (hpi : ∀ (a : ↑A), Nonempty (Unique (RelHomotopyGroup (n + 1) X A a))) : ∃ (l : C(↑(disk (n + 1)), X)), Set.range ⇑l ⊆ A ∧ f.HomotopicRel l (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (diskBoundaryIncl (n + 1))))

Suppose n ≥ 1 and the relative homotopy group π_rel n X A a is zero for all a : A. If f is a continuous map of pairs from (∂𝔻 n, 𝔻 n) to (X, A), then it is relative to ∂𝔻 n homotopic to a map into A.

theorem TopCat.disk.isCompressible_subtype_val_of_unique_pi (n : ℕ) (X : Type u) [TopologicalSpace X] (A : Set X) (hpi : ∀ (a : ↑A), Nonempty (Unique (RelHomotopyGroup (n + 1) X A a))) : IsCompressible (diskBoundaryIncl (n + 1)) (ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })

For n ≥ 1, if the relative homotopy group π_rel (n + 1) X A a is zero (regardless of the basepoint a), then the inclusion map form A to X is n-compressible.

theorem TopCat.disk.isCompressible_zero_subtype_val_of_bijective_iStar_zero (X : Type u) [TopologicalSpace X] (A : Set X) (pt : ↑A) (hbi : Function.Bijective (RelHomotopyGroup.iStar 0 X A pt)) : IsCompressible (diskBoundaryIncl 0) (ofHom { toFun := Subtype.val, continuous_toFun := ⋯ })

If iStar : π_ 0 A pt → π_ 0 X pt is bijective (for some basepoint pt, which is irrelevant), then the inclusion map from A to X is 0-compressible.

theorem TopCat.disk.isCompressible_mapcyl_domInclFromTop_of_isWeakHomotopyEquiv (n : ℕ) {X Y : TopCat} (φ : X ⟶ Y) (hφ : IsWeakHomotopyEquiv (Hom.hom φ)) : IsCompressible (diskBoundaryIncl n) (ofHom (MapCyl.domInclFromTop φ))

If φ is a weak homotopy equivalence, then the inclusion map MapCyl.domInclFromTop φ from the top surface of the mapping cylinder of φ to the mapping cylinder of φ is n-compressible for each natural number n.

theorem TopCat.disk.isCompressible_mapCyl_domIncl_of_isWeakHomotopyEquiv (n : ℕ) {X Y : TopCat} (φ : X ⟶ Y) (hφ : IsWeakHomotopyEquiv (Hom.hom φ)) : IsCompressible (diskBoundaryIncl n) (MapCyl.domIncl φ)

If φ : X ⟶ Y is a weak homotopy equivalence, then the inclusion map MapCyl.domIncl φ from X to the mapping cylinder of φ is n-compressible for each natural number n.