A constructive notion of codimension (Q2445023)

The general framework for this paper is a reformulation of Hilbert's program in commutative algebra using formal topology. A formal topology is defined to be a triple \((S,\triangleleft,\circ)\) with a cover relation \(\triangleleft\) that satisfies usual point-cover properties and the convergence operation \(\circ\) that has weakening, contraction and stability properties. The author gives a point-free and constructively meaningful characterization of the notion of codimension for ideals of a commutative ring, which, with classical logic and the axiom of choice is equivalent to the usual one. This characterization is based on notions from formal topology, and upon the elementary characterization of Krull dimension provided earlier by Coquand, Lombardi, and Roy. Among a number of results proved, the author uses this notion to give a constructive proof of Krull's principal ideal theorem: For a Noetherian ring \(A\) and \(x_1,\dots, x_n\in A\), Codim\((x_1,\dots,x_n)>n\longrightarrow 1\in(x_1,\dots,x_n)\).