Links of old faces after stellar subdivision

Starring σ at v changes the link of a face τ avoiding v by starring its old link at σ \ τ. This includes faces meeting σ: their links are starred at the complementary part of σ, rather than at σ itself. If τ contains σ, it is removed and both sides of the formula are void, since starring the empty set gives the void complex.

These link identities transfer sphere-or-ball link conditions at surviving old vertices when the starring vertex is unused in their old links, and preserve void links in dimension zero. The complementary new-vertex link is the boundary of the closed star, computed in Subdivision.Stellar.Basic.

References

• G. Cunningham, D. Zach, S. Friedl, Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean (2026), Theorem 3.9 in the preprint (Theorem 19 in the published version), and the associated not-gary/pachner formalization, stellarSubdivision_anticomm_link in Pachner/Results/StellarSubdivAnticommLink.lean. link_stellarSubdivision_of_notMem extends their link–stellar-subdivision identity to arbitrary precomplexes and sets avoiding the starring vertex.
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2 and 3 (stellar subdivision and links).
• W. B. R. Lickorish, Simplicial moves on complexes and manifolds, Geom. Topol. Monogr. 2 (1999), 299–320.

@[simp]

theorem PreAbstractSimplicialComplex.link_stellarSubdivision_of_notMem {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} (hvτ : v ∉ τ) : (K.stellarSubdivision σ v).link τ = (K.link τ).stellarSubdivision (σ \ τ) v

The link of a face avoiding the starring vertex is the stellar subdivision of its old link at the part of the starred set outside that face. No face or freshness hypotheses are required; in particular, a removed face has void link on both sides.

theorem PreAbstractSimplicialComplex.stellarEquivalent_link_stellarSubdivision_of_notMem {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} (hv : {v} ∉ K.link τ) (hvτ : v ∉ τ) (hne : (σ \ τ).Nonempty) : (K.link τ).StellarEquivalent ((K.stellarSubdivision σ v).link τ)

If the starring vertex is unused in the old link and the starred set has a vertex outside τ, its links before and after starring are stellar equivalent. This applies to every set avoiding the starring vertex, not only to surviving faces.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.link_stellarSubdivision_eq_bot {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v w : ι} (hK : K.IsCombinatorialManifold 0) (hwv : w ≠ v) (hw : {w} ∈ K.stellarSubdivision σ v) : (K.stellarSubdivision σ v).link {w} = ⊥

A surviving old vertex of a zero-dimensional combinatorial manifold still has void link after stellar subdivision.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.isCombinatorialSphere_or_isCombinatorialBall_link_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v w : ι} {n : ℕ} (hK : K.IsCombinatorialManifold (n + 1)) (hvlink : {v} ∉ K.link {w}) (hwv : w ≠ v) (hw : {w} ∈ K.stellarSubdivision σ v) : ((K.stellarSubdivision σ v).link {w}).IsCombinatorialSphere n ∨ ((K.stellarSubdivision σ v).link {w}).IsCombinatorialBall n

Every surviving old vertex of a positive-dimensional combinatorial manifold retains its sphere-or-ball link condition under stellar subdivision when the starring vertex is unused in its old link. The condition at the new vertex is separate: its link is the boundary of the starred closed star.