nLab Cartesian fibration




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 p:CDp : C \to D may be thought of as a family of (infinity,1)-categories (C d) dD(C_d)_{d \in D} which is functorial in dd only in the sense of correspondences. Then the condition of pp being a cartesian fibration ensures that the family is actually functorial. More precisely, if an (∞,1)-functor p:CDp : C \to D is a Cartesian fibration, then it is possible to interpret its value over any morphism f:d 1d 2f : d_1 \to d_2 in DD as an (∞,1)-functor p 1(f):p 1(d 2)p 1(d 1)p^{-1}(f) : p^{-1}(d_2) \to p^{-1}(d_1) between the fibers p 1(d 2)p^{-1}(d_2) and p 1(d 1)p^{-1}(d_1) over its source and target objects.

This way a Cartesian fibration p:CDp : C \to D determines and is determined by an (∞,1)-functor D op(,1)CatD^{op} \to (\infty,1)Cat into the (∞,1)-category of (∞,1)-categories. This is the content of the (∞,1)-Grothendieck construction.

Cartesian fibrations over SS are the fibrant objects in the model structure on marked simplicial over-sets over SS.



A morphism p:XYp : X \to Y in sSet is a Cartesian fibration (or Grothendieck fibration) if

  • it is an inner fibration

  • for every edge f:xyf : x \to y of YY and for every lift y^\hat {y} of yy (that is: p(y^)=yp(\hat{y})=y) there is a Cartesian edge f^:x^y^\hat{f} : \hat{x} \to \hat{y} in XX lifting ff (that is: such that p(f^)=fp(\hat f) = f)

The morphism is a cocartesian fibration (or Cartesian opfibration, Grothendieck opfibration) if the opposite p op:X opY opp^{op} : X^{op} \to Y^{op} is a Cartesian fibration.

This is HTT, def.


Given cartesian fibrations p:XCp : X \to C and q:YCq : Y \to C, let Map C cart(p,q)Map C(p,q)Map_C^{cart}(p,q) \subseteq Map_C(p,q) and Fun C cart(p,q)Fun C(p,q)Fun_C^{cart}(p,q) \subseteq Fun_C(p,q) 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 Map C cartMap_C^{cart} are the mapping spaces in the (cartesian) model structure on marked simplicial sets over CC.


General properties


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.


Every Cartesian fibration is a fibration in the Joyal-model structure for quasi-categories.


This is HTT, prop.

Behaviour under pullback

Since a Cartesian fibration is in particular an inner fibration and since inner fibrations are stable under pullback in sSet, it follows that for p:ECp : E \to C a Cartesian fibration, the fiber E xE_x over every point xC 0x \in C_0 is a quasi-category

E x E {x} C. \array{ E_x &\to& E \\ \downarrow && \downarrow \\ \{x\} &\to& C } \,.

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 CC. 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.

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 we have that in a pullback diagram

E q E p p C k C \array{ E' &\stackrel{q}{\to}& E \\ {}^{\mathllap{p'}}\downarrow && \downarrow^{\mathrlap{p}} \\ C' &\stackrel{k}{\to}& C }

a morphism fEf \in E' is pp'-Cartesian if q(f)q(f) is pp-Cartesian. Since the morphisms of EE' are pairs of morphisms (γ,f^)C 1×E 1(\gamma, \hat f) \in C'_1 \times E_1 and since by assumption pp is a Cartesian fibration, there is for γC 1\gamma \in C'_1 and yE 0y \in E'_0 such that p(y)p'(y) is the target of the morphism γ\gamma a Cartesian lift f^E\hat f \in E of k(γ)k(\gamma) such that q(y)q(y) is the target of f^\hat f. Hence a Cartesian lift (γ,f^)(\gamma, \hat f) of γ\gamma in EE' having yy as target.

We can test locally if a morphism is a Cartesian fibration:


An inner fibration p:XYp : X \to Y is Cartesian precisely if for each n2n \leq 2 and for every nn-simplex σ:Δ[n]Y\sigma : \Delta[n] \to Y the sSet-pullback σ *p:X× YΔ[n]Δ[n]\sigma^* p : X \times_Y \Delta[n] \to \Delta[n] in

X× YΔ[n] X p Δ[n] σ Y \array{ X \times_Y \Delta[n] &\to& X \\ \downarrow && \downarrow^{\mathrlap{p}} \\ \Delta[n] &\stackrel{\sigma}{\to}& Y }

is a Cartesian fibration.


