Projective modules over polynomial rings: a constructive approach

pdf file.
with Sami Barhoumi and Ihsen Yengui
Math. Nachrichten 320 (2009), 792-799.

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.