Spaces of finite CW type

A topological space has finite CW type (TauCeti.FiniteCWType) if it is homotopy equivalent to a finite CW complex, that is, to a subspace C of a Hausdorff space carrying one of Mathlib's classical CWComplex structures with finitely many cells. The model lives in the same universe as the space, which is where singular homology compares the two.

Finite CW type is the finiteness hypothesis under which homotopy invariants are computed from cells: it is inherited along homotopy equivalences and homeomorphisms, and holds for finite CW complexes themselves. The discrete CW structure on a space makes every finite discrete space a finite CW complex, so finite discrete spaces and contractible spaces, being homotopy equivalent to a point, have finite CW type.

References

• A. Hatcher, Algebraic Topology, Chapter 0.

instance TauCeti.isEmpty_cell_univ_succ {X : Type w} [TopologicalSpace X] [DiscreteTopology X] (n : ℕ) : IsEmpty (Topology.RelCWComplex.cell Set.univ (n + 1))

In the discrete CW structure on a discrete space there are no cells of positive dimension.

theorem TauCeti.nat_card_cell_univ_zero {X : Type w} [TopologicalSpace X] [DiscreteTopology X] : Nat.card (Topology.RelCWComplex.cell Set.univ 0) = Nat.card X

The zero-cells of the discrete CW structure on a discrete space are its points.

instance TauCeti.finiteDimensional_univ_of_discreteTopology {X : Type w} [TopologicalSpace X] [DiscreteTopology X] : Topology.RelCWComplex.FiniteDimensional Set.univ

The discrete CW structure on a discrete space is finite-dimensional.

instance TauCeti.finite_univ_of_discreteTopology {X : Type w} [TopologicalSpace X] [DiscreteTopology X] [Finite X] : Topology.RelCWComplex.Finite Set.univ

The discrete CW structure on a finite discrete space is a finite CW complex.

class TauCeti.FiniteCWType (X : Type w) [TopologicalSpace X] : Prop

A topological space has finite CW type if it is homotopy equivalent to a finite CW complex: a subspace C of a Hausdorff space Y in the same universe, with a classical CW structure having finitely many cells.

• exists_homotopyEquiv : ∃ (Y : Type w) (x : TopologicalSpace Y) (_ : T2Space Y) (C : Set Y) (x_2 : Topology.CWComplex C) (_ : Topology.RelCWComplex.Finite C), Nonempty (ContinuousMap.HomotopyEquiv X ↑C)

  A finite CW complex homotopy equivalent to the space.

instance TauCeti.FiniteCWType.of_cwComplex {Y : Type w} [TopologicalSpace Y] [T2Space Y] (C : Set Y) [Topology.CWComplex C] [Topology.RelCWComplex.Finite C] : FiniteCWType ↑C

A finite CW complex has finite CW type.

theorem ContinuousMap.HomotopyEquiv.finiteCWType {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] [h : TauCeti.FiniteCWType Y] (e : HomotopyEquiv X Y) : TauCeti.FiniteCWType X

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

theorem Homeomorph.finiteCWType {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.FiniteCWType Y] (e : X ≃ₜ Y) : TauCeti.FiniteCWType X

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

theorem ContinuousMap.HomotopyEquiv.finiteCWType_iff {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : TauCeti.FiniteCWType X ↔ TauCeti.FiniteCWType Y

Two homotopy equivalent spaces either both have finite CW type or both do not.

instance TauCeti.FiniteCWType.of_discreteTopology (X : Type w) [TopologicalSpace X] [DiscreteTopology X] [Finite X] : FiniteCWType X

A finite discrete space has finite CW type: it is a finite CW complex with only zero-cells.

instance TauCeti.FiniteCWType.of_contractibleSpace (X : Type w) [TopologicalSpace X] [ContractibleSpace X] : FiniteCWType X

A contractible space has finite CW type: it is homotopy equivalent to a point, the discrete CW complex with a single zero-cell.