The join of simplicial sets

The join K ⋆ L of simplicial sets K and L is the simplicial set whose n-simplices are the decompositions of the vertices {0, …, n} into an initial segment I and a final segment J, together with a simplex of K with vertices I and a simplex of L with vertices J, where a simplex on the empty set of vertices is a single point. Thus K and L are the parts of K ⋆ L over the two vertices of Δ[1], and every simplex of K is joined to every simplex of L. The join is the operation through which cone and slice quasicategories, and hence limits and colimits in quasicategories, are defined: a cocone on a diagram Y ⟶ C is a map Y ⋆ Δ[0] ⟶ C extending it.

The decomposition of the vertices of a simplex is a map to Δ[1], and the simplices of K and L are maps from the parts over the vertices 0 and 1 of Δ[1]. Accordingly, a map from any simplicial set X to the join is described by join data (SSet.JoinData X K L): a map p : X ⟶ Δ[1] together with maps to K and L from the subcomplexes SSet.joinFiber p 0 and SSet.joinFiber p 1 of X lying over the two vertices. The join is the simplicial set of join data on standard simplices, and SSet.join.homEquiv identifies its maps from X with the join data on X.

Main definitions

• SSet.joinFiber p e: the part of X over the vertex e of Δ[1] along p : X ⟶ Δ[1].
• SSet.JoinData X K L: the data of a map X ⟶ K ⋆ L, with its restriction SSet.JoinData.precomp along maps Y ⟶ X.
• SSet.join K L: the join K ⋆ L, whose simplices are the join data on standard simplices (SSet.join.objEquiv).
• SSet.join.π: the projection K ⋆ L ⟶ Δ[1].
• SSet.join.inl, SSet.join.inr: the inclusions of K and L as the parts over 0 and 1.
• SSet.join.joinFiberZeroIso, SSet.join.joinFiberOneIso: the parts of K ⋆ L over the vertices 0 and 1 are K and L, through the inverses of the inclusions.
• SSet.join.map: the functoriality of the join in both variables.
• SSet.join.edgeMk: the edge of K ⋆ L from a vertex of K to a vertex of L.
• SSet.joinFiberZeroRetraction: the retraction of Δ[m] onto its part over the vertex 0 of Δ[1], when that part contains the vertex 0.
• SSet.Subcomplex.unionJoin A B: for subcomplexes A of K and B of L, the subcomplex (A ⋆ L) ∪ (K ⋆ B) of K ⋆ L, the domain of the pushout-join of their inclusions.

Main results

• SSet.join.homEquiv: maps X ⟶ K ⋆ L correspond to join data on X, naturally in X (SSet.join.homEquiv_comp); this is the representability SSet.join.representableBy.
• SSet.join.edge_mem_joinFiber_zero: an edge of K ⋆ L ending over the vertex 0 lies over 0.
• SSet.join.exists_eq_comp_inr_or_exists_eq_comp_map: every simplex of K ⋆ L comes from L or is the image of a simplex of Δ[m] ⋆ L under g ⋆ L for a simplex g : Δ[m] ⟶ K.
• SSet.Subcomplex.mem_unionJoin_iff: a simplex of K ⋆ L lies in (A ⋆ L) ∪ (K ⋆ B) exactly when its part in K lies in A or its part in L lies in B.
• SSet.Subcomplex.unionJoin_le_iff: (A ⋆ L) ∪ (K ⋆ B) lies in a subcomplex exactly when the images of A ⋆ L and K ⋆ B do.
• SSet.Subcomplex.unionJoin.isPushout: (A ⋆ L) ∪ (K ⋆ B) is the pushout of A ⋆ L and K ⋆ B along A ⋆ B.
• SSet.join.isoOfIsTerminal: the join of two terminal simplicial sets, such as Δ[0] ⋆ Δ[0], is Δ[1].
• SSet.join.isIso_inl, SSet.join.isIso_inr: the join with an empty simplicial set is the other factor.
• SSet.join.quasicategory: the join of two quasicategories is a quasicategory (Joyal).

Implementation notes

The universal property reduces Joyal's theorem to horn filling in K, L and Δ[1] (SSet.JoinData.exists_precomp_horn_ι_eq): over Δ[1], an inner horn lies either entirely over one vertex, or so that its parts over both vertices are faces contained in the horn.

The pushout square SSet.Subcomplex.unionJoin.isPushout is obtained, as Mathlib's SSet.Subcomplex.unionProd.isPushout (Joël Riou and Jack McKoen) is for products, from the bicartesian square of subcomplexes formed by A ⋆ B, A ⋆ L, K ⋆ B and their union.

References

• J. Lurie, Higher Topos Theory, Definition 1.2.8.1 and Proposition 1.2.8.3.
• A. Joyal, Quasi-categories and Kan complexes, J. Pure Appl. Algebra 175 (2002).

def SSet.joinFiber {X : SSet} (p : X ⟶ stdSimplex.obj { len := 1 }) (e : Fin 2) : X.Subcomplex

The part of a simplicial set X lying over the vertex e of Δ[1] along p : X ⟶ Δ[1]: the subcomplex of the simplices all of whose vertices are sent to e.

@[simp]

theorem SSet.mem_joinFiber_iff {X : SSet} (p : X ⟶ stdSimplex.obj { len := 1 }) (e : Fin 2) {d : ℕ} (x : X.obj (Opposite.op { len := d })) : x ∈ (joinFiber p e).obj (Opposite.op { len := d }) ↔ ∀ (j : Fin (d + 1)), ((CategoryTheory.ConcreteCategory.hom (p.app (Opposite.op { len := d }))) x) j = e

@[simp]

theorem SSet.joinFiber_const_self {X : SSet} (e : Fin 2) : joinFiber (const (stdSimplex.const 1 e (Opposite.op { len := 0 }))) e = ⊤

The whole of X lies over the vertex e along the constant map at e.

@[simp]

theorem SSet.joinFiber_const_of_ne {X : SSet} {e e' : Fin 2} (h : e ≠ e') : joinFiber (const (stdSimplex.const 1 e (Opposite.op { len := 0 }))) e' = ⊥

Nothing lies over the vertex e' along the constant map at a different vertex e.

@[simp]

