Stellar equivalence preserves purity

Starring a face at a fresh vertex preserves and reflects purity in every dimension. Consequently purity is invariant under stellar equivalence, including injective relabelings. This transfers purity of standard simplices and simplex boundaries to combinatorial balls and spheres.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapters 2--3.

theorem PreAbstractSimplicialComplex.insert_erase_mem_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v w : ι} (hτ : τ ∈ K) (hv : v ∉ τ) (hστ : σ ⊆ τ) (hw : w ∈ σ) : insert v (τ.erase w) ∈ K.stellarSubdivision σ v

Replacing one vertex of the starred set in a containing face τ by a vertex absent from τ gives a face of the stellar subdivision.

theorem PreAbstractSimplicialComplex.IsPure.stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} {n : ℕ} (h : K.IsPure n) (hv : {v} ∉ K) : (K.stellarSubdivision σ v).IsPure n

Starring at a fresh vertex preserves purity.

@[simp]

theorem PreAbstractSimplicialComplex.isPure_stellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} {n : ℕ} (hσ : σ ∈ K) (hv : {v} ∉ K) : (K.stellarSubdivision σ v).IsPure n ↔ K.IsPure n

Purity is also reflected by a genuine stellar subdivision: no lower-dimensional maximal face can be hidden by starring.

theorem PreAbstractSimplicialComplex.StellarEquivalent.isPure_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.StellarEquivalent L) : K.IsPure n ↔ L.IsPure n

Stellar equivalent complexes are pure in exactly the same dimensions.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.isPure_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.StellarEquivalentUpToRelabeling L) : K.IsPure n ↔ L.IsPure n

Intrinsic stellar equivalence, allowing arbitrary injective relabelings, preserves and reflects purity.