Joins of standard simplices

The join Δ[n] ⋆ Δ[m] is the standard simplex Δ[n + m + 1], with Δ[n] and Δ[m] as the faces spanned by the first n + 1 and the last m + 1 vertices. Under this isomorphism the joins of horns and boundaries are horns: for n ≠ 0, the subcomplex (Λ[n, i] ⋆ Δ[m]) ∪ (Δ[n] ⋆ ∂Δ[m]) of Δ[n] ⋆ Δ[m] is the horn Λ[n + m + 1, i], and for m ≠ 0, (∂Δ[n] ⋆ Δ[m]) ∪ (Δ[n] ⋆ Λ[m, j]) is the horn Λ[n + m + 1, n + 1 + j]. Hence the pushout-join of a horn inclusion Λ[n, i] ⟶ Δ[n] with 0 < i and a boundary inclusion ∂Δ[m] ⟶ Δ[m] is an inner anodyne extension, and so is the pushout-join of ∂Δ[n] ⟶ Δ[n] and Λ[m, j] ⟶ Δ[m] with j < m. These are the generating cases of the lifting properties showing that slices and coslices of quasicategories are quasicategories, whose projections are right and left fibrations.

Main definitions

• SSet.join.stdSimplexIso n m: the isomorphism Δ[n] ⋆ Δ[m] ≅ Δ[n + m + 1].
• SSet.join.coneEdgeEquiv x y: maps Δ[0] ⋆ Δ[0] ⟶ X sending the cone point to y and the base to x are the edges from y to x.

Main results

• SSet.join.yonedaEquiv_inl_comp_stdSimplexIso_hom, SSet.join.yonedaEquiv_inr_comp_stdSimplexIso_hom: under SSet.join.stdSimplexIso, the vertex j of Δ[n] is the vertex j of Δ[n + m + 1] and the vertex j of Δ[m] is the vertex n + 1 + j. In particular (SSet.join.yonedaEquiv_inl_comp_stdSimplexIso_hom_eq_edge), Δ[1] is the edge of Δ[1 + m + 1] from 0 to 1.
• SSet.join.inl_comp_stdSimplexIso_hom, SSet.join.mkOfSucc_zero_comp_stdSimplexIso_inv, SSet.join.mkOfSucc_succ_comp_stdSimplexIso_inv: under Δ[0] ⋆ Δ[n] ≅ Δ[n + 1], the cone point is the vertex 0, the first edge of the spine is the cone on the vertex 0 of Δ[n], and the other edges of the spine are those of Δ[n].
• SSet.join.hom_ext_of_isStrictSegal: maps from the cone Δ[0] ⋆ Δ[n] to a strict Segal simplicial set are determined by their restrictions to the base Δ[n] and to the edge from the cone point to the vertex 0.
• SSet.join.preimage_unionJoin_horn_boundary: (Λ[n, i] ⋆ Δ[m]) ∪ (Δ[n] ⋆ ∂Δ[m]) corresponds to Λ[n + m + 1, i], for n ≠ 0.
• SSet.join.preimage_unionJoin_boundary_horn: (∂Δ[n] ⋆ Δ[m]) ∪ (Δ[n] ⋆ Λ[m, j]) corresponds to Λ[n + m + 1, n + 1 + j], for m ≠ 0.
• SSet.join.innerAnodyneExtensions_unionJoin_horn_boundary, SSet.join.innerAnodyneExtensions_unionJoin_boundary_horn: the corresponding pushout-joins are inner anodyne extensions.

Implementation notes

The isomorphism sends a simplex of Δ[n] ⋆ Δ[m], described by its join data, to the simplex of Δ[n + m + 1] whose vertices are the images of its vertices in Δ[n], and in Δ[m] shifted by n + 1; its inverse is the map given by the universal property of the join from the join data on Δ[n + m + 1] that splits its vertices after n. To identify the pushout-join with the horn, note that a simplex x of Δ[n + m + 1] that misses a vertex misses it in all faces of its parts in Δ[n] and Δ[m]; conversely, if x misses no vertex other than the horn vertex, a face of its part in Δ[n] and a face of its part in Δ[m] are constructed, as sections of x, that meet all the corresponding vertices.

References

• J. Lurie, Higher Topos Theory, §1.2.8 and Lemma 2.1.2.3.

noncomputable def SSet.join.stdSimplexIso (n m : ℕ) : (stdSimplex.obj { len := n }).join (stdSimplex.obj { len := m }) ≅ stdSimplex.obj { len := n + m + 1 }

The join of standard simplices: Δ[n] ⋆ Δ[m] is isomorphic to Δ[n + m + 1], with Δ[n] and Δ[m] as the faces spanned by the first n + 1 and the last m + 1 vertices.

@[simp]

theorem SSet.join.yonedaEquiv_stdSimplexIso_inv_comp_π {n m : ℕ} (j : Fin (n + m + 2)) : (yonedaEquiv (CategoryTheory.CategoryStruct.comp (stdSimplexIso n m).inv (π (stdSimplex.obj { len := n }) (stdSimplex.obj { len := m })))) j = if ↑j ≤ n then 0 else 1

