Relative CW inclusions are closed cofibrations

The base D of a relative CW complex C has the homotopy extension property inside C, and so does every skeleton of C. As X is Hausdorff, these subsets are closed (TauCeti.HasHomotopyExtensionProperty.isClosed), so their inclusions are closed cofibrations. This is what makes skeletal induction and homotopy-invariance arguments for CW pairs work: maps and homotopies can be modified on the base or on a skeleton and extended over the whole complex.

Main results

• TauCeti.hasHomotopyExtensionProperty_skeletonLT_succ: skeletonLT C n has the homotopy extension property inside skeletonLT C (n + 1).
• TauCeti.hasHomotopyExtensionProperty_skeletonLT: every skeleton has the homotopy extension property inside the complex.
• TauCeti.hasHomotopyExtensionProperty_base: the base of a relative CW complex has the homotopy extension property inside the complex.

Related results

TauCeti.hasHomotopyExtensionProperty_sphere_closedBall gives the homotopy extension property for the boundary of a closed cell. The homotopies are extended over the closed cells and glued over the skeleta by TauCeti.exists_continuousMap_prod_skeletonLT_succ and TauCeti.exists_continuousMap_prod_complex_of_skeletonLT.

References

• A. Hatcher, Algebraic Topology, Chapter 0, Proposition 0.16: a CW pair has the homotopy extension property.

theorem TauCeti.hasHomotopyExtensionProperty_skeletonLT_succ {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) : HasHomotopyExtensionProperty (Subtype.val ⁻¹' ↑(Topology.RelCWComplex.skeletonLT C ↑n))

skeletonLT C n has the homotopy extension property inside skeletonLT C (n + 1).

theorem TauCeti.hasHomotopyExtensionProperty_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (k : ℕ) : HasHomotopyExtensionProperty (Subtype.val ⁻¹' ↑(Topology.RelCWComplex.skeletonLT C ↑k))

Every skeleton of a relative CW complex has the homotopy extension property inside the complex.

theorem TauCeti.hasHomotopyExtensionProperty_base {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] : HasHomotopyExtensionProperty (Subtype.val ⁻¹' D)

Relative CW inclusions are cofibrations: the base of a relative CW complex has the homotopy extension property inside the complex. The base is also closed (TauCeti.HasHomotopyExtensionProperty.isClosed), so the inclusion is a closed cofibration.