The Stacks project

Proof. We get a $2$-commutative diagram by Lemma 97.12.1 and hence we get a $1$-morphism (i.e., a functor)

We indicate why this functor is essentially surjective. Namely, an object of the category on the right hand side is given by a scheme $U$ over $S$, an object $y'$ of $\mathcal{Y}'_ U$, an object $(U, Z, y, x, \alpha )$ of $\mathcal{H}_ d(\mathcal{X}/\mathcal{Y})$ over $U$ and an isomorphism $H(y') \to y$ in $\mathcal{Y}_ U$. The assumption means exactly that there exists an object $x'$ of $\mathcal{X}'_ Z$ such that there exist isomorphisms $G(x') \cong x$ and $\alpha ' : y'|_ Z \to F'(x')$ compatible with $\alpha $. Then we see that $(U, Z, y', x', \alpha ')$ is an object of $\mathcal{H}_ d(\mathcal{X}'/\mathcal{Y}')$ over $U$. Details omitted. $\square$