The vertex j of Δ[n + m + 1] lies over the vertex 0 of Δ[1] in Δ[n] ⋆ Δ[m] exactly when j ≤ n.

@[simp]

theorem SSet.join.yonedaEquiv_inl_comp_stdSimplexIso_hom {n m : ℕ} (j : Fin (n + 1)) : (yonedaEquiv (CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := n }) (stdSimplex.obj { len := m })) (stdSimplexIso n m).hom)) j = Fin.castLE ⋯ j

Under Δ[n] ⋆ Δ[m] ≅ Δ[n + m + 1], Δ[n] is the face on the first n + 1 vertices.

theorem SSet.join.yonedaEquiv_inl_comp_stdSimplexIso_hom_eq_edge (m : ℕ) : yonedaEquiv (CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := 1 }) (stdSimplex.obj { len := m })) (stdSimplexIso 1 m).hom) = stdSimplex.edge (1 + m + 1) 0 1 ⋯

Under Δ[1] ⋆ Δ[m] ≅ Δ[1 + m + 1], Δ[1] is the edge from 0 to 1.

@[simp]

theorem SSet.join.yonedaEquiv_inr_comp_stdSimplexIso_hom {n m : ℕ} (j : Fin (m + 1)) : (yonedaEquiv (CategoryTheory.CategoryStruct.comp (inr (stdSimplex.obj { len := n }) (stdSimplex.obj { len := m })) (stdSimplexIso n m).hom)) j = Fin.cast ⋯ (Fin.natAdd (n + 1) j)

Under Δ[n] ⋆ Δ[m] ≅ Δ[n + m + 1], Δ[m] is the face on the last m + 1 vertices.

Cones Δ[0] ⋆ Δ[n]

theorem SSet.join.inl_comp_stdSimplexIso_hom (n : ℕ) : CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := n })) (stdSimplexIso 0 n).hom = stdSimplex.map ({ len := 0 }.const { len := 0 + n + 1 } 0)

Under Δ[0] ⋆ Δ[n] ≅ Δ[n + 1], the cone point is the vertex 0.

theorem SSet.join.inl_comp_stdSimplexIso_hom_assoc (n : ℕ) {Z : SSet} (h : stdSimplex.obj { len := 0 + n + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := n })) (CategoryTheory.CategoryStruct.comp (stdSimplexIso 0 n).hom h) = CategoryTheory.CategoryStruct.comp (stdSimplex.map ({ len := 0 }.const { len := 0 + n + 1 } 0)) h

Under Δ[0] ⋆ Δ[n] ≅ Δ[n + 1], the cone point is the vertex 0.

theorem SSet.join.δ_one_comp_stdSimplexIso_inv : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) (stdSimplexIso 0 0).inv = inl (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })

Under Δ[0] ⋆ Δ[0] ≅ Δ[1], the cone point is the source of the edge.

theorem SSet.join.δ_zero_comp_stdSimplexIso_inv : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) (stdSimplexIso 0 0).inv = inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })

Under Δ[0] ⋆ Δ[0] ≅ Δ[1], the base of the cone is the target of the edge.

noncomputable def SSet.join.coneEdgeEquiv {X : SSet} (x y : X.obj (Opposite.op { len := 0 })) : { τ : (stdSimplex.obj { len := 0 }).join (stdSimplex.obj { len := 0 }) ⟶ X // CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })) τ = const y ∧ CategoryTheory.CategoryStruct.comp (inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })) τ = const x } ≃ Edge y x

Maps Δ[0] ⋆ Δ[0] ⟶ X sending the cone point to y and the base to x are the edges from y to x, through Δ[0] ⋆ Δ[0] ≅ Δ[1].

@[simp]

theorem SSet.join.coneEdgeEquiv_apply_edge {X : SSet} (x y : X.obj (Opposite.op { len := 0 })) (τ : { τ : (stdSimplex.obj { len := 0 }).join (stdSimplex.obj { len := 0 }) ⟶ X // CategoryTheory.CategoryStruct.comp (inl (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })) τ = const y ∧ CategoryTheory.CategoryStruct.comp (inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })) τ = const x }) : ((coneEdgeEquiv x y) τ).edge = yonedaEquiv (CategoryTheory.CategoryStruct.comp (stdSimplexIso 0 0).inv ↑τ)

The edge attached to a map τ : Δ[0] ⋆ Δ[0] ⟶ X is its composite with Δ[1] ≅ Δ[0] ⋆ Δ[0].

@[simp]

theorem SSet.join.coneEdgeEquiv_symm_apply_coe {X : SSet} (x y : X.obj (Opposite.op { len := 0 })) (e : Edge y x) : ↑((coneEdgeEquiv x y).symm e) = CategoryTheory.CategoryStruct.comp (stdSimplexIso 0 0).hom (yonedaEquiv.symm e.edge)

The map Δ[0] ⋆ Δ[0] ⟶ X attached to an edge e is the composite of Δ[0] ⋆ Δ[0] ≅ Δ[1] with e.

theorem SSet.join.mkOfSucc_zero_comp_stdSimplexIso_inv (n : ℕ) : CategoryTheory.CategoryStruct.comp (stdSimplex.map (SimplexCategory.mkOfSucc 0)) (stdSimplexIso 0 n).inv = CategoryTheory.CategoryStruct.comp (stdSimplexIso 0 0).inv (map (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := 0 })) (stdSimplex.map ({ len := 0 }.const { len := n } 0)))

Under Δ[0] ⋆ Δ[n] ≅ Δ[n + 1], the first edge of the spine of Δ[n + 1] is the cone on the vertex 0 of Δ[n].

theorem SSet.join.mkOfSucc_succ_comp_stdSimplexIso_inv (n : ℕ) (j : Fin (0 + n)) : CategoryTheory.CategoryStruct.comp (stdSimplex.map (SimplexCategory.mkOfSucc j.succ)) (stdSimplexIso 0 n).inv = CategoryTheory.CategoryStruct.comp (stdSimplex.map (SimplexCategory.mkOfSucc (Fin.cast ⋯ j))) (inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := n }))