theorem SSet.joinFiber_ι_comp {X : SSet} (p : X ⟶ stdSimplex.obj { len := 1 }) (e : Fin 2) : CategoryTheory.CategoryStruct.comp (joinFiber p e).ι p = const (stdSimplex.const 1 e (Opposite.op { len := 0 }))

The part of X over the vertex e lies over e.

@[simp]

theorem SSet.joinFiber_ι_comp_assoc {X : SSet} (p : X ⟶ stdSimplex.obj { len := 1 }) (e : Fin 2) {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (joinFiber p e).ι (CategoryTheory.CategoryStruct.comp p h) = CategoryTheory.CategoryStruct.comp (const (stdSimplex.const 1 e (Opposite.op { len := 0 }))) h

The part of X over the vertex e lies over e.

theorem SSet.obj₀Equiv_symm_mem_joinFiber_iff {m : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }) (e : Fin 2) (j : Fin (m + 1)) : stdSimplex.obj₀Equiv.symm j ∈ (joinFiber q e).obj (Opposite.op { len := 0 }) ↔ (yonedaEquiv q) j = e

The vertex j of Δ[m] lies over the vertex e of Δ[1] along q exactly when q sends j to e.

theorem SSet.yonedaEquiv_apply_of_mem_joinFiber {d : ℕ} {q : stdSimplex.obj { len := d } ⟶ stdSimplex.obj { len := 1 }} {c : Fin 2} {a : ℕ} {y : (stdSimplex.obj { len := d }).obj (Opposite.op { len := a })} (hy : y ∈ (joinFiber q c).obj (Opposite.op { len := a })) (t : Fin (a + 1)) : (yonedaEquiv q) (y t) = c

Every vertex of a simplex of Δ[d] over the vertex c of Δ[1] along q is sent to c by q.

theorem SSet.joinFiber_hom_vertex_le {d k : ℕ} {q : stdSimplex.obj { len := d } ⟶ stdSimplex.obj { len := 1 }} {c : Fin 2} (g : (joinFiber q c).toSSet ⟶ stdSimplex.obj { len := k }) {j l : Fin (d + 1)} (hjl : j ≤ l) (hj : (yonedaEquiv q) j = c) (hl : (yonedaEquiv q) l = c) : ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) ⟨stdSimplex.obj₀Equiv.symm j, ⋯⟩) 0 ≤ ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) ⟨stdSimplex.obj₀Equiv.symm l, ⋯⟩) 0

A map to Δ[k] from the part of Δ[d] over a vertex c of Δ[1] is monotone on the vertices over c.

noncomputable def SSet.joinFiberZeroRetraction {m : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }) (h : (yonedaEquiv q) 0 = 0) : stdSimplex.obj { len := m } ⟶ (joinFiber q 0).toSSet

When the vertex 0 of Δ[m] lies over the vertex 0 of Δ[1] along q, the retraction of Δ[m] onto its part over 0, which collapses the vertices over 1 onto the last vertex over 0.

theorem SSet.joinFiberZeroRetraction_app_of_mem {m : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }) (h : (yonedaEquiv q) 0 = 0) {k : ℕ} (y : (stdSimplex.obj { len := m }).obj (Opposite.op { len := k })) (hy : y ∈ (joinFiber q 0).obj (Opposite.op { len := k })) : (CategoryTheory.ConcreteCategory.hom ((joinFiberZeroRetraction q h).app (Opposite.op { len := k }))) y = ⟨y, hy⟩

The retraction joinFiberZeroRetraction fixes the part of Δ[m] over 0.

@[simp]

theorem SSet.ι_joinFiberZeroRetraction {m : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }) (h : (yonedaEquiv q) 0 = 0) : CategoryTheory.CategoryStruct.comp (joinFiber q 0).ι (joinFiberZeroRetraction q h) = CategoryTheory.CategoryStruct.id (joinFiber q 0).toSSet

The retraction joinFiberZeroRetraction is a retraction of the inclusion of the part of Δ[m] over 0.

@[simp]

theorem SSet.ι_joinFiberZeroRetraction_assoc {m : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }) (h : (yonedaEquiv q) 0 = 0) {Z : SSet} (h✝ : (joinFiber q 0).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (joinFiber q 0).ι (CategoryTheory.CategoryStruct.comp (joinFiberZeroRetraction q h) h✝) = h✝

The retraction joinFiberZeroRetraction is a retraction of the inclusion of the part of Δ[m] over 0.

theorem SSet.joinFiber_one_eq_top {m : ℕ} {q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := 1 }} (h : (yonedaEquiv q) 0 ≠ 0) : joinFiber q 1 = ⊤

If the vertex 0 of Δ[m] does not lie over 0 along q, the whole of Δ[m] lies over 1.

structure SSet.JoinData (X K L : SSet) : Type u

The data of a map from X to the join of K and L: a map p : X ⟶ Δ[1], a map to K from the part of X over the vertex 0, and a map to L from the part of X over the vertex 1.

• p : X ⟶ stdSimplex.obj { len := 1 }

  The map to Δ[1].

• left : (joinFiber self.p 0).toSSet ⟶ K

  The map to K from the part over the vertex 0.

• right : (joinFiber self.p 1).toSSet ⟶ L

  The map to L from the part over the vertex 1.

theorem SSet.JoinData.ext {X K L : SSet} {d d' : X.JoinData K L} (hp : d.p = d'.p) (hl : ∀ (n : SimplexCategoryᵒᵖ) (x : X.obj n) (hx : x ∈ (joinFiber d.p 0).obj n) (hx' : x ∈ (joinFiber d'.p 0).obj n), (CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.left.app n)) ⟨x, hx'⟩) (hr : ∀ (n : SimplexCategoryᵒᵖ) (x : X.obj n) (hx : x ∈ (joinFiber d.p 1).obj n) (hx' : x ∈ (joinFiber d'.p 1).obj n), (CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.right.app n)) ⟨x, hx'⟩) : d = d'

Join data are equal when their maps to Δ[1] agree and their maps to K and L agree on every simplex.

