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

TL;DR

This paper develops constructive versions of Krull's dimension theory for rings and lattices, providing explicit computational content for classical theorems like Going Up and Going Down, advancing Hilbert's program in algebra.

Contribution

It introduces constructive frameworks for classical dimension theory, enabling explicit computation and element existence proofs in commutative algebra.

Findings

Constructive versions of Krull's dimension theory established.

Classical theorems like Going Up and Going Down are reformulated constructively.

Provides computational content and element existence proofs in algebraic structures.

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.