A constructive notion of codimension

We give 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 customary 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 other things, we use this notion to prove Krullʼs principal ideal theorem in the context of constructive algebra.