# The dimension modulo a principal ideal in a Noetherian local ring

Let $(A,\mathfrak m)$ be a Noetherian local ring and $f$ an element in the maximal ideal $\mathfrak m$. Is it true that $\dim A/(f) \geq \dim A - 1$?

I don't really see a way to connect the two dimensions, what I tried to prove was that any maximal chain of prime ideals in $A$ would contain a prime that is minimal among those containing $f$ - then the result would follow from Krull's Principal Ideal theorem but I couldn't do this.

Perhaps one can just prove this directly without resource to any other theorems?

• Isn't this incorrect? If I have a maximal chain of prime ideals in $A$, if I take $f$ to be an element in $\mathfrak{m}$ but in none of the smaller primes, then $\dim A/(f)=1$ but $\dim A-1$ could be as large as I want. Jan 6, 2017 at 8:32

To prove the formula, we'll show that, for any chain $\mathfrak p_0\subset\dots\subset\mathfrak p_n=\mathfrak m$ of prime ideals, there exists another chain $$\mathfrak p'_0\subset\dots\subset\mathfrak p'_n=\mathfrak m,\enspace\text{such that}\enspace f\in\mathfrak p'_1.$$ We prove this by induction on $n$. If $n=1$, there's nothing to prove. So suppose $n\ge 2$.
• If $f\in\mathfrak p_{n-1}$, localising $A$ at $\mathfrak p_{n-1}$, we obtain a chain of prime ideals of length $n-1$ in $A_{\mathfrak p_{n-1}}$ satisfying the above condition, by the inductive hypothesis. This chain corresponds to a chain in $A$, which we complete with $\mathfrak m$ to obtain a chain of length $n$ such that $f\in\mathfrak p'_1$.
• If $x\notin\mathfrak p_{n-1}$, let $\mathfrak p'_{n-1}$ an element which is minimal among the prime ideals which contain $\mathfrak p_{n-2}+Af$. By the Hauptidealsatz, the ideal $\mathfrak p'_{n-1}/\mathfrak p_{n-2}\subset A/\mathfrak p_{n-2}$ has height $1$, hence $\mathfrak p_{n-2}\subset \mathfrak p'_{n-1}\subset \mathfrak m$ is a chain of length $2$. Thus we've come down to the previous case – a chain: $$\mathfrak p_0\subset\dots\subset\mathfrak p_{n-2}\subset \mathfrak p'_{n-1}\subset \mathfrak p_n=\mathfrak m,\enspace\text{such that}\enspace f\in\mathfrak p'_{n-1}.$$