This is HTT, cor.


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


Equivalences in sSet JoyalsSet_{Joyal} are stable under pullback along Cartesian fibrations:


X× ST X T S \array{ X \times_S T &\to & X \\ \downarrow && \downarrow \\ T &\stackrel{\simeq}{\to}& S }

is a pullback square in sSet with TST \to S a weak equivalence in sSet JoyalsSet_{Joyal} and XSX \to S a Cartesian fibration, then X× STXX \times_S T \to X is also a weak equivalence.


This is HTT, prop.

The following proposition asserts that the ordinary pullback (in sSet) of Cartesian fibrations already models the correct homotopy pullback.



X X S S \array{ X &\to& X' \\ \downarrow && \downarrow \\ S &\to & S' }

be an pullback diagram in sSet of quasi-categories, where XSX' \to S' 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 We factor the bottom morphism as STS S \stackrel{\simeq}{\to} T \to S' into a weak equivalence and a fibration in sSet JoyalsSet_{Joyal}. Then the right square in

X T× SX X S T S \array{ X &\to& T \times_{S'} X'& \to& X' \\ \downarrow && \downarrow && \downarrow \\ S &\to & T &\to& S' }

is the ordinary pullback over a fibrant replacement of the original diagram hence is a homotopy pullback. The claim follows thus if XT× SXX \to T \times_{S'} X' is a weak equivalence, which it is by one of the above lemmas.

Straightening and unstraightening

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.

Relation to other kinds of fibrations

The notion of right fibration is a special case of that of Cartesian fibration:


The following are equivalent:

  • p:XYp : X \to Y is a Cartesian fibration and every edge in XX is pp-Cartesian

  • pp is a right fibration;

  • pp is a Cartesian fibration and every fiber is a Kan complex.


This is HTT, prop.

There are also the “categorical fibrations”, the fibrations in the Joyal model structure for quasi-categories on sSetsSet. 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 p:XYp : X \to Y in sSet is a fibration with respect to the Joyal model structure for quasi-categories on sSet.


This is HTT, prop.

However, when the base is an \infty-groupoid, then the difference between Cartesian fibrations and categorical fibrations disappears:

Proposition (over \infty-groupoids)

Let p:XYp : X \to Y be a morphism of simplicial sets where YY is a Kan complex. Then the following are equivalent:

  1. pp is a Cartesian fibration

  2. pp is a coCartesian fibration

  3. pp is a categorical fibration


This is HTT, prop.

There is however another model category structure, which does model Cartesian fibrations.


Let sSet +/SsSet^+/S be the overcategory of the category of marked simplicial sets over SS, equipped with the model structure on marked simplicial over-sets.

An object XSX \to S is fibrant in that model category precisely if

  • the underlying morphism of simplicial sets XSX \to S is a Cartesian fibration;

  • the marked edges in XX are precisely the Cartesian morphisms.


This is HTT, prop.

Adjoints to the inclusion into (∞,1)Cat/C

The inclusion of the cartesian fibrations and cartesian functors in the category (,1)Cat /C cart(,1)Cat /C(\infty,1)Cat_{/C}^{cart} \subseteq (\infty,1)Cat_{/C} has both a left and a right adjoint.

The left adjoint is given by the construction of “free fibrations”


For maps p:XCp : X \to C and cartesian fibrations q:YCq : Y \to C, there are a natural equivalences

Fun C(p,q)Fun C cart((Cp),q) Fun_C(p, q) \simeq Fun_C^{cart}((C \downarrow p), q)

Dually, for maps p:XCp : X \to C and cocartesian fibrations q:YCq : Y \to C, there are natural equivalences

Fun C(p,q)Fun C cocart((pC),q) Fun_C(p, q) \simeq Fun_C^{cocart}((p \downarrow C), q)

The cartesian case for mapping spaces is theorem 4.11 of Gepner-Haugseng-Nikolaus. For the cocartesian case,

Fun C(p,q)Fun C op(p op,q op) opFun C op cart((C opp op),q op) opFun C cocart((pC),q) Fun_C(p,q) \simeq Fun_{C^{op}}(p^{op}, q^{op})^{op} \simeq \Fun_{C^{op}}^{cart}((C^{op} \downarrow p^{op}), q^{op})^{op} \simeq \Fun_C^{cocart}((p \downarrow C), q)

On the other side,


The inclusions (,1)Cat /C cart(,1)Cat /C(\infty,1)Cat_{/C}^{cart} \subseteq (\infty,1)Cat_{/C} and (,1)Cat /C cocart(,1)Cat /C(\infty,1)Cat_{/C}^{cocart} \subseteq (\infty,1)Cat_{/C} have right adjoints.


We handle the cartesian case. The functor tensor product CC /- \otimes_C C_{/\bullet} is the left adjoint part of an adjunction between Fun(C op,(,1)Cat)Fun(C^{op}, (\infty,1)Cat) and (,1)Cat(\infty,1)Cat. Since it sends 1C1 \mapsto C, we also get an adjunction between Fun(C op,(,1)Cat)Fun(C^{op}, (\infty,1)Cat) and (,1)Cat /C(\infty,1)Cat_{/C}

By the description of the (∞,1)-Grothendieck construction as a lax (∞,1)-colimit, the left adjoint part is an equivalence Fun(C op,(,1)Cat)(,1)Cat /C cartFun(C^{op}, (\infty,1)Cat) \to (\infty,1)Cat_{/C}^{cart}


Projections from comma categories


Given functors F:ACF : A \to C and G:BCG : B \to C between quasi-categories, the projection (FG)A(F \downarrow G) \to A is a Cartesian fibration and the projection (FG)B(F \downarrow G) \to B is a coCartesian fibration.

In particular, if CC is a quasi-category, then eval 0:C Δ 1Ceval_0 : C^{\Delta^1} \to C is a Cartesian fibration and eval 1:C Δ 1Ceval_1 : C^{\Delta^1} \to C is a coCartesian fibration.


Consider the diagram of pullback squares

(FG) (id CG) B G (Fid C) C Δ 1 1 C 0 A F C \array{ (F \downarrow G) &\to& (id_C \downarrow G) &\to& B \\ \downarrow && \downarrow && \downarrow G\!\! \\ (F \downarrow id_C) &\to& C^{\Delta^1} &\xrightarrow{1}& C \\ \downarrow && \downarrow 0\!\! \\ A &\xrightarrow{F}& C }

HTT, prop. states the projection (id CG)C(id_C \downarrow G) \to C is a Cartesian fibration. Then (FG)A(F \downarrow G) \to A is as well, since fibrations are preserved by pullback. Dually for the other projection.

The fiber of eval 1:C Δ 1Ceval_1 : C^{\Delta^1} \to C at an object XCX \in C is the slice category C /XC_{/X}. So, by the (infinity,1)-Grothendieck construction, this fibration corresponds to the slice functor C(,1)Cat:XC /XC \to (\infty,1)Cat : X \mapsto C_{/X}, where a morphism XYX \to Y induces the composition map C /XC /YC_{/X} \to C_{/Y}.

Cartesian fibrations over one morphism and Adjunctions

By the (infinity,1)-Grothendieck construction a Cartesian fibration KΔ[1]K \to \Delta[1] corresponds to a morphism Δ[1] op(,1)Cat\Delta[1]^{op} \to (\infty,1)Cat, hence to an (infinity,1)-functor f:CDf : C \to D.

Obtaining this through the straightening functor above is tedious, but there is a more immediate way to characterize ff:


For p:KΔ[1]p : K \to \Delta[1] a Cartesian fibration with specified equivalences

h 0:Cp 1(0) h_0 : C \stackrel{\simeq}{\to} p^{-1}(0)


h 1:Dp 1(1) h_1 : D \stackrel{\simeq}{\to} p^{-1}(1)

an (infinity,1)-functor f:DCf : D \to C is associated to pp if there exists a commuting diagram

D×Δ[1] s K Δ[1] \array{ D \times \Delta[1] &&\stackrel{s}{\to}&& K \\ & \searrow && \swarrow \\ && \Delta[1] }

such that

  • s| D×{1}=h 1s|_{D \times \{1\}} = h_1;

  • s| D×{0}=h 0fs|_{D \times \{0\}} = h_0 \circ f

  • for every object xx of DD we have that s| {x}×Δ[1]s|_{\{x\} \times \Delta[1]} is a p-Cartesian morphism of KK.

This is HTT, def.

If p:KΔ[1]p : K \to \Delta[1] is both a Cartesian fibration as well as a coCartesian fibration, then it determines (,1)(\infty,1)-functors in both directions

CD. C \stackrel{\leftarrow}{\to} D \,.

Such a pair is a pair of adjoint (infinity,1)-functors.

Cartesian fibrations over simplices

… for the moment see HTT, section 3.2.2

The universal Cartesian fibration

for the moment see


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.