Coslices of simplicial sets #
For a simplicial set C and a diagram p : K ⟶ C, the coslice C_{p/} is the simplicial set
whose n-simplices are the maps K ⋆ Δ[n] ⟶ C from the join that restrict to p on K. Its
vertices are the cocones under p, with cone point the image of Δ[0], and its edges are
morphisms of cocones. A colimit of p in a quasicategory is an initial object of C_{p/}, and for
a vertex y of C the coslice under y : Δ[0] ⟶ C is the quasicategory of objects under y,
through which finality of maps into C is tested.
The coslice is dual to the slice C_{/p} of SSet.slice: it is defined as the opposite
(Cᵒᵖ_{/pᵒᵖ})ᵒᵖ, and its universal property (SSet.coslice.homEquiv), maps X ⟶ C_{p/}
correspond to maps K ⋆ X ⟶ C extending p, naturally in X, is deduced from that of the slice
through the isomorphism (K ⋆ X)ᵒᵖ ≅ Xᵒᵖ ⋆ Kᵒᵖ (SSet.join.opIso).
For the inclusion of a vertex x : Δ[0] ⟶ C, the fibre {x} ×_C C_{y/} over a vertex y of the
projection from the coslice under y is the left mapping space Hom^L_C(y, x): maps to it are the
maps Δ[0] ⋆ Z ⟶ C sending the cone point to y and Z to x, and its vertices are the edges
from y to x. If C is strict Segal, for instance the nerve of a category, it is the discrete
simplicial set on these edges.
Main definitions #
SSet.coslice.functor p: the mapsK ⋆ X ⟶ Cextendingp, as a presheaf inX.SSet.coslice p: the cosliceC_{p/}, whose simplices are described bySSet.coslice.objEquiv.SSet.coslice.π p: the projectionC_{p/} ⟶ C, restricting a simplexK ⋆ Δ[n] ⟶ CtoΔ[n].SSet.coslice.map i g h: the map of coslicesC_{p/} ⟶ D_{q/}induced byi : L ⟶ Kandg : C ⟶ Dwithi ≫ p ≫ g = q, restricting alongiand composing withg; it is functorial (SSet.coslice.map_id,SSet.coslice.map_comp).SSet.coslice.pullbackConstHomEquiv x y: maps to the fibre{x} ×_C C_{y/}are the mapsΔ[0] ⋆ Z ⟶ Csending the cone point toyandZtox.SSet.coslice.pullbackConstObj₀Equiv x y: the vertices of this fibre are the edges fromytox.SSet.coslice.constEdgeIso x y: for a strict SegalC, this fibre is the discrete simplicial set on the edges fromytox.SSet.coslice.opSliceIso p: the identification ofC_{p/}with(Cᵒᵖ_{/pᵒᵖ})ᵒᵖ.
Main results #
SSet.coslice.homEquiv: the universal property of the coslice, mapsX ⟶ C_{p/}correspond to mapsK ⋆ X ⟶ Cextendingp, naturally inX(SSet.coslice.homEquiv_comp_coe); that is,C_{p/}representsSSet.coslice.functor p(SSet.coslice.representableBy).SSet.coslice.objEquiv_app_coe: the simplices of the image of a mapF : X ⟶ C_{p/}are the restrictions of the corresponding mapK ⋆ X ⟶ C.SSet.coslice.comp_π: under the universal property, the projection toCis the restriction toX.SSet.coslice.isIso_π: the coslice under the empty diagram is the whole simplicial set.
References #
- J. Lurie, Higher Topos Theory, §1.2.2 (left mapping spaces) and §1.2.9.
The maps K ⋆ X ⟶ C extending p : K ⟶ C along the inclusion K ⟶ K ⋆ X, as a presheaf on
simplicial sets, acting by precomposition with K ⋆ g.
Instances For
The coslice C_{p/} of a simplicial set C under a diagram p : K ⟶ C. Its n-simplices are
the maps K ⋆ Δ[n] ⟶ C extending p along the inclusion of K (SSet.coslice.objEquiv); in
particular its vertices are the cocones K ⋆ Δ[0] ⟶ C under p. It is defined as the opposite of
the slice Cᵒᵖ_{/pᵒᵖ}.
Instances For
The coslice C_{p/} represents the presheaf of maps K ⋆ X ⟶ C extending p.
Instances For
The n-simplices of the coslice C_{p/} are the maps K ⋆ Δ[n] ⟶ C extending p.
Instances For
The simplex of C_{p/} given by σ corresponds to the map Δ[n] ⟶ C_{p/} given by σ.
The simplex of the coslice that a map F : X ⟶ C_{p/} assigns to a simplex x of X is the
restriction along K ⋆ x of the map K ⋆ X ⟶ C corresponding to F.
The map to the coslice given by τ : K ⋆ X ⟶ C sends a simplex x of X to the simplex
(K ⋆ x) ≫ τ.
The faces and degeneracies of the coslice act on a simplex σ : K ⋆ Δ[n] ⟶ C by precomposition
with the induced maps of joins.
The projection C_{p/} ⟶ C, restricting a simplex K ⋆ Δ[n] ⟶ C of the coslice to Δ[n]
(SSet.coslice.π_app).
Instances For
The projection of the coslice to C corresponds, under the universal property, to restricting
along the inclusion X ⟶ K ⋆ X.
The coslice under the empty diagram is the whole simplicial set: when K is empty, the
projection C_{p/} ⟶ C is an isomorphism.
The projection to C sends a simplex σ : K ⋆ Δ[n] ⟶ C of the coslice to its restriction to
Δ[n].
The map of coslices C_{p/} ⟶ D_{q/} induced by maps i : L ⟶ K and g : C ⟶ D with
i ≫ p ≫ g = q: it restricts a simplex K ⋆ Δ[n] ⟶ C of C_{p/} along i ⋆ Δ[n] and composes
with g. For g = 𝟙 C this is the restriction of cocones along i.
Instances For
Under the universal property, the map of coslices induced by i and g is restriction along
i ⋆ X followed by composition with g.
The map of coslices induced by identities is the identity.
Maps of coslices compose by composing the restrictions and the postcompositions.
Maps of coslices compose by composing the restrictions and the postcompositions.
The map of coslices induced by i and g lies over g.
The map of coslices induced by i and g lies over g.
Fibres of the inclusion of a vertex #
Maps from Z to the fibre {x} ×_L L_{y/} over y of the inclusion of the vertex x are
the maps Δ[0] ⋆ Z ⟶ L sending the cone point to y and Z to x. This is the universal
property of the left mapping space Hom^L_L(y, x).
Instances For
The universal property of the fibre {x} ×_L L_{y/} is natural: precomposing with
g : Z' ⟶ Z corresponds to precomposing with Δ[0] ⋆ g.
The map Δ[0] ⋆ Z ⟶ L attached to g : Z ⟶ {x} ×_L L_{y/} is the map attached by the
universal property of the coslice to the projection g ≫ pullback.snd _ _ of g to L_{y/}.
The projection to the coslice L_{y/} of the map to the fibre {x} ×_L L_{y/} attached to
τ : Δ[0] ⋆ Z ⟶ L is the map attached to τ by the universal property of the coslice.
The vertices of the fibre {x} ×_L L_{y/} over y of the inclusion of the vertex x are the
edges from y to x.
Instances For
The edge attached to a vertex s of the fibre {x} ×_L L_{y/} is the map
Δ[1] ≅ Δ[0] ⋆ Δ[0] ⟶ L corresponding to s.
The map Δ[0] ⋆ Δ[0] ⟶ L attached to the vertex of the fibre {x} ×_L L_{y/} corresponding to
an edge e from y to x is the map attached to e by SSet.join.coneEdgeEquiv.
If L is strict Segal, sending an edge from y to x to the totally degenerate simplices at
the corresponding vertex of the fibre {x} ×_L L_{y/} is an isomorphism from the discrete
simplicial set on these edges.
If L is strict Segal, for instance the nerve of a category, the fibre {x} ×_L L_{y/} over
y of the inclusion of the vertex x is the discrete simplicial set on the edges from y
to x.
Instances For
On vertices, the discreteness isomorphism sends an edge from y to x to the corresponding
vertex of the fibre {x} ×_L L_{y/}.
On vertices, the inverse of the discreteness isomorphism sends a vertex of the fibre
{x} ×_L L_{y/} to the corresponding edge from y to x.