CW approximation of an arbitrary space

Every space X, path-connected or not, is the target of a weak homotopy equivalence from a CW complex (Hatcher, Proposition 4.13). The CW complex TauCeti.sigmaCWApproximation X is the disjoint union, over the path components c of X, of the CW approximations TauCeti.cwApproximation X x_c built from a chosen point x_c of each component, and TauCeti.sigmaCWApproximationMap X is the map cwApproximationMap X x_c on the summand of c.

It is a weak homotopy equivalence (TauCeti.isWeakHomotopyEquivalence_sigmaCWApproximationMap):

• it is a bijection on path components, since each summand is path-connected and is sent into the path component it approximates (TauCeti.zerothHomotopyMk_sigmaCWApproximationMap);
• on πₖ, k ≥ 1, at a point of the summand of c, it is the inverse of the bijection on πₖ induced by the inclusion of the summand (HomotopyGroup.bijective_map_sigmaMk), followed by the map induced by cwApproximationMap X x_c, which is bijective on πₖ although X need not be path-connected (TauCeti.bijective_homotopyGroupMap_cwApproximationMap).

The disjoint union of CW complexes is a CW complex (Topology.CWComplex.sigmaUniv), so TauCeti.sigmaCWApproximation X has CW type. The lift through an arbitrary weak homotopy equivalence (ContinuousMap.IsWeakHomotopyEquivalence.lift) then makes the construction natural up to homotopy, with no connectedness hypothesis: a map φ : X → Y induces Γφ = TauCeti.sigmaCWApproximationLift φ, for which the square

ΓX --Γφ--> ΓY
 |          |
 v          v
 X ---φ---> Y

commutes up to homotopy (TauCeti.comp_sigmaCWApproximationLift_homotopic, Hatcher, Proposition 4.18), Γφ is determined up to homotopy by this (TauCeti.homotopic_sigmaCWApproximationLift), and Γ is functorial up to homotopy. Any other CW approximation of X is homotopy equivalent to this one compatibly with the maps to X (ContinuousMap.IsWeakHomotopyEquivalence.exists_homotopyEquiv_comp_homotopic).

Main definitions

• TauCeti.sigmaCWApproximation X: the CW approximation of X, one summand for each path component.
• TauCeti.sigmaCWApproximationMap X: its map to X.
• TauCeti.sigmaCWApproximationLift φ: the map of CW approximations induced by φ : X → Y.

Main results

• TauCeti.cwType_sigmaCWApproximation: the approximation has CW type.
• TauCeti.isWeakHomotopyEquivalence_sigmaCWApproximationMap: CW approximation of an arbitrary space.
• TauCeti.comp_sigmaCWApproximationLift_homotopic and TauCeti.homotopic_sigmaCWApproximationLift: naturality up to homotopy, and uniqueness of the induced map.
• TauCeti.sigmaCWApproximationLift_id_homotopic and TauCeti.sigmaCWApproximationLift_comp_homotopic: functoriality up to homotopy.
• TauCeti.isWeakHomotopyEquivalence_sigmaCWApproximationLift_iff: Γφ is a weak homotopy equivalence exactly when φ is.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Propositions 4.13 and 4.18 and Corollary 4.19.

noncomputable def TauCeti.sigmaCWApproximation (X : TopCat) : TopCat

The CW approximation of an arbitrary space X: the disjoint union, over the path components c of X, of the CW approximations TauCeti.cwApproximation X x_c built from the point x_c = Quotient.out c of the component. The body is exposed so that points of the summands are points of this space by definition.

noncomputable def TauCeti.sigmaCWApproximationMap (X : TopCat) : sigmaCWApproximation X ⟶ X

The map from the CW approximation TauCeti.sigmaCWApproximation X to X: on the summand of a path component c, the map TauCeti.cwApproximationMap X x_c.

@[simp]

theorem TauCeti.sigmaCWApproximationMap_mk (X : TopCat) (c : ZerothHomotopy ↑X) (p : ↑(cwApproximation X (Quotient.out c))) : (CategoryTheory.ConcreteCategory.hom (sigmaCWApproximationMap X)) ⟨c, p⟩ = (CategoryTheory.ConcreteCategory.hom (cwApproximationMap X (Quotient.out c))) p

On the summand of c, the map TauCeti.sigmaCWApproximationMap X is TauCeti.cwApproximationMap X x_c.

theorem TauCeti.sigmaCWApproximationMap_comp_sigmaMk (X : TopCat) (c : ZerothHomotopy ↑X) : (TopCat.Hom.hom (sigmaCWApproximationMap X)).comp (ContinuousMap.sigmaMk c) = TopCat.Hom.hom (cwApproximationMap X (Quotient.out c))

The inclusion of the summand of c followed by TauCeti.sigmaCWApproximationMap X is TauCeti.cwApproximationMap X x_c.

@[simp]