Under Δ[0] ⋆ Δ[n] ≅ Δ[n + 1], the edges of the spine of Δ[n + 1] other than the first one are the edges of the spine of Δ[n].

theorem SSet.join.hom_ext_of_isStrictSegal {X : SSet} [X.IsStrictSegal] {n : ℕ} {σ σ' : (stdSimplex.obj { len := 0 }).join (stdSimplex.obj { len := n }) ⟶ X} (h₀ : CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := 0 })) (stdSimplex.map ({ len := 0 }.const { len := n } 0))) σ = CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := 0 })) (stdSimplex.map ({ len := 0 }.const { len := n } 0))) σ') (h : CategoryTheory.CategoryStruct.comp (inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := n })) σ = CategoryTheory.CategoryStruct.comp (inr (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := n })) σ') : σ = σ'

Maps from the cone Δ[0] ⋆ Δ[n] to a strict Segal simplicial set, such as the nerve of a category, are determined by their restrictions to the base Δ[n] and to the edge Δ[0] ⋆ {0} from the cone point to the vertex 0: these contain the spine of Δ[0] ⋆ Δ[n] ≅ Δ[n + 1].

Pushout-joins of horns and boundaries

theorem SSet.join.preimage_unionJoin_horn_boundary {n : ℕ} (m : ℕ) (hn : n ≠ 0) (i : Fin (n + 1)) : ((horn n i).unionJoin (boundary m)).preimage (stdSimplexIso n m).inv = horn (n + m + 1) (Fin.castLE ⋯ i)

The pushout-join of a horn and a boundary is a horn. Under Δ[n] ⋆ Δ[m] ≅ Δ[n + m + 1], the subcomplex (Λ[n, i] ⋆ Δ[m]) ∪ (Δ[n] ⋆ ∂Δ[m]) of Δ[n] ⋆ Δ[m] corresponds to the horn Λ[n + m + 1, i], for n ≠ 0 and every i ≤ n.

theorem SSet.join.preimage_unionJoin_boundary_horn (n : ℕ) {m : ℕ} (hm : m ≠ 0) (j : Fin (m + 1)) : ((boundary n).unionJoin (horn m j)).preimage (stdSimplexIso n m).inv = horn (n + m + 1) (Fin.cast ⋯ (Fin.natAdd (n + 1) j))

The pushout-join of a boundary and a horn is a horn. Under Δ[n] ⋆ Δ[m] ≅ Δ[n + m + 1], the subcomplex (∂Δ[n] ⋆ Δ[m]) ∪ (Δ[n] ⋆ Λ[m, j]) of Δ[n] ⋆ Δ[m] corresponds to the horn Λ[n + m + 1, n + 1 + j], for m ≠ 0 and every j ≤ m.

theorem SSet.join.innerAnodyneExtensions_unionJoin_horn_boundary {n : ℕ} (m : ℕ) {i : Fin (n + 1)} (hi : 0 < i) : innerAnodyneExtensions ((horn n i).unionJoin (boundary m)).ι

The pushout-join of a horn Λ[n, i] with 0 < i and a boundary is inner anodyne: the inclusion of (Λ[n, i] ⋆ Δ[m]) ∪ (Δ[n] ⋆ ∂Δ[m]) into Δ[n] ⋆ Δ[m] is isomorphic to the inner horn inclusion Λ[n + m + 1, i] ⟶ Δ[n + m + 1].

theorem SSet.join.innerAnodyneExtensions_unionJoin_boundary_horn (n : ℕ) {m : ℕ} {j : Fin (m + 1)} (hj : j < Fin.last m) : innerAnodyneExtensions ((boundary n).unionJoin (horn m j)).ι

The pushout-join of a boundary and a horn Λ[m, j] with j < m is inner anodyne: the inclusion of (∂Δ[n] ⋆ Δ[m]) ∪ (Δ[n] ⋆ Λ[m, j]) into Δ[n] ⋆ Δ[m] is isomorphic to the inner horn inclusion Λ[n + m + 1, n + 1 + j] ⟶ Δ[n + m + 1].