Attaching cells of a single dimension is a relative CW complex

Let c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f express that Y is obtained from X by attaching n-disks along their boundary spheres, f : X ⟶ Y being the inclusion. Then f is a categorical relative CW complex (HomotopicalAlgebra.AttachCells.toRelativeCWComplex): its sequence of stages is constantly X up to stage n and constantly Y from stage n + 1 on (TauCeti.attachStageFunctor), the cells attached at stage n are those of c, and no cells are attached at the other stages (HomotopicalAlgebra.AttachCells.ofIsIso).

Through the comparison TopCat.RelativeCWComplex.toRelCWComplex, Y is therefore a classical relative CW complex relative to the range of f, whose cells all have dimension n (HomotopicalAlgebra.AttachCells.isEmpty_cell_toRelCWComplex, HomotopicalAlgebra.AttachCells.cellToRelCWComplexEquiv), with the characteristic maps of c (HomotopicalAlgebra.AttachCells.map_cellToRelCWComplexEquiv_symm). In particular its skeleta up to dimension n are the range of f (HomotopicalAlgebra.AttachCells.skeletonLT_toRelCWComplex), so the cellular theory of classical relative CW complexes, such as Hatcher's Corollary 4.12, applies to a single attachment of cells. This is how cells are attached to kill homotopy groups.

Main definitions

• TauCeti.attachStageFunctor f n: the sequence X = ⋯ = X → Y = Y = ⋯, with f from stage n to stage n + 1.
• HomotopicalAlgebra.AttachCells.toRelativeCWComplex: the relative CW complex of a single attachment of n-cells.
• HomotopicalAlgebra.AttachCells.cellToRelCWComplexEquiv: its classical n-cells are the cells of c.

Main results

• HomotopicalAlgebra.AttachCells.toRelativeCWComplex_cells_ι: its cells are included as in c.
• HomotopicalAlgebra.AttachCells.isEmpty_cell_toRelCWComplex: it has no classical cells outside dimension n.
• HomotopicalAlgebra.AttachCells.skeletonLT_toRelCWComplex: its skeleta up to dimension n are the range of f.
• HomotopicalAlgebra.AttachCells.skeletonLT_toRelCWComplex_eq_univ: its skeleta above dimension n are all of Y.
• HomotopicalAlgebra.AttachCells.coe_cellAttachingMap_toRelCWComplex_apply: the attaching maps of its classical cells are those of c.

References

• A. Hatcher, Algebraic Topology, Chapter 0 for attaching cells, and Section 4.1 for attaching cells to kill homotopy groups.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical definition of relative CW complexes.

Implementation notes

The stages and their colimit follow the pattern of Mathlib's CategoryTheory.TransfiniteCompositionOfShape.iic, which restricts a transfinite composition along a monotone reindexing: here the fixed diagram ComposableArrows.mk₁ f over Fin 2 is reindexed along the monotone step function TauCeti.attachStageIndex n, its colimit cocone comes from the terminal object Fin.last 1 (CategoryTheory.Limits.colimitOfDiagramTerminal), and it is transported along the final reindexing by CategoryTheory.Functor.Final.isColimitWhiskerEquiv.

def TauCeti.attachStageIndex (n k : ℕ) : Fin 2

The step function ℕ → Fin 2 which is 0 up to n and 1 afterwards: stage k of the relative CW complex attaching n-cells is the source of the attachment for k ≤ n and its target for n < k.

@[simp]

theorem TauCeti.attachStageIndex_of_le {n k : ℕ} (h : k ≤ n) : attachStageIndex n k = 0

Up to stage n, the index is 0.

@[simp]

theorem TauCeti.attachStageIndex_of_lt {n k : ℕ} (h : n < k) : attachStageIndex n k = 1

After stage n, the index is 1.

theorem TauCeti.monotone_attachStageIndex (n : ℕ) : Monotone (attachStageIndex n)

The index is monotone in the stage.

theorem TauCeti.attachStageIndex_succ_of_ne {n k : ℕ} (h : k ≠ n) : attachStageIndex n (k + 1) = attachStageIndex n k

The index changes only from stage n to stage n + 1.

instance TauCeti.final_monotone_attachStageIndex_functor (n : ℕ) : ⋯.functor.Final

The reindexing ℕ ⥤ Fin 2 along attachStageIndex n is final: its value 1 is reached.

@[reducible, inline]

abbrev TauCeti.attachStageFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.Functor ℕ C

The sequence X = ⋯ = X → Y = Y = ⋯ which is constantly X up to stage n, constantly Y from stage n + 1 on, and f from stage n to stage n + 1.

theorem TauCeti.isIso_attachStageFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (n : ℕ) {k : ℕ} (hk : k ≠ n) : CategoryTheory.IsIso ((attachStageFunctor f n).map (CategoryTheory.homOfLE ⋯))

Away from stage n, the steps of attachStageFunctor f n are isomorphisms.

def TauCeti.attachStageArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk ((attachStageFunctor f n).map (CategoryTheory.homOfLE ⋯))

The step of attachStageFunctor f n from stage n to stage n + 1 is f.

noncomputable def HomotopicalAlgebra.AttachCells.toRelativeCWComplex {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) : TopCat.RelativeCWComplex f

