A relative CW complex is the colimit of its skeleta

The skeleta skeletonLT C j of a relative CW complex C in a Hausdorff space, with their inclusions into each other, form a sequential diagram in TopCat (TauCeti.skeletonFunctor), and their inclusions into C form a cocone over it (TauCeti.skeletonCocone). This cocone is a colimit (TauCeti.isColimitSkeletonCocone): this is the weak topology of the complex, and maps out of C are built skeleton by skeleton with TauCeti.exists_continuousMap_prod_complex_of_skeletonLT.

The mathematical source is Hatcher, Algebraic Topology, Appendix, Proposition A.2.

@[reducible, inline]

abbrev TauCeti.skeletonFunctor {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : CategoryTheory.Functor ℕ TopCat

The skeleta skeletonLT C j of a relative CW complex and their inclusions, as a sequential diagram of spaces.

def TauCeti.skeletonCocone {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : CategoryTheory.Limits.Cocone (skeletonFunctor C)

The inclusions of the skeleta into the whole complex.

theorem TauCeti.coe_skeletonCocone_ι_app_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (j : ℕ) (x : ↑(skeletonObj C j)) : ↑((CategoryTheory.ConcreteCategory.hom ((skeletonCocone C).ι.app j)) x) = ↑x

noncomputable def TauCeti.isColimitSkeletonCocone {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : CategoryTheory.Limits.IsColimit (skeletonCocone C)

A relative CW complex is the colimit of its skeleta in TopCat. This is the weak topology of the complex.