Documentation

TauCeti.Topology.CWComplex.Abstract.Trans

Attaching cells to a CW complex gives a CW complex #

Let c : TopCat.RelativeCWComplex f be a categorical relative CW complex, so that Y is obtained from X by attaching cells along f : X ⟶ Y, and let X carry a classical CW structure. If all the cells of X have dimension less than some N, and c attaches no cells of dimension less than N, then Y is a CW complex (TopCat.RelativeCWComplex.cwComplexTrans) when it is Hausdorff. Its m-cells are the m-cells of X, included by f, together with the cells that c attaches in dimension m (TopCat.RelativeCWComplex.cwComplexTransCellEquiv).

The structure combines the classical relative structure c.toRelCWComplex with the CW structure of X carried to the range of the closed embedding f, by composing relative CW complexes (TauCeti.relCWComplexTrans). The condition on dimensions guarantees the compatibility that composition needs: the boundary of an attached m-cell meets the range of f inside its skeleton below dimension m, which is all of it.

This is how spaces built from a CW complex by attaching cells of higher dimension, such as a presentation complex built from a wedge of circles, or the colimit of a tower of cell attachments killing homotopy groups, are read as CW complexes.

Main definitions #

Main results #

References #

source
@[instance_reducible]
noncomputable def TopCat.RelativeCWComplex.cwComplexTrans {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] [Topology.CWComplex Set.univ] {N : ℕ} (hX : ∀ (m : ℕ), N ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (hc : ∀ m < N, IsEmpty (c.attachCells m ⋯).ι) :
Topology.CWComplex Set.univ

Attaching cells to a CW complex gives a CW complex. If X is a CW complex all of whose cells have dimension less than N, and the relative CW complex c attaches no cells of dimension less than N, then the Hausdorff space Y is a CW complex. Its m-cells are the m-cells of X, included by f, together with the cells attached in dimension m (TopCat.RelativeCWComplex.cwComplexTransCellEquiv).

Instances For
    source
    noncomputable def TopCat.RelativeCWComplex.cwComplexTransCellEquiv {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] [Topology.CWComplex Set.univ] {N : ℕ} (hX : ∀ (m : ℕ), N ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (hc : ∀ m < N, IsEmpty (c.attachCells m ⋯).ι) (m : ℕ) :
    Topology.RelCWComplex.cell Set.univ m ≃ Topology.RelCWComplex.cell Set.univ m ⊕ (c.attachCells m ⋯).ι

    The m-cells of TopCat.RelativeCWComplex.cwComplexTrans are the m-cells of X together with the cells attached in dimension m.

    Instances For
      source
      @[simp]
      theorem TopCat.RelativeCWComplex.coe_map_cwComplexTransCellEquiv_symm_inl {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] [Topology.CWComplex Set.univ] {N : ℕ} (hX : ∀ (m : ℕ), N ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (hc : ∀ m < N, IsEmpty (c.attachCells m ⋯).ι) (m : ℕ) (i : Topology.RelCWComplex.cell Set.univ m) :
      ↑(Topology.RelCWComplex.map m ((c.cwComplexTransCellEquiv hX hc m).symm (Sum.inl i))) = ⇑(CategoryTheory.ConcreteCategory.hom f) ∘ ↑(Topology.RelCWComplex.map m i)

      The characteristic map of an m-cell of X, as a cell of TopCat.RelativeCWComplex.cwComplexTrans, is its characteristic map in X followed by f.

      source
      @[simp]
      theorem TopCat.RelativeCWComplex.map_cwComplexTransCellEquiv_symm_inr {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] [Topology.CWComplex Set.univ] {N : ℕ} (hX : ∀ (m : ℕ), N ≤ m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (hc : ∀ m < N, IsEmpty (c.attachCells m ⋯).ι) (m : ℕ) (i : (c.attachCells m ⋯).ι) (y : ↑(Metric.closedBall 0 1)) :
      ↑(Topology.RelCWComplex.map m ((c.cwComplexTransCellEquiv hX hc m).symm (Sum.inr i))) ↑y = (CategoryTheory.ConcreteCategory.hom { j := m, hj := ⋯, k := i }.ι) ((TauCeti.diskHomeomorphClosedBall m).symm y)

      The characteristic map of a cell attached in dimension m, as a cell of TopCat.RelativeCWComplex.cwComplexTrans, is the inclusion of the attached disk, read on the closed unit ball of the sup norm through the radial homeomorphism TauCeti.diskHomeomorphClosedBall.