A constructive comparison of the rings R(X) and R〈X〉 and application to the Lequain–Simis Induction Theorem

We constructively prove that for any ring R with Krull dimension ⩽d, the ring R〈X〉 locally behaves like the ring R(X) or a localization of a polynomial ring of type (S−1R)[X] with S a multiplicative subset of R such that the Krull dimension of S−1R is ⩽d−1. As an application, we give a simple and constructive proof of the Lequain–Simis Induction Theorem which is an important variation of the Quillen Induction Theorem.