The skeleton with the cores of its top cells removed

Let C be a relative CW complex and n : ℕ, and write Xⁿ = skeletonLT C (n + 1) and Xⁿ⁻¹ = skeletonLT C n for the skeleta made of the cells of dimension at most n and below n. Removing from Xⁿ the image map n j '' ball 0 2⁻¹ of the inner half of every open n-cell leaves TauCeti.skeletonNeighborhood C n: Xⁿ⁻¹ together with the outer halves of the open n-cells. It is a neighbourhood of Xⁿ⁻¹ in Xⁿ, and it deformation retracts onto Xⁿ⁻¹, so (Xⁿ, Xⁿ⁻¹) is a good pair in the sense of Hatcher.

The deformation is one homotopy TauCeti.skeletonNeighborhoodHomotopy C n of the whole of Xⁿ, starting at the identity. Inside each closed n-cell, read through the characteristic map, it pushes points radially outwards: the point y of the closed unit ball moves along the segment from y to 2 • y if ‖y‖ ≤ 2⁻¹, and to ‖y‖⁻¹ • y otherwise. It fixes Xⁿ⁻¹ pointwise at all times, keeps skeletonNeighborhood C n inside itself at all times, and at the end sends skeletonNeighborhood C n into Xⁿ⁻¹. Consequently the inclusion of pairs (Xⁿ, Xⁿ⁻¹) ⟶ (Xⁿ, skeletonNeighborhood C n) is a homotopy equivalence of pairs, while in the second pair Xⁿ⁻¹ lies in the interior of the subspace and can be excised.

Main definitions

• TauCeti.skeletonNeighborhood C n: Xⁿ minus the inner halves of the open n-cells.
• TauCeti.skeletonNeighborhoodHomotopy C n: the homotopy of Xⁿ from the identity to TauCeti.skeletonNeighborhoodEndpoint C n.

Main results

• TauCeti.isClosed_iUnion_map_closedBall: the closed cores of radius r < 1 of the open n-cells form a closed set.
• TauCeti.skeletonLT_subset_interior_skeletonNeighborhood: skeletonNeighborhood C n is a neighbourhood of Xⁿ⁻¹ in Xⁿ.
• TauCeti.skeletonNeighborhoodHomotopy_apply_of_mem: the homotopy fixes Xⁿ⁻¹.
• TauCeti.skeletonNeighborhoodHomotopy_mem: the homotopy keeps skeletonNeighborhood C n inside itself.
• TauCeti.skeletonNeighborhoodEndpoint_mem: its endpoint sends skeletonNeighborhood C n into Xⁿ⁻¹.

References

• A. Hatcher, Algebraic Topology, Section 2.1 (good pairs) and Section 2.2, Lemma 2.34, whose proof uses that (Xⁿ, Xⁿ⁻¹) is a good pair.

def TauCeti.skeletonNeighborhood {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : Set X

The n-skeleton Xⁿ = skeletonLT C (n + 1) of a relative CW complex with the inner half map n j '' ball 0 2⁻¹ of every open n-cell removed: Xⁿ⁻¹ = skeletonLT C n together with the outer halves of the open n-cells. It is a neighbourhood of Xⁿ⁻¹ in Xⁿ (TauCeti.skeletonLT_subset_interior_skeletonNeighborhood) which deformation retracts onto Xⁿ⁻¹ through TauCeti.skeletonNeighborhoodHomotopy.

Equations

• TauCeti.skeletonNeighborhood C n = ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)) \ ⋃ (j : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n j) '' Metric.ball 0 2⁻¹

theorem TauCeti.mem_skeletonNeighborhood {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} {x : X} : x ∈ skeletonNeighborhood C n ↔ x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)) ∧ ∀ (j : Topology.RelCWComplex.cell C n) (y : Fin n → ℝ), ‖y‖ < 2⁻¹ → ↑(Topology.RelCWComplex.map n j) y ≠ x

theorem TauCeti.skeletonNeighborhood_subset_skeletonLT_succ {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonNeighborhood C n ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))

theorem TauCeti.skeletonLT_subset_skeletonNeighborhood {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeletonLT C ↑n) ⊆ skeletonNeighborhood C n

