Whitehead's theorem

Whitehead's theorem says that a weak homotopy equivalence between CW complexes is a homotopy equivalence (Hatcher, Algebraic Topology, Theorem 4.5). This file proves it for spaces of CW type, using Mathlib's classical CW complexes as models, as ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv, whose forward map is the given weak homotopy equivalence.

The proof goes through the surjectivity half of Hatcher's Proposition 4.22, i.e. surjectivity of [K, X] → [K, Y]: if f : X → Y is a weak homotopy equivalence, then every map g : K → Y out of a space K of CW type lifts through f up to homotopy (ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic).

• In the mapping cylinder M_f, which contains X as the bottom face incl f and deformation retracts onto Y, the relative homotopy groups π_{n+1}(M_f, X, x) all vanish (ContinuousMap.IsWeakHomotopyEquivalence.subsingleton_relHomotopyGroup_mappingCylinder). The inclusion X ↪ M_f composed with the retraction M_f → Y is f, so it induces bijections on all homotopy groups, and the exact sequence of the pair (M_f, X) does the rest (TauCeti.RelHomotopyGroup.subsingleton_of_injective_of_surjective).
• The compression lemma (TauCeti.exists_homotopicRel_range_subset_of_relHomotopyGroup) then deforms K → Y ↪ M_f into X, and retracting back to Y gives the lift.
• For a space homotopy equivalent to a CW complex, compose with the inverse of the equivalence, lift on the CW complex, and compose back. The inverse law gives the required homotopy on the original space.

The same compression gives the injectivity half of Proposition 4.22: if g₀, g₁ : K → X become homotopic after composing with f, then they are homotopic (ContinuousMap.IsWeakHomotopyEquivalence.homotopic_of_comp_homotopic). In M_f the inclusion of the bottom face X is homotopic to f followed by the inclusion of Y, so a homotopy f ∘ g₀ ≃ f ∘ g₁ gives a homotopy K × I → M_f which already maps the two ends K × {0, 1} into X. For a CW complex K the cylinder K × I is a CW complex relative to its two ends (TauCeti.relCWComplexCylinder), so the compression lemma deforms this homotopy into X relative to the ends. Together, the two halves say that composition with f is a bijection [K, X] → [K, Y] of homotopy classes (ContinuousMap.IsWeakHomotopyEquivalence.comp_homotopic_comp_iff and ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic).

Consequently a map φ : X → Y, together with a : A → X out of a space of CW type and a weak homotopy equivalence b : B → Y, induces a map A → B making the square commute up to homotopy (ContinuousMap.IsWeakHomotopyEquivalence.lift), unique up to homotopy and functorial up to homotopy in φ (Hatcher, Proposition 4.18, for arbitrary CW approximations a and b).

Applied to the identity of Y, when Y has CW type, the lift is a map g : Y → X with f ∘ g ≃ id. By two out of three, g is again a weak homotopy equivalence, so when X has CW type g has a right homotopy inverse h in turn. Then f ≃ f ∘ g ∘ h ≃ h, and so g ∘ f ≃ g ∘ h ≃ id. Unlike Hatcher's proof of Theorem 4.5, this argument needs neither a CW structure on the mapping cylinder nor cellular approximation: the only cell-by-cell argument is the skeletal induction inside the compression lemma.

Main declarations

• ContinuousMap.IsNConnected.subsingleton_relHomotopyGroup_mappingCylinder: the relative homotopy groups of the mapping cylinder of an n-connected map vanish up to dimension n.
• ContinuousMap.IsWeakHomotopyEquivalence.subsingleton_relHomotopyGroup_mappingCylinder: the relative homotopy groups of the mapping cylinder of a weak homotopy equivalence vanish.
• ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic: maps out of spaces of CW type lift through a weak homotopy equivalence up to homotopy.
• ContinuousMap.IsWeakHomotopyEquivalence.homotopic_of_comp_homotopic and ContinuousMap.IsWeakHomotopyEquivalence.comp_homotopic_comp_iff: such lifts are unique up to homotopy.
• ContinuousMap.IsWeakHomotopyEquivalence.lift: the map induced on CW approximations, with ContinuousMap.IsWeakHomotopyEquivalence.comp_lift_homotopic, ContinuousMap.IsWeakHomotopyEquivalence.homotopic_lift, ContinuousMap.IsWeakHomotopyEquivalence.lift_id_homotopic and ContinuousMap.IsWeakHomotopyEquivalence.lift_comp_homotopic.
• ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv: Whitehead's theorem.
• ContinuousMap.IsWeakHomotopyEquivalence.exists_homotopyEquiv_comp_homotopic: CW approximations are unique up to homotopy equivalence.
• TauCeti.contractibleSpace_of_subsingleton_homotopyGroup: a weakly contractible space of CW type is contractible.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Theorem 4.5 (Whitehead's theorem), Lemma 4.6 (the compression lemma), Proposition 4.18 and the uniqueness of CW approximations stated after it, Proposition 4.22, and the corollary after Theorem 4.5 on weakly contractible CW complexes.

theorem ContinuousMap.IsNConnected.subsingleton_relHomotopyGroup_mappingCylinder {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} {n : ℕ} (hf : f.IsNConnected n) (N : Type w) [Finite N] (hN : Nat.card N < n) (b : ↑(Set.range ⇑(TauCeti.MappingCylinder.incl f))) : Subsingleton (TauCeti.RelHomotopyGroup N { pair := TopPair.ofSubset (Set.range ⇑(TauCeti.MappingCylinder.incl f)), basepoint := b })

The relative homotopy groups π_{k+1}(M_f, X, x) of the mapping cylinder of an n-connected map f : X → Y, relative to its bottom face X, are trivial for k < n at every basepoint of the bottom face. Here k is the number of cube directions N.

theorem ContinuousMap.IsWeakHomotopyEquivalence.subsingleton_relHomotopyGroup_mappingCylinder {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} (hf : f.IsWeakHomotopyEquivalence) (N : Type w) [Finite N] (b : ↑(Set.range ⇑(TauCeti.MappingCylinder.incl f))) : Subsingleton (TauCeti.RelHomotopyGroup N { pair := TopPair.ofSubset (Set.range ⇑(TauCeti.MappingCylinder.incl f)), basepoint := b })

The relative homotopy groups π_{n+1}(M_f, X, x) of the mapping cylinder of a weak homotopy equivalence f : X → Y, relative to its bottom face X, are trivial at every basepoint of the bottom face.

theorem ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} {K : Type u_4} [TopologicalSpace K] [hK : TauCeti.CWType K] (hf : f.IsWeakHomotopyEquivalence) (g : C(K, Y)) : ∃ (g' : C(K, X)), (f.comp g').Homotopic g

