Attaching 2-cells along loops is attaching disks

TauCeti.TwoCellAttachment γ attaches a square I × I to a space X along each loop γ i at a point x: the edge {0} × I is glued to X along γ i and the other three edges are collapsed to x. The square with its boundary is homeomorphic to the disk 𝔻 2 with its boundary circle (TauCeti.diskHomeomorphCube), so this is an attachment of 2-disks in the sense of TauCeti.cellAttachment, the pushout in TopCat of the boundary inclusions of the disks.

The attaching map TauCeti.TwoCellAttachment.attachingMap γ i of the i-th disk sends a point of the boundary circle to the point of X to which the corresponding boundary point of the square is glued. The isomorphism TauCeti.TwoCellAttachment.isoCellAttachment γ from the disk attachment to TwoCellAttachment γ is the identity on X and is the characteristic map of the i-th square on the i-th disk. Its inverse comes from the universal property of TwoCellAttachment: each disk is a nullhomotopy of the image of the loop γ i.

The comparison transfers the point-set results proved for disk attachments. In particular, attaching 2-cells along loops in a Hausdorff space gives a Hausdorff space. This is what lets the presentation complex of a group presentation, built from squares, start the tower of TauCeti.killHomotopyGroups.

Read through Mathlib's categorical AttachCells (TauCeti.TwoCellAttachment.attachCells), the comparison also transfers CW structures: if X is a Hausdorff CW complex without cells of dimension at least 2, such as a wedge of circles, then TwoCellAttachment γ is a CW complex (TauCeti.TwoCellAttachment.cwComplex) whose cells are those of X and the attached squares.

Main definitions

• TauCeti.TwoCellAttachment.diskCell: the characteristic map of the i-th cell, on the disk.
• TauCeti.TwoCellAttachment.attachingMap: the attaching map of the i-th cell, on the boundary circle of the disk.
• TauCeti.TwoCellAttachment.isoCellAttachment: the isomorphism cellAttachment (attachingMap γ) ≅ TwoCellAttachment γ.
• TauCeti.TwoCellAttachment.attachCells: TwoCellAttachment γ is obtained from X by attaching 2-disks, in the sense of AttachCells.
• TauCeti.TwoCellAttachment.cwComplex: the CW structure on TwoCellAttachment γ over a CW complex of dimension at most 1, with its cells described by TauCeti.TwoCellAttachment.cwComplexCellEquiv and TauCeti.TwoCellAttachment.cwComplexCellTwoEquiv.

Main results

• TauCeti.TwoCellAttachment.incl_attachingMap_apply: the characterization of the attaching map.
• TauCeti.TwoCellAttachment.cellAttachmentIncl_isoCellAttachment_hom, TauCeti.TwoCellAttachment.cellAttachmentCell_isoCellAttachment_hom: the isomorphism is the inclusion on X and the characteristic map of the square on each disk.
• TauCeti.TwoCellAttachment.instT2Space: attaching 2-cells along loops in a Hausdorff space gives a Hausdorff space.

Implementation notes

TauCeti.cellAttachment takes a space in TopCat.{u} and cells indexed by a type in the same universe u, so the comparison is stated for loops indexed by a type in the universe of X.

References

• A. Hatcher, Algebraic Topology, Chapter 0 for attaching cells, and Section 1.2, the construction of the space X_G before Corollary 1.28.

noncomputable def TauCeti.TwoCellAttachment.diskCell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) : TopCat.disk 2 ⟶ ↧(TwoCellAttachment γ)

The characteristic map of the i-th cell, on the disk 𝔻 2: the characteristic map TauCeti.TwoCellAttachment.cell γ i of the square, through the homeomorphism TauCeti.diskHomeomorphCube of the disk with the square I^(Fin 2) = I × I.

@[simp]

theorem TauCeti.TwoCellAttachment.diskCell_apply {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) (z : ↑(TopCat.disk 2)) : (CategoryTheory.ConcreteCategory.hom (diskCell γ i)) z = (cell γ i) ((diskHomeomorphCube 2) z 0, (diskHomeomorphCube 2) z 1)

The characteristic map of the i-th cell on the disk, at a point of the disk.

noncomputable def TauCeti.TwoCellAttachment.attachingMap {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) : TopCat.diskBoundary 2 ⟶ ↧X

The attaching map of the i-th cell, on the boundary circle of the disk 𝔻 2: a point of the circle goes to the point of X to which the corresponding boundary point of the square I × I is glued, through the homeomorphism TauCeti.diskHomeomorphCube of the disk with the square. It is characterized by TauCeti.TwoCellAttachment.incl_attachingMap_apply.

theorem TauCeti.TwoCellAttachment.incl_attachingMap_apply {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) (s : ↑(TopCat.diskBoundary 2)) : (incl γ) ((CategoryTheory.ConcreteCategory.hom (attachingMap γ i)) s) = (CategoryTheory.ConcreteCategory.hom (diskCell γ i)) ((CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion 2)) s)

The attaching map of the i-th cell sends a point of the boundary circle to the point of X to which the corresponding point of the square is glued.

noncomputable def TauCeti.TwoCellAttachment.isoCellAttachment {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) : cellAttachment (attachingMap γ) ≅ ↧(TwoCellAttachment γ)

Attaching 2-cells along loops is attaching disks. The isomorphism from the space obtained by attaching a disk 𝔻 2 along each attachingMap γ i to TwoCellAttachment γ: it is the inclusion on X, and the characteristic map of the i-th square on the i-th disk, through the homeomorphism TauCeti.diskHomeomorphCube of the disk with the square.

@[simp]