theorem SSet.JoinData.ext_iff {X K L : SSet} {d d' : X.JoinData K L} : d = d' ↔ d.p = d'.p ∧ (∀ (n : SimplexCategoryᵒᵖ) (x : X.obj n) (hx : x ∈ (joinFiber d.p 0).obj n) (hx' : x ∈ (joinFiber d'.p 0).obj n), (CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.left.app n)) ⟨x, hx'⟩) ∧ ∀ (n : SimplexCategoryᵒᵖ) (x : X.obj n) (hx : x ∈ (joinFiber d.p 1).obj n) (hx' : x ∈ (joinFiber d'.p 1).obj n), (CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.right.app n)) ⟨x, hx'⟩

theorem SSet.JoinData.congr_left_app {X K L : SSet} {d d' : X.JoinData K L} (h : d = d') {n : SimplexCategoryᵒᵖ} (x : X.obj n) (hx : x ∈ (joinFiber d.p 0).obj n) (hx' : x ∈ (joinFiber d'.p 0).obj n) : (CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.left.app n)) ⟨x, hx'⟩

Equal join data have equal maps to K.

theorem SSet.JoinData.congr_right_app {X K L : SSet} {d d' : X.JoinData K L} (h : d = d') {n : SimplexCategoryᵒᵖ} (x : X.obj n) (hx : x ∈ (joinFiber d.p 1).obj n) (hx' : x ∈ (joinFiber d'.p 1).obj n) : (CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (d'.right.app n)) ⟨x, hx'⟩

Equal join data have equal maps to L.

def SSet.JoinData.precomp {X Y K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) : Y.JoinData K L

The restriction of join data on X along a map g : Y ⟶ X.

@[simp]

theorem SSet.JoinData.precomp_p {X Y K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) : (d.precomp g).p = CategoryTheory.CategoryStruct.comp g d.p

@[simp]

theorem SSet.JoinData.precomp_left_app {X Y K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) {n : SimplexCategoryᵒᵖ} (y : Y.obj n) (hy : y ∈ (joinFiber (d.precomp g).p 0).obj n) : (CategoryTheory.ConcreteCategory.hom ((d.precomp g).left.app n)) ⟨y, hy⟩ = (CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨(CategoryTheory.ConcreteCategory.hom (g.app n)) y, hy⟩

@[simp]

theorem SSet.JoinData.precomp_right_app {X Y K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) {n : SimplexCategoryᵒᵖ} (y : Y.obj n) (hy : y ∈ (joinFiber (d.precomp g).p 1).obj n) : (CategoryTheory.ConcreteCategory.hom ((d.precomp g).right.app n)) ⟨y, hy⟩ = (CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨(CategoryTheory.ConcreteCategory.hom (g.app n)) y, hy⟩

theorem SSet.JoinData.yonedaEquiv_precomp_p_apply {K L : SSet} {k k' : ℕ} (d : (stdSimplex.obj { len := k }).JoinData K L) (g : stdSimplex.obj { len := k' } ⟶ stdSimplex.obj { len := k }) (j : Fin (k' + 1)) : (yonedaEquiv (d.precomp g).p) j = (yonedaEquiv d.p) ((yonedaEquiv g) j)

Along join data on Δ[k] restricted by g : Δ[k'] ⟶ Δ[k], the vertex j of Δ[k'] lies over the vertex of Δ[1] over which yonedaEquiv g j lies.

@[simp]

theorem SSet.JoinData.precomp_id {X K L : SSet} (d : X.JoinData K L) : d.precomp (CategoryTheory.CategoryStruct.id X) = d

@[simp]

theorem SSet.JoinData.precomp_precomp {X Y Z K L : SSet} (d : X.JoinData K L) (g : Y ⟶ X) (h : Z ⟶ Y) : (d.precomp g).precomp h = d.precomp (CategoryTheory.CategoryStruct.comp h g)

def SSet.JoinData.postcomp {X K L K' L' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') : X.JoinData K' L'

Composition of join data with maps f : K ⟶ K' and g : L ⟶ L'.

@[simp]

theorem SSet.JoinData.postcomp_p {X K L K' L' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') : (d.postcomp f g).p = d.p

@[simp]

theorem SSet.JoinData.postcomp_left_app {X K L K' L' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') {n : SimplexCategoryᵒᵖ} (x : X.obj n) (hx : x ∈ (joinFiber (d.postcomp f g).p 0).obj n) : (CategoryTheory.ConcreteCategory.hom ((d.postcomp f g).left.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (f.app n)) ((CategoryTheory.ConcreteCategory.hom (d.left.app n)) ⟨x, ⋯⟩)

@[simp]

theorem SSet.JoinData.postcomp_right_app {X K L K' L' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') {n : SimplexCategoryᵒᵖ} (x : X.obj n) (hx : x ∈ (joinFiber (d.postcomp f g).p 1).obj n) : (CategoryTheory.ConcreteCategory.hom ((d.postcomp f g).right.app n)) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom (g.app n)) ((CategoryTheory.ConcreteCategory.hom (d.right.app n)) ⟨x, ⋯⟩)

@[simp]

theorem SSet.JoinData.postcomp_id {X K L : SSet} (d : X.JoinData K L) : d.postcomp (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) = d

@[simp]

theorem SSet.JoinData.postcomp_postcomp {X K L K' L' K'' L'' : SSet} (d : X.JoinData K L) (f : K ⟶ K') (g : L ⟶ L') (f' : K' ⟶ K'') (g' : L' ⟶ L'') : (d.postcomp f g).postcomp f' g' = d.postcomp (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g')

theorem SSet.JoinData.precomp_postcomp {X Y K L K' L' : SSet} (d : X.JoinData K L) (h : Y ⟶ X) (f : K ⟶ K') (g : L ⟶ L') : (d.postcomp f g).precomp h = (d.precomp h).postcomp f g

theorem SSet.JoinData.postcomp_injective {X K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') [CategoryTheory.Mono f] [CategoryTheory.Mono g] : Function.Injective fun (d : X.JoinData K L) => d.postcomp f g

Composition of join data with monomorphisms is injective.

def SSet.JoinData.functor (K L : SSet) : CategoryTheory.Functor SSetᵒᵖ (Type u)

Join data, as a presheaf on simplicial sets.

@[simp]

theorem SSet.JoinData.functor_obj (K L : SSet) (X : SSetᵒᵖ) : (functor K L).obj X = (Opposite.unop X).JoinData K L

@[simp]

theorem SSet.JoinData.functor_map (K L : SSet) {X✝ Y✝ : SSetᵒᵖ} (g : X✝ ⟶ Y✝) : (functor K L).map g = TypeCat.ofHom fun (d : (Opposite.unop X✝).JoinData K L) => d.precomp g.unop

def SSet.join (K L : SSet) : SSet

The join K ⋆ L of simplicial sets K and L. Its n-simplices are the join data on Δ[n]: a splitting of the vertices of Δ[n] into an initial segment and a final segment, with a simplex of K on the first and a simplex of L on the second, either of which is omitted when its segment is empty.

theorem SSet.JoinData.precomp_yonedaEquiv_symm_left_app {X K L : SSet} (d : X.JoinData K L) {n : SimplexCategory} (x : X.obj (Opposite.op n)) (hx : x ∈ (joinFiber d.p 0).obj (Opposite.op n)) (h : yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj n)) ∈ (joinFiber (d.precomp (yonedaEquiv.symm x)).p 0).obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((d.precomp (yonedaEquiv.symm x)).left.app (Opposite.op n))) ⟨yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj n)), h⟩ = (CategoryTheory.ConcreteCategory.hom (d.left.app (Opposite.op n))) ⟨x, hx⟩

Restricting join data along the simplex x and evaluating its map to K on the top simplex gives the value of the map to K at x.

theorem SSet.JoinData.precomp_yonedaEquiv_symm_right_app {X K L : SSet} (d : X.JoinData K L) {n : SimplexCategory} (x : X.obj (Opposite.op n)) (hx : x ∈ (joinFiber d.p 1).obj (Opposite.op n)) (h : yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj n)) ∈ (joinFiber (d.precomp (yonedaEquiv.symm x)).p 1).obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((d.precomp (yonedaEquiv.symm x)).right.app (Opposite.op n))) ⟨yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj n)), h⟩ = (CategoryTheory.ConcreteCategory.hom (d.right.app (Opposite.op n))) ⟨x, hx⟩

Restricting join data along the simplex x and evaluating its map to L on the top simplex gives the value of the map to L at x.

def SSet.join.objEquiv {K L : SSet} {n : SimplexCategoryᵒᵖ} : (K.join L).obj n ≃ (stdSimplex.obj (Opposite.unop n)).JoinData K L

The n-simplices of the join K ⋆ L are the join data on Δ[n].

@[simp]

theorem SSet.join.objEquiv_map {K L : SSet} {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : (K.join L).obj n) : objEquiv ((CategoryTheory.ConcreteCategory.hom ((K.join L).map f)) x) = (objEquiv x).precomp (stdSimplex.map f.unop)

def SSet.join.π (K L : SSet) : K.join L ⟶ stdSimplex.obj { len := 1 }

The projection of the join K ⋆ L to Δ[1].

@[simp]

theorem SSet.join.π_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : (K.join L).obj n) : (CategoryTheory.ConcreteCategory.hom ((π K L).app n)) x = yonedaEquiv (objEquiv x).p

theorem SSet.join.mem_joinFiber_π_iff {K L : SSet} {n : SimplexCategory} (x : (K.join L).obj (Opposite.op n)) (e : Fin 2) : x ∈ (joinFiber (π K L) e).obj (Opposite.op n) ↔ yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj (Opposite.unop (Opposite.op n)))) ∈ (joinFiber (objEquiv x).p e).obj (Opposite.op n)

