A proof of $\dim(R[T])=\dim(R)+1$ without prime ideals?

Question

Background. If $R$ is a commutative ring, it is easy to prove $\dim(R[T]) \geq \dim(R)+1$, where $\dim$ denotes the Krull dimension. If $R$ is Noetherian, we have equality. Every proof of this fact I'm aware of uses quite a bit of commutative algebra and non-trivial theorems such as Krull's intersection theorem. It is worth mentioning that Gelfand-Kirillov dimension satisfies $\mathrm{GK}\dim(R[T])=\mathrm{GK}\dim(R)+1$ for every $K$-algebra $R$.

T. Coquand and H. Lombardi have found a surprisingly elementary, first-order characterization of the Krull dimension that does not use prime ideals at all.

T. Coquand, H. Lombardi, A Short Proof for the Krull Dimension of a Polynomial Ring, The American Mathematical Monthly, Vol. 112, No. 9 (Nov., 2005), pp. 826-829 (4 pages)

You can read the article here. Here is a summary.

For $x \in R$ let $R_{\{x\}}$ denote the localization of $R$ at the multiplicative subset $x^{\mathbb{N}} (1+xR) \subseteq R$. Then we have

$$\qquad \dim(R) = \sup_{x \in R} \left(\dim(R_{\{x\}})+1\right)\!. \label{1}\tag{$\ast$}$$

It follows that for $k \in \mathbb{N}$ we have $\dim(R) \leq k$ if and only if for all $x_0,\dotsc,x_k \in R$ there are $a_0,\dotsc,a_k \in R$ and $m_0,\ldots,m_k \in \mathbb{N}$ such that $$x_0^{m_0} (\cdots ( x_k^{m_k} (1+a_k x_k)+\cdots)+a_0 x_0)=0.$$ You can use this to define the Krull dimension.

This new characterization of $\dim(R) \leq k$ can be seen as a statement in first-order logic (whereas the usual definition with prime ideals uses second-order logic): Use two sorts $N,R$, the usual ring operations for $R$, but also the "mixed" operation $N \times R \to R$, $(n,x) \mapsto x^n$. Every ring becomes a model of this language.

A consequence of this is a new short proof of $\dim(K[x_1,\dotsc,x_n])=n$, where $K$ is a field. Using Noether normalization and the fact that integral extensions don't change the dimension, it follows that $\dim(R\otimes_K S)=\dim(R)+\dim(S)$ if $R,S$ are finitely generated commutative $K$-algebras. In particular $\dim(R[T])=\dim(R)+1$. This could be useful for introductory courses on algebraic geometry which don't want to waste too much time with dimension theory.

Question. Can we use the characterization \eqref{1} of the Krull dimension by Coquand-Lombardi to prove the formula $$\dim(R[T])=\dim(R)+1$$ for Noetherian commutative rings $R$?

Such a proof should not use the prime ideal characterization/definition of the Krull dimension. Notice that the claim is equivalent to $\dim(R[T]_{\{f\}}) \leq \dim(R)$ for all $f \in R[T]$. I suspect that this can only work if we find a first-order property of commutative rings (with powers) which is satisfied in particular by Noetherian rings and prove the formula for these rings.

Please read this first before answering. This question is only concerned with a proof of the dimension formula using the Coquand-Lombardi characterization. If you post an answer that doesn't mention the characterization, then it's not an answer to my question and therefore offtopic. As of writing this, 20 answers have been posted, all of which have been deleted.

Answer 1

