nLab
Cartesian fibration

Contents

Idea

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.

If an (∞,1)-functor p:CD if a Cartesian fibration then it possible to interpret its value over any morphism f:d 1d 2 in D as an (∞,1)-functor p 1(f):p 1(d 2)p 1(d 1) between the fibers p 1(d 2) and p 1(d 1) over its source and target objects.

This way a Cartesian fibration p:CD determines and is determined by an (∞,1)-functor D op(,1)Cat into the (∞,1)-category of (∞,1)-categories. This is the content of the (∞,1)-Grothendieck construction.

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

Definition

Definition

A morphism p:XY in sSet is a Cartesian fibration if

  • it is an inner fibration

  • for every edge f:xy of Y and for every lift y^ of y (that is: p(y^)=y) there is a Cartesian edge f^:x^y^ in X lifting f (that is: such that p(f^)=f)

The morphism is a Cartesian opfibration if the opposite p op:X opY op is a Cartesian fibation.

This is HTT, def. 2.4.2.1.

Properties

General properties

Proposition

We have:

  • Every isomorphism of simplicial sets is a Cartesian fibration.

  • The composite of two Cartesian fibrations is again a Cartesian fibration.

Proof

This is HTT, prop. 2.4.2.3.

Proposition

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

Proof

This is HTT, prop. 3.3.1.7.

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:EC a Cartesian fibration, the fiber E x over every point xC 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 C. This is the content of the (∞,1)-Grothendieck construction.

But moreover:

Proposition

The pullback of a Cartesian fibration in sSet is again a Cartesian fibration.

Proof

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

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 fE is p-Cartesian if q(f) is p-Cartesian. Since the morphisms of E are pairs of morphisms (γ,f^)C 1×E 1 and since by assumption p is a Cartesian, there is for γC 1 a Cartesian lift f^E of k(γ). Hence a Cartesian lift (γ,f^) of γ in E.

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

Proposition

An inner fibration p:XY is Cartesian precisely if for every n-simplex σ:Δ[n]Y the sSet-pullback σ *p:X× YΔ[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.

Proof

This is HTT, cor. 2.4.2.10.

Proposition

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

Proof

This is HTT, prop 3.3.1.3

Lemma

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

if

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 TS a weak equivalence in sSet Joyal and XS a Cartesian fibration, then X× STX is also a weak equivalence.

Proof

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

Proposition

Let

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

be an pullback diagram in sSet of quasi-categories, where XS is a Cartesian fibration. Then this is already a homotopy pullback diagram with respect to the model structure for quasi-categories.

Proof

This is HTT, prop 3.3.1.4. We factor the bottom morphism as STS into a weak equivalence and a fibration in sSet Joyal. Then 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× SX is a weak equivalence, which it is by one of the above lemmas.

Relation to other kinds of fibrations

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

Proposition

The following are equivalent:

  • p:XY is a Cartesian fibration and every edge in X is p-Cartesian

  • p is a right fibration;

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

Proof

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

Proposition

Every Cartesian p:XY in sSet is a fibration with respect to the Joyal model structure for quasi-categories on sSet.

Proof

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:

Proposition (over -groupoids)

Let p:XY be a morphism of simplicial sets where Y is a Kan complex. Then the following are equivalent:

  1. p is a Cartesian fibration

  2. p is a coCartesian fibration

  3. p is a categorical fibration

Proof

This is HTT, prop. 3.3.1.8.

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

Proposition

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

An object XY is fibrant in that model category precisely if

  • the underlying morphism of simplicial sets XY is a Cartesian fibration;

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

Proof

This is HTT, prop. 3.1.4.1.

Examples

Cartesian fibrations over one morphism and Adjunctions

By the (infinity,1)-Grothendieck construction a Cartesian fibration KΔ[1] corresponds to a morphism Δ[1] op(,1)Cat, hence to an (infinity,1)-functor f:CoD.

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

Definition

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

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

and

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

an (infinity,1)-functor f:DC is associated to p 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 1;

  • s D×{0}=h 0g

  • for every object x of D we have that s {x}×Δ[1] is a p-Cartesian morphism of K.

This is HTT, def. 5.2.1.1.

If p:KΔ[1] is noth a Cartesian fibration as well as a coCartesian fibration, then it determines (,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

References

Section 2.4.2 in