Stellar equivalence and joins

Starring a face in either factor of a join stars the corresponding face of the join. Thus joins preserve stellar equivalence, including intrinsic stellar equivalence up to relabeling. This allows the factors of a link of the form ∂σ ∗ link K σ to be replaced by standard models when checking the sphere-or-ball condition for a combinatorial manifold.

The void complex is allowed in either factor. Only the starred face must be nonempty; starring the empty set gives the void complex, whereas joining a void factor retains the other factor.

Main results

• PreAbstractSimplicialComplex.stellarSubdivision_join_inl and PreAbstractSimplicialComplex.stellarSubdivision_join_inr: starring a nonempty face commutes with joining in either factor.
• PreAbstractSimplicialComplex.IsStellarMove.join_left and PreAbstractSimplicialComplex.IsStellarMove.join_right: a stellar move in either factor induces one in the join.
• PreAbstractSimplicialComplex.StellarEquivalent.join: stellar equivalences in both factors induce an equivalence of joins.
• PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.join: the same transport for intrinsic stellar equivalence.

References

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

@[simp]

theorem PreAbstractSimplicialComplex.stellarSubdivision_join_inl {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset α} (hσ : σ.Nonempty) (v : α) : (K.join L).stellarSubdivision (Finset.map Function.Embedding.inl σ) (Sum.inl v) = (K.stellarSubdivision σ v).join L

Starring a nonempty left face commutes with joining another complex.

theorem PreAbstractSimplicialComplex.IsStellarMove.join_left {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} (h : K.IsStellarMove K') (L : PreAbstractSimplicialComplex β) : (K.join L).IsStellarMove (K'.join L)

A stellar move in the left factor induces a stellar move in the join.

theorem PreAbstractSimplicialComplex.StellarEquivalent.join_left {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} (h : K.StellarEquivalent K') (L : PreAbstractSimplicialComplex β) : (K.join L).StellarEquivalent (K'.join L)

A stellar equivalence in the left factor induces one of the joins.

@[simp]

theorem PreAbstractSimplicialComplex.stellarSubdivision_join_inr {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset β} (hσ : σ.Nonempty) (v : β) : (K.join L).stellarSubdivision (Finset.map Function.Embedding.inr σ) (Sum.inr v) = K.join (L.stellarSubdivision σ v)

Starring a nonempty right face commutes with joining another complex.

theorem PreAbstractSimplicialComplex.IsStellarMove.join_right {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {L L' : PreAbstractSimplicialComplex β} (h : L.IsStellarMove L') (K : PreAbstractSimplicialComplex α) : (K.join L).IsStellarMove (K.join L')

A stellar move in the right factor induces a stellar move in the join.

theorem PreAbstractSimplicialComplex.StellarEquivalent.join_right {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {L L' : PreAbstractSimplicialComplex β} (h : L.StellarEquivalent L') (K : PreAbstractSimplicialComplex α) : (K.join L).StellarEquivalent (K.join L')

A stellar equivalence in the right factor induces one of the joins.

theorem PreAbstractSimplicialComplex.StellarEquivalent.join {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (hK : K.StellarEquivalent K') (hL : L.StellarEquivalent L') : (K.join L).StellarEquivalent (K'.join L')

Stellar equivalences in both factors induce a stellar equivalence of joins.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.join_left {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} (h : K.StellarEquivalentUpToRelabeling K') (L : PreAbstractSimplicialComplex β) : (K.join L).StellarEquivalentUpToRelabeling (K'.join L)

An intrinsic stellar equivalence in the left factor induces one of the joins, even when the two complexes use different vertex names in their common enlarged vertex type.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.join_right {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {L L' : PreAbstractSimplicialComplex β} (h : L.StellarEquivalentUpToRelabeling L') (K : PreAbstractSimplicialComplex α) : (K.join L).StellarEquivalentUpToRelabeling (K.join L')

An intrinsic stellar equivalence in the right factor induces one of the joins.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.join {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {K K' : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (hK : K.StellarEquivalentUpToRelabeling K') (hL : L.StellarEquivalentUpToRelabeling L') : (K.join L).StellarEquivalentUpToRelabeling (K'.join L')

Intrinsic stellar equivalences in both factors induce an intrinsic stellar equivalence of their joins.