CW approximation of path-connected spaces

Every path-connected space X is the target of a weak homotopy equivalence from a CW complex (Hatcher, Proposition 4.13). This file builds one, TauCeti.cwApproximationMap X x, out of the CW complex TauCeti.cwApproximation X x, by attaching cells dimension by dimension, starting from a point x of X. The tower of stages starts with the empty space, and:

• stage 1 is a single 0-cell, sent to x;
• stage 2 attaches a circle at the vertex for every loop of X at x, sent onto that loop, so that the map is surjective on π₁;
• stage n + 2, for n ≥ 1, is the inductive step TauCeti.cwApproximationStep applied to stage n + 1: it attaches (n + 1)-cells killing the kernel of the map on πₙ, and (n + 1)-spheres sent onto representatives of every class of πₙ₊₁(X, x).

So step m of the tower attaches m-cells, and the tower is a CW complex in Mathlib's categorical sense (TauCeti.cwApproximationCWComplex). The space TauCeti.cwApproximation X x is its colimit. It is Hausdorff, has CW type (TauCeti.cwType_cwApproximation), and is path-connected, for every X.

Let k ≥ 1. Stage k + 2 carries the cells of dimension at most k + 1, so it maps onto πₖ of the colimit (Hatcher, Corollary 4.12). Its map to X is injective on πₖ by the inductive step, and surjective on πₖ because it extends the map of stage k + 1. So the map from the colimit is bijective on πₖ, for every X (TauCeti.bijective_homotopyGroupMap_cwApproximationMap), and it is a weak homotopy equivalence when X is path-connected (TauCeti.isWeakHomotopyEquivalence_cwApproximationMap). For a space that is not path-connected, the CW approximation sees only the path component of x; assembling one approximation for each path component gives TauCeti.sigmaCWApproximation.

Main definitions

• TauCeti.cwApproximationStage X x m: stage m + 1 of the tower, with its base point and its map to X.
• TauCeti.cwApproximationTower X x: the tower, as a functor ℕ ⥤ TopCat, starting with the empty space.
• TauCeti.cwApproximation X x: its colimit, with the map TauCeti.cwApproximationMap X x to X and the base point TauCeti.cwApproximationBasepoint X x, which the map sends to x.
• TauCeti.cwApproximationCWComplex X x: the categorical CW structure of the colimit.

Main results

• TauCeti.cwType_cwApproximation: the colimit has CW type.
• TauCeti.bijective_homotopyGroupMap_cwApproximationMap: for every X, the map to X is bijective on πₖ for k ≥ 1, at every point.
• TauCeti.isWeakHomotopyEquivalence_cwApproximationMap: for path-connected X, the map to X is a weak homotopy equivalence.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Proposition 4.13 (CW approximation) and Corollary 4.12.

noncomputable def TauCeti.cwApproximationVertexAttachingMap : PUnit.{u + 1} → (TopCat.diskBoundary 0 ⟶ ⊥_ TopCat)

The attaching map of the single 0-cell of the CW approximation: the empty map out of the empty boundary of the 0-disk into the empty space.

def TauCeti.cwApproximationCircleAttachingMap (X : TopCat) {Y : TopCat} (g : Y ⟶ X) (y : ↑Y) : ↑(GenLoop (Fin 1) (↑X) ((CategoryTheory.ConcreteCategory.hom g) y)) → (TopCat.diskBoundary 1 ⟶ Y)

The attaching maps of the circles of the CW approximation: the constant map at the vertex y, once for every loop of X at the image of y under g.

def TauCeti.cwApproximationStage (X : TopCat) (x : ↑X) : ℕ → (Y : TopCat) × ↑Y × (Y ⟶ X)

The stages of the tower of the CW approximation of X built from x, each with a base point and a map to X. cwApproximationStage X x m is stage m + 1 of the tower, which starts with the empty space:

• stage 1 is a single 0-cell, sent to x;
• stage 2 attaches a circle at the vertex for every loop of X at the image of the vertex, sent onto that loop;
• stage n + 2 is TauCeti.cwApproximationStep applied to stage n + 1, for n ≥ 1.

The body is exposed so that each stage is a cell attachment to the previous one by definition.

noncomputable def TauCeti.cwApproximationStageIncl (X : TopCat) (x : ↑X) (m : ℕ) : (cwApproximationStage X x m).fst ⟶ (cwApproximationStage X x (m + 1)).fst

The inclusion of each stage of the tower into the next. The body is exposed so that the tower is a sequence of cell attachments by definition.

@[simp]

theorem TauCeti.cwApproximationStageIncl_basepoint (X : TopCat) (x : ↑X) (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (cwApproximationStageIncl X x m)) (cwApproximationStage X x m).snd.1 = (cwApproximationStage X x (m + 1)).snd.1

The inclusion of each stage into the next preserves the base points.

@[simp]

theorem TauCeti.cwApproximationStageIncl_comp (X : TopCat) (x : ↑X) (m : ℕ) : CategoryTheory.CategoryStruct.comp (cwApproximationStageIncl X x m) (cwApproximationStage X x (m + 1)).snd.2 = (cwApproximationStage X x m).snd.2

The map of each stage to X extends the map of the previous stage.

@[simp]

