Valuative dimension, constructive points of view.

H. Lombardi, S. Neuwirth and I. Yengui.
Valuative dimension, constructive points of view.
Journal of Algebra. 647, 206--229, (2024).
(hal-04274384)

Version bilingue de l'article publié en anglais.

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. To the contrary of the classical versions, the constructive versions have a clear computational content and can be used for the usual examples of commutative rings. 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.

Résumé :
Il existe plusieurs caractérisations de la dimension valuative d'un anneau commutatif. Des versions constructives de cette dimension ont été proposées, et démontrées équivalentes à la notion classique dans le cadre des mathématiques classiques. Contrairement aux version classiques, les versions constructives ont un contenu calculatoire clair et elles peuvent être utilisées dans les cas usuels d'anneaux commutatifs. Cet article étudie les relations en termes de calculs explicites entre trois définitions constructives qui ont été proposées. De cette manière ces trois versions sont prouvées équivalentes directement en mathématiques constructives.