Maps out of a space of CW type lift through a weak homotopy equivalence up to homotopy (the surjectivity half of Hatcher, Proposition 4.22).

theorem ContinuousMap.IsWeakHomotopyEquivalence.homotopic_of_comp_homotopic {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} {K : Type u_4} [TopologicalSpace K] [hK : TauCeti.CWType K] (hf : f.IsWeakHomotopyEquivalence) {g₀ g₁ : C(K, X)} (h : (f.comp g₀).Homotopic (f.comp g₁)) : g₀.Homotopic g₁

Lifts through a weak homotopy equivalence are unique up to homotopy (the injectivity half of Hatcher, Proposition 4.22). If f : X → Y is a weak homotopy equivalence and K has CW type, then two maps g₀, g₁ : K → X are homotopic as soon as f ∘ g₀ and f ∘ g₁ are.

@[simp]

theorem ContinuousMap.IsWeakHomotopyEquivalence.comp_homotopic_comp_iff {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} {K : Type u_4} [TopologicalSpace K] [hK : TauCeti.CWType K] (hf : f.IsWeakHomotopyEquivalence) {g₀ g₁ : C(K, X)} : (f.comp g₀).Homotopic (f.comp g₁) ↔ g₀.Homotopic g₁

Composition with a weak homotopy equivalence is injective on homotopy classes of maps out of a space of CW type (Hatcher, Proposition 4.22): f ∘ g₀ ≃ f ∘ g₁ exactly when g₀ ≃ g₁. Surjectivity is ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic.

noncomputable def ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} [TauCeti.CWType X] [TauCeti.CWType Y] (hf : f.IsWeakHomotopyEquivalence) : HomotopyEquiv X Y

Whitehead's theorem (Hatcher, Theorem 4.5). A weak homotopy equivalence f between spaces of CW type is a homotopy equivalence. This is the homotopy equivalence whose forward map is f itself (ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv_toFun); its homotopy inverse is a lift of the identity through f given by ContinuousMap.IsWeakHomotopyEquivalence.exists_comp_homotopic.

@[simp]

theorem ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv_toFun {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : C(X, Y)} [TauCeti.CWType X] [TauCeti.CWType Y] (hf : f.IsWeakHomotopyEquivalence) : hf.homotopyEquiv.toFun = f

