Simplify proof

Thanks to Matthew Emerton
http://stacks.math.columbia.edu/tag/0BPU#comment-1916

stacks-more-morphisms.tex

@@ -88,7 +88,7 @@ \section{Thickenings}
 immersion inducing a bijection $|\mathcal{X}| \to |\mathcal{X}'|$.
 By More on Morphisms of Spaces, Lemmas
 \ref{spaces-more-morphisms-lemma-descending-property-thickening} and
-\ref{spaces-more-morphisms-lemma-base-change-thickening}.
+\ref{spaces-more-morphisms-lemma-base-change-thickening}
 the property $P$ that a morphism of algebraic spaces is a
 (first order) thickening is fpqc local on the base and stable under base
 change. Thus an alternative definition of a
@@ -176,69 +176,9 @@ \section{Thickenings}
 \end{lemma}
 
 \begin{proof}
-Observe that the right vertical arrow in the diagram is a thickening
-by Example \ref{example-reduction-thickening} and
-Lemmas \ref{lemma-composition-thickening} and
-\ref{lemma-base-change-thickening}.
-Hence the projection
-$$
-\mathcal{X} \times_{(\mathcal{X} \times_Y \mathcal{X})}
-(\mathcal{X}_{red} \times_Y \mathcal{X}_{red})
-\longrightarrow \mathcal{X}
-$$
-is a thickening (Lemma \ref{lemma-base-change-thickening}).
-Hence by Example \ref{example-reduction-thickening}
-it suffices to prove that the source of this arrow is reduced.
-
-\medskip\noindent
-Let $U \to \mathcal{X}$ be a surjective smooth morphism
-where $U$ is a scheme. Then
-$U \times_Y U \to \mathcal{X} \times_Y \mathcal{X}$ and
-$U_{red} \times_Y U_{red} \to \mathcal{X}_{red} \times_Y \mathcal{X}_{red}$
-are smooth and surjective. Juggling with $2$-fibre products
-(as in Algebraic Stacks, Lemma \ref{algebraic-lemma-representable-diagonal})
-we see that
-$$
-R = U \times_{\mathcal{X}} U =
-\mathcal{X} \times_{(\mathcal{X} \times_Y \mathcal{X})} (U \times_Y U)
-$$
-is an algebraic space smooth over $\mathcal{X}$. Moreover, we
-obtain a commutative diagram
-$$
-\xymatrix{
-R \ar[d] \ar[r] &
-U \times_Y U \ar[d] &
-U_{red} \times_Y U_{red} \ar[d] \ar[l] \\
-\mathcal{X} \ar[r] &
-\mathcal{X} \times_Y \mathcal{X} &
-\mathcal{X}_{red} \times_Y \mathcal{X}_{red} \ar[l]
-}
-$$
-with $2$-cartesian squares and smooth vertical arrows.
-Since the lower right arrow is a closed immersion, we see that
-$$
-R \times_{(U \times_Y U)} (U_{red} \times_Y U_{red})
-$$
-is an algebraic space with a smooth surjective morphism towards
-$\mathcal{X}\times_{(\mathcal{X} \times_Y \mathcal{X})}
-(\mathcal{X}_{red} \times_Y \mathcal{X}_{red})$. It now suffices
-to show this algebraic space is reduced.
-
-\medskip\noindent
-The morphism 
-$$
-R \times_{U \times_Y U} (U_{red} \times_Y U_{red})
-\longrightarrow
-R \times_{U \times_Y U} (U_{red} \times_Y U)
-$$
-induced by the closed immersion $U_{red} \to U$ is a thickening and so
-it suffices to show that its target is reduced. This target may be identified
-with $R \times_U U_{red}$ (the fibre product
-being taken with respect to the first projection $R \to U$).  
-The projection from this fibre product onto $U_{red}$ is smooth
-(being the base-change of the projection $R \to U$, which is smooth
-as $R = U \times_\mathcal{X} U$ and as $U \to \mathcal{X}$ is smooth),
-and thus this fibre product is indeed reduced, as we wanted to show.
+Since $\mathcal{X}_{red} \to \mathcal{X}$ is a monomorphism,
+this lemma is a special case of Properties of Stacks, Lemma
+\ref{stacks-properties-lemma-monomorphism-diagonal}.
 \end{proof}
 
 \begin{lemma}

stacks-properties.tex

@@ -1512,7 +1512,27 @@ \section{Monomorphisms of algebraic stacks}
 as desired.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-monomorphism-diagonal}
+Let $\mathcal{X} \to \mathcal{X}' \to \mathcal{Y}$ be morphisms
+of algebraic stacks. If $\mathcal{X} \to \mathcal{X}'$ is a monomorphism
+then the canonical diagram
+$$
+\xymatrix{
+\mathcal{X} \ar[r] \ar[d] &
+\mathcal{X} \times_\mathcal{Y} \mathcal{X} \ar[d] \\
+\mathcal{X}' \ar[r] &
+\mathcal{X}' \times_\mathcal{Y} \mathcal{X}'
+}
+$$
+is a fibre product square.
+\end{lemma}
 
+\begin{proof}
+We have $\mathcal{X} = \mathcal{X} \times_{\mathcal{X}'} \mathcal{X}$
+by Lemma \ref{lemma-monomorphism}. Thus the result by applying
+Categories, Lemma \ref{categories-lemma-fibre-product-after-map}.
+\end{proof}