# 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.

## Key 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.