Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
The -Grothendieck construction is the generalization of the Grothendieck construction from category theory to (∞,1)-category theory.
Recall that the 1-category-theoretic Grothendieck construction establishes equivalences of categories,
between (a) fibered categories (or just categories fibered in groupoids) and (b) pseudofunctors to Cat (or just to Grpd).
Analogously, the full Grothendieck construction for (∞,1)-categories constitutes an equivalence of (∞,1)-categories
between (a) Cartesian fibrations of quasi-categories and (b) indexed (∞,1)-categories, that is, (∞,1)-functors to (∞,1)Cat;
while its restriction to the Grothendieck construction for ∞-groupoids constitutes an equivalence of (∞,1)-categories
between right fibrations of quasi-categories and (∞,1)-functors to ∞Grpd.
This correspondence may be modeled:
in the case of -groupoids by a Quillen equivalence between the model structure for right fibrations and the projective global model structure on simplicial presheaves,
in the case of -categories by a Quillen equivalence between the model structure for Cartesian fibrations and the global model structure on functors with values in the model structure on marked simplicial sets.
The generalization of a category fibered in groupoids to quasi-category theory is a right fibration of quasi-categories.
(-Grothendieck construction)
Let be a small (∞,1)-category. The operation of homotopy pullback of the universal fibration of -groupoids constitutes an equivalence of (∞,1)-categories
from the (∞,1)-category of (∞,1)-functors from the opposite category to ∞Grpd, i.e. the (∞,1)-category of (∞,1)-presheaves on ;
to the (∞,1)-category of right fibrations – incarnated as the full SSet-subcategory of the overcategory on right fibrations;
Cisinski19
In the next section we discuss how this statement is presented in terms of model categories.
(-fibrations over an -groupoid)
If itself be an -groupoid, then is equivalently the slice -category of ∞Grpd over , and hence the above Prop. reduces to
By the fact that there is the classical model structure on simplicial sets we have that every morphism of -groupoids factors as
where the top morphism is an equivalence and the right morphism a Kan fibration. Moreover, as discussed at right fibration, over an -groupoid the notions of left/right fibrations and Kan fibrations coincide. This shows that the full sub-(∞,1)-category of on the right fibrations is equivalent to all of .
We discuss a presentation of the -Grothendieck construction by a simplicial Quillen adjunction between simplicial model categories. (HTT, section 2.2.1).
(extracting a simplicial presheaf from a fibration)
Let
be a simplicial set, the corresponding SSet-category (under the left adjoint of the homotopy coherent nerve, denoted in HTT);
an SSet-category;
a morphism of SSet-categories.
In particular we will be interested in the case that is the identity, or at least an equivalence, identifying with .
For any object in consider the sSet-category obtained as the (ordinary) pushout in SSet Cat
where is the join of simplicial sets of with a single vertex .
Using this construction, define a functor, the straightening functor,
from the overcategory of sSet over to the enriched functor category of sSet-enriched functors from to by defining it on objects to act as
The straightening functor effectively computes the fibers of a Cartesian fibration over every point . As an illustration for how this is expressed in terms of morphisms in that pushout, consider the simple situation where
only has a single point;
is a category with three objects, two of them connected by a morphism
is the only possible functor, sending everything to the point.
Then
and
Therefore the category of morphisms in this pushout from to is indeed again the category .
More on this is at Grothendieck construction in the section of adjoints to the Grothendieck construction.
With the definitions as above, let be an sSet-enriched functor between sSet-categories. Write
for the left sSet-Kan extension along .
There is a natural isomorphism of the straightening functor for the composite and the original straightening functor for followed by left Kan extension along :
This is HTT, prop. 2.2.1.1.. The following proof has kindly been spelled out by Harry Gindi.
We unwind what the sSet-categories with a single object adjoined to them look like:
let
be an sSet-enriched functor. Define from this a new sSet-category by setting
The composition operation is that induced from the composition in and the enriched functoriality of .
Observe that the sSet-category appearing in the definition of the straightening functor is
(because is with a single object and some morphisms to adjoined, such that there are no non-degenerate morphisms originating at , we have that is of form for some ; and is that by definition).
To prove the proposition, we need to compute the pushout
and show that indeed .
Using the pasting law for pushouts (see pullback) we just have to compute the lower square pushout. Here the statement is a special case of the following statement: for every sSet-category of the form , the pushout of the canonical inclusion along any -functor is .
This follows by inspection of what a cocone
is like: by the nature of the functor is characterized by a functor , an object together with a natural transformation
being the component of the -functor.
We may write this natural transformation as
where etc. means precomposition with the functor .
By commutativity of the diagram this is
Now by the definition of left Kan extension as the left adjoint to prescomposition with a functor, this is bijectively a transformation
Using this we see that we may find a universal cocone by setting with the canonical inclusion and given by on the restriction to and by the unit on . For this the adjunct transformation is the identity, which makes this universal among all cocones.
This functor has a right adjoint
that takes a simplicial presheaf on to a simplicial set over – this is the unstraightening functor.
One checks that preserves colimits. The claim then follows with the adjoint functor theorem.
(presentation of the -Grothendieck construction)
The straightening and the unstraightening functor constitute a Quillen adjunction
between the model structure for right fibrations and the global projective model structure on simplicial presheaves on .
If is a weak equivalence in the model structure on simplicial categories then this Quillen adjunction is a Quillen equivalence.
This is HTT, theorem 2.2.1.2.
This models the Grothendieck construction for ∞-groupoids in the following way:
the (∞,1)-category presented by is
the (∞,1)-category presented by the global model structure on simplicial presheaves is (∞,1)-category of (∞,1)-presheaves
Hence the unstraightening functor is what models the Grothendieck construction proper, in the sense of a construction that generalizes the construction of a fibered category from a pseudofunctor.
The generalization of a fibered category to quasi-category theory is a Cartesian fibration of quasi-categories.
(-Grothendieck construction)
Let be a small (∞,1)-category. There is an equivalence
on the left we have the -category of Cartesian fibrations over with small fibers and cartesian functors between them – incarnated as a sSet-subcategory of the overcategory on Cartesian fibrations;
and on the right the (∞,1)-category of (∞,1)-functors from to the (∞,1)-category of (∞,1)-categories.
Furthermore, this is equivalence is natural for , where acts by taking pullbacks and acts by composition.
A reference for the naturality in small is corollary A.32 of Gepner-Haugseng-Nikolaus 15. The dual statement is made in remark 1.13 of Mazel-Gee.
In the next section we discuss how this statement is presented in terms of model categories.
Regard the (∞,1)-category in its incarnation as a simplicially enriched category.
Let be a simplicial set, the corresponding simplicially enriched category (where is the left adjoint of the homotopy coherent nerve) and let be an sSet-enriched functor.
(extracting a marked simplicial presheaf from a marked fibration) (HTT, section 3.2.1)
The straightening functor
from marked simplicial sets over to marked simplicial presheaves on is on the underlying simplicial sets (forgetting the marking) the same straightening functor as above.
On the markings the functor acts as follows.
Each edge of gives rise to an edge : the join 2-simplex of
with image in the pushout .
We define the straightening functor to assign that marking of edges which is the minimal one such that all such morphisms are marked in , for all marked in : this means that this marking is being completed under the constraint that be sSet-enriched functorial.
For that, recall that the hom simplicial sets of are the spaces , which consist of those simplices of the internal hom whose edges are all marked:
So we need to find a marking on the such that for all the composite
is a marked edge of the mapping complex. By the internal hom-adjunction this edge corresponds to a morphism
and to be marked needs to carry edges of the form i.e. 1-cells to marked edges
in . So we need to ensure that the edges of this form are marked:
we define that the straightening functor marks an edge in iff it is of this form , for a marked edge of and .
As in the unmarked cae, the straightening functor has an sSet-right adjoint, the unstraightening functor
This functor exhibits the -Grothendieck-construction proper, in that it constructs a Cartesian fibration from a given -functor:
(presentation of -Grothendieck construction)
This induces a Quillen adjunction
between the model structure for Cartesian fibrations and the projective global model structure on functors with values in the model structure on marked simplicial sets.
If is an equivalence in the model structure on simplicial categories then this Quillen adjunction is a Quillen equivalence.
This is HTT, theorem 3.2.0.1.
In the case that happens to be an ordinary category, the -Grothendieck construction can be simplified and given more explicitly.
This is HTT, section 3.2.5.
(relative nerve functor)
Let be a small category and let be a functor. The simplicial set , the relative nerve of under is defined as follows:
an -cell of is
a functor ;
for every a morphism ;
such that for all the diagram
commutes.
There is a canonical morphism
to the ordinary nerve of , obtained by forgetting the s.
This is HTT, def. 3.2.5.2.
When is constant on the point, then is an isomorphism of simplicial sets, so this is the ordinary nerve of .
The fiber of over an object is given by taking to be constant on . Then all the s are fixed by the maximal . So the fiber of over is .
(marked relative nerve functor)
Let be a small category. Define a functor
by
where is with the marking forgotten, where is the relative nerve of under , and where the marking is given by …
This is HTT, def. 3.2.5.12.
This functor has a left adjoint . The value of on some is equivalent to the value of .
This is HTT, Lemma 3.2.5.17.
(-Grothendieck construction over a category)
The adjunction
is a Quillen equivalence between the model structure for coCartesian fibrations and the projective global model structure on functors.
This is HTT, prop. 3.2.5.18.
Let be a simplicial set.
There is a sequence of Quillen adjunctions
Where from left to right we have
the model structure on an overcategory for the Joyal model structure for quasi-categories;
some localizaton of the model structure for Cartesian fibrations;
the model structure on an overcategory for the Quillen model structure on simplicial sets;
The first and third Quillen adjunction here is a Quillen equivalence if is a Kan complex.
The -Grothendieck construction on an -functor is equivalently its lax (infinity,1)-colimit (Gepner-Haugseng-Nikolaus 15).
See also at Grothendieck construction as a lax colimit.
For the base category being the point , the -Grothendieck construction naturally becomes essentially trivial. However, its model by the Quillen functor
is not entirely trivial and in fact produces a Quillen auto-equivalence of with itself that plays a central role in the proof of the corresponding Quillen equivalence over general .
Definition
Let be the cosimplicial simplicial set given by
where
Then: nerve and realization associated to yield a Quillen equivalence of with itself.
…
A Cartesian fibration over the 1-simplex corresponds to a morphism (∞,1)Cat, hence to an (∞,1)-functor .
By the above procedure we can express as the image of under the straightening functor. The characterization via lax colimits leads to describing as the mapping cylinder .
However, there is a more immediate way to extract this functor, which we now describe. This construction also provides additional strictness properties in the quasicategory model.
First recall the situation for the ordinary Grothendieck construction: given a Grothendieck fibration , we obtain a functor between the fibers, by choosing for each object a Cartesian morphism . Then the universal property of Cartesian morphism yields for every morphism in the unique left vertical filler in
And again by universality, this assignment is functorial: .
Diagrammatically, the choice of Cartesian morphisms here is a lift in the diagram
This diagrammatic way of encoding the functor associated to a Grothendieck fibration over the interval generalizes straightforwardly to the quasi-category context.
Given a Cartesian fibration with fibers the quasi-categories and , an -functor associated to the Cartesian fibration is a functor such that there exists a commuting diagram in sSet
such that
;
;
and for all , is a Cartesian morphism in .
More generally, if we also specify possibly nontrivial equivalences of quasi-categories and , then a functor is associated to and this choice of equivalences if the first twoo conditions above are generalized to
;
;
This is HTT, def. 5.2.1.1.
For a Cartesian fibration, the associated functor exists and is unique up to equivalence in the (∞,1)-category of (∞,1)-functors .
This is HTT, prop 5.2.1.5.
Set and .
With the notation described at model structure for Cartesian fibrations, consider the commuting diagram
in the category of marked simplicial sets.
Here the left vertical morphism is marked anodyne: it is the smash product of the marked cofibration (monomorphism) with the marked anodyne morphism . By the stability properties discussed at Marked anodyne morphisms, this implies that the morphism itself is marked anodyne.
As discussed there, this means that a lift against the Cartesian fibration in
exists. This exhibits an associated functor .
Suppose now that another associated functor is given. It will correspondingly come with its diagram
Together this may be arranged to a diagram
where the top horizontal morphism picks the 2-horn in whose two edges are labeled by and , respectively.
Now, the left vertical morphism is still marked anodyne, and hence the lift exists, as indicated. Being a morphism of marked simplicial sets, it must map for each the edge to a Cartesian morphism in , and due to the commutativity of the diagram this morphism must be in , sitting over . But as discussed there, a Cartesian morphism over a point is an equivalence. This means that the restriction
is an invertible natural transformation between and , hence these are equivalent in the functor category.
Conversely, every functor gives rise to a Cartesian fibration that it is associated to, in the above sense.
Every -functor is associated to some Cartesian fibration , and this is unique up to equivalence.
This is HTT, prop 5.2.1.3.
The idea is that we obtain from first forming the cylinder and the identifying the left boundary of that with , using .
Formally this means that we form the pushout
in , where and are and with precisely the equivalences marked. This comes canonically with a morphism
and does have the property that , and that is associated to it in that the restriction of the canonical morphism to the 0-fiber is . But it may fail to be a Cartesian fibration.
To fix this, use the small object argument to factor as
where the first morphism is marked anodyne and the second has the right lifting property with respect to all marked anodyne morphisms and is hence (since every morphism in is marked) a Cartesian fibration.
It then remains to check that is still associated to this . This is done by observing that in the small object argument is built succesively from pushouts of the form
where the morphisms on the left are the generators of marked anodyne morphisms (see here). from this one checks that if the fiber is equivalent to , then so is and similarly for . By induction, it follows that is indeed associated to .
To see that the obtained this way is unique up to equivalence, consider…
… for the moment see HTT, section 3.2.2 …
for the moment see
Textbook accounts:
Jacob Lurie, Section 3.2 of: Higher Topos Theory, Annals of Mathematics Studies 170, Princeton University Press 2009 (pup:8957, pdf)
Denis-Charles Cisinski, Section 5.2 of: Higher Categories and Homotopical Algebra, Cambridge University Press 2019 (doi:10.1017/9781108588737, pdf)
(for -groupoids)
More on model-category theoretic construction of the -Grothendieck construction with values in -groupoids is in
Gijs Heuts, Ieke Moerdijk, Left fibrations and homotopy colimits (arXiv:1308.0704)
Gijs Heuts, Ieke Moerdijk, Left fibrations and homotopy colimits II [arXiv:1602.01274]
Discussion in terms of lax (infinity,1)-colimits is in
Section 1 of this paper reviews properties of the Grothendieck construction for quasicategories:
Another review is
Discussion of the -Grothendieck construction for -functors to -toposes from inverse images of -groupoids:
Discussion entirely within the context of quasi-categories:
which lends itself to understanding the universal coCartesian fibration as categorical semantics for the type universe in directed homotopy type theory:
(see video 3 at 1:16:58 and slides 3.33)
Last revised on April 16, 2024 at 08:20:22. See the history of this page for a list of all contributions to it.