A quantitative Hilbert's basis theorem and the constructive Krull dimension

TL;DR

This paper develops a constructive approach to Hilbert's basis theorem and Krull dimension, introducing $oldsymbol{ ext{α}}$-Noetherian modules and providing new proofs for bounds on the dimension of polynomial rings over fields and integers.

Contribution

It introduces $oldsymbol{ ext{α}}$-Noetherian modules as a constructive analogue of Noetherian modules and offers new constructive proofs of classical dimension bounds.

Findings

Constructive proof of $ ext{dim } K[X_0, ext{...,}X_{n-1}]<1+n$

Constructive proof of $ ext{dim } extbf{Z}[X_0, ext{...,}X_{n-1}]<2+n$

Introduction of $oldsymbol{ ext{α}}$-Noetherian modules as a new concept

Abstract

In classical mathematics, Gulliksen has introduced the length of Noetherian modules, and Brookfield has determined the length of Noetherian polynomial rings. Brookfield's result can be regarded as a quantitative version of Hilbert's basis theorem. In this paper, based on the inductive definition of Noetherian modules in constructive algebra, we introduce a constructive version of the length called $\alpha$-Noetherian modules, and present a constructive proof of some results by Brookfield. As a consequence, we obtain a new constructive proof of $\dim K[X_0,\ldots,X_{n-1}]<1+n$ and $\dim\mathbb{Z}[X_0,\ldots,X_{n-1}]<2+n$, where $K$ is a discrete field.

Equations

$${\omega }^{n-1}\cdot a_{n-1}+\cdots +{\omega }^1\cdot a_1+{\omega }^0\cdot a_0(n\in \mathbb{N},a_0,\dots ,a_{n-1}\in \mathbb{N},a_{n-1}\ge 1).$$

$$[f({\alpha }_0),\dots ,f({\alpha }_{n-1}),f(\beta ),f({\alpha }_{n+1}),\dots ,f({\alpha }_{n+m})]$$

$$x_0^{e_0}\cdots x_{n-1}^{e_{n-1}}\in ⟨x_0^{e_0+1},x_0^{e_0}{x}_1^{e_1+1},\dots ,x_0^{e_0}\cdots x_{n-2}^{e_{n-2}}{x}_{n-1}^{e_{n-1}+1}⟩.$$

$$({\alpha }_1,{\beta }_1)\prec ({\alpha }_0,{\beta }_0):\equiv ({\alpha }_1<{\alpha }_0)\vee ({\beta }_1<{\beta }_0).$$

$$\{\prec x\}:=\{y\in \alpha \times \beta :y\prec x\}.$$

$$\{\prec S\}:=\bigcap _{x\in S}\{\prec x\}.$$

$$S<T:\equiv \{\prec S\}⊊\{\prec T\}.$$

$${\lambda }_M(N):=\sup \{{\lambda }_M(L)+1:N⪇L\le M\}.$$

Full text

1. Introduction

In this paper, all rings are assumed to have an identity, and the term “module” refers to a left module. In constructive arguments, an ordinal means a Cantor normal form (i.e., an ordinal less than $\varepsilon_{0}$). See [CC06, Gri13, NFXG20, KNFX21, KNFX23] for type-theoretic treatments of Cantor normal forms. In fact, we only need ordinals less than $\omega^{\omega}$ to obtain results on the Krull dimension, and such ordinals can be expressed as

[TABLE]

Hilbert’s basis theorem is an important topic in constructive algebra. In exploring constructive versions of Hilbert’s basis theorem, several definitions of Noetherian rings have been considered [BSB23], including Richman–Seidenberg Noetherian rings [Ric74, Sei74, MRR88]. Among them, Jacobsson and Löfwall’s one [JL91, Definition 3.4] and Coquand and Persson’s one [CP99, Section 3.1] are (generalized) inductive definitions.

In this paper, we quantify the inductive definition and define $\alpha$-Noetherian rings for an ordinal $\alpha$. Then we constructively prove a quantitative version of Hilbert’s basis theorem and present an application to the Krull dimension of polynomial rings.

In Section 2, based on the inductive definitions of Noetherianity [JL91, CP99], we define the notion of $\alpha$-Noetherian modules and $\alpha$-Noetherian rings for an ordinal $\alpha$. Every discrete field is $1$-Noetherian, and $\mathbb{Z}$ is $\omega$-Noetherian. If a commutative ring $A$ is $\alpha$-Noetherian for some $\alpha<\omega^{n}$, then $\operatorname{\mathsf{Kdim}}A<n$ holds (Theorem 2.13).

