Attaching a family of cells

For a family of maps φ i : ∂𝔻 n ⟶ X, this file constructs the space obtained by attaching one n-disk along each φ i. The construction is the pushout of the coproduct of the boundary inclusions. It comes with its inclusion of X, characteristic maps for the new cells, the pushout universal property, and an AttachCells witness.

The inclusion of the old space is a closed embedding, and the attachment is Hausdorff when the old space is. Each attaching map becomes null-homotopic after inclusion, since it extends over its characteristic disk. These facts are the point-set input for killing chosen homotopy classes by cell attachment.

Main definitions

• TauCeti.cellAttachment: the space obtained by attaching the disks.
• TauCeti.cellAttachmentIncl: the inclusion of the old space.
• TauCeti.cellAttachmentCell: the characteristic map of an attached cell.
• TauCeti.cellAttachmentAttachCells: the categorical cell-attachment witness.
• TauCeti.cellAttachmentLift: the map induced by compatible maps from the old space and disks.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and Section 4.1.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990.

@[reducible, inline]

noncomputable abbrev TauCeti.cellAttachment {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) : TopCat

The space obtained from X by attaching one n-disk along each map φ i : ∂𝔻 n ⟶ X.

@[reducible, inline]

noncomputable abbrev TauCeti.cellAttachmentIncl {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) : X ⟶ cellAttachment φ

The inclusion of the old space into a cell attachment.

noncomputable def TauCeti.cellAttachmentCell {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (i : ι) : TopCat.disk n ⟶ cellAttachment φ

The characteristic map of the cell attached along φ i.

theorem TauCeti.cellAttachment_boundary {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (i : ι) : CategoryTheory.CategoryStruct.comp (φ i) (cellAttachmentIncl φ) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (cellAttachmentCell φ i)

The characteristic map of an attached cell restricts on its boundary to the attaching map.

theorem TauCeti.cellAttachment_boundary_assoc {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (i : ι) {Z : TopCat} (h : cellAttachment φ ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (cellAttachmentIncl φ) h) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (CategoryTheory.CategoryStruct.comp (cellAttachmentCell φ i) h)

The characteristic map of an attached cell restricts on its boundary to the attaching map.

noncomputable def TauCeti.cellAttachmentAttachCells {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) : HomotopicalAlgebra.AttachCells (TopCat.RelativeCWComplex.basicCell n) (cellAttachmentIncl φ)

The inclusion into cellAttachment φ is obtained by attaching n-disks in the sense of Mathlib's categorical AttachCells structure.

@[simp]

theorem TauCeti.cellAttachmentAttachCells_cell {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (i : ι) : (cellAttachmentAttachCells φ).cell i = cellAttachmentCell φ i

The cells in cellAttachmentAttachCells have the prescribed characteristic maps.

noncomputable def TauCeti.cellAttachmentLift {X Y : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (f : X ⟶ Y) (F : ι → (TopCat.disk n ⟶ Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (φ i) f = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (F i)) : cellAttachment φ ⟶ Y

A compatible map on the old space and on every characteristic disk induces a map out of the cell attachment.

@[simp]

theorem TauCeti.cellAttachmentIncl_lift {X Y : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (f : X ⟶ Y) (F : ι → (TopCat.disk n ⟶ Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (φ i) f = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (F i)) : CategoryTheory.CategoryStruct.comp (cellAttachmentIncl φ) (cellAttachmentLift φ f F h) = f

The lift out of a cell attachment restricts to the prescribed map on the old space.

@[simp]

theorem TauCeti.cellAttachmentIncl_lift_assoc {X Y : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (f : X ⟶ Y) (F : ι → (TopCat.disk n ⟶ Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (φ i) f = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (F i)) {Z : TopCat} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellAttachmentIncl φ) (CategoryTheory.CategoryStruct.comp (cellAttachmentLift φ f F h) h✝) = CategoryTheory.CategoryStruct.comp f h✝

The lift out of a cell attachment restricts to the prescribed map on the old space.

@[simp]

theorem TauCeti.cellAttachmentCell_lift {X Y : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (f : X ⟶ Y) (F : ι → (TopCat.disk n ⟶ Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (φ i) f = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (F i)) (i : ι) : CategoryTheory.CategoryStruct.comp (cellAttachmentCell φ i) (cellAttachmentLift φ f F h) = F i

The lift out of a cell attachment restricts to the prescribed map on each disk.

@[simp]

theorem TauCeti.cellAttachmentCell_lift_assoc {X Y : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (f : X ⟶ Y) (F : ι → (TopCat.disk n ⟶ Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (φ i) f = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (F i)) (i : ι) {Z : TopCat} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellAttachmentCell φ i) (CategoryTheory.CategoryStruct.comp (cellAttachmentLift φ f F h) h✝) = CategoryTheory.CategoryStruct.comp (F i) h✝

The lift out of a cell attachment restricts to the prescribed map on each disk.

theorem TauCeti.isClosedEmbedding_cellAttachmentIncl {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (cellAttachmentIncl φ))

The inclusion of the old space into a cell attachment is a closed embedding.

instance TauCeti.instT2SpaceCellAttachment {X : TopCat} {n : ℕ} {ι : Type u} [T2Space ↑X] (φ : ι → (TopCat.diskBoundary n ⟶ X)) : T2Space ↑(cellAttachment φ)

Attaching disks to a Hausdorff space produces a Hausdorff space.

theorem TauCeti.cellAttachment_attachingMap_nullhomotopic {X : TopCat} {n : ℕ} {ι : Type u} (φ : ι → (TopCat.diskBoundary n ⟶ X)) (i : ι) : ((TopCat.Hom.hom (cellAttachmentIncl φ)).comp (TopCat.Hom.hom (φ i))).Nullhomotopic

Every prescribed attaching map becomes null-homotopic after inclusion into the cell attachment: its characteristic disk gives an extension.