Skeletal induction for relative CW complexes

Continuous maps out of a relative CW complex C, and more generally out of Z × C for a locally compact space Z, can be built one skeleton at a time.

• Passing from skeletonLT C n to skeletonLT C (n + 1) means extending over the closed n-cells. A map on Z × skeletonLT C n, together with one map on Z × closedBall 0 1 for each n-cell that agrees with it on Z × sphere 0 1 through the characteristic map, glues to a continuous map on Z × skeletonLT C (n + 1).
• Maps on Z × skeletonLT C (k + j) for all j : ℕ, each restricting to the previous one, glue to a continuous map on Z × C.

In both cases continuity of the glued map is the weak-topology axiom of the complex, in the form TauCeti.continuous_prod_complex_iff. Taking Z = I builds homotopies, as in the proof that relative CW inclusions have the homotopy extension property; taking Z to be a point builds maps, as in the extension lemma for maps into a space whose spheres are null-homotopic.

Main results

• TauCeti.exists_continuousMap_prod_skeletonLT_succ: extension over the closed n-cells, from Z × skeletonLT C n to Z × skeletonLT C (n + 1).
• TauCeti.exists_continuousMap_closedCell_comp_map: a map on the closed ball compatible on its boundary with a map on skeletonLT C n descends to the closed n-cell.
• TauCeti.exists_continuousMap_prod_complex_of_skeletonLT: a compatible family of maps on the products of Z with the skeleta from the k-th one on glues to a map on Z × C.

References

• A. Hatcher, Algebraic Topology, Chapter 0, Proposition 0.16, and Section 4.1, Lemma 4.7, where maps and homotopies are extended over a CW complex cell by cell and skeleton by skeleton.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter II.

theorem TauCeti.exists_continuousMap_prod_skeletonLT_succ {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Z : Type u_1} {Y : Type u_2} [TopologicalSpace Z] [TopologicalSpace Y] {n : ℕ} (G : C(Z × ↑↑(Topology.RelCWComplex.skeletonLT C ↑n), Y)) (K : Topology.RelCWComplex.cell C n → C(Z × ↑(Metric.closedBall 0 1), Y)) [LocallyCompactSpace Z] (hK : ∀ (j : Topology.RelCWComplex.cell C n) (z : Z) (y : ↑(Metric.closedBall 0 1)) (hy : ↑y ∈ Metric.sphere 0 1), (K j) (z, y) = G (z, ⟨↑(Topology.RelCWComplex.map n j) ↑y, ⋯⟩)) : ∃ (F : C(Z × ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)), Y)), (∀ (z : Z) (x : X) (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)), F (z, ⟨x, ⋯⟩) = G (z, ⟨x, hx⟩)) ∧ ∀ (j : Topology.RelCWComplex.cell C n) (z : Z) (y : ↑(Metric.closedBall 0 1)), F (z, ⟨↑(Topology.RelCWComplex.map n j) ↑y, ⋯⟩) = (K j) (z, y)

Extension over the closed n-cells. A map G on Z × skeletonLT C n and maps K j on Z × closedBall 0 1, one for each n-cell j, that agree with G on Z × sphere 0 1 through the characteristic map of j, glue to a continuous map on Z × skeletonLT C (n + 1) that restricts to G and, through each characteristic map, to K j.

theorem TauCeti.exists_continuousMap_closedCell_comp_map {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Y : Type u_2} [TopologicalSpace Y] {n : ℕ} (j : Topology.RelCWComplex.cell C n) (ψ : C(Fin n → ℝ, Y)) (f : C(↑↑(Topology.RelCWComplex.skeletonLT C ↑n), Y)) (hψ : ∀ (y : Fin n → ℝ) (hy : y ∈ Metric.sphere 0 1), ψ y = f ⟨↑(Topology.RelCWComplex.map n j) y, ⋯⟩) : ∃ (L : C(↑(Topology.RelCWComplex.closedCell n j), Y)), ∀ (y : ↑(Metric.closedBall 0 1)), L ⟨↑(Topology.RelCWComplex.map n j) ↑y, ⋯⟩ = ψ ↑y

Descent to a closed cell. A map ψ on the closed ball that agrees on the boundary sphere, through the characteristic map of an n-cell j, with a map f on skeletonLT C n, descends along the characteristic map to a continuous map on the closed cell of j.

theorem TauCeti.exists_continuousMap_prod_complex_of_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Z : Type u_1} {Y : Type u_2} [TopologicalSpace Z] [TopologicalSpace Y] {k : ℕ} (F : (j : ℕ) → C(Z × ↑↑(Topology.RelCWComplex.skeletonLT C ↑(k + j)), Y)) [LocallyCompactSpace Z] (hF : ∀ (j : ℕ) (z : Z) (x : X) (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(k + j))), (F (j + 1)) (z, ⟨x, ⋯⟩) = (F j) (z, ⟨x, hx⟩)) : ∃ (G : C(Z × ↑C, Y)), ∀ (j : ℕ) (z : Z) (x : X) (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(k + j))), G (z, ⟨x, ⋯⟩) = (F j) (z, ⟨x, hx⟩)

Gluing over the skeleta. Maps F j on Z × skeletonLT C (k + j) for all j : ℕ, each restricting to the previous one, glue to a continuous map on Z × C that restricts to every F j.