Documentation

TauCeti.Topology.CWComplex.Classical.CWType

Spaces of CW type #

A space has CW type if it is homotopy equivalent to a subspace of a Hausdorff space carrying a classical CW structure. No finiteness condition is imposed on the cells. The model lives in the same universe as the space.

This property permits cellular arguments about homotopy invariants to apply to spaces without a chosen CW structure. In particular, Whitehead's theorem applies to weak homotopy equivalences between spaces of CW type. The property is preserved by homotopy equivalences and homeomorphisms.

References #

source
class TauCeti.CWType (X : Type u) [TopologicalSpace X] :
Prop

A space has CW type if it is homotopy equivalent to a classical CW complex in a Hausdorff ambient space in the same universe.

Instances
    source
    instance TauCeti.CWType.of_cwComplex {Y : Type u} [TopologicalSpace Y] [T2Space Y] (C : Set Y) [Topology.CWComplex C] :
    CWType ↑C

    A classical CW complex has CW type.

    source
    theorem ContinuousMap.HomotopyEquiv.cwType {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [h : TauCeti.CWType Y] (e : HomotopyEquiv X Y) :
    TauCeti.CWType X

    A space homotopy equivalent to a space of CW type has CW type.

    source
    theorem ContinuousMap.HomotopyEquiv.cwType_iff {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) :
    TauCeti.CWType X ↔ TauCeti.CWType Y

    CW type is invariant under homotopy equivalence.

    source
    theorem Homeomorph.cwType {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.CWType Y] (e : X ≃ₜ Y) :
    TauCeti.CWType X

    A space homeomorphic to a space of CW type has CW type.

    source
    instance TauCeti.CWType.of_cwComplex_univ (X : Type u) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] :
    CWType X

    A Hausdorff space with a CW structure on the whole space has CW type. This covers every discrete space, with its points as zero-cells.