Lemma about depth of localization

algebra.tex

@@ -17299,6 +17299,31 @@ \section{Depth}
 $\dim(R/\mathfrak q) \geq \text{depth}(M/x^nM)$ and we win.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-depth-localization}
+Let $R$ be a local Noetherian ring and $M$ a finite $R$-module.
+For a prime ideal $\mathfrak p \subset R$ we have
+$\text{depth}(M_\mathfrak p) + \dim(R/\mathfrak p) \geq \text{depth}(M)$.
+\end{lemma}
+
+\begin{proof}
+If $M_\mathfrak p = 0$, then $\text{depth}(M_\mathfrak p) = \infty$ and
+the lemma holds.
+If $\text{depth}(M) \leq \dim(R/\mathfrak p)$, then the lemma is true.
+If $\text{depth}(M) > \dim(R/\mathfrak p)$, then $\mathfrak p$ is not
+contained in any associated prime $\mathfrak q$ of $M$ by
+Lemma \ref{lemma-depth-dim-associated-primes}.
+Hence we can find an $x \in \mathfrak p$ not contained in any
+associated prime of $M$ by Lemma \ref{lemma-silly} and
+Lemma \ref{lemma-finite-ass}. Then $x$ is a nonzerodivisor
+on $M$, see Lemma \ref{lemma-ass-zero-divisors}.
+Hence $\text{depth}(M/xM) = \text{depth}(M) - 1$ and
+$\text{depth}(M_\mathfrak p / x M_\mathfrak p) =
+\text{depth}(M_\mathfrak p) - 1$ provided $M_\mathfrak p$ is nonzero,
+see Lemma \ref{lemma-depth-drops-by-one}.
+Thus we conclude by induction on $\text{depth}(M)$.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-depth-goes-down-finite}
 Let $(R, \mathfrak m)$ be a Noetherian local ring. Let $R \to S$
@@ -24145,43 +24170,22 @@ \section{Cohen-Macaulay modules}
 \end{lemma}
 
 \begin{proof}
+We may and do assume $\mathfrak p \not = \mathfrak m$ and $M$ not zero.
 Choose a maximal chain of primes $\mathfrak p = \mathfrak p_c \subset
 \mathfrak p_{c - 1} \subset \ldots \subset \mathfrak p_1 \subset \mathfrak m$.
 If we prove the result for $M_{\mathfrak p_1}$ over $R_{\mathfrak p_1}$,
 then the lemma will follow by induction on $c$. Thus we may assume that
 there is no prime strictly between $\mathfrak p$ and $\mathfrak m$.
-
-\medskip\noindent
-If $M_\mathfrak p = 0$, then the lemma holds. Assume
-$M_\mathfrak p \not = 0$.
-We have $\dim(\text{Supp}(M_\mathfrak p)) \leq \dim(\text{Supp}(M)) - 1$
-as a chain of primes in the support of $M_\mathfrak p$ is a chain a primes in
-the support of $M$ not including $\mathfrak m$. Thus it suffices to
-show that the depth of $M_\mathfrak p$ is at least the depth of
-$M$ minus $1$. We will prove by induction on the depth of $M$
-that there exists an $M$-regular sequence
-$f_1, \ldots, f_{\text{depth}(M) - 1}$ in $\mathfrak p$.
-This will prove the lemma since localization at $\mathfrak p$ is exact.
-Since $\text{depth}(M) = \dim((\text{Supp}(M))
-\geq \dim(\text{Supp}(M_\mathfrak p)) + 1 \geq 1$
-we see that the base case happens when the depth of $M$ is $1$
-and this case is trivial. Assume the depth
-of $M$ is at least $2$.
-
-\medskip\noindent
-Let $I \subset R$ be the annihilator of $M$ such that
-$\Spec(R/I) = V(I) = \text{Supp}(M)$ (Lemma \ref{lemma-support-closed}).
-By Lemmas \ref{lemma-CM-over-quotient} and
-\ref{lemma-maximal-chain-maximal-CM}
-every maximal chain of primes in $V(I)$ has length $\geq 2$.
-Hence none of the minimal primes of $V(I)$ are equal to $\mathfrak p$.
-Thus we can use Lemma \ref{lemma-silly}
-to find a $f_1 \in \mathfrak p$ which is not contained in any
-of the minimal primes of $V(I)$. Then $f_1$ is a nonzerodivisor
-on $M$ and $M/f_1M$ has depth exactly one less by Lemma \ref{lemma-CM-one-g}.
-By induction we can extend to an $M$-regular sequence
-$f_1, \ldots, f_r \in \mathfrak p$ with $r = \text{depth}(M) - 1$
-as desired.
+Note that
+$\dim(\text{Supp}(M_\mathfrak p)) \leq \dim(\text{Supp}(M)) - 1$
+because any chain of primes in the support of $M_\mathfrak p$
+can be extended by one more prime (namely $\mathfrak m$) in the
+support of $M$. On the other hand, we have
+$\text{depth}(M_\mathfrak p) \geq \text{depth}(M) - \dim(R/\mathfrak p) =
+\text{depth}(M) - 1$ by Lemma \ref{lemma-depth-localization} and our
+choice of $\mathfrak p$.
+Thus $\text{depth}(M_\mathfrak p) \geq \dim(\text{Supp}(M_\mathfrak p)$
+as desired (the other inequality is Lemma \ref{lemma-bound-depth}).
 \end{proof}
 
 \begin{definition}