CW-complexes

This file defines (relative) CW-complexes using a categorical approach.

Main definitions

• RelativeCWComplex: A relative CW-complex is the colimit of an expanding sequence of subspaces sk i (called the $(i-1)$-skeleton) for i ≥ 0, where sk 0 (i.e., the $(-1)$-skeleton) is an arbitrary topological space, and each sk (n + 1) (i.e., the $n$-skeleton) is obtained from sk n (i.e., the $(n-1)$-skeleton) by attaching n-disks.

• CWComplex: A CW-complex is a relative CW-complex whose sk 0 (i.e., $(-1)$-skeleton) is empty.

Implementation Notes

This file provides a categorical approach to CW complexes, defining them via colimits and transfinite compositions. For a classical approach that defines CW complexes via explicit cells and attaching maps, see Topology.CWComplex.Classical.Basic. The two approaches are equivalent but serve different purposes:

• This approach is more suitable for categorical arguments and generalizations
• The classical approach is more convenient for concrete geometric arguments

References

• [R. Fritsch and R. Piccinini, Cellular Structures in Topology][fritsch-piccinini1990]

TODO

• Prove the equivalence between this categorical approach and the classical approach in Topology.CWComplex.Classical.Basic. Currently there is no way to move between the two definitions.

@[reducible, inline]

abbrev TopCat.RelativeCWComplex.basicCell (n : ℕ) : Unit → (diskBoundary n ⟶ disk n)

For each n : ℕ, this is the family of morphisms which sends the unique element of Unit to diskBoundaryInclusion n : ∂𝔻 n ⟶ 𝔻 n.

Equations

• TopCat.RelativeCWComplex.basicCell n x✝ = TopCat.diskBoundaryInclusion n

@[reducible, inline]

abbrev TopCat.RelativeCWComplex {X Y : TopCat} (f : X ⟶ Y) : Type (u + 1)

A relative CW-complex is a morphism f : X ⟶ Y equipped with data expressing that Y identifies to the colimit of a functor F : ℕ ⥤ TopCat with that F.obj 0 ≅ X and for any n : ℕ, F.obj (n + 1) is obtained from F.obj n by attaching n-disks.

Equations

• TopCat.RelativeCWComplex f = HomotopicalAlgebra.RelativeCellComplex TopCat.RelativeCWComplex.basicCell f

@[reducible, inline]

abbrev TopCat.CWComplex (X : TopCat) : Type (u + 1)

A CW-complex is a topological space such that ⊥_ _ ⟶ X is a relative CW-complex.

Equations

• X.CWComplex = TopCat.RelativeCWComplex (CategoryTheory.Limits.initial.to X)