Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Valuative dimension, constructive points of view

Stefan Neuwirth, Henri Lombardi, Ihsen Yengui

TL;DR

The paper develops three constructive definitions of the valuative dimension for commutative rings within Bishop-style constructive mathematics: vdim, Vdim, and dimv. It introduces the minimal pp-closure to handle nonintegral rings, and uses both a valuative lattice approach and graded monomial orders to define and connect these notions. The central result proves the constructive equivalence of all three definitions, first in the integral case and then generally via the minimal pp-closure, thereby aligning the constructive framework with the classical theory while preserving computational content. This work leverages dynamical algebraic structures and the Zariski lattice to provide a computation-friendly foundation for valuative dimension, with potential impact on algorithmic algebra and Hilbert-type decision procedures in constructive settings.

Abstract

There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics.

Valuative dimension, constructive points of view

TL;DR

The paper develops three constructive definitions of the valuative dimension for commutative rings within Bishop-style constructive mathematics: vdim, Vdim, and dimv. It introduces the minimal pp-closure to handle nonintegral rings, and uses both a valuative lattice approach and graded monomial orders to define and connect these notions. The central result proves the constructive equivalence of all three definitions, first in the integral case and then generally via the minimal pp-closure, thereby aligning the constructive framework with the classical theory while preserving computational content. This work leverages dynamical algebraic structures and the Zariski lattice to provide a computation-friendly foundation for valuative dimension, with potential impact on algorithmic algebra and Hilbert-type decision procedures in constructive settings.

Abstract

There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics.
Paper Structure (20 sections, 20 theorems, 64 equations)

This paper contains 20 sections, 20 theorems, 64 equations.

Table of Contents

  1. Introduction
  2. Definition and characterisations of the valuative dimension in classical mathematics
  3. Basic constructive terminology
  4. Valuation rings
  5. Dimension of a distributive lattice
  6. Krull dimension of a commutative ring
  7. Dynamical algebraic structures
  8. Three constructive definitions of the valuative dimension
  9. Minimal pp-closure of a reduced ring
  10. First constructive approach to the valuative dimension: vdim
  11. Second approach: valuative lattice and valuative spectrum, Vdim
  12. Third approach: graded monomial order, dimv
  13. Constructive equivalence of the three constructive definitions
  14. vdim=dimv
  15. vdim=Vdim in the integral case
  16. ...and 5 more sections

Key Result

Theorem 1.1

Let $\mathbf{R}$ be a nontrivial commutative integral ring with $\mathbf{K}=\mathop{\mathrm{Frac}}\nolimits(\mathbf{R})$. The following properties are equivalent. Moreover, without supposing $\mathbf{R}$ to be integral, but supposing it to be nontrivial, Items thclassdimval1, thclassdimval3, and thclassdimval4 are still equivalent.

Theorems & Definitions (31)

  • Theorem 1.1
  • Lemma 1.2: pp-ring splitting lemma
  • Definition 1.3
  • Theorem 1.4: fundamental theorem of entailment relations, Lor1951CC00
  • Theorem 1.5: dimension of a distributive lattice, see CL2003Lom02Lom2020, CACM
  • Lemma 1.6
  • Proposition 1.7: Joyal's definition of the spectrum of a commutative ring
  • Lemma 2.1
  • Lemma 2.2
  • Lemma 2.3
  • ...and 21 more