In Section 3, we prove a quantitative version of Hilbert’s basis theorem (Theorem 3.7): if a ring $A$ is $\alpha$-Noetherian, then $A[X]$ is $(\omega\otimes\alpha)$-Noetherian, where $\otimes$ denotes the Hessenberg natural product. This gives a new constructive proof of $\operatorname{\mathsf{Kdim}}K[X_{1},\ldots,X_{n}]<1+n$ and $\operatorname{\mathsf{Kdim}}\mathbb{Z}[X_{1},\ldots,X_{n}]<2+n$, where $K$ is a discrete field.

In classical mathematics, our main theorems have already been proved. The notion of $\alpha$-Noetherian rings is essentially introduced by Gulliksen [Gul73] and developed by Brookfield [Bro02] in the form of the length $l(M)$ of a Noetherian module $M$. In fact, a module $M$ is $\alpha$-Noetherian if and only if $M$ is Noetherian and $l(M)\leq\alpha$ (Theorem 4.8). For every Noetherian ring $A$, Brookfield [Bro03, Theorem 3.1] has proved that $l(A[X])=\omega\otimes l(A)$. As noted in [Bro03], when $A$ is Noetherian, Brookfield’s theorem implies $\operatorname{\mathsf{Kdim}}A[X]=\operatorname{\mathsf{Kdim}}A+1$ since $l(A)<\omega^{n}$ is equivalent to $\operatorname{\mathsf{Kdim}}A<n$ [Gul73, Theorem 2.3].

2. $\alpha$-Noetherian rings

We first introduce some notation. Let $[\alpha,\beta]:=\{\gamma:\alpha\leq\gamma\leq\beta\}$, $[\alpha,\beta):=\{\gamma:\alpha\leq\gamma<\beta\}$, and $(\alpha,\beta]:=\{\gamma:\alpha<\gamma\leq\beta\}$. Let $\operatorname{\mathsf{List}}S$ denote the set of finite lists of elements of a set $S$. We may sometimes write a list $[x_{0},\ldots,x_{n-1}]\in\operatorname{\mathsf{List}}S$ as $[x_{0},\ldots,x_{n-1}]_{S}$. The expression $[]$ denotes the empty list. For $\sigma=[x_{0},\ldots,x_{n-1}]_{S}$ and $x\in S$, let $\sigma.x:=[x_{0},\ldots,x_{n-1},x]_{S}$. For a module $M$ over a ring $A$, let $\langle{x_{0},\ldots,x_{n-1}}\rangle$ denote the submodule of $M$ generated by $x_{0},\ldots,x_{n-1}\in M$. Let $\langle{[x_{0},\ldots,x_{n-1}]_{M}}\rangle:=\langle{x_{0},\ldots,x_{n-1}}\rangle$.

We define $\alpha$-good lists and $\alpha$-Noetherian rings for an ordinal $\alpha$.

Definition 2.1**.**

Let $M$ be a module over a ring $A$ and $\alpha$ be an ordinal.

1. (1)

A list $[x_{0},\ldots,x_{n-1}]_{M}$ is called $(-1)$-good (or simply good), if $n\geq 1$ and $x_{n-1}\in\langle{x_{0},\ldots,x_{n-2}}\rangle$. Note that this definition is different from the definition of a good list in [CP99, Section 3.1]. 2. (2)

A list $\sigma\in\operatorname{\mathsf{List}}M$ is called $\alpha$-good if for every $x\in M$, there exists $\beta\in[-1,\alpha)$ such that $\sigma.x$ is $\beta$-good. 3. (3)

A module $M$ is called $\alpha$-Noetherian if $[]_{M}$ is $\alpha$-good. A ring $A$ is called (left) $\alpha$-Noetherian if it is $\alpha$-Noetherian as a left $A$-module.

Remark 2.2**.**

The above definition of $\alpha$-Noetherian modules is a quantitative version of the following generalized inductive definition of Noetherian modules:

1. (1)

A list $[x_{0},\ldots,x_{n-1}]_{M}$ is called good if $n\geq 1$ and $x_{n-1}\in\langle{x_{0},\ldots,x_{n-2}}\rangle$. 2. (2)

We inductively generate the predicate “good bars $\sigma$” by the following constructors:

1. (a)

