The Stacks project

Proof. Applying the inverse isomorphisms $i : R \to R$ and $i' : R' \to R'$ to the (first) cartesian diagram of the statement of the lemma we see that

is cartesian as well. By Lemma 78.21.2 we have a $2$-fibre square

where $U'' = U \times _{f, U', t'} R'$ and $R'' = R \times _{f \circ s, U', t'} R'$. By the above we see that $(t, f) : R \to U''$ is an isomorphism, and that

Explicitly the isomorphism $R \times _{s, U, t} R \to R''$ is given by the rule $(r_0, r_1) \mapsto (r_0, f(r_1))$. Moreover, $s'', t'', c''$ translate into the maps

and

Precomposing with the isomorphism

we see that $t''$ and $s''$ turn into $\text{pr}_0$ and $\text{pr}_1$ and that $c''$ turns into $\text{pr}_{02} : R \times _{s, U, s} R \times _{s, U, s} R \to R \times _{s, U, s} R$. Hence we see that there is an isomorphism $[U''/R''] \cong [R/R \times _{s, U, s} R]$ where as a groupoid in algebraic spaces $(R, R \times _{s, U, s} R, s'', t'', c'')$ is the restriction of the trivial groupoid $(U, U, \text{id}, \text{id}, \text{id})$ via $s : R \to U$. Since $s : R \to U$ is a surjection of fppf sheaves (as it has a right inverse) the morphism

is an equivalence by Lemma 78.25.2. This proves the lemma. $\square$