Skeletal objects of relative CW complexes

The stages of a relative CW complex's skeletal filtration, bundled as topological spaces. Characteristic-map lemmas describe how open cells sit outside the lower skeleton, how their coordinates are unique, and how cells account for points in consecutive skeleta.

The mathematical source is Hatcher, Algebraic Topology, Section 2.2.

@[reducible, inline]

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

The n-th stage of the skeletal filtration, as an object of TopCat.

Equations

• TauCeti.skeletonObj C n = ↧↑↑(Topology.RelCWComplex.skeletonLT C ↑n)

theorem TauCeti.skeletonLT_eq_complex_of_isEmpty_cell {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → IsEmpty (Topology.RelCWComplex.cell C m)) : ↑(Topology.RelCWComplex.skeletonLT C ↑n) = C

If there are no cells of dimension at least n, the stage skeletonLT C n is the whole relative CW complex, including its base.

theorem TauCeti.map_notMem_skeletonLT {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) {y : Fin n → ℝ} (hy : ‖y‖ < 1) : ↑(Topology.RelCWComplex.map n j) y ∉ ↑(Topology.RelCWComplex.skeletonLT C ↑n)

The characteristic map of an n-cell sends the open unit ball into its open cell, which is disjoint from skeletonLT C n.

theorem TauCeti.map_eq_map_iff {X : Type w} [TopologicalSpace X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} {i j : Topology.RelCWComplex.cell C n} {y z : Fin n → ℝ} (hy : ‖y‖ < 1) (hz : ‖z‖ < 1) : ↑(Topology.RelCWComplex.map n i) y = ↑(Topology.RelCWComplex.map n j) z ↔ i = j ∧ y = z

Two points of open unit balls with the same image under characteristic maps of n-cells come from the same cell and are equal.

theorem TauCeti.mem_skeletonLT_or_exists_map {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} {x : X} (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n) ∨ ∃ (j : Topology.RelCWComplex.cell C n) (y : Fin n → ℝ), ‖y‖ < 1 ∧ ↑(Topology.RelCWComplex.map n j) y = x

A point of skeletonLT C (n + 1) lies in skeletonLT C n or is the image of a point of the open unit ball under the characteristic map of an n-cell.

theorem TauCeti.map_mem_skeletonLT_succ {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) {y : Fin n → ℝ} (hy : ‖y‖ ≤ 1) : ↑(Topology.RelCWComplex.map n j) y ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))

The characteristic map of a closed n-cell lands in the (n + 1)-skeleton.