Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
Cartesian fibrations are one of the types of fibrations of quasi-categories.
A Cartesian fibration of quasi-categories – or more generally of simplicial sets – is a morphism that generalizes the notion of Grothendieck fibration from category theory to (∞,1)-category theory, specifically with (∞,1)-categories incarnated as quasi-categories:
It is an inner fibration that lifts also all right outer horn inclusions whose last edge is a cartesian morphism, and such that there is a sufficient supply of cartesian morphisms.
An inner fibration may be thought of as a family of (infinity,1)-categories which is functorial in only in the sense of correspondences. Then the condition of being a cartesian fibration ensures that the family is actually functorial. More precisely, if an (∞,1)-functor is a Cartesian fibration, then it is possible to interpret its value over any morphism in as an (∞,1)-functor between the fibers and over its source and target objects.
This way a Cartesian fibration determines and is determined by an (∞,1)-functor into the (∞,1)-category of (∞,1)-categories. This is the content of the (∞,1)-Grothendieck construction.
Cartesian fibrations over are the fibrant objects in the model structure on marked simplicial over-sets over .
A morphism in sSet is a Cartesian fibration (or Grothendieck fibration) if
it is an inner fibration
for every edge of and for every lift of (that is: ) there is a Cartesian edge in lifting (that is: such that )
The morphism is a cocartesian fibration (or Cartesian opfibration, Grothendieck opfibration) if the opposite is a Cartesian fibration.
This is HTT, def. 2.4.2.1.
Given cartesian fibrations and , let and be the full subsimplicial sets spanned by the functors that preserve cartesian morphisms. We call such functors cartesian functors.
Dually, we make the analogous definition of cocartesian functor.
The are the mapping spaces in the (cartesian) model structure on marked simplicial sets over .
We have:
Every isomorphism of simplicial sets is a Cartesian fibration.
The composite of two Cartesian fibrations is again a Cartesian fibration.
This is HTT, prop. 2.4.2.3.
Every Cartesian fibration is a fibration in the Joyal-model structure for quasi-categories.
This is HTT, prop. 3.3.1.7.
Since a Cartesian fibration is in particular an inner fibration and since inner fibrations are stable under pullback in sSet, it follows that for a Cartesian fibration, the fiber over every point is a quasi-category
The difference between inner fibrations and Cartesian fibrations is that only for Cartesian fibrations is it generally guaranteed that these fibers over the points are functorially related over the morphisms in . This is the content of the (∞,1)-Grothendieck construction.
But moreover:
The pullback of a Cartesian fibration in sSet is again a Cartesian fibration.
This is HTT, prop. 2.4.2.3.
We know from the discussion at inner fibration that the pullback is an inner fibration. It remains to check if it has enough Cartesian morphisms. By HTT, prop 2.4.1.3 we have that in a pullback diagram
a morphism is -Cartesian if is -Cartesian. Since the morphisms of are pairs of morphisms and since by assumption is a Cartesian fibration, there is for and such that is the target of the morphism a Cartesian lift of such that is the target of . Hence a Cartesian lift of in having as target.
We can test locally if a morphism is a Cartesian fibration:
An inner fibration is Cartesian precisely if for each and for every -simplex the sSet-pullback in
is a Cartesian fibration.
This is HTT, cor. 2.4.2.10.
The pullback in sSet of a weak equivalence in the Joyal-model structure for quasi-categories along a Cartesian fibration is again a Joyal-weak equivalence
This is HTT, prop 3.3.1.3
Equivalences in are stable under pullback along Cartesian fibrations:
if
is a pullback square in sSet with a weak equivalence in and a Cartesian fibration, then is also a weak equivalence.
This is HTT, prop. 3.3.1.3.
The following proposition asserts that the ordinary pullback (in sSet) of Cartesian fibrations already models the correct homotopy pullback.
Let
be an pullback diagram in sSet of quasi-categories, where is a Cartesian fibration. Then this is already a homotopy pullback diagram with respect to the model structure for quasi-categories.
This is HTT, prop 3.3.1.4. We factor the bottom morphism as into a weak equivalence and a fibration in . Then the right square in
is the ordinary pullback over a fibrant replacement of the original diagram hence is a homotopy pullback. The claim follows thus if is a weak equivalence, which it is by one of the above lemmas.
There is a Quillen equivalence between the model category of cartesian fibrations and the model category of presheaves valued in quasicategories. See the article straightening functor for more information.
The notion of right fibration is a special case of that of Cartesian fibration:
The following are equivalent:
is a Cartesian fibration and every edge in is -Cartesian
is a right fibration;
is a Cartesian fibration and every fiber is a Kan complex.
This is HTT, prop. 2.4.2.4.
There are also the “categorical fibrations”, the fibrations in the Joyal model structure for quasi-categories on . These turn out not to have much of an intrinsic category theoretic meaning. By the following proposition one can understand the notion of Cartesian fibration as a suitable refinement of the notion of categorical fibration
Every Cartesian fibration in sSet is a fibration with respect to the Joyal model structure for quasi-categories on sSet.
This is HTT, prop. 3.3.1.7.
However, when the base is an -groupoid, then the difference between Cartesian fibrations and categorical fibrations disappears:
Let be a morphism of simplicial sets where is a Kan complex. Then the following are equivalent:
is a Cartesian fibration
is a coCartesian fibration
This is HTT, prop. 3.3.1.8.
There is however another model category structure, which does model Cartesian fibrations.
Let be the overcategory of the category of marked simplicial sets over , equipped with the model structure on marked simplicial over-sets.
An object is fibrant in that model category precisely if
the underlying morphism of simplicial sets is a Cartesian fibration;
the marked edges in are precisely the Cartesian morphisms.
This is HTT, prop. 3.1.4.1.
The inclusion of the cartesian fibrations and cartesian functors in the category has both a left and a right adjoint.
The left adjoint is given by the construction of “free fibrations”
For maps and cartesian fibrations , there are a natural equivalences
Dually, for maps and cocartesian fibrations , there are natural equivalences
The cartesian case for mapping spaces is theorem 4.11 of Gepner-Haugseng-Nikolaus. For the cocartesian case,
On the other side,
The inclusions and have right adjoints.
We handle the cartesian case. The functor tensor product is the left adjoint part of an adjunction between and . Since it sends , we also get an adjunction between and
By the description of the (∞,1)-Grothendieck construction as a lax (∞,1)-colimit, the left adjoint part is an equivalence
Given functors and between quasi-categories, the projection is a Cartesian fibration and the projection is a coCartesian fibration.
In particular, if is a quasi-category, then is a Cartesian fibration and is a coCartesian fibration.
Consider the diagram of pullback squares
HTT, prop. 2.4.7.12 states the projection is a Cartesian fibration. Then is as well, since fibrations are preserved by pullback. Dually for the other projection.
The fiber of at an object is the slice category . So, by the (infinity,1)-Grothendieck construction, this fibration corresponds to the slice functor , where a morphism induces the composition map .
By the (infinity,1)-Grothendieck construction a Cartesian fibration corresponds to a morphism , hence to an (infinity,1)-functor .
Obtaining this through the straightening functor above is tedious, but there is a more immediate way to characterize :
For a Cartesian fibration with specified equivalences
and
an (infinity,1)-functor is associated to if there exists a commuting diagram
such that
;
for every object of we have that is a p-Cartesian morphism of .
This is HTT, def. 5.2.1.1.
If is both a Cartesian fibration as well as a coCartesian fibration, then it determines -functors in both directions
Such a pair is a pair of adjoint (infinity,1)-functors.
… for the moment see HTT, section 3.2.2 …
for the moment see
Cartesian fibration, Cartesian fibration of dendroidal sets
Jacob Lurie, section 2.4.2 in Higher Topos Theory
Aaron Mazel-Gee, A user’s guide to co/cartesian fibrations (arXiv:1510.02402)
David Gepner, Rune Haugseng, Thomas Nikolaus, Lax colimits and free fibrations in -categories (arXiv:1501.02161)
Discussion internal to any (∞,1)-topos:
Last revised on November 15, 2022 at 09:42:34. See the history of this page for a list of all contributions to it.