theorem TauCeti.zerothHomotopyMk_sigmaCWApproximationMap (X : TopCat) (p : ↑(sigmaCWApproximation X)) : ZerothHomotopy.mk ((CategoryTheory.ConcreteCategory.hom (sigmaCWApproximationMap X)) p) = p.fst

The map TauCeti.sigmaCWApproximationMap X sends the summand of a path component c into c.

instance TauCeti.instT2SpaceSigmaCWApproximation (X : TopCat) : T2Space ↑(sigmaCWApproximation X)

TauCeti.sigmaCWApproximation X is Hausdorff.

instance TauCeti.cwType_sigmaCWApproximation (X : TopCat) : CWType ↑(sigmaCWApproximation X)

The CW approximation of an arbitrary space has CW type: a disjoint union of CW complexes is a CW complex.

theorem TauCeti.isWeakHomotopyEquivalence_sigmaCWApproximationMap (X : TopCat) : (TopCat.Hom.hom (sigmaCWApproximationMap X)).IsWeakHomotopyEquivalence

CW approximation (Hatcher, Proposition 4.13). For every space X, the map TauCeti.sigmaCWApproximationMap X from the CW complex TauCeti.sigmaCWApproximation X to X is a weak homotopy equivalence.

noncomputable def TauCeti.sigmaCWApproximationLift {X Y : TopCat} (φ : C(↑X, ↑Y)) : C(↑(sigmaCWApproximation X), ↑(sigmaCWApproximation Y))

The map Γφ : ΓX → ΓY of CW approximations induced by a map φ : X → Y: a lift of φ ∘ sigmaCWApproximationMap X through the weak homotopy equivalence sigmaCWApproximationMap Y (ContinuousMap.IsWeakHomotopyEquivalence.lift), so that the square of φ and Γφ with the two CW approximation maps commutes up to homotopy (TauCeti.comp_sigmaCWApproximationLift_homotopic). It is determined up to homotopy by this property (TauCeti.homotopic_sigmaCWApproximationLift).

theorem TauCeti.comp_sigmaCWApproximationLift_homotopic {X Y : TopCat} (φ : C(↑X, ↑Y)) : ((TopCat.Hom.hom (sigmaCWApproximationMap Y)).comp (sigmaCWApproximationLift φ)).Homotopic (φ.comp (TopCat.Hom.hom (sigmaCWApproximationMap X)))

CW approximation is natural up to homotopy (Hatcher, Proposition 4.18): sigmaCWApproximationMap Y ∘ Γφ ≃ φ ∘ sigmaCWApproximationMap X.

theorem TauCeti.homotopic_sigmaCWApproximationLift {X Y : TopCat} {φ : C(↑X, ↑Y)} {ψ : C(↑(sigmaCWApproximation X), ↑(sigmaCWApproximation Y))} (hψ : ((TopCat.Hom.hom (sigmaCWApproximationMap Y)).comp ψ).Homotopic (φ.comp (TopCat.Hom.hom (sigmaCWApproximationMap X)))) : ψ.Homotopic (sigmaCWApproximationLift φ)

Uniqueness of the induced map (Hatcher, Proposition 4.18). Every map ψ : ΓX → ΓY for which the CW approximation square of φ commutes up to homotopy is homotopic to Γφ.

theorem TauCeti.sigmaCWApproximationLift_homotopic_of_homotopic {X Y : TopCat} {φ φ' : C(↑X, ↑Y)} (h : φ.Homotopic φ') : (sigmaCWApproximationLift φ).Homotopic (sigmaCWApproximationLift φ')

Homotopic maps induce homotopic maps of CW approximations.

theorem TauCeti.sigmaCWApproximationLift_id_homotopic {X : TopCat} : (sigmaCWApproximationLift (ContinuousMap.id ↑X)).Homotopic (ContinuousMap.id ↑(sigmaCWApproximation X))

The identity induces the identity up to homotopy.

theorem TauCeti.sigmaCWApproximationLift_comp_homotopic {X Y Z : TopCat} (χ : C(↑Y, ↑Z)) (φ : C(↑X, ↑Y)) : (sigmaCWApproximationLift (χ.comp φ)).Homotopic ((sigmaCWApproximationLift χ).comp (sigmaCWApproximationLift φ))

Composites induce composites up to homotopy: Γ(χ ∘ φ) ≃ Γχ ∘ Γφ.

@[simp]

theorem TauCeti.isWeakHomotopyEquivalence_sigmaCWApproximationLift_iff {X Y : TopCat} {φ : C(↑X, ↑Y)} : (sigmaCWApproximationLift φ).IsWeakHomotopyEquivalence ↔ φ.IsWeakHomotopyEquivalence

Γφ is a weak homotopy equivalence exactly when φ is. Since the CW approximations have CW type, Γφ is then a homotopy equivalence by Whitehead's theorem (ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv).