Proof.
In this proof we use the notation $x/U$ to denote an object $x$ of $\mathcal{S}$ which lies over $U$ in $\mathcal{C}$. Similarly $y/V$ denotes an object $y$ of $\mathcal{T}$ which lies over $V$ in $\mathcal{D}$. In the same vein $\alpha /a : x/U \to x'/U'$ denotes the morphism $\alpha : x \to x'$ with image $a : U \to U'$ in $\mathcal{C}$.
Let $G : u_ p\mathcal{S} \to \mathcal{T}$ be a $1$-morphism of fibred categories over $\mathcal{D}$. Denote $G' : u_{pp}\mathcal{S} \to \mathcal{T}$ the composition of $G$ with the canonical (localization) functor $u_{pp}\mathcal{S} \to u_ p\mathcal{S}$. Then consider the functor $H : \mathcal{S} \to u^ p\mathcal{T}$ given by
\[ H(x/U) = (U, G'(U, \text{id}_{u(U)} : u(U) \to u(U), x)) \]
on objects and by
\[ H((\alpha , a) : x/U \to x'/U') = G'(a, u(a), \alpha ) \]
on morphisms. Since $G$ transforms strongly cartesian morphisms into strongly cartesian morphisms, we see that if $\alpha $ is strongly cartesian, then $H(\alpha )$ is strongly cartesian. Namely, we've seen in the proof of Lemma 8.12.6 that in this case the map $(a, u(a), \alpha )$ becomes strongly cartesian in $u_ p\mathcal{S}$. Clearly this construction is functorial in $G$ and we obtain a functor
\[ A : \mathop{\mathrm{Mor}}\nolimits _{\textit{Fib}/\mathcal{D}}(u_ p\mathcal{S}, \mathcal{T}) \longrightarrow \mathop{\mathrm{Mor}}\nolimits _{\textit{Fib}/\mathcal{C}}(\mathcal{S}, u^ p\mathcal{T}) \]
Conversely, let $H : \mathcal{S} \to u^ p\mathcal{T}$ be a $1$-morphism of fibred categories. Recall that an object of $u^ p\mathcal{T}$ is a pair $(U, y)$ with $y \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{T}_{u(U)})$. We denote $\text{pr} : u^ p\mathcal{T} \to \mathcal{T}$ the functor $(U, y) \mapsto y$. In this case we define a functor $G' : u_{pp}\mathcal{S} \to \mathcal{T}$ by the rules
\[ G'(U, \phi : V \to u(U), x) = \phi ^*\text{pr}(H(x)) \]
on objects and we let
\[ G'((a, b, \alpha ) : (U, \phi : V \to u(U), x) \to (U', \phi ' : V' \to u(U'), x')) = \beta \]
be the unique morphism $\beta : \phi ^*\text{pr}(H(x)) \to (\phi ')^*\text{pr}(H(x'))$ such that $q(\beta ) = b$ and the diagram
\[ \xymatrix{ \phi ^*\text{pr}(H(x)) \ar[d] \ar[r]_-{\beta } & (\phi ')^*\text{pr}(H(x')) \ar[d] \\ \text{pr}(H(x)) \ar[r]^{\text{pr}(H(a, \alpha ))} & \text{pr}(H(x')) } \]
Such a morphism exists and is unique because $\mathcal{T}$ is a fibred category.
We check that $G'(r)$ is an isomorphism if $r \in R$. Namely, if
\[ (a, \text{id}_ V, \alpha ) : (U', \phi ' : V \to u(U'), x') \longrightarrow (U, \phi : V \to u(U), x) \]
with $\alpha $ strongly cartesian is an element of the right multiplicative system $R$ of Lemma 8.12.5 then $H(\alpha )$ is strongly cartesian, and $\text{pr}(H(\alpha ))$ is strongly cartesian, see proof of Lemma 8.12.1. Hence in this case the morphism $\beta $ has $q(\beta ) = \text{id}_ V$ and is strongly cartesian. Hence $\beta $ is an isomorphism by Categories, Lemma 4.33.2. Thus by Categories, Lemma 4.27.16 we obtain a canonical extension $G : u_ p\mathcal{S} \to \mathcal{T}$.
Next, let us prove that $G$ transforms strongly cartesian morphisms into strongly cartesian morphisms. Suppose that $f : X \to Y$ is a strongly cartesian. By the characterization of strongly cartesian morphisms in $u_ p\mathcal{S}$ we can write $f$ as $((a, b, \alpha ) : X' \to Y, r : X' \to Y)$ where $r \in R$ and $\alpha $ strongly cartesian in $\mathcal{S}$. By the above it suffices to show that $G'(a, b \alpha )$ is strongly cartesian. As before the condition that $\alpha $ is strongly cartesian implies that $\text{pr}(H(a, \alpha )) : \text{pr}(H(x)) \to \text{pr}(H(x'))$ is strongly cartesian in $\mathcal{T}$. Since in the commutative square above now all arrows except possibly $\beta $ is strongly cartesian it follows that also $\beta $ is strongly cartesian as desired. Clearly the construction $H \mapsto G$ is functorial in $H$ and we obtain a functor
\[ B : \mathop{\mathrm{Mor}}\nolimits _{\textit{Fib}/\mathcal{C}}(\mathcal{S}, u^ p\mathcal{T}) \longrightarrow \mathop{\mathrm{Mor}}\nolimits _{\textit{Fib}/\mathcal{D}}(u_ p\mathcal{S}, \mathcal{T}) \]
To finish the proof of the lemma we have to show that the functors $A$ and $B$ are mutually quasi-inverse. We omit the verifications.
$\square$
Comments (0)
There are also: