Attaching cells: homotopy groups below their dimension, and killing π_n

Let Y be obtained from a Hausdorff space X by attaching (n + 1)-cells along maps of their boundary spheres Sⁿ → X, and let f : X ⟶ Y be the inclusion. Then f induces a bijection π_k(X, x) → π_k(Y, f x) for k < n and a surjection for k = n, at every base point x (HomotopicalAlgebra.AttachCells.bijective_homotopyGroupMap, HomotopicalAlgebra.AttachCells.surjective_homotopyGroupMap). For the space TauCeti.cellAttachment φ obtained by attaching cells along a family φ of maps from spheres, these are TauCeti.bijective_homotopyGroupMap_cellAttachmentIncl and TauCeti.surjective_homotopyGroupMap_cellAttachmentIncl.

This is Hatcher's Corollary 4.12 for the pair (Y, X), all of whose cells outside X have dimension n + 1. More generally, for any relative CW complex f : X ⟶ Y in Mathlib's categorical sense, on a Hausdorff space X, the classical skeleton skeletonLT Y (n + 1) is the image of the stage c.F.obj (n + 1), and it is the range of f when no cells of dimension at most n are attached. So the statements for the inclusion of a skeleton (TauCeti.surjective_homotopyGroupMap_skeletonLT, TauCeti.injective_homotopyGroupMap_skeletonLT) apply: the stage c.F.obj (n + 1) is surjective on π_k for k ≤ n (TopCat.RelativeCWComplex.surjective_homotopyGroupMap_incl_app), and f is bijective on π_k for k < n when there are no cells of dimension at most n (TopCat.RelativeCWComplex.bijective_homotopyGroupMap). The stages and f are closed embeddings, which identifies them with their ranges. Attaching cells of a single dimension is such a relative CW complex (HomotopicalAlgebra.AttachCells.toRelativeCWComplex).

Conversely, a cell attached along the constant map at x closes up to a sphere at x, so a map out of Y that is a generalized loop γ on such a cell sends the class of that sphere to the class of γ (TauCeti.mk_mem_range_homotopyGroupMap_of_cellAttachmentCell_comp). This is how cells realize classes of a target space in CW approximation.

When n ≥ 1, attaching cells kills chosen classes of π_n(X, x). A generalized loop p representing a class gives the attaching map GenLoop.diskBoundaryMap p, the corresponding pointed map Sⁿ → X. It becomes null-homotopic in Y (TauCeti.cellAttachment_attachingMap_nullhomotopic), so the class of p maps to the identity (TauCeti.map_cellAttachmentIncl_mk_eq_one). If the classes of the attaching loops generate π_n(X, x) as a normal subgroup, the surjection on π_n then makes π_n(Y, f x) trivial (TauCeti.subsingleton_homotopyGroup_cellAttachment).

Main results

• TopCat.RelativeCWComplex.surjective_homotopyGroupMap_incl_app: the stage carrying the cells of dimension at most n of a relative CW complex is surjective on π_k for k ≤ n.
• TopCat.RelativeCWComplex.surjective_homotopyGroupMap, TopCat.RelativeCWComplex.bijective_homotopyGroupMap: a relative CW complex without cells of dimension at most n is surjective on π_k for k ≤ n and bijective for k < n.
• HomotopicalAlgebra.AttachCells.surjective_homotopyGroupMap: attaching (n + 1)-cells is surjective on π_k for k ≤ n.
• HomotopicalAlgebra.AttachCells.bijective_homotopyGroupMap: attaching (n + 1)-cells is bijective on π_k for k < n.
• TauCeti.mk_mem_range_homotopyGroupMap_of_cellAttachmentCell_comp: a cell attached along a constant map realizes the class of the generalized loop it is sent onto.
• TauCeti.subsingleton_homotopyGroup_cellAttachment: attaching (n + 1)-cells along generators of π_n(X, x) kills π_n.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Corollary 4.12, the same section for attaching cells to kill homotopy groups, and Proposition 4.13 for attaching spheres to realize them.

