Attaching 2-cells along loops

Let γ : ι → Path x x be a family of loops at a point x of a space X. The space TauCeti.TwoCellAttachment γ is obtained from X by attaching one 2-cell along each loop γ i. The 2-cell is the square I × I, attached along its boundary: the edge {0} × I is glued to X along γ i, and the other three edges are collapsed to x. A map of the square into a space Y with this boundary behaviour is exactly a homotopy, relative to the endpoints, from the image of γ i to the constant path, so the square is a 2-cell bounding the loop γ i.

This is the operation that builds the presentation complex of a group presentation from a wedge of circles, and it is how the relators of a presentation are realized topologically: the loops γ i become nullhomotopic, and a map out of X extends over the attached cells exactly when it makes every loop γ i nullhomotopic.

The space is the quotient of X ⊕ Σ _ : ι, I × I which glues the boundary of each square to X; the quotient presentation is private, and the space is used through the inclusion incl γ of X, the characteristic maps cell γ i of the cells, and the universal property lift.

Attaching 2-cells does not create new loops: the inclusion of X induces a surjection on fundamental groups. The open square of each cell is embedded as an open, simply connected subset, the open cell, and X is embedded as a closed subspace. Every loop is first pushed off the centres of the cells through the open cells (Path.exists_range_subset_homotopic), and then retracted onto X along the radial deformation of each punctured cell onto its boundary (unitInterval.radialPush).

Main definitions

• TauCeti.TwoCellAttachment γ: the space obtained from X by attaching a 2-cell along each loop γ i.
• TauCeti.TwoCellAttachment.incl: the inclusion of X.
• TauCeti.TwoCellAttachment.cell: the characteristic map of the i-th cell.
• TauCeti.TwoCellAttachment.cellHomotopy: the i-th cell, as a nullhomotopy of the image of γ i.
• TauCeti.TwoCellAttachment.lift: the universal property, which extends a map out of X together with nullhomotopies of the images of the loops.
• TauCeti.TwoCellAttachment.inclHomeomorphOfIsEmpty: with no loops, the inclusion of X is a homeomorphism.

Main results

• TauCeti.TwoCellAttachment.isQuotientMap_sumElim: the space is a quotient of X ⊕ Σ _ : ι, I × I.
• TauCeti.TwoCellAttachment.instPathConnectedSpace: the space is path connected when X is.
• TauCeti.TwoCellAttachment.hom_ext: maps out of the space are determined on X and the cells.
• TauCeti.TwoCellAttachment.exists_comp_incl_eq_iff: a map out of X extends over the attached cells exactly when it makes every loop γ i nullhomotopic.
• TauCeti.TwoCellAttachment.map_incl_fromPath: the inclusion kills the class of every loop γ i in the fundamental group.
• TauCeti.TwoCellAttachment.cell_eq_cell_iff, TauCeti.TwoCellAttachment.incl_ne_cell: a point of the open square of a cell is identified with no other point.
• TauCeti.TwoCellAttachment.isOpenEmbedding_restrict_cell, TauCeti.TwoCellAttachment.isSimplyConnected_image_cell: the open cells are open, embedded and simply connected.
• TauCeti.TwoCellAttachment.cell_eq_incl_iff: the points of a cell which are points of X.
• TauCeti.TwoCellAttachment.isClosedEmbedding_incl: X is a closed subspace.
• TauCeti.TwoCellAttachment.surjective_map_incl: the inclusion of X induces a surjection on fundamental groups.

References

• A. Hatcher, Algebraic Topology, Chapter 0 for attaching cells, and Section 1.2, Proposition 1.26 for the effect of attaching 2-cells on the fundamental group.

def TauCeti.TwoCellAttachment {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} (γ : ι → Path x x) : Type (max u v)

The space obtained from X by attaching a 2-cell along each loop γ i: the square I × I, with the edge {0} × I glued to X along γ i and the other three edges collapsed to x. It carries the quotient topology.

The presentation as a quotient is private: points come from TauCeti.TwoCellAttachment.incl and TauCeti.TwoCellAttachment.cell, maps out of the space from TauCeti.TwoCellAttachment.lift, and statements about all of its points from TauCeti.TwoCellAttachment.ind.

The topology is transported from the private quotient; the instance is @[no_expose], which is what lets its body name the private constant.

@[instance_reducible]

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

noncomputable def TauCeti.TwoCellAttachment.incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} (γ : ι → Path x x) : C(X, TwoCellAttachment γ)

The inclusion of X into the space with the 2-cells attached.

noncomputable def TauCeti.TwoCellAttachment.cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} (γ : ι → Path x x) (i : ι) : C(↑unitInterval × ↑unitInterval, TwoCellAttachment γ)

