Cartesian Fibration

Definition

A Cartesian fibration is a functor of $\infty$-categories¹² (e.g. quasicategories) $p:\mathcal{C}\Rightarrow \mathcal{S}$ such that for every morphism $f:s\to t$ in $\mathcal{S}$ and object $x\in \mathcal{C}$ with $p(x)=t$, there exists a $p$-Cartesian edge $\phi :x^{\prime }\to x$ in $\mathcal{C}$ with $p(\phi )=f$. An edge $\phi :x^{\prime }\to x$ over $f:s\to t$ is $p$-Cartesian if it satisfies the expected lifting/universal property on mapping spaces (or equivalently, induces a homotopy pullback on over-categories).³⁴

Equivalently, cartesian fibrations over $\mathcal{S}$ classify contravariant functors ${\mathcal{S}}^{op}\to {\mathbf{Cat}}_{\infty }$ via straightening/unstraightening, generalising the 1-categorical correspondence between Grothendieck fibrations and pseudofunctors ${\mathcal{B}}^{op}\to \mathbf{Cat}$.³

References

Footnotes

1. Weak Infinity Category ↩

2. riehl2019-infinity-categories ↩

3. https://www.math.ias.edu/~lurie/papers/HTT.pdf ↩ ↩²

4. https://ncatlab.org/nlab/show/cartesian+fibration ↩