Hidden constructions in abstract algebra,
Krull Dimension, Going Up, Going Down

Technical report. H. Lombardi, T. Coquand (2001)
fichier pdf, fichier dvi, fichier ps.
Version française en pdf

Abstract :
We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors.
We show that this gives a constructive version of basic classical theorems (dimension of finitely presented algebras, Going up and Going down theorem, ...), and hence that we get an explicit computational content where these abstract results are used to show the existence of concrete elements.
This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.

Key words :
Krull dimension, Going Up, Going Down, Constructive Mathematics.


See also
Hidden constructions in abstract algebra (3) Krull dimension of distributive lattices and commutative rings.
Henri Lombardi, Thierry Coquand.
Commutative ring theory and applications. Eds: Fontana M., Kabbaj S.-E., Wiegand S. Lecture notes in pure and applied mathematics vol 131. M. Dekker.
Proceedings for the Fourth International Conference on Commutative Ring Theory and Applications held June 7 - 11 , 2001 in Fez, Morocco (2002) pp. 477-499.

Résumé :
Nous présentons des versions constructives de la théorie de la dimension de Krull des anneaux commutatifs et des treillis distributifs. Les fondements de ces versions constructives sont dues à Joyal, Español et aux auteurs. Nous obtenons un contenu calculatoire explicite pour des théorèmes classiques abstraits: dimension de Krull des algèbres de présentation finie, going up, going down etc.
Nous pouvons alors obtenir un contenu explicite lorsque des résultats abstraits concernant les dimensions sont utilisés pour prédire l'existence d'objets concrets.
Ceci peut être vu comme une réalisation partielle du programme de Hilbert pour l'algèbre commutative abstraite classique.