Simplicial realizations are cellular

The CW filtration of a weak simplicial realization agrees with its simplicial filtration: skeletonLT n consists of points with at most n nonzero barycentric coordinates, and the ordinary n-skeleton is the image of the realization of the simplicial n-skeleton. Consequently every simplicial map induces a cellular map, including maps that identify vertices and collapse dimensions. This supplies the cellularity hypothesis needed to apply cellular chains to simplicial realizations.

The CW structures are the existing AbstractSimplicialComplex.realizationCWComplex structures. The induced map is the existing SimplicialMap.realizationMap, restricted to the universal subsets as required by TauCeti.IsCellular; no second realization map is introduced.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and Section 2.2 (simplicial CW structures and cellular maps).

theorem AbstractSimplicialComplex.skeleton_realizationCWComplex {ι : Type u_1} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (n : ℕ) : ↑(Topology.RelCWComplex.skeleton Set.univ ↑n) = Set.range (realizationMap ⋯)

The ordinary CW n-skeleton is the realized simplicial n-skeleton, with its existing subspace inclusion into the weak realization.

theorem PreAbstractSimplicialComplex.SimplicialMap.mapsTo_realizationMap_skeletonLT {ι : Type u_1} {κ : Type u_2} [LinearOrder ι] [LinearOrder κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (n : ℕ∞) : Set.MapsTo ⇑f.realizationMap ↑(Topology.RelCWComplex.skeletonLT Set.univ n) ↑(Topology.RelCWComplex.skeletonLT Set.univ n)

A simplicial realization preserves every stage of the classical CW filtration. No injectivity assumption on the vertex map is needed.

theorem PreAbstractSimplicialComplex.SimplicialMap.isCellular_realizationMap {ι κ : Type u} [LinearOrder ι] [LinearOrder κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) : TauCeti.IsCellular Set.univ Set.univ (TopCat.ofHom (f.realizationMap.restrictPreimage Set.univ))

Every simplicial map induces a cellular map for the canonical simplicial CW structures. The universal-subset restriction is the map used by the cellular-chain functor. The common universe is required by the existing TauCeti.IsCellular interface.