A simplex x of the join lies over the vertex e exactly when the top simplex of Δ[n] lies over e for the join data of x.

def SSet.join.univ (K L : SSet) : (K.join L).JoinData K L

The tautological join data on the join K ⋆ L, corresponding to its identity map.

@[simp]

theorem SSet.join.univ_p {K L : SSet} : (univ K L).p = π K L

theorem SSet.join.univ_left_app {K L : SSet} {n : SimplexCategory} (x : (K.join L).obj (Opposite.op n)) (hx : x ∈ (joinFiber (univ K L).p 0).obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((univ K L).left.app (Opposite.op n))) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom ((objEquiv x).left.app (Opposite.op (Opposite.unop (Opposite.op n))))) ⟨yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj (Opposite.unop (Opposite.op n)))), ⋯⟩

theorem SSet.join.univ_right_app {K L : SSet} {n : SimplexCategory} (x : (K.join L).obj (Opposite.op n)) (hx : x ∈ (joinFiber (univ K L).p 1).obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((univ K L).right.app (Opposite.op n))) ⟨x, hx⟩ = (CategoryTheory.ConcreteCategory.hom ((objEquiv x).right.app (Opposite.op (Opposite.unop (Opposite.op n))))) ⟨yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj (Opposite.unop (Opposite.op n)))), ⋯⟩

theorem SSet.join.univ_precomp_yonedaEquiv_symm {K L : SSet} {n : SimplexCategory} (x : (K.join L).obj (Opposite.op n)) : (univ K L).precomp (yonedaEquiv.symm x) = objEquiv x

Restricting the tautological join data along a simplex x of the join gives the join data of x.

def SSet.join.homEquiv {X K L : SSet} : (X ⟶ K.join L) ≃ X.JoinData K L

The universal property of the join: maps of simplicial sets X ⟶ K ⋆ L correspond to join data on X, that is, to a map p : X ⟶ Δ[1] together with maps to K and L from the parts of X over the vertices 0 and 1. The join data of a map F is the restriction of the tautological join data along F.

theorem SSet.join.homEquiv_apply {X K L : SSet} (F : X ⟶ K.join L) : homEquiv F = (univ K L).precomp F

@[simp]

theorem SSet.join.homEquiv_comp {X Y K L : SSet} (f : Y ⟶ X) (F : X ⟶ K.join L) : homEquiv (CategoryTheory.CategoryStruct.comp f F) = (homEquiv F).precomp f

@[simp]

theorem SSet.join.homEquiv_id {K L : SSet} : homEquiv (CategoryTheory.CategoryStruct.id (K.join L)) = univ K L

@[simp]

theorem SSet.join.homEquiv_p {X K L : SSet} (F : X ⟶ K.join L) : (homEquiv F).p = CategoryTheory.CategoryStruct.comp F (π K L)

The join data of a map F to the join has F ≫ π K L as its map to Δ[1].

