Slices of simplicial sets #

For a simplicial set C and a diagram p : K ⟶ C, the slice C_{/p} is the simplicial set whose n-simplices are the maps Δ[n] ⋆ K ⟶ C from the join that restrict to p on K. Its vertices are the cones over p, with cone point the image of Δ[0], and its edges are morphisms of cones. A limit of p in a quasicategory is a final object of C_{/p}, so this is the construction through which limits are defined; colimits are dually the initial objects of the coslice C_{p/}, built from the joins K ⋆ Δ[n].

The slice is characterized by its universal property (SSet.slice.homEquiv): maps of simplicial sets X ⟶ C_{/p} correspond to maps X ⋆ K ⟶ C extending p, naturally in X. In other words, C_{/p} represents the presheaf SSet.slice.functor p of such maps (SSet.slice.representableBy), and the definition of C_{/p} is the restriction of this presheaf to standard simplices.

Main definitions #

SSet.slice.functor p: the maps X ⋆ K ⟶ C extending p, as a presheaf in X.
SSet.slice p: the slice C_{/p}, whose simplices are described by SSet.slice.objEquiv.
SSet.slice.π p: the projection C_{/p} ⟶ C, restricting a simplex Δ[n] ⋆ K ⟶ C to Δ[n].
SSet.slice.map i g h: the map of slices C_{/p} ⟶ D_{/q} induced by i : L ⟶ K and g : C ⟶ D with i ≫ p ≫ g = q, restricting cones along i and pushing them forward along g.
SSet.slice.restrictionMap i p σ: for p : X ⟶ S and σ : K ⟶ X, the map X_{/σ} ⟶ X_{/i ≫ σ} ×_{S_{/i ≫ σ ≫ p}} S_{/σ ≫ p}, through which Cartesian edges are defined.

Main results #

SSet.slice.homEquiv: the universal property of the slice, maps X ⟶ C_{/p} correspond to maps X ⋆ K ⟶ C extending p, naturally in X (SSet.slice.homEquiv_comp_coe).
SSet.slice.objEquiv_app_coe: the simplices of the image of a map F : X ⟶ C_{/p} are the restrictions of the corresponding map X ⋆ K ⟶ C.
SSet.slice.comp_π: under the universal property, the projection to C is the restriction to X.
SSet.slice.isIso_π: the slice over the empty diagram is the whole simplicial set.
SSet.slice.isPullback_map: slices preserve pullback squares.
SSet.slice.isPullback_restrictionMap, SSet.slice.restrictionMap_comp and SSet.slice.isPullback_restrictionMapComp: the behaviour of restriction maps under base change and composition.

Implementation notes #

Given F : X ⟶ C_{/p}, the map X ⋆ K ⟶ C is defined simplexwise. A simplex of X ⋆ K either lies in K, where it is sent through p, or meets X; in the second case it is the image of a simplex of Δ[m] ⋆ K under g ⋆ K for a simplex g : Δ[m] ⟶ X extending its part in X (SSet.join.exists_eq_comp_inr_or_exists_eq_comp_map), and it is sent to the value of F g on that simplex. The extension g is chosen along the retraction SSet.joinFiberZeroRetraction of Δ[m] onto its part over the vertex 0 of Δ[1], and the value is independent of the choice of factorization because F is compatible with the faces and degeneracies of X.

References #

J. Lurie, Higher Topos Theory, §1.2.9 and the proof of Proposition 2.4.1.3.