Joins of combinatorial balls and spheres

The join of two combinatorial spheres is a combinatorial sphere. Joining a combinatorial sphere with a combinatorial ball, or two combinatorial balls, gives a combinatorial ball. In each case dimensions add with an extra 1.

These results classify links expressed as a join of a simplex boundary with another link, as occurs at the new vertex of a stellar subdivision. Unlike the standard-model calculations in Simplex.Join, the factors here may themselves have undergone arbitrary stellar moves and injective relabelings. The transport uses PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.join.

References

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

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.join {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {m n : ℕ} (hK : K.IsCombinatorialSphere m) (hL : L.IsCombinatorialSphere n) : (K.join L).IsCombinatorialSphere (m + n + 1)

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

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.join_ball {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {m n : ℕ} (hK : K.IsCombinatorialSphere m) (hL : L.IsCombinatorialBall n) : (K.join L).IsCombinatorialBall (m + n + 1)

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

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.join {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {m n : ℕ} (hK : K.IsCombinatorialBall m) (hL : L.IsCombinatorialBall n) : (K.join L).IsCombinatorialBall (m + n + 1)

The join of combinatorial m- and n-balls is a combinatorial (m + n + 1)-ball.