Lemma 4.35.3. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a fibred category. Let $\mathcal{S}'$ be the subcategory of $\mathcal{S}$ defined as follows
$\mathop{\mathrm{Ob}}\nolimits (\mathcal{S}') = \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$, and
for $x, y \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}')$ the set of morphisms between $x$ and $y$ in $\mathcal{S}'$ is the set of strongly cartesian morphisms between $x$ and $y$ in $\mathcal{S}$.
Let $p' : \mathcal{S}' \to \mathcal{C}$ be the restriction of $p$ to $\mathcal{S}'$. Then $p' : \mathcal{S}' \to \mathcal{C}$ is fibred in groupoids.
Proof.
Note that the construction makes sense since by Lemma 4.33.2 the identity morphism of any object of $\mathcal{S}$ is strongly cartesian, and the composition of strongly cartesian morphisms is strongly cartesian. The first lifting property of Definition 4.35.1 follows from the condition that in a fibred category given any morphism $f : V \to U$ and $x$ lying over $U$ there exists a strongly cartesian morphism $\varphi : y \to x$ lying over $f$. Let us check the second lifting property of Definition 4.35.1 for the category $p' : \mathcal{S}' \to \mathcal{C}$ over $\mathcal{C}$. To do this we argue as in the discussion following Definition 4.35.1. Thus in Diagram 4.35.1.1 the morphisms $\phi $, $\psi $ and $\gamma $ are strongly cartesian morphisms of $\mathcal{S}$. Hence $\gamma $ and $\phi \circ \psi $ are strongly cartesian morphisms of $\mathcal{S}$ lying over the same arrow of $\mathcal{C}$ and having the same target in $\mathcal{S}$. By the discussion following Definition 4.33.1 this means these two arrows are isomorphic as desired (here we use also that any isomorphism in $\mathcal{S}$ is strongly cartesian, by Lemma 4.33.2 again).
$\square$
Comments (0)
There are also: