Add lemma on irred comps of univ catenary

THanks to David Hansen
https://stacks.math.columbia.edu/tag/02J9#comment-5477

Author: aisejohan

Diff for: morphisms.tex

@@ -3047,6 +3047,17 @@ \section{Universally catenary schemes}
 catenary. Thus $R_{\mathfrak p}$ is universally catenary.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-catenary-check-irreducible}
+Let $S$ be a locally Noetherian scheme. Then $S$ is universally catenary
+if and only if the irreducible components of $S$ are universally catenary.
+\end{lemma}
+
+\begin{proof}
+Omitted. For the affine case, please see
+Algebra, Lemma \ref{algebra-lemma-catenary-check-irreducible}.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-ubiquity-uc}
 The following types of schemes are universally catenary.