If $\sigma$ is good, then good bars $\sigma$. 2. (b)

If good bars $\sigma.x$ for every $x$, then good bars $\sigma$. 3. (3)

A module $M$ is called Noetherian if good bars $[]\in\operatorname{\mathsf{List}}M$.

Inductive definitions of Noetherian rings have been introduced by Jacobsson, Löfwall [JL91, Definition 3.4], Coquand, and Persson [CP99, Section 3.1]. Although the above inductive definition is similar to these, it is different from the definition in [JL91] because the above definition does not contain negation, and it is also different from the one in [CP99] (at least on the surface) because the above definition uses a stronger notion of goodness. We do not know whether the above definition of Noetherian modules is equivalent to the one in [CP99].

Remark 2.3**.**

We also have the following alternative definition of $\alpha$-Noetherian modules.

1. (1)

A finitely generated submodule $N$ of $M$ is $\alpha$-blocked if for every $x\in M$,

1. (a)

$x\in N$, or 2. (b)

there exists $\beta\in[0,\alpha)$ such that $N+\langle{x}\rangle$ is $\beta$-blocked. 2. (2)

A module $M$ is called $\alpha$-Noetherian if $0\subseteq M$ is $\alpha$-blocked.

The above definition of $\alpha$-blocked module is a quantitative version of the following modified negation-free definition of the blocked modules [JL91, Definition 3.1]:

• •

A finitely generated submodule $N$ of $M$ is blocked if for every $x\in M$,

1. (1)

$x\in N$ or 2. (2)

there exists $\beta\in[0,\alpha)$ such that $N+\langle{x}\rangle$ is blocked.

Example 2.4**.**

Let $K$ be a discrete field.

1. (1)

A ring is [math]-Noetherian if and only if it is trivial. 2. (2)

A ring is $1$-Noetherian if and only if it is a discrete field. 3. (3)

Let $n\in\mathbb{N}$. The rings $\mathbb{Z}/\langle{2^{n}}\rangle$ and $K[X]/\langle{X^{n}}\rangle$ are $n$-Noetherian. 4. (4)

The rings $\mathbb{Z}$ and $K[X]$ are $\omega$-Noetherian.

More generally, we can define $\alpha$-Euclidean rings and prove that they are $\alpha$-Noetherian.

Definition 2.5**.**

Let $M$ be a module over a ring $A$ and $\alpha$ be an ordinal.

1. (1)

An element $x\in M$ is called $(-1)$-Euclidean if $x=0$. 2. (2)

An element $x\in M$ is called $\alpha$-Euclidean if for every $y\in M$, there exist $\beta\in[-1,\alpha)$ and $\beta$-Euclidean element $z\in M$ such that $z-y\in\langle{x}\rangle$. 3. (3)

A module $M$ is called $\alpha$-Euclidean if for every $x\in M$, there exists $\beta\in[-1,\alpha)$ such that $x$ is $\beta$-Euclidean. A ring $A$ is called (left) $\alpha$-Euclidean if it is $\alpha$-Euclidean as a left $A$-module.

Remark 2.6**.**

In classical mathematics, Motzkin [Mot49, Section 2] has introduced a transfinite version of the Euclidean ring, and it has been studied by several authors [Fle71, Sam71, Hib75, Hib77, Nag78, Nag85, Cla15, CNT19]. Non-commutative Euclidean rings are studied in [Ore33, Coh61, Bru73]. Euclidean modules are studied in [Len74, Rah02, LC14]. We note that Lenstra [Len74] has treated all three generalizations of Euclidean rings.

Example 2.7**.**

Let $K$ be a discrete field.

1. (1)

A ring is [math]-Euclidean if and only if it is a trivial ring. 2. (2)

A ring is $1$-Euclidean if and only if it is a discrete field. 3. (3)

Let $n\in\mathbb{N}$. The rings $\mathbb{Z}/\langle{2^{n}}\rangle$ and $K[X]/\langle{X^{n}}\rangle$ are $n$-Euclidean. 4. (4)

The rings $\mathbb{Z}$ and $K[X]$ are $\omega$-Euclidean.

We use the following lemma to prove that every $\alpha$-Euclidean module is $\alpha$-Noetherian.

Lemma 2.8**.**

Let $M$ be a module over a ring $A$, $\alpha$ be an ordinal, and $\sigma\in\operatorname{\mathsf{List}}M$. If $\langle{\sigma}\rangle$ contains an $\alpha$-Euclidean element $x$, then $\sigma$ is $\alpha$-good.

Proof.

We prove this by induction on $\alpha$.

• •

Let $y\in M$. Since $x\in\langle{\sigma}\rangle$ is $\alpha$-Euclidean, there exists $\beta\in[-1,\alpha)$ and a $\beta$-Euclidean element $z\in M$ such that $z-y\in\langle{\sigma}\rangle$.

1. (1)

If $\beta=-1$, then $z=0$. Hence $y\in\langle{\sigma}\rangle$, and $\sigma.y$ is good. 2. (2)

If $\beta\in[0,\alpha)$, then $z\in\langle{\sigma.y}\rangle$. Hence $\sigma.y$ is $\beta$-good by the inductive hypothesis.

Hence $\sigma$ is $\alpha$-good. ∎

Theorem 2.9** (Classically proved in [Cla15, Theorem 3.17]).**

Let $\alpha$ be an ordinal and $M$ be a module over a ring $A$. If $M$ is an $\alpha$-Euclidean module over a ring $A$, then $M$ is $\alpha$-Noetherian.

Proof.

Let $x\in M$. Then, there exists $\beta\in[-1,\alpha)$ such that $x$ is $\beta$-Euclidean.

1. (1)

If $\beta=-1$, then $x=0$. Hence $[x]$ is good. 2. (2)

If $\beta\in[0,\alpha)$, then $[x]$ is $\beta$-good by Lemma 2.8.

Hence $[]_{M}$ is $\alpha$-good. ∎

We next prove that a sequence indexed by $[0,\alpha]$ in an $\alpha$-Noetherian module contains a reversed good subsequence.

Lemma 2.10**.**

Let $M$ be a module over a ring $A$, $\alpha$ be an ordinal, and $f:[0,\alpha)\to M$ be a function. Let $\beta\in[-1,\alpha)$. If there exist $n\in\mathbb{N}$ and a strictly decreasing sequence $\alpha_{0},\ldots,\alpha_{n-1}\in(\beta,\alpha]$ such that $[f(\alpha_{0}),\ldots,f(\alpha_{n-1})]$ is $\beta$-good, then there exist $m\in\mathbb{N}$ and a strictly decreasing sequence $\alpha_{n},\ldots,\alpha_{n+m-1}\in[0,\alpha_{n-1})$ such that $[f(\alpha_{0}),\ldots,f(\alpha_{n+m-1})]$ is good.

Proof.

We prove this by induction on $\beta$.

1. (1)

If $\beta=-1$, then $[f(\alpha_{0}),\ldots,f(\alpha_{n-1})]$ is good. 2. (2)

Let $\beta\in[0,\alpha)$. Since $[f(\alpha_{0}),\ldots,f(\alpha_{n-1})]$ is $\beta$-good, there exists $\beta^{\prime}\in[-1,\beta)$ such that $[f(\alpha_{1}),\ldots,f(\alpha_{n-1}),f(\beta)]$ is $\beta^{\prime}$-good. By the inductive hypothesis, there exist $m\in\mathbb{N}$ and a strictly decreasing sequence $\alpha_{n+1},\ldots,\alpha_{n+m}\in[0,\beta)$ such that

[TABLE]

is good.∎

Theorem 2.11**.**

Let $M$ be a module over a ring $A$, $\alpha$ be an ordinal, $f:[0,\alpha)\to M$ be a function, and $\beta\in[0,\alpha)$. If $M$ is $\beta$-Noetherian, then there exist $m\in\mathbb{N}$ and a strictly decreasing sequence $\alpha_{0},\ldots,\alpha_{m-1}\in[0,\alpha)$ such that $[f(\alpha_{0}),\ldots,f(\alpha_{m-1})]$ is good.

Proof.

Let $n:=0$ in Lemma 2.10. ∎

We recall the following elementary characterization of the Krull dimension by Lombardi [Lom02, Définition 5.1]. See [Lom23, Note historique] for the background of the constructive definition of the Krull dimension.

Definition 2.12**.**

Let $n\in\mathbb{N}$. A ring $A$ is of Krull dimension less than $n$ if for every $x_{0},\ldots,x_{n-1}\in A$, there exists $e_{0},\ldots,e_{n-1}\geq 0$ such that

[TABLE]

Let $\operatorname{\mathsf{Kdim}}A<n$ denote the statement that $A$ is of Krull dimension less than $n$.

