The pair of a CW complex and its skeleton is highly connected

Let C be a relative CW complex with base D in a Hausdorff space, and write Xⁿ = skeletonLT C (n + 1) for its n-skeleton. This file proves Hatcher's Corollary 4.12: the pair (C, Xⁿ) is n-connected. That is, the relative homotopy set π_{k+1}(C, Xⁿ, a) is trivial for k + 1 ≤ n and every a ∈ Xⁿ (TauCeti.subsingleton_relHomotopyGroup_skeletonLT), and so the inclusion Xⁿ ↪ C induces a surjection π_k(Xⁿ, a) → π_k(C, a) for k ≤ n (TauCeti.surjective_homotopyGroupMap_skeletonLT) and an injection for k < n (TauCeti.injective_homotopyGroupMap_skeletonLT). In degree zero these say that every point of C is joined by a path to a point of Xⁿ, and that for n ≥ 1 two points of Xⁿ joined by a path in C are joined by a path in Xⁿ.

The subspace A of the statements is any set equal to Xⁿ, together with the inclusion A ⊆ C from which the pair (C, A) is built. Taking A = Xⁿ gives the statement about the skeleton. When C has no cells of dimension at most n, the skeleton Xⁿ is the base D (TauCeti.skeletonLT_eq_base_of_isEmpty_cell), and taking A = D gives Hatcher's statement for a CW pair (C, D) all of whose cells outside D have dimension greater than n: attaching such cells does not change π_k for k < n, and induces a surjection on π_n.

The input is the compression of maps of low-dimensional compacta into skeleta (TauCeti.exists_homotopicRel_skeletonLT_finrank), the step of cellular approximation that concerns a single map. A relative cube I × Iᵏ → C is a map of pairs (I × Iᵏ, ∂(I × Iᵏ)) → (C, Xⁿ) out of a compactum of dimension k + 1 ≤ n, so it is homotopic, relative to the boundary of the cube, to a map into Xⁿ; by the compression criterion (TauCeti.RelHomotopyGroup.subsingleton_iff) its class is trivial. The absolute statements follow from the exact homotopy sequence of the pair (C, Xⁿ).

Main results

• TauCeti.subsingleton_relHomotopyGroup_skeletonLT: π_{k+1}(C, Xⁿ, a) is trivial for k < n.
• TauCeti.exists_joined_skeletonLT, TauCeti.joined_skeletonLT_iff: every point of C is joined to Xⁿ, and for n ≥ 1 points of Xⁿ joined in C are joined in Xⁿ.
• TauCeti.surjective_homotopyGroupMap_skeletonLT: π_k(Xⁿ, a) → π_k(C, a) is surjective for k ≤ n.
• TauCeti.injective_homotopyGroupMap_skeletonLT: π_k(Xⁿ, a) → π_k(C, a) is injective for k < n.
• TauCeti.isNConnected_inclusion_skeletonLT: the inclusion Xⁿ ↪ C is an n-connected map.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Corollary 4.12.

theorem TauCeti.subsingleton_relHomotopyGroup_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} {N : Type v} [Finite N] (hN : Nat.card N < n) (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) (a : ↑A) : Subsingleton (RelHomotopyGroup N { pair := TopPair.ofInclusion hAC, basepoint := a })

The pair (C, Xⁿ) is n-connected (Hatcher, Corollary 4.12). If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then the relative homotopy set π_{k+1}(C, A, a) is trivial for every a ∈ A, where k = Nat.card N < n.

theorem TauCeti.surjective_homotopyGroupMap_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} {N : Type v} [Finite N] (hN : Nat.card N ≤ n) (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) (a : ↑A) : Function.Surjective (HomotopyGroup.map (ContinuousMap.inclusion hAC) ⋯)

The inclusion of the n-skeleton is surjective on π_k for k ≤ n (Hatcher, Corollary 4.12). If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then the inclusion A ↪ C induces a surjection π_k(A, a) → π_k(C, a), where k = Nat.card N ≤ n.

theorem TauCeti.injective_homotopyGroupMap_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} {N : Type v} [Finite N] (hN : Nat.card N < n) (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) (a : ↑A) : Function.Injective (HomotopyGroup.map (ContinuousMap.inclusion hAC) ⋯)

The inclusion of the n-skeleton is injective on π_k for k < n (Hatcher, Corollary 4.12). If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then the inclusion A ↪ C induces an injection π_k(A, a) → π_k(C, a), where k = Nat.card N < n.

theorem TauCeti.isNConnected_inclusion_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) : (ContinuousMap.inclusion hAC).IsNConnected n

The inclusion of the n-skeleton is an n-connected map (Hatcher, Corollary 4.12). If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then the inclusion A ↪ C is n-connected.