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

1. $\mathop{\mathrm{Ob}}\nolimits (\mathcal{S}') = \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$, and

2. 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$

There are also:

• 2 comment(s) on Section 4.35: Categories fibred in groupoids

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).