The following relation between the notion of $\alpha$-Noetherian rings and the Krull dimension easily follows from Theorem 2.11:

Theorem 2.13** (Classically proved in [Gul73, Theorem 2.3]).**

Let $n\in\mathbb{N}$ and $A$ be a commutative ring. If $A$ is $\alpha$-Noetherian for some $\alpha<\omega^{n}$, then $\operatorname{\mathsf{Kdim}}A<n$.

Proof.

Let $x_{0},\ldots,x_{n-1}\in A$. Define $f:\omega^{n}\to A$ by $f(e_{n-1},\ldots,e_{1},e_{0}):=x_{0}^{e_{0}}\cdots x_{n-1}^{e_{n-1}}$. We put the anti-lexicographic order on $\omega^{n}$ and identify it with $[0,\omega^{n})$. By Theorem 2.11, there exist $m\in\mathbb{N}$ and a strictly decreasing sequence $\alpha_{0},\ldots,\alpha_{m-1}\in[0,\omega^{n})$ such that $[f(\alpha_{0}),\ldots,f(\alpha_{m-1})]$ is good. Hence $\operatorname{\mathsf{Kdim}}A<n$. ∎

Example 2.14**.**

Since $\mathbb{Z}$ is $\omega$-Noetherian, every sequence $a_{0},a_{1},\ldots,a_{\omega}\in\mathbb{Z}$ has a reversed good subsequence. In particular, $x^{0},x^{1},\ldots,y\in\mathbb{Z}$ has a reversed good subsequence for every $x,y\in\mathbb{Z}$. This implies $\operatorname{\mathsf{Kdim}}\mathbb{Z}<2$.

3. The quantitative Hilbert’s basis theorem

In this section, we will prove the following quantitative version of Hilbert’s basis theorem:

• •

If a module $M$ over a ring $A$ is $\alpha$-Noetherian, then the $A[X]$-module $M[X]$ is $(\omega\otimes\alpha)$-Noetherian, where $\otimes$ denotes the Hessenberg natural product.

We use some basic facts about transfinite chomp described in [HS02].

Definition 3.1**.**

A set $S$ is called finite if there exist $n\in\mathbb{N}$ and a surjection from $\{0,\ldots,n-1\}$ to $S$. Let $\operatorname{\mathsf{Fin}}S$ denote the set of all finite subsets of a set $S$.

Definition 3.2**.**

Let $\alpha,\beta$ be ordinals. We define a binary relation $\prec$ on $\alpha\times\beta$ by

[TABLE]

For $x\in\alpha\times\beta$, we define a detachable subset $\{\prec x\}\subseteq\alpha\times\beta$ by

[TABLE]

For $S\in\operatorname{\mathsf{Fin}}(\alpha\times\beta)$, let

[TABLE]

We define a decidable binary relation $<$ on $\operatorname{\mathsf{Fin}}(\alpha\times\beta)$ by

[TABLE]

We can regard an element $S\in\operatorname{\mathsf{Fin}}(\alpha\times\beta)$ as the position $\{\prec S\}$ of $(\alpha\times\beta)$-chomp. A function $\operatorname{\mathsf{size}}:\operatorname{\mathsf{Fin}}(\omega\times\alpha)\to[0,\omega\otimes\alpha]$ is defined in [HS02, Section 2]. It satisfies the following conditions:

1. (1)

$\operatorname{\mathsf{size}}(\emptyset)=\omega\otimes\alpha$. 2. (2)

If $S<T$, then $\operatorname{\mathsf{size}}S<\operatorname{\mathsf{size}}T$.

Definition 3.3**.**

Let $M$ be a module over a ring $A$. Let $M[X]=\{x_{0}+\cdots+x_{d-1}X^{d-1}:x_{0},\ldots,x_{d-1}\in M\}$ denote the polynomial module regarded as an $A[X]$-module. We regard a list $[x_{0},\ldots,x_{d-1}]\in\operatorname{\mathsf{List}}M$ as a polynomial $x_{0}+\cdots+x_{d-1}X^{d-1}\in M[X]$. Let $\deg{[x_{0},\ldots,x_{d-1}]}:=d-1$. If $d\geq 1$, let $\operatorname{lc}{[x_{0},\ldots,x_{d-1}]}:=x_{d-1}$.

Definition 3.4**.**

