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.