The CW structure on a simplicial realization

The weak geometric realization of an abstract simplicial complex is a classical CW complex. Its n-cells are the nonempty faces with n + 1 vertices, and the characteristic map of a cell is the ball parametrization of its closed simplex. The boundary sphere lands in the proper subfaces, while the open ball consists of the points whose barycentric support is the whole face.

A linear order on the vertex type chooses one enumeration of each face. This avoids duplicate cells and fixes the orientations of the characteristic maps. The resulting open and closed cells themselves depend only on the underlying faces. The equivalence realizationCellEquiv identifies the cells of realizationCWComplex K with RealizationCell K, through which its open cells, closed cells, and cell frontiers are described by barycentric supports. In positive dimensions, each frontier is the union of its codimension-one closed cells. The CW filtration stage skeletonLT n consists of points with at most n nonzero barycentric coordinates. The attaching maps are injective, so this CW structure is regular.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (simplicial complexes as CW complexes).
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

noncomputable def AbstractSimplicialComplex.RealizationCell.characteristicMap {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : PartialEquiv (Fin n → ℝ) K.Realization

The characteristic map of a simplicial cell, using its increasing vertex enumeration.

theorem AbstractSimplicialComplex.RealizationCell.characteristicMap_def {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : c.characteristicMap = K.simplexCharacteristicMap c.vertexEmbedding ⋯

A cell's characteristic map uses its increasing vertex enumeration.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.characteristicMap_source {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : c.characteristicMap.source = Metric.ball 0 1

The source of a simplicial cell's characteristic map is the open unit ball.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.characteristicMap_target {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : c.characteristicMap.target = {x : K.Realization | (↑x).support = ↑↑c}

The open cell consists of the points whose barycentric support is its face.

theorem AbstractSimplicialComplex.RealizationCell.injOn_characteristicMap_closedBall {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : Set.InjOn (↑c.characteristicMap) (Metric.closedBall 0 1)

A cell's characteristic map is injective on the closed ball.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.image_characteristicMap_ball {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : ↑c.characteristicMap '' Metric.ball 0 1 = {x : K.Realization | (↑x).support = ↑↑c}

The open ball maps onto the points whose support is the cell's face.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.image_characteristicMap_closedBall {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : ↑c.characteristicMap '' Metric.closedBall 0 1 = {x : K.Realization | (↑x).support ⊆ ↑↑c}

The closed ball maps onto the closed simplex spanned by the cell's face.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.image_characteristicMap_sphere {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : ↑c.characteristicMap '' Metric.sphere 0 1 = {x : K.Realization | (↑x).support ⊂ ↑↑c}

The boundary sphere maps onto the proper subfaces of the cell's face.

@[instance_reducible]

noncomputable def AbstractSimplicialComplex.realizationCWComplex {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) : Topology.CWComplex Set.univ

The classical CW structure on a weak simplicial realization. Its n-cells are the faces with n + 1 vertices, enumerated increasingly, and its characteristic maps are the canonical closed-simplex parametrizations by sup-norm balls.

noncomputable def AbstractSimplicialComplex.realizationCellEquiv {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (n : ℕ) : Topology.RelCWComplex.cell Set.univ n ≃ K.RealizationCell n

The n-cells of realizationCWComplex K are the faces of K with n + 1 vertices.

theorem AbstractSimplicialComplex.map_realizationCellEquiv_symm {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (c : K.RealizationCell n) : Topology.RelCWComplex.map n ((K.realizationCellEquiv n).symm c) = c.characteristicMap

The characteristic maps of realizationCWComplex K are those of its simplicial cells.

@[simp]

theorem AbstractSimplicialComplex.openCell_realizationCellEquiv_symm {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (c : K.RealizationCell n) : Topology.RelCWComplex.openCell n ((K.realizationCellEquiv n).symm c) = {x : K.Realization | (↑x).support = ↑↑c}

The open cells of realizationCWComplex K are the points whose support is the cell's face.

@[simp]

theorem AbstractSimplicialComplex.closedCell_realizationCellEquiv_symm {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (c : K.RealizationCell n) : Topology.RelCWComplex.closedCell n ((K.realizationCellEquiv n).symm c) = {x : K.Realization | (↑x).support ⊆ ↑↑c}

The closed cells of realizationCWComplex K are the closed simplices of the cell's face.

@[simp]

theorem AbstractSimplicialComplex.cellFrontier_realizationCellEquiv_symm {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (c : K.RealizationCell n) : Topology.RelCWComplex.cellFrontier n ((K.realizationCellEquiv n).symm c) = {x : K.Realization | (↑x).support ⊂ ↑↑c}

The cell frontiers of realizationCWComplex K are the proper subfaces of the cell's face.

theorem AbstractSimplicialComplex.cellFrontier_realizationCellEquiv_symm_eq_iUnion_face {ι : Type u_1} [LinearOrder ι] {n : ℕ} (K : AbstractSimplicialComplex ι) (c : K.RealizationCell (n + 1)) : Topology.RelCWComplex.cellFrontier (n + 1) ((K.realizationCellEquiv (n + 1)).symm c) = ⋃ (j : Fin (n + 2)), Topology.RelCWComplex.closedCell n ((K.realizationCellEquiv n).symm (c.face j))

The frontier of a positive-dimensional realization cell is the union of the closed cells obtained by deleting one vertex.

@[simp]

theorem AbstractSimplicialComplex.skeletonLT_realizationCWComplex {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (n : ℕ∞) : ↑(Topology.RelCWComplex.skeletonLT Set.univ n) = {x : K.Realization | ↑(↑x).support.card ≤ n}

Stage n of the CW filtration consists exactly of points with at most n nonzero barycentric coordinates. Stage zero is empty and stage infinity is the whole realization.

theorem TauCeti.cellAttachingMap_realization_injective {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (cellAttachingMap ((K.realizationCellEquiv n).symm c)))

Simplicial realizations are regular CW complexes: the attaching map of every simplicial cell is injective, since its characteristic map is injective on the closed ball.