theorem ContinuousMap.IsWeakHomotopyEquivalence.exists_homotopyEquiv_comp_homotopic {A : Type u_1} {A' : Type u_2} {X : Type u_5} [TopologicalSpace A] [TopologicalSpace A'] [TopologicalSpace X] [TauCeti.CWType A] [TauCeti.CWType A'] {a : C(A, X)} {a' : C(A', X)} (ha : a.IsWeakHomotopyEquivalence) (ha' : a'.IsWeakHomotopyEquivalence) : ∃ (e : HomotopyEquiv A A'), (a'.comp e.toFun).Homotopic a

CW approximations are unique up to homotopy equivalence (Hatcher, after Proposition 4.18). If a : A → X and a' : A' → X are weak homotopy equivalences out of spaces of CW type, there is a homotopy equivalence e : A ≃ₕ A' with a' ∘ e ≃ a.

noncomputable def ContinuousMap.IsWeakHomotopyEquivalence.lift {A : Type u_1} {B : Type u_3} {X : Type u_5} {Y : Type u_6} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType A] {b : C(B, Y)} (hb : b.IsWeakHomotopyEquivalence) (a : C(A, X)) (φ : C(X, Y)) : C(A, B)

The map A → B induced by φ : X → Y between spaces over X and Y: given a : A → X with A of CW type and a weak homotopy equivalence b : B → Y, a lift of φ ∘ a through b, so that the square of φ and the lift with a and b commutes up to homotopy (ContinuousMap.IsWeakHomotopyEquivalence.comp_lift_homotopic). It is determined up to homotopy by this property (ContinuousMap.IsWeakHomotopyEquivalence.homotopic_lift).

theorem ContinuousMap.IsWeakHomotopyEquivalence.comp_lift_homotopic {A : Type u_1} {B : Type u_3} {X : Type u_5} {Y : Type u_6} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType A] {b : C(B, Y)} (hb : b.IsWeakHomotopyEquivalence) (a : C(A, X)) (φ : C(X, Y)) : (b.comp (hb.lift a φ)).Homotopic (φ.comp a)

The square of φ and its lift commutes up to homotopy: b ∘ lift ≃ φ ∘ a.

theorem ContinuousMap.IsWeakHomotopyEquivalence.homotopic_lift {A : Type u_1} {B : Type u_3} {X : Type u_5} {Y : Type u_6} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType A] {b : C(B, Y)} (hb : b.IsWeakHomotopyEquivalence) {a : C(A, X)} {φ : C(X, Y)} {ψ : C(A, B)} (hψ : (b.comp ψ).Homotopic (φ.comp a)) : ψ.Homotopic (hb.lift a φ)

Uniqueness of the lift. Every map ψ : A → B with b ∘ ψ ≃ φ ∘ a is homotopic to the lift of φ.

theorem ContinuousMap.IsWeakHomotopyEquivalence.lift_homotopic_of_homotopic {A : Type u_1} {B : Type u_3} {X : Type u_5} {Y : Type u_6} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType A] {b : C(B, Y)} (hb : b.IsWeakHomotopyEquivalence) (a : C(A, X)) {φ φ' : C(X, Y)} (h : φ.Homotopic φ') : (hb.lift a φ).Homotopic (hb.lift a φ')

Homotopic maps have homotopic lifts.

theorem ContinuousMap.IsWeakHomotopyEquivalence.lift_id_homotopic {A : Type u_1} {X : Type u_5} [TopologicalSpace A] [TopologicalSpace X] [TauCeti.CWType A] {a : C(A, X)} (ha : a.IsWeakHomotopyEquivalence) : (ha.lift a (ContinuousMap.id X)).Homotopic (ContinuousMap.id A)

The identity lifts to the identity up to homotopy.

theorem ContinuousMap.IsWeakHomotopyEquivalence.lift_comp_homotopic {A : Type u_1} {B : Type u_3} {D : Type u_4} {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace D] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TauCeti.CWType A] [TauCeti.CWType B] {b : C(B, Y)} {d : C(D, Z)} (hb : b.IsWeakHomotopyEquivalence) (hd : d.IsWeakHomotopyEquivalence) (a : C(A, X)) (χ : C(Y, Z)) (φ : C(X, Y)) : (hd.lift a (χ.comp φ)).Homotopic ((hd.lift b χ).comp (hb.lift a φ))

Composites lift to composites up to homotopy: the lift of χ ∘ φ is homotopic to the composite of the lifts of φ and χ.

@[simp]

theorem ContinuousMap.IsWeakHomotopyEquivalence.isWeakHomotopyEquivalence_lift_iff {A : Type u_1} {B : Type u_3} {X : Type u_5} {Y : Type u_6} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType A] {a : C(A, X)} {b : C(B, Y)} (ha : a.IsWeakHomotopyEquivalence) (hb : b.IsWeakHomotopyEquivalence) {φ : C(X, Y)} : (hb.lift a φ).IsWeakHomotopyEquivalence ↔ φ.IsWeakHomotopyEquivalence

The lift of φ is a weak homotopy equivalence exactly when φ is, when a is also a weak homotopy equivalence.

theorem ContinuousMap.isWeakHomotopyEquivalence_iff_exists_homotopyEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType X] [TauCeti.CWType Y] (f : C(X, Y)) : f.IsWeakHomotopyEquivalence ↔ ∃ (e : HomotopyEquiv X Y), e.toFun = f

Between spaces of CW type, a map is a weak homotopy equivalence exactly when it is the forward map of a homotopy equivalence.

theorem TauCeti.contractibleSpace_of_subsingleton_homotopyGroup {X : Type w} [TopologicalSpace X] [CWType X] [PathConnectedSpace X] (x : X) (h : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 1) X x)) : ContractibleSpace X

A weakly contractible space of CW type is contractible (Hatcher, the corollary after Theorem 4.5). A path-connected space of CW type whose homotopy groups in every positive dimension vanish at one base point is contractible: its map to a point is a weak homotopy equivalence, hence a homotopy equivalence by Whitehead's theorem.