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 231. 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.
ps. pdf, dvi.

See also the technical report Krull dimension, Going Up, Going Down.

Citation of G. C. Rota given in this paper : Elementary though it has become after successive presentations and simplifications, the theory of distributive lattices is the ideal instance of a mathematical theory, where a syntax is specified together with a complete description of all models, and what is more, a table of semantic concepts and syntactic concepts is given, together with a translation algorithm between the two kinds of concepts. Such an algorithm is a ``completeness theorem''.
G. C. Rota : Indiscrete Thoughts. Birkhauser, 1995.

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 the notion of Krull dimension has an explicit computational content in the form of existence (or lack of existence) of some algebraic identities. We can then get an explicit computational content where abstract results about dimensions 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.

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 montrons que la notion de dimension de Krull a un contenu calculatoire explicite sous la forme de l'existence (ou de la non existence) de certaines identités algébriques.
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.