Clarifiying lemma on dimension of quotient of regular local ring

Question

https://stacks.math.columbia.edu/tag/00KW proves that if $R$ is a regular local ring and $x\in\mathfrak{m}$ is not a zero divisor, then $\dim(R) = \dim (R/(x)) + 1.$

I have a question about one part of their proof. They write that if $x$ is not a zero divisor, then $x$ is not contained in any minimal prime (this is fine to me), and therefore any chain of primes in $R/(x)$ can be extended by one prime in $R.$

They don't elaborate on the last part. I tried to fill it in as follows. Let $0 < \mathfrak{p}_1/(x) < \cdots < \mathfrak{p}_n/(x) < R/(x)$ be a chain of primes in $R/(x).$ Then we claim we can find some prime $\mathfrak{q}$ of $R$ so that $0 < \mathfrak{q} < \mathfrak{p}_1,$ thus extending the chain by at least 1 and proving $\dim(R/(x)) \leq \dim(R) - 1$ (which is what this part of the argument is showing).

But how do we find $\mathfrak{q}$? It seems that to use $x$ is not contained in any minimal prime, I'd say "okay, take $\mathfrak{q}$ a minimal prime containing $\mathfrak{p}_1$, then it doesn't contain $x$ but $\mathfrak{p}_1$ does so the inclusion is proper, boom!"

Except we don't know that $0 < \mathfrak{q}$ is proper (and in fact, this lemma is used to prove that a regular local ring is a domain, so the minimal prime in question must be 0!).

Does anyone see a way to fill in the Stacks' project proof?

Answer 1

First, recall that a chain of primes in $R$ might not include $0$, as it might not be a domain! (At least, not yet.) Thus, when you take a chain of prime ideals of length $n$ in $R/(x)$, we have to consider $$ \mathfrak{p}_0/(x) \subsetneq \mathfrak{p}_1/(x) \subsetneq \dots \subsetneq \mathfrak{p}_n/(x), $$ where each $\mathfrak{p}_i/(x)$ is a prime ideal in $R/(x)$ (note that there are not assumptions about $\mathfrak{p}_i/(x)$ being zero or nonzero).

Now, we lift this chain to $R$, getting $\mathfrak{p}_0 \subsetneq \mathfrak{p}_1 \subsetneq \dots \subsetneq \mathfrak{p}_n$ in $R$. Note also that $(x) \subseteq \mathfrak{p}_0$ (and that we might have equality!) But $x$ was not contained in any minimal prime, hence $\mathfrak{p}_0$ is not minimal. Therefore, there is some prime ideal $\mathfrak{q} \subsetneq \mathfrak{p}_0$. This gives us the chain $$ \mathfrak{q} \subsetneq \mathfrak{p}_0 \subsetneq \mathfrak{p}_1 \subsetneq \dots \subsetneq \mathfrak{p}_n $$ of length $n+1$ in $R$. Then $n+1 \leq \dim R$, proving the claim.