theorem SSet.join.homEquiv_symm_app {X K L : SSet} {n : SimplexCategory} (d : X.JoinData K L) (x : X.obj (Opposite.op n)) : (CategoryTheory.ConcreteCategory.hom ((homEquiv.symm d).app (Opposite.op n))) x = objEquiv.symm (d.precomp (yonedaEquiv.symm x))

def SSet.join.representableBy (K L : SSet) : (JoinData.functor K L).RepresentableBy (K.join L)

The join K ⋆ L represents join data.

def SSet.join.map {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') : K.join L ⟶ K'.join L'

The map of joins K ⋆ L ⟶ K' ⋆ L' induced by maps f : K ⟶ K' and g : L ⟶ L'.

@[simp]

theorem SSet.join.homEquiv_comp_map {X K L K' L' : SSet} (F : X ⟶ K.join L) (f : K ⟶ K') (g : L ⟶ L') : homEquiv (CategoryTheory.CategoryStruct.comp F (map f g)) = (homEquiv F).postcomp f g

instance SSet.join.mono_map {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') [CategoryTheory.Mono f] [CategoryTheory.Mono g] : CategoryTheory.Mono (map f g)

The join of two monomorphisms is a monomorphism.

@[simp]

theorem SSet.join.map_π {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') : CategoryTheory.CategoryStruct.comp (map f g) (π K' L') = π K L

@[simp]

theorem SSet.join.map_π_assoc {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f g) (CategoryTheory.CategoryStruct.comp (π K' L') h) = CategoryTheory.CategoryStruct.comp (π K L) h

@[simp]

theorem SSet.join.map_id {K L : SSet} : map (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (K.join L)

theorem SSet.join.map_comp {K L K' L' K'' L'' : SSet} (f : K ⟶ K') (g : L ⟶ L') (f' : K' ⟶ K'') (g' : L' ⟶ L'') : map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (map f g) (map f' g')

theorem SSet.join.map_comp_assoc {K L K' L' K'' L'' : SSet} (f : K ⟶ K') (g : L ⟶ L') (f' : K' ⟶ K'') (g' : L' ⟶ L'') {Z : SSet} (h : K''.join L'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g')) h = CategoryTheory.CategoryStruct.comp (map f g) (CategoryTheory.CategoryStruct.comp (map f' g') h)

def SSet.join.inl (K L : SSet) : K ⟶ K.join L

The inclusion of K into the join K ⋆ L, as the part over the vertex 0.

def SSet.join.inr (K L : SSet) : L ⟶ K.join L

The inclusion of L into the join K ⋆ L, as the part over the vertex 1.

@[simp]

theorem SSet.join.inl_π (K L : SSet) : CategoryTheory.CategoryStruct.comp (inl K L) (π K L) = const (stdSimplex.const 1 0 (Opposite.op { len := 0 }))

@[simp]

theorem SSet.join.inl_π_assoc (K L : SSet) {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (inl K L) (CategoryTheory.CategoryStruct.comp (π K L) h) = CategoryTheory.CategoryStruct.comp (const (stdSimplex.const 1 0 (Opposite.op { len := 0 }))) h

@[simp]

theorem SSet.join.inr_π (K L : SSet) : CategoryTheory.CategoryStruct.comp (inr K L) (π K L) = const (stdSimplex.const 1 1 (Opposite.op { len := 0 }))

@[simp]

theorem SSet.join.inr_π_assoc (K L : SSet) {Z : SSet} (h : stdSimplex.obj { len := 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (inr K L) (CategoryTheory.CategoryStruct.comp (π K L) h) = CategoryTheory.CategoryStruct.comp (const (stdSimplex.const 1 1 (Opposite.op { len := 0 }))) h

theorem SSet.join.univ_left_app_inl_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : K.obj n) (hx : (CategoryTheory.ConcreteCategory.hom ((inl K L).app n)) x ∈ (joinFiber (univ K L).p 0).obj n) : (CategoryTheory.ConcreteCategory.hom ((univ K L).left.app n)) ⟨(CategoryTheory.ConcreteCategory.hom ((inl K L).app n)) x, hx⟩ = x

On the part of K over the vertex 0, the inclusion of K is inverse to the map to K of the tautological join data.

theorem SSet.join.univ_right_app_inr_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : L.obj n) (hx : (CategoryTheory.ConcreteCategory.hom ((inr K L).app n)) x ∈ (joinFiber (univ K L).p 1).obj n) : (CategoryTheory.ConcreteCategory.hom ((univ K L).right.app n)) ⟨(CategoryTheory.ConcreteCategory.hom ((inr K L).app n)) x, hx⟩ = x

On the part of L over the vertex 1, the inclusion of L is inverse to the map to L of the tautological join data.

theorem SSet.join.homEquiv_inl_left_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : K.obj n) (hx : x ∈ (joinFiber (homEquiv (inl K L)).p 0).obj n) : (CategoryTheory.ConcreteCategory.hom ((homEquiv (inl K L)).left.app n)) ⟨x, hx⟩ = x

The join data of the inclusion of K into K ⋆ L restrict to the identity of K over the vertex 0.

theorem SSet.join.homEquiv_inr_right_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : L.obj n) (hx : x ∈ (joinFiber (homEquiv (inr K L)).p 1).obj n) : (CategoryTheory.ConcreteCategory.hom ((homEquiv (inr K L)).right.app n)) ⟨x, hx⟩ = x

The join data of the inclusion of L into K ⋆ L restrict to the identity of L over the vertex 1.

@[simp]

theorem SSet.join.univ_left_comp_inl (K L : SSet) : CategoryTheory.CategoryStruct.comp (univ K L).left (inl K L) = (joinFiber (univ K L).p 0).ι

Every simplex of the join over the vertex 0 is the inclusion of its image in K under the map to K of the tautological join data.

@[simp]

theorem SSet.join.univ_right_comp_inr (K L : SSet) : CategoryTheory.CategoryStruct.comp (univ K L).right (inr K L) = (joinFiber (univ K L).p 1).ι

Every simplex of the join over the vertex 1 is the inclusion of its image in L under the map to L of the tautological join data.

theorem SSet.join.inl_app_univ_left_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : (K.join L).obj n) (hx : x ∈ (joinFiber (univ K L).p 0).obj n) : (CategoryTheory.ConcreteCategory.hom ((inl K L).app n)) ((CategoryTheory.ConcreteCategory.hom ((univ K L).left.app n)) ⟨x, hx⟩) = x

On the part of the join over the vertex 0, the map to K of the tautological join data is inverse to the inclusion of K.

theorem SSet.join.inr_app_univ_right_app {K L : SSet} {n : SimplexCategoryᵒᵖ} (x : (K.join L).obj n) (hx : x ∈ (joinFiber (univ K L).p 1).obj n) : (CategoryTheory.ConcreteCategory.hom ((inr K L).app n)) ((CategoryTheory.ConcreteCategory.hom ((univ K L).right.app n)) ⟨x, hx⟩) = x

On the part of the join over the vertex 1, the map to L of the tautological join data is inverse to the inclusion of L.

theorem SSet.join.range_inl_le_joinFiber (K L : SSet) : Subcomplex.range (inl K L) ≤ joinFiber (univ K L).p 0

The inclusion of K lands in the part of the join over the vertex 0.

theorem SSet.join.range_inr_le_joinFiber (K L : SSet) : Subcomplex.range (inr K L) ≤ joinFiber (univ K L).p 1

The inclusion of L lands in the part of the join over the vertex 1.

def SSet.join.joinFiberZeroIso (K L : SSet) : (joinFiber (univ K L).p 0).toSSet ≅ K

The part of the join K ⋆ L over the vertex 0 is K, through the map to K of the tautological join data and the inclusion of K.

def SSet.join.joinFiberOneIso (K L : SSet) : (joinFiber (univ K L).p 1).toSSet ≅ L

The part of the join K ⋆ L over the vertex 1 is L, through the map to L of the tautological join data and the inclusion of L.

@[simp]

theorem SSet.join.joinFiberZeroIso_hom (K L : SSet) : (joinFiberZeroIso K L).hom = (univ K L).left

The isomorphism joinFiberZeroIso is the map to K of the tautological join data.

@[simp]

theorem SSet.join.joinFiberOneIso_hom (K L : SSet) : (joinFiberOneIso K L).hom = (univ K L).right

The isomorphism joinFiberOneIso is the map to L of the tautological join data.

@[simp]

theorem SSet.join.joinFiberZeroIso_inv_ι (K L : SSet) : CategoryTheory.CategoryStruct.comp (joinFiberZeroIso K L).inv (joinFiber (univ K L).p 0).ι = inl K L

The inverse of joinFiberZeroIso is the inclusion of K.

@[simp]

theorem SSet.join.joinFiberZeroIso_inv_ι_assoc (K L : SSet) {Z : SSet} (h : K.join L ⟶ Z) : CategoryTheory.CategoryStruct.comp (joinFiberZeroIso K L).inv (CategoryTheory.CategoryStruct.comp (joinFiber (univ K L).p 0).ι h) = CategoryTheory.CategoryStruct.comp (inl K L) h

The inverse of joinFiberZeroIso is the inclusion of K.

@[simp]

theorem SSet.join.joinFiberOneIso_inv_ι (K L : SSet) : CategoryTheory.CategoryStruct.comp (joinFiberOneIso K L).inv (joinFiber (univ K L).p 1).ι = inr K L

The inverse of joinFiberOneIso is the inclusion of L.

@[simp]

theorem SSet.join.joinFiberOneIso_inv_ι_assoc (K L : SSet) {Z : SSet} (h : K.join L ⟶ Z) : CategoryTheory.CategoryStruct.comp (joinFiberOneIso K L).inv (CategoryTheory.CategoryStruct.comp (joinFiber (univ K L).p 1).ι h) = CategoryTheory.CategoryStruct.comp (inr K L) h

The inverse of joinFiberOneIso is the inclusion of L.

@[simp]

theorem SSet.join.inl_map {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') : CategoryTheory.CategoryStruct.comp (inl K L) (map f g) = CategoryTheory.CategoryStruct.comp f (inl K' L')

@[simp]

theorem SSet.join.inl_map_assoc {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Z : SSet} (h : K'.join L' ⟶ Z) : CategoryTheory.CategoryStruct.comp (inl K L) (CategoryTheory.CategoryStruct.comp (map f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (inl K' L') h)

@[simp]

theorem SSet.join.inr_map {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') : CategoryTheory.CategoryStruct.comp (inr K L) (map f g) = CategoryTheory.CategoryStruct.comp g (inr K' L')

@[simp]

theorem SSet.join.inr_map_assoc {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Z : SSet} (h : K'.join L' ⟶ Z) : CategoryTheory.CategoryStruct.comp (inr K L) (CategoryTheory.CategoryStruct.comp (map f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (inr K' L') h)

def SSet.join.isoOfIsTerminal {K L : SSet} (hK : CategoryTheory.Limits.IsTerminal K) (hL : CategoryTheory.Limits.IsTerminal L) : K.join L ≅ stdSimplex.obj { len := 1 }

The join of two terminal simplicial sets, such as Δ[0] ⋆ Δ[0], is Δ[1], through the projection π K L.

@[simp]

theorem SSet.join.isoOfIsTerminal_hom {K L : SSet} (hK : CategoryTheory.Limits.IsTerminal K) (hL : CategoryTheory.Limits.IsTerminal L) : (isoOfIsTerminal hK hL).hom = π K L

theorem SSet.join.joinFiber_univ_p_zero_eq_top {K L : SSet} (hL : ¬L.Nonempty) : joinFiber (univ K L).p 0 = ⊤

When L is empty, the whole join K ⋆ L lies over the vertex 0: a vertex over 1 would be a vertex of L.

theorem SSet.join.joinFiber_univ_p_one_eq_top {K L : SSet} (hK : ¬K.Nonempty) : joinFiber (univ K L).p 1 = ⊤

When K is empty, the whole join K ⋆ L lies over the vertex 1: a vertex over 0 would be a vertex of K.

theorem SSet.join.isIso_inl {K L : SSet} (hL : ¬L.Nonempty) : CategoryTheory.IsIso (inl K L)

When L is empty, the inclusion K ⟶ K ⋆ L is an isomorphism.

theorem SSet.join.isIso_inr {K L : SSet} (hK : ¬K.Nonempty) : CategoryTheory.IsIso (inr K L)

When K is empty, the inclusion L ⟶ K ⋆ L is an isomorphism.

def SSet.join.edgeMk {K L : SSet} (x : K.obj (Opposite.op { len := 0 })) (y : L.obj (Opposite.op { len := 0 })) : Edge ((CategoryTheory.ConcreteCategory.hom ((inl K L).app (Opposite.op { len := 0 }))) x) ((CategoryTheory.ConcreteCategory.hom ((inr K L).app (Opposite.op { len := 0 }))) y)

The edge of the join K ⋆ L from a vertex x of K to a vertex y of L: the join data on Δ[1] splitting its vertices as {0} and {1}, with the constant maps at x and y.

@[simp]

theorem SSet.join.objEquiv_edgeMk_edge {K L : SSet} (x : K.obj (Opposite.op { len := 0 })) (y : L.obj (Opposite.op { len := 0 })) : objEquiv (edgeMk x y).edge = { p := CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := 1 }), left := const x, right := const y }

The join data of the edge edgeMk x y on Δ[1].

theorem SSet.join.edge_mem_joinFiber_zero {K L : SSet} {v w : (K.join L).obj (Opposite.op { len := 0 })} (e : Edge v w) (hw : w ∈ (joinFiber (univ K L).p 0).obj (Opposite.op { len := 0 })) : e.edge ∈ (joinFiber (univ K L).p 0).obj (Opposite.op { len := 1 })

An edge of the join K ⋆ L whose target lies over the vertex 0 lies over 0, since the projection to Δ[1] is monotone along the edge.

@[simp]

theorem SSet.join.homEquiv_symm_objEquiv {K L : SSet} {n : SimplexCategory} (s : (K.join L).obj (Opposite.op n)) : homEquiv.symm (objEquiv s) = yonedaEquiv.symm s

The map from a standard simplex given by the join data of a simplex s of the join is the map yonedaEquiv.symm s corresponding to s.

theorem SSet.join.exists_eq_comp_inr {K L : SSet} {m : ℕ} (t : stdSimplex.obj { len := m } ⟶ K.join L) (h : (yonedaEquiv (homEquiv t).p) 0 ≠ 0) : ∃ (l : stdSimplex.obj { len := m } ⟶ L), t = CategoryTheory.CategoryStruct.comp l (inr K L)

A simplex t of K ⋆ L none of whose vertices lies over 0 comes from L.

theorem SSet.join.homEquiv_symm_eq_comp_map {K L : SSet} {m : ℕ} (e : (stdSimplex.obj { len := m }).JoinData K L) (h : (yonedaEquiv e.p) 0 = 0) : homEquiv.symm e = CategoryTheory.CategoryStruct.comp (homEquiv.symm { p := e.p, left := (joinFiber e.p 0).ι, right := e.right }) (map (CategoryTheory.CategoryStruct.comp (joinFiberZeroRetraction e.p h) e.left) (CategoryTheory.CategoryStruct.id L))

A simplex of K ⋆ L with join data e whose vertex 0 lies over 0 is the image, under g ⋆ L, of the simplex of Δ[m] ⋆ L with the same splitting and the same part in L, where g : Δ[m] ⟶ K extends the part of e in K along the retraction joinFiberZeroRetraction.

theorem SSet.join.exists_eq_comp_inr_or_exists_eq_comp_map {K L : SSet} {m : ℕ} (s : stdSimplex.obj { len := m } ⟶ K.join L) : (∃ (l : stdSimplex.obj { len := m } ⟶ L), s = CategoryTheory.CategoryStruct.comp l (inr K L)) ∨ ∃ (t : stdSimplex.obj { len := m } ⟶ (stdSimplex.obj { len := m }).join L) (g : stdSimplex.obj { len := m } ⟶ K), s = CategoryTheory.CategoryStruct.comp t (map g (CategoryTheory.CategoryStruct.id L))

Every simplex of K ⋆ L either comes from L, or is the image of a simplex of Δ[m] ⋆ L under g ⋆ L for a simplex g : Δ[m] ⟶ K.

@[simp]

theorem SSet.join.objEquiv_map_app {K L K' L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {n : SimplexCategory} (s : (K.join L).obj (Opposite.op n)) : objEquiv ((CategoryTheory.ConcreteCategory.hom ((map f g).app (Opposite.op n))) s) = (objEquiv s).postcomp f g

The join data of the image of a simplex s under f ⋆ g is the composition of the join data of s with f and g.

theorem SSet.join.mem_range_map_ι_id_iff {K L : SSet} (A : K.Subcomplex) {n : SimplexCategory} (s : (K.join L).obj (Opposite.op n)) : s ∈ (Subcomplex.range (map A.ι (CategoryTheory.CategoryStruct.id L))).obj (Opposite.op n) ↔ ∀ (k : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).obj k) (hx : x ∈ (joinFiber (objEquiv s).p 0).obj k), (CategoryTheory.ConcreteCategory.hom ((objEquiv s).left.app k)) ⟨x, hx⟩ ∈ A.obj k

A simplex of K ⋆ L lies in the image of A ⋆ L for a subcomplex A of K exactly when its part in K lies in A.

theorem SSet.join.mem_range_map_id_ι_iff {K L : SSet} (B : L.Subcomplex) {n : SimplexCategory} (s : (K.join L).obj (Opposite.op n)) : s ∈ (Subcomplex.range (map (CategoryTheory.CategoryStruct.id K) B.ι)).obj (Opposite.op n) ↔ ∀ (k : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).obj k) (hx : x ∈ (joinFiber (objEquiv s).p 1).obj k), (CategoryTheory.ConcreteCategory.hom ((objEquiv s).right.app k)) ⟨x, hx⟩ ∈ B.obj k

A simplex of K ⋆ L lies in the image of K ⋆ B for a subcomplex B of L exactly when its part in L lies in B.

def SSet.Subcomplex.unionJoin {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : (K.join L).Subcomplex

For subcomplexes A of K and B of L, the subcomplex (A ⋆ L) ∪ (K ⋆ B) of K ⋆ L: the domain of the pushout-join of the inclusions of A and B.

theorem SSet.Subcomplex.unionJoin_def {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : A.unionJoin B = range (join.map A.ι (CategoryTheory.CategoryStruct.id L)) ⊔ range (join.map (CategoryTheory.CategoryStruct.id K) B.ι)

(A ⋆ L) ∪ (K ⋆ B) is the union of the images of A ⋆ L and K ⋆ B in K ⋆ L.

theorem SSet.Subcomplex.range_join_map_ι_id_le_unionJoin {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : range (join.map A.ι (CategoryTheory.CategoryStruct.id L)) ≤ A.unionJoin B

The image of A ⋆ L in K ⋆ L is contained in (A ⋆ L) ∪ (K ⋆ B).

theorem SSet.Subcomplex.range_join_map_id_ι_le_unionJoin {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : range (join.map (CategoryTheory.CategoryStruct.id K) B.ι) ≤ A.unionJoin B

The image of K ⋆ B in K ⋆ L is contained in (A ⋆ L) ∪ (K ⋆ B).

theorem SSet.Subcomplex.unionJoin_le_iff {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) {Z : (K.join L).Subcomplex} : A.unionJoin B ≤ Z ↔ range (join.map A.ι (CategoryTheory.CategoryStruct.id L)) ≤ Z ∧ range (join.map (CategoryTheory.CategoryStruct.id K) B.ι) ≤ Z

(A ⋆ L) ∪ (K ⋆ B) is contained in a subcomplex Z of K ⋆ L exactly when the images of A ⋆ L and K ⋆ B are.

theorem SSet.Subcomplex.mem_unionJoin_iff {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) {n : SimplexCategory} (s : (K.join L).obj (Opposite.op n)) : s ∈ (A.unionJoin B).obj (Opposite.op n) ↔ (∀ (k : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).obj k) (hx : x ∈ (joinFiber (join.objEquiv s).p 0).obj k), (CategoryTheory.ConcreteCategory.hom ((join.objEquiv s).left.app k)) ⟨x, hx⟩ ∈ A.obj k) ∨ ∀ (k : SimplexCategoryᵒᵖ) (x : (stdSimplex.obj n).obj k) (hx : x ∈ (joinFiber (join.objEquiv s).p 1).obj k), (CategoryTheory.ConcreteCategory.hom ((join.objEquiv s).right.app k)) ⟨x, hx⟩ ∈ B.obj k

A simplex of K ⋆ L lies in (A ⋆ L) ∪ (K ⋆ B) exactly when its part in K lies in A or its part in L lies in B.

theorem SSet.Subcomplex.range_join_map_ι_ι {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : range (join.map A.ι B.ι) = range (join.map A.ι (CategoryTheory.CategoryStruct.id L)) ⊓ range (join.map (CategoryTheory.CategoryStruct.id K) B.ι)

The images of A ⋆ L and K ⋆ B in K ⋆ L meet in the image of A ⋆ B.

noncomputable def SSet.Subcomplex.unionJoin.ι₁ {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : A.toSSet.join L ⟶ (A.unionJoin B).toSSet

The inclusion A ⋆ L ⟶ (A ⋆ L) ∪ (K ⋆ B).

noncomputable def SSet.Subcomplex.unionJoin.ι₂ {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : K.join B.toSSet ⟶ (A.unionJoin B).toSSet

The inclusion K ⋆ B ⟶ (A ⋆ L) ∪ (K ⋆ B).

@[simp]

theorem SSet.Subcomplex.unionJoin.ι₁_ι {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : CategoryTheory.CategoryStruct.comp (ι₁ A B) (A.unionJoin B).ι = join.map A.ι (CategoryTheory.CategoryStruct.id L)

@[simp]

theorem SSet.Subcomplex.unionJoin.ι₁_ι_assoc {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) {Z : SSet} (h : K.join L ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι₁ A B) (CategoryTheory.CategoryStruct.comp (A.unionJoin B).ι h) = CategoryTheory.CategoryStruct.comp (join.map A.ι (CategoryTheory.CategoryStruct.id L)) h

@[simp]

theorem SSet.Subcomplex.unionJoin.ι₂_ι {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : CategoryTheory.CategoryStruct.comp (ι₂ A B) (A.unionJoin B).ι = join.map (CategoryTheory.CategoryStruct.id K) B.ι

@[simp]

theorem SSet.Subcomplex.unionJoin.ι₂_ι_assoc {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) {Z : SSet} (h : K.join L ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι₂ A B) (CategoryTheory.CategoryStruct.comp (A.unionJoin B).ι h) = CategoryTheory.CategoryStruct.comp (join.map (CategoryTheory.CategoryStruct.id K) B.ι) h

theorem SSet.Subcomplex.unionJoin.bicartSq {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : (range (join.map A.ι B.ι)).BicartSq (range (join.map A.ι (CategoryTheory.CategoryStruct.id L))) (range (join.map (CategoryTheory.CategoryStruct.id K) B.ι)) (A.unionJoin B)

In the lattice of subcomplexes of K ⋆ L, the square formed by the images of A ⋆ B, A ⋆ L, K ⋆ B and their union (A ⋆ L) ∪ (K ⋆ B) is bicartesian.

theorem SSet.Subcomplex.unionJoin.isPushout {K L : SSet} (A : K.Subcomplex) (B : L.Subcomplex) : CategoryTheory.IsPushout (join.map (CategoryTheory.CategoryStruct.id A.toSSet) B.ι) (join.map A.ι (CategoryTheory.CategoryStruct.id B.toSSet)) (ι₁ A B) (ι₂ A B)

(A ⋆ L) ∪ (K ⋆ B) is the pushout of A ⋆ L and K ⋆ B along A ⋆ B. Hence maps out of the domain of the pushout-join of the inclusions of A and B are glued from compatible maps out of A ⋆ L and K ⋆ B.

theorem SSet.JoinData.exists_precomp_horn_ι_eq {K L : SSet} {n : ℕ} {i : Fin (n + 3)} (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) [K.Quasicategory] [L.Quasicategory] (d : (horn (n + 2) i).toSSet.JoinData K L) : ∃ (D : (stdSimplex.obj { len := n + 2 }).JoinData K L), D.precomp (horn (n + 2) i).ι = d

Inner horn extension for join data: if K and L are quasicategories, join data on an inner horn Λ[n + 2, i] is the restriction of join data on Δ[n + 2].

instance SSet.join.quasicategory {K L : SSet} [K.Quasicategory] [L.Quasicategory] : (K.join L).Quasicategory

Joyal: the join of two quasicategories is a quasicategory.