theorem TauCeti.cwApproximationStageIncl_comp_assoc (X : TopCat) (x : ↑X) (m : ℕ) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (cwApproximationStageIncl X x m) (CategoryTheory.CategoryStruct.comp (cwApproximationStage X x (m + 1)).snd.2 h) = CategoryTheory.CategoryStruct.comp (cwApproximationStage X x m).snd.2 h

The map of each stage to X extends the map of the previous stage.

noncomputable def TauCeti.cwApproximationTower (X : TopCat) (x : ↑X) : CategoryTheory.Functor ℕ TopCat

The tower of the CW approximation of X built from x, as a functor ℕ ⥤ TopCat: the empty space, followed by the stages TauCeti.cwApproximationStage X x and their inclusions. The body is exposed so that its objects are the stages by definition.

@[simp]

theorem TauCeti.cwApproximationTower_map_homOfLE_succ (X : TopCat) (x : ↑X) (m : ℕ) : (cwApproximationTower X x).map (CategoryTheory.homOfLE ⋯) = cwApproximationStageIncl X x m

The step from stage m + 1 to stage m + 2 of the tower is the inclusion of the stages.

noncomputable def TauCeti.cwApproximation (X : TopCat) (x : ↑X) : TopCat

The CW approximation of X built from x: the colimit of the tower TauCeti.cwApproximationTower X x. The body is exposed so that the colimit inclusions of the stages are maps into this space by definition.

noncomputable def TauCeti.cwApproximationMap (X : TopCat) (x : ↑X) : cwApproximation X x ⟶ X

The map from the CW approximation TauCeti.cwApproximation X x to X, induced by the maps of the stages.

@[simp]

theorem TauCeti.colimit_ι_cwApproximationMap (X : TopCat) (x : ↑X) (m : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (cwApproximationTower X x) (m + 1)) (cwApproximationMap X x) = (cwApproximationStage X x m).snd.2

On each stage, the map TauCeti.cwApproximationMap X x is the map of the stage.

theorem TauCeti.colimit_ι_cwApproximationMap_assoc (X : TopCat) (x : ↑X) (m : ℕ) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (cwApproximationTower X x) (m + 1)) (cwApproximationMap X x)) h = CategoryTheory.CategoryStruct.comp (cwApproximationStage X x m).snd.2 h

On each stage, the map TauCeti.cwApproximationMap X x is the map of the stage.

noncomputable def TauCeti.cwApproximationCWComplex (X : TopCat) (x : ↑X) : (cwApproximation X x).CWComplex

The CW approximation is a CW complex, in Mathlib's categorical sense: step m of its tower attaches m-cells to the previous stage.

instance TauCeti.instT2SpaceCWApproximation (X : TopCat) (x : ↑X) : T2Space ↑(cwApproximation X x)

TauCeti.cwApproximation X x is Hausdorff.

instance TauCeti.cwType_cwApproximation (X : TopCat) (x : ↑X) : CWType ↑(cwApproximation X x)

The CW approximation has CW type.

instance TauCeti.instT2SpaceCWApproximationStage (X : TopCat) (x : ↑X) (m : ℕ) : T2Space ↑(cwApproximationStage X x m).fst

Every stage of the tower is Hausdorff, as a closed subspace of the colimit.

@[simp]

theorem TauCeti.cwApproximationStage_map_basepoint (X : TopCat) (x : ↑X) (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (cwApproximationStage X x m).snd.2) (cwApproximationStage X x m).snd.1 = x

The map of each stage to X sends the base point of the stage to x.

noncomputable def TauCeti.cwApproximationBasepoint (X : TopCat) (x : ↑X) : ↑(cwApproximation X x)

The base point of the CW approximation TauCeti.cwApproximation X x: the image of the vertex of stage 1.

@[simp]

theorem TauCeti.colimit_ι_cwApproximationBasepoint (X : TopCat) (x : ↑X) (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι (cwApproximationTower X x) (m + 1))) (cwApproximationStage X x m).snd.1 = cwApproximationBasepoint X x

The base point of each stage goes to the base point of the CW approximation.

@[simp]

theorem TauCeti.cwApproximationMap_cwApproximationBasepoint (X : TopCat) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (cwApproximationMap X x)) (cwApproximationBasepoint X x) = x

The map TauCeti.cwApproximationMap X x sends the base point of the CW approximation to x.

instance TauCeti.instPathConnectedSpaceCWApproximation (X : TopCat) (x : ↑X) : PathConnectedSpace ↑(cwApproximation X x)

The CW approximation is path-connected: its only 0-cell is the vertex.

theorem TauCeti.bijective_homotopyGroupMap_cwApproximationMap (X : TopCat) (x : ↑X) (k : ℕ) (p : ↑(cwApproximation X x)) : Function.Bijective (HomotopyGroup.map (TopCat.Hom.hom (cwApproximationMap X x)) ⋯)

The map TauCeti.cwApproximationMap X x induces a bijection on πₖ₊₁ at every point, whether or not X is path-connected: the CW approximation only sees the path component of x.

theorem TauCeti.isWeakHomotopyEquivalence_cwApproximationMap (X : TopCat) (x : ↑X) [PathConnectedSpace ↑X] : (TopCat.Hom.hom (cwApproximationMap X x)).IsWeakHomotopyEquivalence

CW approximation (Hatcher, Proposition 4.13). For a path-connected space X, the map TauCeti.cwApproximationMap X x from the CW complex TauCeti.cwApproximation X x to X is a weak homotopy equivalence.