The Stacks project

Proof. This is formal. Let $U \subset U'$ be a first order thickening of affine schemes over $S$, let $z'$ be an object of $\mathcal{Z}$ over $U'$, let $w$ be an object of $\mathcal{X} \times _\mathcal {Y} \mathcal{Z}$ over $U$, and let $\delta : p'(w) \to z'|_ U$ be an isomorphism. We may write $w = (U, x, z, \alpha )$ for some object $x$ of $\mathcal{X}$ over $U$ and object $z$ of $\mathcal{Z}$ over $U$ and isomorphism $\alpha : p(x) \to q(z)$. Note that $p'(w) = z$ hence $\delta : z \to z|_ U$. Set $y' = q(z')$ and $\gamma = q(\delta ) \circ \alpha : p(x) \to y'|_ U$. As $p$ is formally smooth on objects there exists an object $x'$ of $\mathcal{X}$ over $U'$ as well as isomorphisms $\beta : x'|_ U \to x$ and $\gamma ' : p(x') \to y'$ such that (97.6.0.1) commutes. Then we consider the object $w = (U', x', z', \gamma ')$ of $\mathcal{X} \times _\mathcal {Y} \mathcal{Z}$ over $U'$ and define isomorphisms

and

These combine to give a solution to the problem. $\square$

Proof. This is formal. Let $U \subset U'$ be a first order thickening of affine schemes over $S$, let $z'$ be an object of $\mathcal{Z}$ over $U'$, let $x$ be an object of $\mathcal{X}$ over $U$, and let $\gamma : q(p(x)) \to z'|_ U$ be an isomorphism. As $q$ is formally smooth on objects there exist an object $y'$ of $\mathcal{Y}$ over $U'$, an isomorphism $\beta : y'|_ U \to p(x)$, and an isomorphism $\gamma ' : q(y') \to z'$ such that (97.6.0.1) is commutative. As $p$ is formally smooth on objects there exist an object $x'$ of $\mathcal{X}$ over $U'$, an isomorphism $\beta ' : x'|_ U \to x$, and an isomorphism $\gamma '' : p(x') \to y'$ such that (97.6.0.1) is commutative. The solution is to take $x'$ over $U'$ with isomorphism

and isomorphism $\beta ' : x'|_ U \to x$. We omit the verification that (97.6.0.1) is commutative. $\square$

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$