Much better proof of a lemma

Thanks to Kentaro Inoue
https://stacks.math.columbia.edu/tag/0GEC#comment-7753

algebra.tex

@@ -15338,6 +15338,29 @@ \section{Associated primes}
 Lemma \ref{lemma-ass-zero}.
 \end{proof}
 
+\noindent
+This lemma should probably be put somewhere else.
+
+\begin{lemma}
+\label{lemma-dim-not-zero-exists-nonzerodivisor-nonunit}
+Let $k$ be a field. Let $S$ be a finite type $k$ algebra.
+If $\dim(S) > 0$, then there exists an element $f \in S$
+which is a nonzerodivisor and a nonunit.
+\end{lemma}
+
+\begin{proof}
+By Lemma \ref{lemma-finite-ass} the ring $S$ has finitely many associated
+prime ideals. By Lemma \ref{lemma-finite-type-algebra-finite-nr-primes}
+the ring $S$ has infinitely many maximal ideals. Hence we can choose
+a maximal ideal $\mathfrak m \subset S$ which is not an associated prime
+of $S$. By prime avoidance (Lemma \ref{lemma-silly}),
+we can choose a nonzero $f \in \mathfrak m$ 
+which is not contained in any of the associated primes of $S$.
+By Lemma \ref{lemma-ass-zero-divisors} the element $f$ is a nonzerodivisor
+and as $f \in \mathfrak m$ we see that $f$ is not a unit.
+\end{proof}
+
+
 
 \section{Symbolic powers}
 \label{section-symbolic-power}
@@ -33218,51 +33241,6 @@ \section{Openness of Cohen-Macaulay loci}
 has dimension zero and hence is Cohen-Macaulay.
 \end{proof}
 
-\begin{lemma}
-\label{lemma-dim-not-zero-exists-nonzerodivisor-nonunit}
-Let $k$ be a field. Let $S$ be a finite type $k$ algebra.
-If $\dim(S) > 0$, then there exists an element $f \in S$
-which is a nonzerodivisor and a nonunit.
-\end{lemma}
-
-\begin{proof}
-Let $I \subset S$ be the radical ideal such that $V(I) \subset \Spec(S)$
-is the set of primes $\mathfrak q \subset S$ with $S_\mathfrak q$
-not Cohen-Macaulay. See Lemma \ref{lemma-generic-CM} which also
-tells us that $V(I)$ is nowhere dense in $\Spec(S)$.
-Let $\mathfrak m \subset S$ be a maximal ideal such that
-$\dim(S_\mathfrak m) > 0$ and $\mathfrak m \not \in V(I)$.
-Such a maximal ideal exists as $\dim(S) > 0$ using the
-Hilbert Nullstellensatz (Theorem \ref{theorem-nullstellensatz}) and
-Lemma \ref{lemma-dimension-at-a-point-finite-type-over-field}
-which implies that any dense open of
-$\Spec(S)$ has the same dimension as $\Spec(S)$.
-Finally, let $\mathfrak q_1, \ldots, \mathfrak q_m$ be the minimal
-primes of $S$. Choose $f \in S$ with
-$$
-f \equiv 1 \bmod I,\quad
-f \in \mathfrak m,\quad
-f \not \in \bigcup \mathfrak q_i
-$$
-This is possible by Lemma \ref{lemma-silly-silly}. Namely, we have
-$S/(I \cap \mathfrak m) = S/I \times S/\mathfrak m$ by
-Lemma \ref{lemma-chinese-remainder}. Thus we can first choose
-$g \in S$ such that $g \equiv 1 \bmod I$ and $g \in \mathfrak m$.
-Then $g + (I \cap \mathfrak m) \not \subset \mathfrak q_i$
-since $V(I \cap \mathfrak m) \not \supset V(\mathfrak q_i)$.
-Hence the lemma applies. Clearly $f$ is not a unit.
-To show that $f$ is a nonzerodivisor, it suffices to
-prove that $f : S_\mathfrak q \to S_\mathfrak q$ is
-injective for every prime ideal $\mathfrak q \subset S$.
-If $S_\mathfrak q$ is not Cohen-Macaulay, then $\mathfrak q \in V(I)$
-and $f$ maps to a unit of $S_\mathfrak q$. On the other hand, if
-$S_\mathfrak q$ is Cohen-Macaulay, then we use that
-$\dim(S_\mathfrak q/fS_\mathfrak q) < \dim(S_\mathfrak q)$
-by the requirement $f \not \in \mathfrak q_i$ and we conclude
-that $f$ is a nonzerodivisor in $S_\mathfrak q$ by
-Lemma \ref{lemma-reformulate-CM}.
-\end{proof}
-
 \begin{lemma}
 \label{lemma-finite-presentation-flat-CM-locus-open}
 Let $R$ be a ring. Let $R \to S$ be of finite presentation