This file proves that if B and Y are CW-complexes and f : B ⟶ Y is a weak homotopy equivalence, then the induced map $f_* : [X, B] → [X, Y]$ is bijective for all CW-complexes X.

TODO

TopCat.LiftStructUpToRelHomotopy.curriedH_prop is not used, hence the definition TopCat.LiftStructUpToRelHomotopy can be weakened (?)

References

• T. tom Dieck, Algebraic topology. Theorem 8.4.3.

theorem TopCat.IsCompressible.relCWComplex_of_isWeakHomotopyEquiv {B Y : TopCat} {f : B ⟶ Y} (hf : IsWeakHomotopyEquiv (Hom.hom f)) (X : RelCWComplex) : IsCompressible (X.skIncl 0) (MapCyl.domIncl f)

If f : B ⟶ Y is a weak homotopy equivalence and $(X, A)$ is a relative CW-complex, then the inclusion map MapCyl.domIncl φ from B to the mapping cylinder of φ is compressible w.r.t. the inclusion map A ⟶ X from the $(-1)$-skeleton to X.

theorem IsWeakHomotopyEquiv.CWComplex_induced_map_surjective {B Y : TopCat} {f : B ⟶ Y} (hf : IsWeakHomotopyEquiv (TopCat.Hom.hom f)) (X : CWComplex) (g : X.toTopCat ⟶ Y) : ∃ (g' : X.toTopCat ⟶ B), (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g' f)).Homotopic (TopCat.Hom.hom g)

if B and Y are CW-complexes and f : B ⟶ Y is a weak homotopy equivalence, then the induced map $f_* : [X, B] → [X, Y]$ is surjective for all CW-complexes X.

∅ -----z----→ B
|             |
|       MapCyl.domIncl f
|             |
↓             ↓
X -----G----→ MapCyl f

theorem IsWeakHomotopyEquiv.CWComplex_induced_map_injective {B Y : TopCat} {f : B ⟶ Y} (hf : IsWeakHomotopyEquiv (TopCat.Hom.hom f)) (X : CWComplex) (g₀ g₁ : X.toTopCat ⟶ B) (hg : (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g₀ f)).Homotopic (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp g₁ f))) : (TopCat.Hom.hom g₀).Homotopic (TopCat.Hom.hom g₁)

if B and Y are CW-complexes and f : B ⟶ Y is a weak homotopy equivalence, then the induced map $f_* : [X, B] → [X, Y]$ is injective for all CW-complexes X.

{0, 1} × X ------- G₀₁ -------→ B
   |                            |
   |                     MapCyl.domIncl f
X.zeroOneProdInclIProd          |
   ↓                            ↓
I × X ------------ G ------→ MapCyl f