6.2. Right fibrations [0013]

[001O] Definition 6.2·a.

A cartesian fibration $E$ over $B$ is said to be a right fibration when all displayed morphisms in $E$ are cartesian.

Recall from Section 2.5 [0005] that for every $b\in B$, the collection of displayed objects $E\Sub{b}$ and vertical maps $E\Sub{1\Sub{b}}$ forms a category. When $E$ is a right fibration over $B$, this category is in fact a groupoid.

[001P] Theorem 6.2·b (Characterization of right fibrations).

A cartesian fibration $E$ over $B$ is a right fibration if and only if all its vertical maps are isomorphisms.

Proof. Suppose that $E$ is a right fibration over $B$, and fix $b\in B$, $\bar{b}\in E\Sub{b}$, and a vertical map $f:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$. Using the hypothesis that $f$ is cartesian, it has a unique section $g:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$ as follows: Likewise, because $g$ is cartesian, $f$ is the unique section of $g$; thus $f$ is an isomorphism in $E\Sub{b}$.

Conversely, suppose that $E$ is a cartesian fibration whose vertical maps are isomorphisms. Fix $f:x\to y \in B$ and an arbitrary displayed morphism $\bar{g}:\bar{x}\to\Sub{f}\bar{y}$. Then $\bar{g}$ is the precomposition of a cartesian lift $\bar{f}:\bar{x}\tick\to\Sub{f}\bar{y}$ with a vertical map: Because vertical maps are isomorphisms and $\bar{f}$ is cartesian, we can observe that $\bar{g}$ is cartesian as follows, writing $\bar{m} : \bar{u}\to\Sub{m} \bar{x}\tick$ for the unique factorization of $\bar{h}$ through $\bar{f}$ over $m$: