The well-known classical theorem that an integral extension doesn’t change the Krull dimension is treated here from a constructive point of view. Although the Krull dimension Kdim A is not in general a well defined element of \(\mathbb N\cup\{\infty\}\), the sentence that ” Kdim A\(\leq d\)” is well defined and it so happens that most of the classical theorems regarding the Krull dimension are using statements of the latter kind. The authors’ starting point is a theorem that defines Krull dimension in several (constructive) ways, all equivalent to the classical definition, such as: Via induction using ideal boundary, induction using monoid boundary, iterated boundaries, and symmetric form. This is then followed by a number of (constructive) intermediate lemmas and the main results are thus proved constructively:
Theorem 3.4. If B is algebraic over A then KdimB\(\leq\) KdimA.
Corollary 3.5. If A\(\subseteq\)B is an integral extension, then KdimB=KdimA.