Combinatorial zero-balls and zero-spheres

A combinatorial zero-ball is exactly a single vertex, and a combinatorial zero-sphere is exactly two distinct vertices, with no higher faces. These characterizations identify the base cases of the sphere-or-ball link condition without requiring callers to unpack stellar move sequences. In particular, the link of a vertex in a combinatorial one-manifold has one or two vertices, corresponding to a boundary or interior point.

The definitions use stellar equivalence rather than a literal standard model. Their necessity follows from preservation of dimension and, in dimension zero, of face cardinality under every stellar move and injective relabeling.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2 and 3 (combinatorial balls, spheres, and manifold links).

@[simp]

theorem PreAbstractSimplicialComplex.isCombinatorialBall_zero_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} : K.IsCombinatorialBall 0 ↔ ∃ (v : ι), K = simplex {v}

A combinatorial zero-ball is exactly the simplex on a single vertex.

@[simp]

theorem PreAbstractSimplicialComplex.isCombinatorialSphere_zero_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} : K.IsCombinatorialSphere 0 ↔ ∃ (v : ι) (w : ι), v ≠ w ∧ K = simplexBoundary {v, w}

A combinatorial zero-sphere is exactly the boundary of the edge on two distinct vertices.