Joins of standard combinatorial balls and spheres

The join of two simplices is a simplex. The join of a simplex boundary with a simplex or another simplex boundary is obtained by one stellar subdivision of a simplex or its boundary, respectively. These identities classify the joins of the standard ball and sphere models and supply the standard-model calculation for links of new vertices in stellar subdivisions.

The dimensions add with an extra 1: the join of an m-sphere and an n-sphere is an (m + n + 1)-sphere, and the join of an m-sphere and an n-ball is an (m + n + 1)-ball. The assertions here concern standard models; transport to arbitrary combinatorial balls and spheres requires preservation of stellar equivalence under joins.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2 and 3.
• W. B. R. Lickorish, Simplicial moves on complexes and manifolds, Geom. Topol. Monogr. 2 (1999), 299-320.

@[simp]

theorem PreAbstractSimplicialComplex.join_simplex_simplex {α : Type u_1} {β : Type u_2} (V : Finset α) (W : Finset β) : (simplex V).join (simplex W) = simplex (V.disjSum W)

The join of two simplices is the simplex on the disjoint union of their vertices.

@[simp]

theorem PreAbstractSimplicialComplex.stellarSubdivision_simplex_disjSum {α : Type u_1} {β : Type u_2} {V : Finset α} {W : Finset β} {w : β} [DecidableEq α] [DecidableEq β] (hV : V.Nonempty) : (simplex (V.disjSum W)).stellarSubdivision (Finset.map Function.Embedding.inl V) (Sum.inr w) = (simplexBoundary V).join (simplex (insert w W))

Starring the left face of a simplex produces the join of its boundary with the simplex on the right vertices together with the chosen vertex w. The formula also allows w ∈ W.

@[simp]

theorem PreAbstractSimplicialComplex.stellarSubdivision_simplexBoundary_disjSum {α : Type u_1} {β : Type u_2} {V : Finset α} {W : Finset β} {w : β} [DecidableEq α] [DecidableEq β] (hV : V.Nonempty) (hw : w ∉ W) : (simplexBoundary (V.disjSum W)).stellarSubdivision (Finset.map Function.Embedding.inl V) (Sum.inr w) = (simplexBoundary V).join (simplexBoundary (insert w W))

The stellar subdivision of a simplex boundary along its left vertex set is the join of that set's boundary with the boundary on the right vertices and the fresh vertex w.

theorem PreAbstractSimplicialComplex.isCombinatorialBall_join_simplexBoundary_simplex {α : Type u_1} {β : Type u_2} {V : Finset α} {W : Finset β} {m n : ℕ} [DecidableEq α] [DecidableEq β] (hV : V.card = m + 2) (hW : W.card = n + 1) : ((simplexBoundary V).join (simplex W)).IsCombinatorialBall (m + n + 1)

The join of a standard m-sphere with a standard n-ball is a combinatorial (m + n + 1)-ball.

theorem PreAbstractSimplicialComplex.isCombinatorialSphere_join_simplexBoundary_simplexBoundary {α : Type u_1} {β : Type u_2} {V : Finset α} {W : Finset β} {m n : ℕ} [DecidableEq α] [DecidableEq β] (hV : V.card = m + 2) (hW : W.card = n + 2) : ((simplexBoundary V).join (simplexBoundary W)).IsCombinatorialSphere (m + n + 1)

The join of standard m- and n-spheres is a combinatorial (m + n + 1)-sphere.