theorem TauCeti.isClosed_iUnion_map_closedBall {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (n : ℕ) {r : ℝ} (hr : r < 1) : IsClosed (⋃ (j : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n j) '' Metric.closedBall 0 r)

The closed cores of the open n-cells form a closed set: for r < 1, the union over all n-cells of the images of the closed ball of radius r under the characteristic maps is closed. Each core lies in its open cell. A closed cell of dimension n meets the union only in its own compact core; open cells of other dimensions are disjoint from it.

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

TauCeti.skeletonNeighborhood C n is a neighbourhood of Xⁿ⁻¹ = skeletonLT C n in Xⁿ = skeletonLT C (n + 1).

@[simp]

theorem TauCeti.map_mem_skeletonNeighborhood_iff {X : Type u} [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 ∈ skeletonNeighborhood C n ↔ 2⁻¹ ≤ ‖y‖

A point of a closed n-cell belongs to the skeletal neighborhood exactly when it lies outside the inner half of its cell.

noncomputable def TauCeti.skeletonNeighborhoodEndpoint {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : C(↥(Topology.RelCWComplex.skeletonLT C ↑(n + 1)), ↥(Topology.RelCWComplex.skeletonLT C ↑(n + 1)))

The endpoint of TauCeti.skeletonNeighborhoodHomotopy: the self-map of Xⁿ = skeletonLT C (n + 1) which pushes the outer half of every open n-cell onto its boundary and expands the inner half over the whole cell. It sends TauCeti.skeletonNeighborhood C n into Xⁿ⁻¹ = skeletonLT C n.

Equations

• TauCeti.skeletonNeighborhoodEndpoint C n = (TauCeti.pushMap✝ C n).curry 1

noncomputable def TauCeti.skeletonNeighborhoodHomotopy {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : (ContinuousMap.id ↥(Topology.RelCWComplex.skeletonLT C ↑(n + 1))).Homotopy (skeletonNeighborhoodEndpoint C n)

The radial deformation of the n-skeleton Xⁿ = skeletonLT C (n + 1) of a relative CW complex: inside each closed n-cell, read through the characteristic map, it moves y along the segment from y to 2 • y if ‖y‖ ≤ 2⁻¹ and to ‖y‖⁻¹ • y otherwise. It fixes Xⁿ⁻¹ = skeletonLT C n, keeps TauCeti.skeletonNeighborhood C n inside itself, and ends at TauCeti.skeletonNeighborhoodEndpoint C n.

Equations

• TauCeti.skeletonNeighborhoodHomotopy C n = { toContinuousMap := TauCeti.pushMap✝ C n, map_zero_left := ⋯, map_one_left := ⋯ }

theorem TauCeti.skeletonNeighborhoodHomotopy_map {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (t : ↑unitInterval) (j : Topology.RelCWComplex.cell C n) {y : Fin n → ℝ} (hy : ‖y‖ ≤ 1) (x : ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (hx : ↑x = ↑(Topology.RelCWComplex.map n j) y) : ↑((skeletonNeighborhoodHomotopy C n) (t, x)) = ↑(Topology.RelCWComplex.map n j) (radialPush 2⁻¹ t y)

On a closed n-cell, the skeletal deformation is the straight-line homotopy TauCeti.radialPush 2⁻¹ to the scaled radial retraction, read through the characteristic map.

@[simp]

theorem TauCeti.skeletonNeighborhoodHomotopy_apply_of_mem {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (t : ↑unitInterval) (x : ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (hx : ↑x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)) : (skeletonNeighborhoodHomotopy C n) (t, x) = x

The deformation fixes Xⁿ⁻¹ = skeletonLT C n pointwise.

@[simp]

theorem TauCeti.skeletonNeighborhoodEndpoint_apply_of_mem {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (x : ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (hx : ↑x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)) : (skeletonNeighborhoodEndpoint C n) x = x

The endpoint of the deformation fixes Xⁿ⁻¹ = skeletonLT C n pointwise.

theorem TauCeti.skeletonNeighborhoodHomotopy_mem {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (t : ↑unitInterval) (x : ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (hx : ↑x ∈ skeletonNeighborhood C n) : ↑((skeletonNeighborhoodHomotopy C n) (t, x)) ∈ skeletonNeighborhood C n

The deformation keeps TauCeti.skeletonNeighborhood C n inside itself at every time.

theorem TauCeti.skeletonNeighborhoodEndpoint_mem {X : Type u} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (x : ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) (hx : ↑x ∈ skeletonNeighborhood C n) : ↑((skeletonNeighborhoodEndpoint C n) x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)

The endpoint of the deformation sends TauCeti.skeletonNeighborhood C n into Xⁿ⁻¹ = skeletonLT C n.