AN ELEMENTARY CHARACTERIZATION OF KRULL DIMENSION
This chapter contributes to the new direction in constructive algebra originated by Coquand, Lombardi, and others, which aims at a partial realisation of Hilbert's programme. The idea is to prove that theorems in commutative algebra constructively, and at the same low type level at which they can be formulated. To this end, the chapter needs to reduce the complexity of some concepts, in the present case that of Krull dimension of a commutative ring. Although the traditional definition of it seems quite intuitive, it requires quantifying over all prime ideals of the given ring. To circumvent this problem the chapter gives an inductive characterization of Krull dimension, without primes, which carries over to this setting the inductive concept of dimension going back to Brouwer, Menger, and Urysohn. This follows the geometrical intuition that an algebraic variety is of dimension ≤ k if and only if each subvariety has a boundary of dimension < k.
Oxford Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.
If you think you should have access to this title, please contact your librarian.