Abstract :
We give a constructive proof of the fact that finitely generated
projective modules over a polynomial ring with coefficients in a
Prüfer domain with Krull dimension 1 are extended
from R.
In particular, we obtain constructively that finitely
generated projective R[X1,...,Xn]-modules, where R is a
Bezout domain with Krull dimension 1, are free.
Our proof
is essentially based on a dynamical method for decreasing the
Krull dimension and a constructive rereading of the original proof
given by Maroscia and Brewer&Costa.
Moreover, we obtain a simple
constructive proof of a result due to Lequain and Simis stating
that finitely generated modules over R[X1,...,X_n] are extended from R
if and only if this holds for n=1,
where R is an arithmetical ring with finite Krull dimension.