The characteristic map of the i-th attached cell, the square I × I.

@[simp]

theorem TauCeti.TwoCellAttachment.cell_apply_zero {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) (t : ↑unitInterval) : (cell γ i) (0, t) = (incl γ) ((γ i) t)

The edge {0} × I of the i-th cell is glued to X along the loop γ i.

@[simp]

theorem TauCeti.TwoCellAttachment.cell_apply_one {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) (t : ↑unitInterval) : (cell γ i) (1, t) = (incl γ) x

The edge {1} × I of the i-th cell is collapsed to the base point.

@[simp]

theorem TauCeti.TwoCellAttachment.cell_source {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) (s : ↑unitInterval) : (cell γ i) (s, 0) = (incl γ) x

The edge I × {0} of the i-th cell is collapsed to the base point.

@[simp]

theorem TauCeti.TwoCellAttachment.cell_target {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) (s : ↑unitInterval) : (cell γ i) (s, 1) = (incl γ) x

The edge I × {1} of the i-th cell is collapsed to the base point.

theorem TauCeti.TwoCellAttachment.ind {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {p : TwoCellAttachment γ → Prop} (incl : ∀ (y : X), p ((incl γ) y)) (cell : ∀ (i : ι) (q : ↑unitInterval × ↑unitInterval), p ((cell γ i) q)) (z : TwoCellAttachment γ) : p z

Every point of the space comes from X or from one of the attached cells.

theorem TauCeti.TwoCellAttachment.isQuotientMap_sumElim {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} : Topology.IsQuotientMap (Sum.elim ⇑(incl γ) fun (q : (_ : ι) × ↑unitInterval × ↑unitInterval) => (cell γ q.fst) q.snd)

The space is a quotient of X ⊕ Σ _ : ι, I × I, by the inclusion of X and the characteristic maps of the cells.

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

Attaching 2-cells to a path-connected space gives a path-connected space: every point of a cell is joined inside the cell to its edge {1} × I, which is collapsed to the base point.

noncomputable def TauCeti.TwoCellAttachment.lift {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] (f : C(X, Y)) (H : (i : ι) → ((γ i).map ⋯).Homotopy (Path.refl (f x))) : C(TwoCellAttachment γ, Y)

The universal property of attaching 2-cells. A map f out of X, together with a nullhomotopy H i of the image under f of each loop γ i, extends over the attached cells: the i-th cell is sent to Y by H i.

@[simp]

theorem TauCeti.TwoCellAttachment.lift_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] (f : C(X, Y)) (H : (i : ι) → ((γ i).map ⋯).Homotopy (Path.refl (f x))) (y : X) : (lift f H) ((incl γ) y) = f y

@[simp]

theorem TauCeti.TwoCellAttachment.lift_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] (f : C(X, Y)) (H : (i : ι) → ((γ i).map ⋯).Homotopy (Path.refl (f x))) (i : ι) (q : ↑unitInterval × ↑unitInterval) : (lift f H) ((cell γ i) q) = (H i) q

@[simp]

theorem TauCeti.TwoCellAttachment.lift_comp_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] (f : C(X, Y)) (H : (i : ι) → ((γ i).map ⋯).Homotopy (Path.refl (f x))) : (lift f H).comp (incl γ) = f

theorem TauCeti.TwoCellAttachment.hom_ext {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] {f g : C(TwoCellAttachment γ, Y)} (h : f.comp (incl γ) = g.comp (incl γ)) (hcell : ∀ (i : ι), f.comp (cell γ i) = g.comp (cell γ i)) : f = g

Extensionality for maps out of the space. Two maps which agree on X and on every attached cell are equal.

theorem TauCeti.TwoCellAttachment.hom_ext_iff {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] {f g : C(TwoCellAttachment γ, Y)} : f = g ↔ f.comp (incl γ) = g.comp (incl γ) ∧ ∀ (i : ι), f.comp (cell γ i) = g.comp (cell γ i)

The attached cells as nullhomotopies

noncomputable def TauCeti.TwoCellAttachment.cellHomotopy {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) : ((γ i).map ⋯).Homotopy (Path.refl ((incl γ) x))

The i-th attached cell is a nullhomotopy, relative to the endpoints, of the image of the loop γ i in the space.

@[simp]

theorem TauCeti.TwoCellAttachment.cellHomotopy_apply {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) (q : ↑unitInterval × ↑unitInterval) : (cellHomotopy i) q = (cell γ i) q

theorem TauCeti.TwoCellAttachment.homotopic_map_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) : ((γ i).map ⋯).Homotopic (Path.refl ((incl γ) x))

Every loop γ i becomes nullhomotopic in the space with the 2-cells attached.

@[simp]