Let $\alpha$ be an ordinal and $M$ be a module over a ring $A$. Let $\sigma:=[f_{0},\ldots,f_{n-1}]\in\operatorname{\mathsf{List}}(\operatorname{\mathsf{List}}M)$. We say that $S\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ describes $\sigma$ if for every $(d,\alpha^{\prime})\in S$, there exist $l\in\mathbb{N}$ and $g_{0},\ldots,g_{l-1}\in\operatorname{\mathsf{List}}M$ such that

1. (1)

$g_{0},\ldots,g_{l-1}\in\langle{\sigma}\rangle_{M[X]}$, 2. (2)

$\deg g_{0},\ldots,\deg g_{l-1}\leq d$, and 3. (3)

$[\operatorname{lc}g_{0},\ldots,\operatorname{lc}g_{l-1}]_{M}$ is $\alpha^{\prime}$-good.

Lemma 3.5**.**

Let $\alpha$ be an ordinal and $M$ be an $\alpha$-Noetherian module over a ring $A$. Let $n\in\mathbb{N}$, $f_{0},\ldots,f_{n-1}\in\operatorname{\mathsf{List}}M$, and $S:=\{(d_{0},\alpha_{0}),\ldots,(d_{m-1},\alpha_{m-1})\}\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ be an element that describes $\sigma:=[f_{0},\ldots,f_{n-1}]$. Then, for every $f\in\operatorname{\mathsf{List}}M$,

1. (1)

$\sigma.f\in\operatorname{\mathsf{List}}M[X]$* is good, or* 2. (2)

there exists $S^{\prime}\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ such that $S^{\prime}$ describes $\sigma.f$ and $S^{\prime}<S$.

Proof.

We prove this by induction on $\deg f$.

1. (1)

If $\deg f=-1$, then $f=_{M[X]}0$ and $\sigma.f$ is good. 2. (2)

If $\deg f\geq 0$, let $\alpha^{\prime}:=\min\{\gamma\in\{\alpha,\alpha_{0},\ldots,\alpha_{m-1}\}:(\deg f,\gamma)\notin\{\prec S\}\}$. Then, there exist $l\in\mathbb{N}$ and $g_{0},\ldots,g_{l-1}\in\operatorname{\mathsf{List}}M$ such that

1. (a)

$g_{0},\ldots,g_{l-1}\in\langle{\sigma}\rangle_{M[X]}$, 2. (b)

$\deg g_{0},\ldots,\deg g_{l-1}\leq\deg f$, and 3. (c)

$[\operatorname{lc}g_{0},\ldots,\operatorname{lc}g_{l-1}]_{M}$ is $\alpha^{\prime}$-good.

Hence there exists $\beta\in[-1,\alpha^{\prime})$ such that $[\operatorname{lc}g_{0},\ldots,\operatorname{lc}g_{l-1},\operatorname{lc}f]\in\operatorname{\mathsf{List}}M$ is $\beta$-good.

1. (a)

If $\beta=-1$, then $[\operatorname{lc}g_{0},\ldots,\operatorname{lc}g_{l-1},\operatorname{lc}f]_{M}$ is good. Hence there exists $g\in\operatorname{\mathsf{List}}M$ such that $\deg g=\deg f-1$ and $g-f\in\langle{g_{0},\ldots,g_{l-1}}\rangle\subseteq\langle{\sigma}\rangle$. By the inductive hypothesis,

1. (i)

$\sigma.g\in\operatorname{\mathsf{List}}M[X]$ is good, or 2. (ii)

there exists $S^{\prime}\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ such that $S^{\prime}$ describes $\sigma.g$ and $S^{\prime}<S$.

If (i) holds, then $\sigma.f$ is good. If (ii) holds, then $S^{\prime}$ describes $\sigma.f$, and $S^{\prime}<S$. 2. (b)

If $\beta\in[0,\alpha^{\prime})$, then let $S^{\prime}:=S\cup\{(\deg f,\beta)\}$. Then $S^{\prime}$ describes $\sigma.f$, and $S^{\prime}<S$.∎

Lemma 3.6**.**

Let $\alpha$ be an ordinal and $M$ be an $\alpha$-Noetherian module over a ring $A$. Let $n\in\mathbb{N}$, $f_{0},\ldots,f_{n-1}\in\operatorname{\mathsf{List}}M$, and $S:=\{(d_{0},\alpha_{0}),\ldots,(d_{m-1},\alpha_{m-1})\}\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ be an element which describes $\sigma:=[f_{0},\ldots,f_{n-1}]$. Then, $\sigma\in\operatorname{\mathsf{List}}M[X]$ is $(\operatorname{\mathsf{size}}S)$-good.

