Closed stars as joins

The closed star of a face σ is the join of the simplex on σ with its link. The part of that closed star which does not contain σ is the join of the boundary of σ with its link. In particular, this describes the link of the new vertex of a stellar subdivision.

The join uses disjoint tagged vertex types. The identifications below tag a vertex on the left when it belongs to σ, and on the right otherwise. This vertex map is injective: untagging is a left inverse. Thus the equalities are actual relabelings, without identifying distinct used vertices. No nonvoidness assumption is imposed on the link; the formulas include maximal faces and singleton faces, whose links or simplex boundaries may be void.

The combinatorial description follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapters 2--3, and Lickorish, Simplicial moves on complexes and manifolds, Geom. Topol. Monogr. 2 (1999), 299--320.

@[simp]

theorem PreAbstractSimplicialComplex.map_closedStar_eq_join {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ ∈ K) : (K.closedStar σ).map ⇑(TauCeti.partitionEmbedding fun (x : ι) => x ∈ σ) = (simplex σ).join (K.link σ)

Tagging the vertices of a closed star according to membership in σ identifies it with the join of the simplex on σ and the link of σ.

@[simp]

theorem PreAbstractSimplicialComplex.map_closedStar_inf_deletion_eq_join {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ ∈ K) : (K.closedStar σ ⊓ K.deletion σ).map ⇑(TauCeti.partitionEmbedding fun (x : ι) => x ∈ σ) = (simplexBoundary σ).join (K.link σ)

The part of a closed star avoiding the whole starred face is the join of the simplex boundary with the link, after tagging vertices according to membership in that face.