Attaching cells of a single dimension is a relative CW complex. If Y is obtained from X by attaching n-disks along f, then f is a relative CW complex whose stages are X up to stage n and Y afterwards; the cells attached at stage n are those of c, and no cells are attached at the other stages. The body is exposed so that the stages are those of TauCeti.attachStageFunctor f n by definition, which the statements about its attached cells need in order to typecheck; the stages and their inclusions into Y are characterised by toRelativeCWComplex_F and toRelativeCWComplex_incl_app.

theorem HomotopicalAlgebra.AttachCells.toRelativeCWComplex_F {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) : c.toRelativeCWComplex.F = TauCeti.attachStageFunctor f n

The stages of c.toRelativeCWComplex are those of TauCeti.attachStageFunctor f n.

theorem HomotopicalAlgebra.AttachCells.toRelativeCWComplex_incl_app {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) (k : ℕ) : c.toRelativeCWComplex.incl.app k = (CategoryTheory.ComposableArrows.mk₁ f).map ((Fin.isTerminalLast 1).from (TauCeti.attachStageIndex n k))

The inclusion of stage k of c.toRelativeCWComplex into Y is the image under ComposableArrows.mk₁ f of the morphism to the last object of Fin 2.

theorem HomotopicalAlgebra.AttachCells.toRelativeCWComplex_attachCells_self {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) : c.toRelativeCWComplex.attachCells n ⋯ = c.ofArrowIso (TauCeti.attachStageArrowIso f n)

At stage n, the cells of c.toRelativeCWComplex are attached as in c.

theorem HomotopicalAlgebra.AttachCells.isEmpty_toRelativeCWComplex_attachCells_ι {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) {k : ℕ} (hk : k ≠ n) (h : ¬IsMax k) : IsEmpty (c.toRelativeCWComplex.attachCells k h).ι

No cells of c.toRelativeCWComplex are attached at the stages other than n.

def HomotopicalAlgebra.AttachCells.toRelativeCWComplexAttachCellsEquiv {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) : (c.toRelativeCWComplex.attachCells n ⋯).ι ≃ c.ι

The cells of c.toRelativeCWComplex attached at stage n are the cells of c.

theorem HomotopicalAlgebra.AttachCells.toRelativeCWComplex_cells_ι {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) (k : (c.toRelativeCWComplex.attachCells n ⋯).ι) : { j := n, hj := ⋯, k := k }.ι = c.cell (c.toRelativeCWComplexAttachCellsEquiv k)

The inclusion of a cell attached at stage n of c.toRelativeCWComplex is the inclusion of the corresponding cell of c.

theorem HomotopicalAlgebra.AttachCells.isEmpty_cell_toRelCWComplex {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) {m : ℕ} (hm : m ≠ n) : IsEmpty (Topology.RelCWComplex.cell Set.univ m)

The classical relative CW structure on Y, relative to the range of f, read off c.toRelativeCWComplex, has no cells outside dimension n.

noncomputable def HomotopicalAlgebra.AttachCells.cellToRelCWComplexEquiv {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) : Topology.RelCWComplex.cell Set.univ n ≃ c.ι

The n-cells of the classical relative CW structure read off c.toRelativeCWComplex are the cells of c.

theorem HomotopicalAlgebra.AttachCells.map_cellToRelCWComplexEquiv_symm {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) (i : c.ι) (x : ↑(Metric.closedBall 0 1)) : ↑(Topology.RelCWComplex.map n (c.cellToRelCWComplexEquiv.symm i)) ↑x = (CategoryTheory.ConcreteCategory.hom (c.cell i)) ((TauCeti.diskHomeomorphClosedBall n).symm x)

The characteristic map of an n-cell of the classical relative CW structure read off c.toRelativeCWComplex is the inclusion of the corresponding cell of c, read on the closed ball through the radial homeomorphism TauCeti.diskHomeomorphClosedBall.

theorem HomotopicalAlgebra.AttachCells.skeletonLT_toRelCWComplex {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) [T2Space ↑Y] {m : ℕ} (hm : m ≤ n) : ↑(Topology.RelCWComplex.skeletonLT Set.univ ↑m) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)

Up to dimension n, the skeleta of the classical relative CW structure read off c.toRelativeCWComplex are the range of f: there are no cells of dimension less than n.

theorem HomotopicalAlgebra.AttachCells.skeletonLT_toRelCWComplex_eq_univ {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) [T2Space ↑Y] {m : ℕ} (hm : n < m) : ↑(Topology.RelCWComplex.skeletonLT Set.univ ↑m) = Set.univ

From dimension n + 1 on, the skeleta of the classical relative CW structure read off c.toRelativeCWComplex are all of Y: there are no cells of dimension greater than n.

theorem HomotopicalAlgebra.AttachCells.coe_cellAttachingMap_toRelCWComplex_apply {X Y : TopCat} {f : X ⟶ Y} {n : ℕ} (c : AttachCells (TopCat.RelativeCWComplex.basicCell n) f) [T2Space ↑Y] (j : Topology.RelCWComplex.cell Set.univ n) (z : ↑(TopCat.diskBoundary n)) : ↑((CategoryTheory.ConcreteCategory.hom (TauCeti.cellAttachingMap j)) z) = (CategoryTheory.ConcreteCategory.hom (c.cell (c.cellToRelCWComplexEquiv j))) ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion n)) z)

The attaching map of an n-cell of the classical relative CW structure read off c.toRelativeCWComplex is the inclusion of the corresponding cell of c, restricted to the boundary sphere.