Note :- (This is not a complete answer, and I haven't used Noetherian property explicitly.)

Theorem.
Let $R$ be a Noetherian commutative ring and let $T$ be an indeterminate. Then $$ \dim(R[T])=\dim(R)+1, $$ where $\dim$ denotes the Krull dimension, taken here via the Coquand–Lombardi (CL) first–order characterization described below.

Proof.
Write $d:=\dim(R)$. The proof splits into two inequalities.

Preparation (Coquand–Lombardi characterization).
For $k\in\mathbb{N}$ write CL($k$) for the following universal statement: for every tuple $x_0,\dots,x_k\in R$ there exist $a_0,\dots,a_k\in R$ and natural numbers $m_0,\dots,m_k\in\mathbb{N}$ such that the nested zero relation $$ x_0^{m_0}\Big(x_1^{m_1}\big(\cdots (x_k^{m_k}(1+a_k x_k)+\cdots)+a_1x_1\big)+a_0x_0\Big)=0 $$ holds in $R$. One has $\dim(R)\le k$ iff CL($k$) holds in $R$. We will refer to such an identity as a CL-identity of length $k+1$. Elementary facts used below: (i) CL($k$) is preserved under quotients, and (ii) a CL-identity valid over a localization $R_s$ clears denominators to a relation $s^m\cdot(\text{CL-expression})=0$ in $R$.

---

(I) Lower bound: $\dim(R[T])\ge d+1$.
Since $d=\dim(R)$, there are $y_0,\dots,y_d\in R$ which do not satisfy CL($d$) in $R$. View each $y_i$ as a constant polynomial in $R[T]$ and consider the $(d+2)$-tuple $y_0,\dots,y_d,T\in R[T]$. If these satisfied a CL-identity of length $d+2$ in $R[T]$, then evaluating that identity at $T=0$ would produce a CL-identity of length $d+1$ for $y_0,\dots,y_d$ in $R$, contradiction. Hence no CL-identity of length $d+2$ exists in $R[T]$, so $\dim(R[T])\ge d+1$.

---

(II) Upper bound: $\dim(R[T])\le d+1$.
Let $F_0,\dots,F_{d+1}\in R[T]$ be arbitrary and set $$ N:=\sum_{i=0}^{d+1}\deg(F_i)\in\mathbb{N}\cup\{0\}. $$ We prove by induction on $N$ that every $(d+2)$-tuple in $R[T]$ satisfies a CL-identity of length $d+2$.

Base case. If $N=0$ then all $F_i$ are constants in $R$. Since $\dim(R)=d$, CL($d+1$) holds in $R$, hence also in $R[T]$.

Inductive step. Assume the claim for all tuples whose total degree sum is $<N$. Let $F:=F_{d+1}$ and let $\mathcal C=\{c_1,\dots,c_s\}$ be the finite set of coefficients of $F$. Consider the principal localizations $R_{c_j}$ ($j=1,\dots,s$). Two cases occur.

Case A. The ideal $(c_1,\dots,c_s)=R$. Then the principal opens $D(c_j)$ cover $\operatorname{Spec}(R)$. For fixed $j$, work in $R_{c_j}$. Some coefficient of $F$ is invertible, so by multiplying $F$ by a unit we may assume $F$ is monic in $R_{c_j}[T]$. Perform Euclidean division in $R_{c_j}[T]$ to write, for each $i\le d$, $$ F_i = Q_{i,j}\cdot F + R_{i,j},\qquad R_{i,j}\in R_{c_j}[T],\ \deg(R_{i,j})<\deg(F). $$ Replacing $F_i$ by the remainders $R_{i,j}$ does not make the CL-task harder because the multiples $Q_{i,j}F$ are absorbed into the nested form. Thus on $R_{c_j}$ we reduced to a tuple with strictly smaller total degree sum, so by the induction hypothesis there is a CL-identity for these elements in $R_{c_j}[T]$. Clearing denominators yields, for each $j$, an identity $$ u_j\cdot\bigl(\text{a CL-nested polynomial expression in the }F_i\bigr)=0 \quad\text{in }R[T], $$ with $u_j$ a power of $c_j$. Since the $c_j$ generate the unit ideal, the ideal $(u_1,\dots,u_s)=R$, so there exist $r_j\in R$ with $\sum_j r_j u_j=1$. Multiplying the $j$-th identity by $r_j$ and summing gives a global CL-identity in $R[T]$ (the sum of CL-expressions can be rearranged into a single CL-style nested expression). Hence the desired identity exists in this case.

Case B. The ideal $J:=(c_1,\dots,c_s)\subsetneq R$ is proper. Consider the quotient $\overline R:=R/J$. In $\overline R[T]$ the polynomial $F$ becomes $0$, so the total degree sum of $\overline F_0,\dots,\overline F_{d+1}$ is strictly less than $N$. Also $\dim(\overline R)\le d$ (CL-dimension does not increase under quotients). By the induction hypothesis applied to $\overline R$ we obtain a CL-identity in $\overline R[T]$ for the tuple $\overline F_0,\dots,\overline F_{d+1}$; lifting back to $R[T]$ yields an identity of the form $$ \text{(CL-nested expression in the }F_i)=h\in J[T]. $$ Write $h=\sum_{t=1}^s c_t h_t$ with $h_t\in R[T]$. Each identity $c_t\cdot h_t'=0$ (after rearrangement) is of the shape treated in Case A, and the same finite partition-of-unity argument (clearing by powers of the $c_t$ and combining via an $R$-linear combination summing to $1$) produces a global CL-identity in $R[T]$ for $F_0,\dots,F_{d+1}$.

Thus in both cases we obtain the required CL-identity. The induction closes and $\dim(R[T])\le d+1$.

Combining the two inequalities gives $\dim(R[T])=d+1$. □

Remark (used facts).

1. CL($k$) is a universal first-order sentence; it is preserved under quotients.
2. A CL-identity valid over a localization $R_s$ clears denominators to a relation $s^m(\text{CL-expression})=0$ in $R$.