Combinatorial manifolds under stellar subdivision

The link API for a stellar subdivision already transports the sphere-or-ball condition at every old vertex. This file packages that calculation into the corresponding manifold preservation step, leaving the link of the new vertex as an explicit hypothesis. The hypothesis is the exact remaining local calculation: once it is supplied, every vertex link in the subdivision has the required type.

The new-vertex link calculation is kept separate because its proof is the geometric boundary-of-a-closed-star argument.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.stellarSubdivision_zero {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hK : K.IsCombinatorialManifold 0) (hnew : (K.stellarSubdivision σ v).link {v} = ⊥) : (K.stellarSubdivision σ v).IsCombinatorialManifold 0

A stellar subdivision preserves a zero-dimensional combinatorial manifold once the new vertex has void link.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.stellarSubdivision_succ {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} {n : ℕ} (hK : K.IsCombinatorialManifold (n + 1)) (hvK : {v} ∉ K) (hnew : ((K.stellarSubdivision σ v).link {v}).IsCombinatorialSphere n ∨ ((K.stellarSubdivision σ v).link {v}).IsCombinatorialBall n) : (K.stellarSubdivision σ v).IsCombinatorialManifold (n + 1)

A positive-dimensional stellar subdivision preserves the manifold link condition provided the new vertex has a sphere-or-ball link of the complementary dimension.