Proof.

Let $f\in\operatorname{\mathsf{List}}M$. By induction on $\operatorname{\mathsf{size}}S$, we prove that there exists $\beta\in[-1,\operatorname{\mathsf{size}}S)$ such that $\sigma.f\in\operatorname{\mathsf{List}}M[X]$ is $\beta$-good. By Lemma 3.5,

1. (1)

$\sigma.f\in\operatorname{\mathsf{List}}M[X]$ is good, or 2. (2)

there exists $S^{\prime}\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ such that $S^{\prime}$ describes $\sigma.f$ and $S^{\prime}<S$.

If (1) holds, then $\sigma.f$ is $(-1)$-good. If (2) holds, then $\operatorname{\mathsf{size}}S^{\prime}<\operatorname{\mathsf{size}}S$, and $\sigma.f$ is $(\operatorname{\mathsf{size}}S^{\prime})$-good by the inductive hypothesis. Hence there exists $\beta\in[-1,\operatorname{\mathsf{size}}S)$ such that $\sigma.f$ is $\beta$-good.

Hence $\sigma$ is $(\operatorname{\mathsf{size}}S)$-good. ∎

Theorem 3.7**.**

Let $\alpha$ be an ordinal and $M$ be an $\alpha$-Noetherian module over a ring $A$. Then $M[X]$ is an $(\omega\otimes\alpha)$-Noetherian $A[X]$-module.

Proof.

Since $\emptyset\in\operatorname{\mathsf{Fin}}(\omega\times\alpha)$ describes $[]\in\operatorname{\mathsf{List}}(\operatorname{\mathsf{List}}M)$, the list $[]\in\operatorname{\mathsf{List}}(M[X])$ is $\operatorname{\mathsf{size}}(\emptyset)$-good. Since $\operatorname{\mathsf{size}}(\emptyset)=\omega\otimes\alpha$, the module $M[X]$ is $(\omega\otimes\alpha)$-Noetherian. ∎

The following corollary follows from Theorem 3.7 and the definition of $\alpha$-Noetherian rings:

Corollary 3.8** (Classically proved in [Bro03, Theorem 3.1]).**

If $A$ is an $\alpha$-Noetherian ring, then the ring $A[X]$ is $(\omega\otimes\alpha)$-Noetherian.

By Example 2.4, we obtain a new proof of the following well-known constructive results on the Krull dimension:

Example 3.9**.**

1. (1)

If $K$ is a discrete field, then $K[X_{1},\ldots,X_{n}]$ is $\omega^{n}$-Noetherian. In particular, we have $\operatorname{\mathsf{Kdim}}K[X_{1},\ldots,X_{n}]<1+n$. This bound on the Krull dimension is constructively proved in [CL05, Corollary 4] and [LQ15, Theorem XIII-5.1]. 2. (2)

The ring $\mathbb{Z}[X_{1},\ldots,X_{n}]$ is $\omega^{1+n}$-Noetherian. In particular, we have $\operatorname{\mathsf{Kdim}}\mathbb{Z}[X_{1},\ldots,X_{n}]<2+n$. This bound on the Krull dimension is constructively proved in [LQ15, Theorem XIII-8.20]

4. Length of Noetherian modules

In this section, we reason in ZFC. We prove that the notion of $\alpha$-Noetherian ring can be written in terms of the length of Noetherian modules defined by Gulliksen [Gul73]. First, we recall the definition of the length.

Definition 4.1**.**

Let $M$ be a Noetherian module over a ring $A$. For a submodule $N\leq M$, we inductively define an ordinal $\lambda_{M}(N)$ by

[TABLE]

The ordinal $l(M):=\lambda_{M}(0)$ is called the length of $M$.

Lemma 4.2**.**

Let $\alpha$ be an ordinal, $M$ be a module over a ring $A$, and $M_{n}$ $(n\in\mathbb{N})$ be an ascending chain of submodules of $M$. If there exists an $\alpha$-good list $\sigma\in\operatorname{\mathsf{List}}M$ such that $\langle{\sigma}\rangle\subseteq M_{0}$, then there exists $n\in\mathbb{N}$ such that $M_{n}=M_{n+1}$.

Proof.

We prove this by induction on $\alpha$.

1. (1)

If $\alpha=0$, then $M_{0}=M_{1}$. 2. (2)

