Joins of abstract simplicial complexes

The join of complexes K and L has the disjoint sum of their vertex types as vertices. Its faces are the nonempty disjoint unions of a face of K and a face of L, allowing either side to be empty. This file constructs the join first for PreAbstractSimplicialComplex and then for AbstractSimplicialComplex.

Joins are standard infrastructure for the combinatorial-manifold part of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md, layer 11). In particular, combinatorial spheres are generated from the boundary of a simplex using subdivision and joins, links interact with joins, and the simplicial cylinder appearing in collapse arguments is built from closely related product constructions.

The construction follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. The use of the sum type makes the two vertex sets disjoint by construction.

Main definitions

• PreAbstractSimplicialComplex.join: the join of two precomplexes.
• AbstractSimplicialComplex.join: the join of two abstract complexes.

Main results

• mem_join_iff: membership is characterized by the two projected faces.
• disjSum_mem_join_iff: a disjoint union is a face exactly when each nonempty component is.
• join_mono: join is monotone in both arguments.

def PreAbstractSimplicialComplex.join {α : Type u_1} {β : Type u_2} (K : PreAbstractSimplicialComplex α) (L : PreAbstractSimplicialComplex β) : PreAbstractSimplicialComplex (α ⊕ β)

The join of two pre-abstract simplicial complexes, on the disjoint sum of their vertex types. A nonempty finite set is a face when each of its nonempty left and right projections is a face of the corresponding complex.

Equations

• K.join L = { faces := {σ : Finset (α ⊕ β) | σ.Nonempty ∧ (σ.toLeft = ∅ ∨ σ.toLeft ∈ K) ∧ (σ.toRight = ∅ ∨ σ.toRight ∈ L)}, isRelLowerSet_faces := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.mem_join_iff {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {σ : Finset (α ⊕ β)} : σ ∈ K.join L ↔ σ.Nonempty ∧ (σ.toLeft = ∅ ∨ σ.toLeft ∈ K) ∧ (σ.toRight = ∅ ∨ σ.toRight ∈ L)

Membership in a precomplex join is equivalent to nonemptiness together with the left and right projection face conditions.

theorem PreAbstractSimplicialComplex.disjSum_mem_join_iff {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {s : Finset α} {t : Finset β} : s.disjSum t ∈ K.join L ↔ (s.Nonempty ∨ t.Nonempty) ∧ (s = ∅ ∨ s ∈ K) ∧ (t = ∅ ∨ t ∈ L)

A disjoint union is a face of the join exactly when it is nonempty and each nonempty component is a face of its original complex.

theorem PreAbstractSimplicialComplex.map_inl_mem_join {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {s : Finset α} (hs : s ∈ K) : Finset.map Function.Embedding.inl s ∈ K.join L

A left face, tagged into the sum type, is a face of the join.

theorem PreAbstractSimplicialComplex.map_inr_mem_join {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {t : Finset β} (ht : t ∈ L) : Finset.map Function.Embedding.inr t ∈ K.join L

A right face, tagged into the sum type, is a face of the join.

theorem PreAbstractSimplicialComplex.disjSum_mem_join {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {s : Finset α} {t : Finset β} (hs : s ∈ K) (ht : t ∈ L) : s.disjSum t ∈ K.join L

The disjoint union of a left face and a right face is a face of the join.

theorem PreAbstractSimplicialComplex.join_mono {α : Type u_1} {β : Type u_2} {K K' : PreAbstractSimplicialComplex α} {L L' : PreAbstractSimplicialComplex β} (hK : K ≤ K') (hL : L ≤ L') : K.join L ≤ K'.join L'

Join is monotone in both complexes.

@[simp]

theorem PreAbstractSimplicialComplex.map_join {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} {γ : Type u_3} {δ : Type u_4} [DecidableEq γ] [DecidableEq δ] (f : α → γ) (g : β → δ) : (K.join L).map (Sum.map f g) = (K.map f).join (L.map g)

Mapping the vertex types separately commutes with the join. Injectivity is unnecessary.

@[simp]

theorem PreAbstractSimplicialComplex.map_join_swap {α : Type u_1} {β : Type u_2} {K : PreAbstractSimplicialComplex α} {L : PreAbstractSimplicialComplex β} [DecidableEq α] [DecidableEq β] : (K.join L).map Sum.swap = L.join K

Exchanging the tagged vertex sets exchanges the factors of a join.

def AbstractSimplicialComplex.join {α : Type u_1} {β : Type u_2} (K : AbstractSimplicialComplex α) (L : AbstractSimplicialComplex β) : AbstractSimplicialComplex (α ⊕ β)

The join of two abstract simplicial complexes, with vertices in the disjoint sum.

Equations

• K.join L = PreAbstractSimplicialComplex.toAbstractSimplicialComplex (α ⊕ β) (K.join L.toPreAbstractSimplicialComplex) ⋯

@[simp]

theorem AbstractSimplicialComplex.join_toPreAbstractSimplicialComplex {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} : (K.join L).toPreAbstractSimplicialComplex = K.join L.toPreAbstractSimplicialComplex

Forgetting that the join contains every singleton recovers the underlying precomplex join.

@[simp]

theorem AbstractSimplicialComplex.mem_join_iff {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {σ : Finset (α ⊕ β)} : σ ∈ K.join L ↔ σ.Nonempty ∧ (σ.toLeft = ∅ ∨ σ.toLeft ∈ K) ∧ (σ.toRight = ∅ ∨ σ.toRight ∈ L)

Membership in an abstract join is equivalent to nonemptiness together with the left and right projection face conditions.

theorem AbstractSimplicialComplex.disjSum_mem_join_iff {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {s : Finset α} {t : Finset β} : s.disjSum t ∈ K.join L ↔ (s.Nonempty ∨ t.Nonempty) ∧ (s = ∅ ∨ s ∈ K) ∧ (t = ∅ ∨ t ∈ L)

A disjoint union is a face of the abstract join exactly when it is nonempty and each nonempty component is a face of its original complex.

theorem AbstractSimplicialComplex.map_inl_mem_join {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {s : Finset α} (hs : s ∈ K) : Finset.map Function.Embedding.inl s ∈ K.join L

A left face, tagged into the sum type, is a face of the join.

theorem AbstractSimplicialComplex.map_inr_mem_join {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {t : Finset β} (ht : t ∈ L) : Finset.map Function.Embedding.inr t ∈ K.join L

A right face, tagged into the sum type, is a face of the join.

theorem AbstractSimplicialComplex.disjSum_mem_join {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {s : Finset α} {t : Finset β} (hs : s ∈ K) (ht : t ∈ L) : s.disjSum t ∈ K.join L

The disjoint union of faces is a face of the join.

theorem AbstractSimplicialComplex.join_mono {α : Type u_1} {β : Type u_2} {K K' : AbstractSimplicialComplex α} {L L' : AbstractSimplicialComplex β} (hK : K ≤ K') (hL : L ≤ L') : K.join L ≤ K'.join L'

Join is monotone in both abstract simplicial complexes.