Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down
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, Espan\~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, \ldots), 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.
Cite
@article{arxiv.1712.04725,
title = {Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down},
author = {Thierry Coquand and Henri Lombardi},
journal= {arXiv preprint arXiv:1712.04725},
year = {2017}
}
Comments
Technical report, 2001. Gives constructive versions of relative Krull dimension, Going up and Going up, which are available for distributive lattices. Closely related paper: Hidden constructions in abstract algebra (3) Krull dimension of distributive lattices and commutative rings. In: Commutative ring theory and applications. LNPAM vol 231. M. Dekker. (2002) 477-499