Stellar moves in dimension zero

A stellar move on a complex of dimension at most zero replaces one singleton face by a fresh singleton face. Consequently stellar equivalence, including injective relabelings in enlarged vertex types, preserves the number of faces of such a complex. This distinguishes discrete sets of different cardinalities and supplies the base cases for combinatorial balls and spheres.

The cardinality is Set.encard, so no finiteness assumption on the complex or vertex type is needed; the void complex is included.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2 (stellar moves and combinatorial balls and spheres).

@[simp]

theorem PreAbstractSimplicialComplex.faces_stellarSubdivision_of_dimension_le_zero {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hdim : K.dimension ≤ 0) (hσ : σ ∈ K) (hv : {v} ∉ K) : (K.stellarSubdivision σ v).faces = insert {v} (K.faces \ {σ})

Starring a face of a zero-dimensional complex replaces just that face by the fresh vertex. All the faces in this formula are singletons.

theorem PreAbstractSimplicialComplex.StellarEquivalent.encard_faces_eq_of_dimension_le_zero {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) (hdim : K.dimension ≤ 0) : L.faces.encard = K.faces.encard

Stellar equivalence preserves the face cardinality in dimension at most zero.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.encard_faces_eq_of_dimension_le_zero {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) (hdim : K.dimension ≤ 0) : L.faces.encard = K.faces.encard

Intrinsic stellar equivalence preserves the face cardinality in dimension at most zero, even when its generators relabel the complexes in a larger vertex type.