Domenico Fiorenza
over quasi-category



For CC an ordinary category and cCc \in C an object of CC, the ordinary over category CcC\downarrow c satisfies the universal property that for any other category CC' there is a natural equivalence of categories

Hom(C,Cc)Hom c(C[0],C), Hom(C',C\downarrow c) \simeq Hom_{c}(C' \star [0], C) \,,


The object cc can be seen as a functor c:[0]Cc: [0]\to C. From this point of view, γ\gamma is a natural transformation from FιF\circ\iota to cc, where ι:[0]C[0]\iota: [0]\to C' \star [0] is the inclusion functor.

Remaining in the classical setting, even more is true: C[0]C'\star [0] is a particular case of the join operation between categories, which admits a terse description in terms of the cograph of a profunctor.

More precisely, let C,DC,D be two categories; their join CDC\star D is defined to be the category whose set of objects is the disjoint union of the sets of objects of CC and DD, and where we add one and only one morphism between any cCc\in C and any other dDd\in D. This is precisely the cograph of C ωDC\uplus_\omega D of the unique profunctor ω:C op×DrmSet\omega\colon C^\text{op}\times D\to {\rm Set} sending any two (c,d)(c,d) to the singleton.

It is extremely easy, with this definition, to show that given a functor p:KCp\colon K\to C, the category C /pC_{/p} of cones over pp (and the category C p/C_{p/} of co-cones) are uniquely characterized by the following universal properties:

Fun(D,C /p)Fun p(DK,C)\text{Fun}(D, C_{/p})\cong \text{Fun}^{p}(D\star K, C)
Fun(D,C p/)Fun p(KD,C)\text{Fun}(D, C_{p/})\cong \text{Fun}^p(K\star D,C)

where Fun p(DK,C)\text{Fun}^p(D\star K, C) denotes the category whose objects are functors which coincide with pp when restricted to the full subcategory KKDK\subset K\star D (see HTT Prop. This characterize C /pC_{/p} as a representative for the functor DFun p(KD,C)D\mapsto \text{Fun}_p(K\star D,C).

The idea of the definition of over category in the context of quasi-categories is to mimic this universal property. This relies crucially on generalizing the construction C[0]C' \star [0] to the context of quasi-categories, in terms of the join of quasi-categories.

Fosco Loregian Warning: this paragraph is highly conjectural and for the moment I’m not able to offer any proof for these statements. In particular I would like to show * The equivalence between the quasicategorial and the simplicially enriched definition; * Does the “classical” definition of join between simplicial sets KSK\star S coincide with the coherent nerve of the simplicial category C[K]C[S]C[K]\star C[S]? This would automatically entail that the coherent nerve in \star-monoidal, as claimed in HTT

A word about the quasicategorical join operation: Joyal’s Prop. 3.1 suggests to interpret the join operation of simplicial sets as the convolution of presheaves. Nevertheless, it seems that the “pro-functorial” definition has something to say even in the (,1)(\infty,1)-categorical case: instead of the quasicategorical model, we want to consider the simplicially enriched model for (,1)(\infty,1)-categories. In this setting, the join of two (,1)(\infty,1)-categories C,DsSet-CatC,D\in\text{sSet-Cat} can easily be interpreted as the cograph C ωDC\uplus_\omega D of the terminal sSet\text{sSet}-profunctor sending any two objects (C,D)(C,D) to the terminal simplicial set.

See also this question on MO.

Therefore, let F:KCF : K \to C be a morphism of quasi-categories; the over-quasi-category C /FC_{/F} is the quasi-category characterized by the property that for any other quasi-category SS there is a natural equivalence of quasi-categories

Hom(S,C /F)Hom F(SK,C), Hom(S, C_{/F}) \simeq Hom_{F}( S \star K, C ) \,,


Here one sees the advantage of having worked with the full quasi-categories of morphisms rather than with Hom-Sets. Indeed, if [0][0] denotes the terminal quasi-category, then any quasi-category CC is naturally equivalent to Hom([0],C)Hom([0],C).

Therefore the above description of C /FC_{/F} is reduced to the following


Let F:KCF : K \to C be a morphism of quasi-categories. The over-quasi-category C /FC_{/F} is the quasi-category Hom F([0]K,C)Hom_{F}( [0] \star K, C ).


See proposition, p. 44 and the text leading to and including proposition of

See also chapter 3 (_Join and Slices_) in

!redirects over-category in quasi-categories !redirects over quasicategory !redirects over-quasi-category !redirects over-quasicategory !redirects overquasicategory !redirects slice quasi-category !redirects slice quasicategory

Revised on October 27, 2013 12:31:24 by Fosco Loregian