theorem TopCat.RelativeCWComplex.surjective_homotopyGroupMap_incl_app {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑X] {N : Type v} [Finite N] {n : ℕ} (hN : Nat.card N ≤ n) (y : ↑(c.F.obj (n + 1))) : Function.Surjective (HomotopyGroup.map (Hom.hom (c.incl.app (n + 1))) ⋯)

A stage of a relative CW complex is surjective on π_k below its dimension (Hatcher, Corollary 4.12). If f : X ⟶ Y is a relative CW complex on a Hausdorff space X, the inclusion of the stage c.F.obj (n + 1), which carries the cells of dimension at most n, induces a surjection π_k(c.F.obj (n + 1), y) → π_k(Y, y), where k = Nat.card N ≤ n.

theorem TopCat.RelativeCWComplex.surjective_homotopyGroupMap {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑X] {N : Type v} [Finite N] {n : ℕ} (hc : ∀ m ≤ n, IsEmpty (c.attachCells m ⋯).ι) (hN : Nat.card N ≤ n) (x : ↑X) : Function.Surjective (HomotopyGroup.map (Hom.hom f) ⋯)

A relative CW complex without cells of dimension at most n is surjective on π_k for k ≤ n (Hatcher, Corollary 4.12). If f : X ⟶ Y is a relative CW complex on a Hausdorff space X all of whose cells have dimension greater than n, then f induces a surjection π_k(X, x) → π_k(Y, f x), where k = Nat.card N ≤ n.

theorem TopCat.RelativeCWComplex.bijective_homotopyGroupMap {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑X] {N : Type v} [Finite N] {n : ℕ} (hc : ∀ m ≤ n, IsEmpty (c.attachCells m ⋯).ι) (hN : Nat.card N < n) (x : ↑X) : Function.Bijective (HomotopyGroup.map (Hom.hom f) ⋯)

A relative CW complex without cells of dimension at most n is bijective on π_k for k < n (Hatcher, Corollary 4.12). If f : X ⟶ Y is a relative CW complex on a Hausdorff space X all of whose cells have dimension greater than n, then f induces a bijection π_k(X, x) → π_k(Y, f x), where k = Nat.card N < n.

theorem HomotopicalAlgebra.AttachCells.surjective_homotopyGroupMap {X Y : TopCat} {f : X ⟶ Y} {N : Type v} [T2Space ↑X] [Finite N] {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell (n + 1)) f) (hN : Nat.card N ≤ n) (x : ↑X) : Function.Surjective (HomotopyGroup.map (TopCat.Hom.hom f) ⋯)

Attaching (n + 1)-cells is surjective on π_k for k ≤ n (Hatcher, Corollary 4.12). If Y is obtained from a Hausdorff space X by attaching (n + 1)-disks along f, then f induces a surjection π_k(X, x) → π_k(Y, f x), where k = Nat.card N ≤ n.

theorem HomotopicalAlgebra.AttachCells.bijective_homotopyGroupMap {X Y : TopCat} {f : X ⟶ Y} {N : Type v} [T2Space ↑X] [Finite N] {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell (n + 1)) f) (hN : Nat.card N < n) (x : ↑X) : Function.Bijective (HomotopyGroup.map (TopCat.Hom.hom f) ⋯)

Attaching (n + 1)-cells is bijective on π_k for k < n (Hatcher, Corollary 4.12). If Y is obtained from a Hausdorff space X by attaching (n + 1)-disks along f, then f induces a bijection π_k(X, x) → π_k(Y, f x), where k = Nat.card N < n.

theorem TauCeti.surjective_homotopyGroupMap_cellAttachmentIncl {X : TopCat} [T2Space ↑X] {ι : Type u} {n : ℕ} (φ : ι → (TopCat.diskBoundary (n + 1) ⟶ X)) {N : Type v} [Finite N] (hN : Nat.card N ≤ n) (x : ↑X) : Function.Surjective (HomotopyGroup.map (TopCat.Hom.hom (cellAttachmentIncl φ)) ⋯)

