The Stacks project

Proof. Denote $p_ i : \mathcal{H}_ i \to \mathcal{G}$ and $q : \mathcal{G} \to \mathcal{F}$ be the given maps. Let $A' \to A$ be a small extension in $\mathcal{C}_\Lambda $. An object of $\mathcal{H}_1 \times _\mathcal {F} \mathcal{H}_2$ over $A'$ is a triple $(x'_1, x'_2, a')$ where $x'_ i$ is an object of $\mathcal{H}_ i$ over $A'$ and $a' : q(p_1(x'_1)) \to q(p_2(x'_2))$ is a morphism of the fibre category of $\mathcal{F}$ over $A'$. By pushforward along $A' \to A$ we get $(x_1, x_2, a)$. Lifting this to an object of $\mathcal{H}_1 \times _\mathcal {G} \mathcal{H}_2$ over $A$ means finding a morphism $b : p_1(x_1) \to p_2(x_2)$ over $A$ with $q(b) = a$. Thus we have to show that we can lift $b$ to a morphism $b' : p_1(x'_1) \to p_2(x'_2)$ whose image under $q$ is $a'$.

Observe that we can think of

as two objects of $\textit{Lift}(p_2(x_2), A' \to A)$. The functor $q$ sends these objects to the two objects

of $\textit{Lift}(q(p_2(x_2)), A' \to A)$ which are isomorphic using the map $a' : q(p_1(x'_1)) \to q(p_2(x'_2))$. On the other hand, the functor

defines a injection on isomorphism classes by Lemma 90.17.5 and our assumption on tangent spaces. Thus we see that there is a morphism $b' : p_1(x_1') \to p_2(x'_2)$ whose pushforward to $A$ is $b$. However, we may need to adjust our choice of $b'$ to achieve $q(b') = a'$. For this it suffices to see that $q : \text{Inf}(p_2(x'_2)/p_2(x_2)) \to \text{Inf}(q(p_2(x'_2))/q(p_2(x_2)))$ is surjective. This follows from our assumption on infinitesimal automorphisms and Lemma 90.19.11. $\square$