The Stacks project

Proof. Assume (2). Let $U \subset U'$ be a first order thickening of affine schemes over $S$, let $y'$ be an object of $\mathcal{Y}$ over $U'$, let $x$ be an object of $\mathcal{X}$ over $U$, and let $\gamma : p(x) \to y'|_ U$ be an isomorphism. Let $X_{y'}$ denote an algebraic space over $U'$ representing the $2$-fibre product

Note that $\xi = (U, U \to U', x, \gamma ^{-1})$ defines an object of this $2$-fibre product over $U$. Via the $2$-Yoneda lemma $\xi $ corresponds to a morphism $f_\xi : U \to X_{y'}$ over $U'$. As $X_{y'} \to U'$ is formally smooth by assumption there exists a morphism $f' : U' \to X_{y'}$ such that $f_\xi $ is the composition of $f'$ and the morphism $U \to U'$. Also, the $2$-Yoneda lemma tells us that $f'$ corresponds to an object $\xi ' = (U', U' \to U', x', \alpha )$ of the displayed $2$-fibre product over $U'$ whose restriction to $U$ recovers $\xi $. In particular we obtain an isomorphism $\gamma : x'|U \to x$. Note that $\alpha : y' \to p(x')$. Hence we see that taking $x'$, the isomorphism $\gamma : x'|U \to x$, and the isomorphism $\beta = \alpha ^{-1} : p(x') \to y'$ is a solution to the problem.

Assume (1). Choose a scheme $T$ and a $1$-morphism $y : (\mathit{Sch}/T)_{fppf} \to \mathcal{Y}$. Let $X_ y$ be an algebraic space over $T$ representing the $2$-fibre product $(\mathit{Sch}/T)_{fppf} \times _{y, \mathcal{Y}, p} \mathcal{X}$. We have to show that $X_ y \to T$ is formally smooth. Hence it suffices to show that given a first order thickening $U \subset U'$ of affine schemes over $T$, then $X_ y(U') \to X_ y(U')$ is surjective (morphisms in the category of algebraic spaces over $T$). Set $y' = y|_{U'}$. By the $2$-Yoneda lemma morphisms $U \to X_ y$ over $T$ correspond bijectively to isomorphism classes of pairs $(x, \alpha )$ where $x$ is an object of $\mathcal{X}$ over $U$ and $\alpha : y|_ U \to p(x)$ is an isomorphism. Of course giving $\alpha $ is, up to an inverse, the same thing as giving an isomorphism $\gamma : p(x) \to y'|_ U$. Similarly for morphisms $U' \to X_ y$ over $T$. Hence (1) guarantees the surjectivity of $X_ y(U') \to X_ y(U')$ in this situation and we win. $\square$