Attaching (n + 1)-cells to a Hausdorff space X along any family of maps Sⁿ → X induces a surjection π_k(X, x) → π_k(X ∪ eⁿ⁺¹, x) for k = Nat.card N ≤ n.

theorem TauCeti.bijective_homotopyGroupMap_cellAttachmentIncl {X : TopCat} [T2Space ↑X] {ι : Type u} {n : ℕ} (φ : ι → (TopCat.diskBoundary (n + 1) ⟶ X)) {N : Type v} [Finite N] (hN : Nat.card N < n) (x : ↑X) : Function.Bijective (HomotopyGroup.map (TopCat.Hom.hom (cellAttachmentIncl φ)) ⋯)

Attaching (n + 1)-cells to a Hausdorff space X along any family of maps Sⁿ → X induces a bijection π_k(X, x) → π_k(X ∪ eⁿ⁺¹, x) for k = Nat.card N < n.

Realizing classes by spheres

theorem TauCeti.mk_mem_range_homotopyGroupMap_of_cellAttachmentCell_comp {X Y : TopCat} {ι : Type u} {n : ℕ} {x : ↑X} {y : ↑Y} (φ : ι → (TopCat.diskBoundary (n + 1) ⟶ X)) {i : ι} (hi : φ i = TopCat.ofHom (ContinuousMap.const (ULift.{u, 0} ↑(Metric.sphere 0 1)) x)) (g : cellAttachment φ ⟶ Y) (hg : (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom (cellAttachmentIncl φ)) x) = y) (γ : ↑(GenLoop (Fin (n + 1)) (↑Y) y)) (hγ : CategoryTheory.CategoryStruct.comp (cellAttachmentCell φ i) g = GenLoop.diskMap γ) : ⟦γ⟧ ∈ Set.range (HomotopyGroup.map (TopCat.Hom.hom g) hg)

A cell attached along a constant map realizes a class (Hatcher, Proposition 4.13). If the (n + 1)-cell indexed by i is attached along the constant map at x, it closes up to a sphere at x. If a map g out of the cell attachment is a generalized loop γ on this cell, read on the disk through TauCeti.diskHomeomorphCube, then the class of γ is the image under g of the class of that sphere.

Killing πₙ

theorem TauCeti.map_cellAttachmentIncl_mk_eq_one {X : TopCat} {ι : Type u} {n : ℕ} [NeZero n] {x : ↑X} (φ : ι → (TopCat.diskBoundary (n + 1) ⟶ X)) {i : ι} {p : ↑(GenLoop (Fin n) (↑X) x)} (h : φ i = GenLoop.diskBoundaryMap p) : HomotopyGroup.map (TopCat.Hom.hom (cellAttachmentIncl φ)) ⋯ ⟦p⟧ = 1

Attaching a cell along a generalized loop kills its class. If the cell indexed by i is attached along the map GenLoop.diskBoundaryMap p of a generalized loop p, then the class of p maps to the identity of πₙ after attaching the cells.

theorem TauCeti.subsingleton_homotopyGroup_cellAttachment {X : TopCat} {ι : Type u} {n : ℕ} [NeZero n] {x : ↑X} [T2Space ↑X] (p : ι → ↑(GenLoop (Fin n) (↑X) x)) (hp : Subgroup.normalClosure (Set.range fun (i : ι) => ⟦p i⟧) = ⊤) : Subsingleton (HomotopyGroup (Fin n) (↑(cellAttachment fun (i : ι) => GenLoop.diskBoundaryMap (p i))) ((CategoryTheory.ConcreteCategory.hom (cellAttachmentIncl fun (i : ι) => GenLoop.diskBoundaryMap (p i))) x))

Attaching cells along generators kills πₙ (Hatcher, Section 4.1). If the classes of the generalized loops p i generate πₙ(X, x) as a normal subgroup, with n ≥ 1 and X Hausdorff, then attaching (n + 1)-cells along them makes πₙ trivial at the image of x. For n ≥ 2, where πₙ is abelian, this asks that the classes generate πₙ(X, x).