theorem TauCeti.TwoCellAttachment.map_incl_fromPath {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} (i : ι) : (FundamentalGroup.map (incl γ) x) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk (γ i))) = 1

The attached cells kill the loops. The class of every loop γ i is sent to 1 in the fundamental group of the space with the 2-cells attached.

theorem TauCeti.TwoCellAttachment.exists_comp_incl_eq_iff {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {Y : Type w} [TopologicalSpace Y] (f : C(X, Y)) : (∃ (g : C(TwoCellAttachment γ, Y)), g.comp (incl γ) = f) ↔ ∀ (i : ι), ((γ i).map ⋯).Homotopic (Path.refl (f x))

Maps extend over the attached cells exactly when they kill the loops. A map out of X is the restriction of a map out of the space with the 2-cells attached if and only if the image of every loop γ i is nullhomotopic relative to its endpoints.

The open cells

theorem TauCeti.TwoCellAttachment.incl_ne_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} {q : ↑unitInterval × ↑unitInterval} (hq : q ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) (y : X) : (incl γ) y ≠ (cell γ i) q

A point of X is not a point of the open square of a cell.

theorem TauCeti.TwoCellAttachment.cell_eq_cell_iff {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} {q : ↑unitInterval × ↑unitInterval} (hq : q ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) {j : ι} {q' : ↑unitInterval × ↑unitInterval} : (cell γ j) q' = (cell γ i) q ↔ j = i ∧ q' = q

A point of a cell agrees with a point of the open square of a cell only when they are the same point of the same cell.

theorem TauCeti.TwoCellAttachment.isOpen_image_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} {V : Set (↑unitInterval × ↑unitInterval)} (hV : IsOpen V) (hVq : V ⊆ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : IsOpen (⇑(cell γ i) '' V)

The image of an open subset of the open square of a cell is open.

theorem TauCeti.TwoCellAttachment.isOpenEmbedding_restrict_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} : Topology.IsOpenEmbedding ((Set.Ioo 0 1 ×ˢ Set.Ioo 0 1).domRestrict ⇑(cell γ i))

The open cells. The characteristic map of a cell restricts to an open embedding of the open square.

theorem TauCeti.TwoCellAttachment.isSimplyConnected_image_cell {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} : IsSimplyConnected (⇑(cell γ i) '' Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)

The open cells are simply connected.

theorem TauCeti.TwoCellAttachment.cell_mem_range_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} {q : ↑unitInterval × ↑unitInterval} (hq : q ∉ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : (cell γ i) q ∈ Set.range ⇑(incl γ)

A point on an edge of a square is a point of X.

X is a closed subspace

theorem TauCeti.TwoCellAttachment.incl_injective {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} : Function.Injective ⇑(incl γ)

The inclusion of X is injective.

theorem TauCeti.TwoCellAttachment.cell_eq_incl_iff {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} {i : ι} {q : ↑unitInterval × ↑unitInterval} {y : X} : (cell γ i) q = (incl γ) y ↔ q.1 = 0 ∧ (γ i) q.2 = y ∨ y = x ∧ (q.1 = 1 ∨ q.2 = 0 ∨ q.2 = 1)

A point of a cell is the point y of X exactly when it lies on the edge {0} × I over γ i ⁻¹' {y}, or on one of the other three edges and y = x.

theorem TauCeti.TwoCellAttachment.isClosedEmbedding_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} : Topology.IsClosedEmbedding ⇑(incl γ)

X is a closed subspace. The inclusion of X into the space with the 2-cells attached is a closed embedding.

Attaching no cells

theorem TauCeti.TwoCellAttachment.incl_surjective {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} [IsEmpty ι] : Function.Surjective ⇑(incl γ)

With no cells attached, every point comes from X.

noncomputable def TauCeti.TwoCellAttachment.inclHomeomorphOfIsEmpty {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} (γ : ι → Path x x) [IsEmpty ι] : X ≃ₜ TwoCellAttachment γ

Attaching no 2-cells changes nothing. When the family of loops is empty, the inclusion of X is a homeomorphism onto the space with the 2-cells attached.

@[simp]

theorem TauCeti.TwoCellAttachment.inclHomeomorphOfIsEmpty_apply {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} [IsEmpty ι] (y : X) : (inclHomeomorphOfIsEmpty γ) y = (incl γ) y

Attaching 2-cells induces a surjection on fundamental groups

theorem TauCeti.TwoCellAttachment.surjective_map_incl {X : Type u} [TopologicalSpace X] {x : X} {ι : Type v} {γ : ι → Path x x} : Function.Surjective ⇑(FundamentalGroup.map (incl γ) x)

Attaching 2-cells induces a surjection on fundamental groups. Every loop in the space with the 2-cells attached is homotopic to a loop in X.