theorem TauCeti.TwoCellAttachment.cellAttachmentIncl_isoCellAttachment_hom {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) : CategoryTheory.CategoryStruct.comp (cellAttachmentIncl (attachingMap γ)) (isoCellAttachment γ).hom = TopCat.ofHom (incl γ)

The isomorphism isoCellAttachment γ is the inclusion on X.

@[simp]

theorem TauCeti.TwoCellAttachment.cellAttachmentIncl_isoCellAttachment_hom_assoc {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) {Z : TopCat} (h : ↧(TwoCellAttachment γ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellAttachmentIncl (attachingMap γ)) (CategoryTheory.CategoryStruct.comp (isoCellAttachment γ).hom h) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (incl γ)) h

The isomorphism isoCellAttachment γ is the inclusion on X.

@[simp]

theorem TauCeti.TwoCellAttachment.cellAttachmentCell_isoCellAttachment_hom {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) : CategoryTheory.CategoryStruct.comp (cellAttachmentCell (attachingMap γ) i) (isoCellAttachment γ).hom = diskCell γ i

The isomorphism isoCellAttachment γ is the characteristic map of the i-th square on the i-th disk.

@[simp]

theorem TauCeti.TwoCellAttachment.cellAttachmentCell_isoCellAttachment_hom_assoc {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) {Z : TopCat} (h : ↧(TwoCellAttachment γ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellAttachmentCell (attachingMap γ) i) (CategoryTheory.CategoryStruct.comp (isoCellAttachment γ).hom h) = CategoryTheory.CategoryStruct.comp (diskCell γ i) h

The isomorphism isoCellAttachment γ is the characteristic map of the i-th square on the i-th disk.

instance TauCeti.TwoCellAttachment.instT2Space {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] : T2Space (TwoCellAttachment γ)

Attaching 2-cells along loops in a Hausdorff space gives a Hausdorff space, since it is an attachment of disks (TauCeti.instT2SpaceCellAttachment).

The CW structure

noncomputable def TauCeti.TwoCellAttachment.attachCells {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) : HomotopicalAlgebra.AttachCells (TopCat.RelativeCWComplex.basicCell 2) (TopCat.ofHom (incl γ))

TwoCellAttachment γ is obtained from X by attaching 2-disks, in the sense of Mathlib's categorical AttachCells structure, along the inclusion of X. The cells are the characteristic maps TauCeti.TwoCellAttachment.diskCell γ i (TauCeti.TwoCellAttachment.attachCells_cell), indexed by ι through TauCeti.TwoCellAttachment.attachCellsEquiv.

noncomputable def TauCeti.TwoCellAttachment.attachCellsEquiv {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) : (attachCells γ).ι ≃ ι

The cells of TauCeti.TwoCellAttachment.attachCells γ are indexed by ι.

@[simp]

theorem TauCeti.TwoCellAttachment.attachCells_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) (i : ι) : (attachCells γ).cell ((attachCellsEquiv γ).symm i) = diskCell γ i

The cells of TauCeti.TwoCellAttachment.attachCells γ are the characteristic maps of the squares, read on the disk.

@[instance_reducible]

noncomputable def TauCeti.TwoCellAttachment.cwComplex {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), 2 ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) : Topology.CWComplex Set.univ

Attaching 2-cells to a CW complex of dimension at most one gives a CW complex. If X is a Hausdorff CW complex with no cells of dimension at least 2, then TwoCellAttachment γ is a CW complex. Its cells of dimension other than 2 are the cells of X, included by incl γ (TauCeti.TwoCellAttachment.cwComplexCellEquiv), and its 2-cells are the attached squares, indexed by ι (TauCeti.TwoCellAttachment.cwComplexCellTwoEquiv).

noncomputable def TauCeti.TwoCellAttachment.cwComplexCellEquiv {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), 2 ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) {m : ℕ} (hm : m ≠ 2) : Topology.RelCWComplex.cell Set.univ m ≃ Topology.RelCWComplex.cell Set.univ m

The cells of TauCeti.TwoCellAttachment.cwComplex of dimension m ≠ 2 are the cells of X.

noncomputable def TauCeti.TwoCellAttachment.cwComplexCellTwoEquiv {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), 2 ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) : Topology.RelCWComplex.cell Set.univ 2 ≃ ι

The 2-cells of TauCeti.TwoCellAttachment.cwComplex are indexed by ι.

@[simp]

theorem TauCeti.TwoCellAttachment.coe_map_cwComplexCellEquiv_symm {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), 2 ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) {m : ℕ} (hm : m ≠ 2) (i : Topology.RelCWComplex.cell Set.univ m) : ↑(Topology.RelCWComplex.map m ((cwComplexCellEquiv γ hX hm).symm i)) = ⇑(incl γ) ∘ ↑(Topology.RelCWComplex.map m i)

The characteristic map of a cell of X of dimension m ≠ 2, as a cell of TauCeti.TwoCellAttachment.cwComplex, is its characteristic map in X followed by incl γ.

@[simp]

theorem TauCeti.TwoCellAttachment.map_cwComplexCellTwoEquiv_symm {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u} (γ : ι → Path x x) [T2Space X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), 2 ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (i : ι) (y : ↑(Metric.closedBall 0 1)) : ↑(Topology.RelCWComplex.map 2 ((cwComplexCellTwoEquiv γ hX).symm i)) ↑y = (CategoryTheory.ConcreteCategory.hom (diskCell γ i)) ((diskHomeomorphClosedBall 2).symm y)

The characteristic map of the 2-cell indexed by i is the characteristic map TauCeti.TwoCellAttachment.diskCell γ i of the i-th square, read on the closed unit ball of the sup norm through the radial homeomorphism TauCeti.diskHomeomorphClosedBall.