Let $\alpha>0$. We have $M_{0}=M_{1}$ or $M_{0}\subsetneq M_{1}$.

• •

If $M_{0}\subsetneq M_{1}$, then there exists $x\in M_{1}$ such that $x\notin M_{0}$. Since $\sigma$ is $\alpha$-good, there exists $\beta\in[-1,\alpha)$ such that $\sigma.x$ is $\beta$-good. Since $x\notin M_{0}$, we have $x\notin\langle{\sigma}\rangle$. Hence $\beta\neq-1$. We have $\langle{\sigma.x}\rangle\subseteq M_{1}$. Hence, by the inductive hypothesis, there exists $n\geq 1$ such that $M_{n}=M_{n+1}$.

Hence there exists $n\in\mathbb{N}$ such that $M_{n}=M_{n+1}$.∎

Proposition 4.3**.**

Let $\alpha$ be an ordinal, and $M$ be an $\alpha$-Noetherian module over a ring $A$. Then $M$ is Noetherian.

Proof.

Let $\sigma:=[]$ in Lemma 4.2. ∎

Lemma 4.4**.**

Let $\alpha$ be an ordinal, $M$ be an $\alpha$-Noetherian module over a ring $A$, and $N$ be a submodule of $M$. If there exists an $\alpha$-good list $\sigma\in\operatorname{\mathsf{List}}M$ such that $\langle{\sigma}\rangle\subseteq N$, then $\lambda_{M}(N)\leq\alpha$.

Proof.

We prove this by induction on $\alpha$.

• •

Let $L\leq M$ be a submodule such that $N\lneq L$. Then, there exists $x\in L$ such that $x\notin N$. Since $\sigma$ is $\alpha$-good, there exists $\beta\in[-1,\alpha)$ such that $\sigma.x$ is $\beta$-good. Since $x\notin N$, We have $\beta\neq-1$. Hence, by the inductive hypothesis, $\lambda_{M}(L)\leq\beta$. Hence $\lambda_{M}(L)+1\leq\alpha$.

Hence $\lambda_{M}(N)\leq\alpha$. ∎

Proposition 4.5**.**

Let $\alpha$ be an ordinal, and $M$ be an $\alpha$-Noetherian module over a ring $A$. Then $l(M)\leq\alpha$.

Proof.

Let $N:=0$ in Lemma 4.4. ∎

Lemma 4.6**.**

Let $M$ be a Noetherian module over a ring $A$, and $\sigma\in\operatorname{\mathsf{List}}M$. Then, $\sigma$ is $\lambda_{M}(\langle{\sigma}\rangle)$-good.

Proof.

We prove this by induction on $\lambda_{M}(\langle{\sigma}\rangle)$.

• •

Let $x\in M$.

1. (1)

If $x\in\langle{\sigma}\rangle$, then $\sigma.x$ is good. 2. (2)

If $x\notin\langle{\sigma}\rangle$, then $\lambda_{M}(\langle{\sigma.x}\rangle)+1\leq\lambda_{M}(\langle{\sigma}\rangle)$. Hence, by the inductive hypothesis, $\sigma.x$ is $\lambda_{M}(\langle{\sigma.x}\rangle)$-good.

Hence $\sigma$ is $\lambda_{M}(\langle{\sigma}\rangle)$-good. ∎

Proposition 4.7**.**

Let $M$ be a Noetherian module over a ring $A$. Then, $M$ is $l(M)$-Noetherian.

Proof.

Let $\sigma:=[]$ in Lemma 4.6. ∎

Proposition 4.3, Proposition 4.5, and Proposition 4.7 together imply the following theorem.

Theorem 4.8**.**

Let $\alpha$ be an ordinal, and $M$ be a module over a ring $A$. Then $M$ is $\alpha$-Noetherian if and only if $M$ is Noetherian and $l(M)\leq\alpha$.

Acknowledgments

The author would like to express his deepest gratitude to his supervisor, Ryu Hasegawa, for his support. The author would like to thank Thierry Coquand for his helpful advice. The author would also like to thank Yuto Arai, Ryuya Hora, Sangwoo Kim, Koki Kurahashi, Yuto Ikeda, Hiromasa Kondo, Haruki Toyota, and Minoru Sekiyama for their helpful comments in the graduate seminar.

This research was supported by Forefront Physics and Mathematics Program to Drive Transformation (FoPM), a World-leading Innovative Graduate Study (WINGS) Program, the University of Tokyo.