Projective modules over polynomial rings: a constructive approach

We give a constructive proof of the fact that finitely generated projective modules over a polynomial ring with coefficients in a Prüfer domain R with Krull dimension ≤ 1 are extended from R . In particular, we obtain constructively that finitely generated projective R [ X 1 , …, X n ]‐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 [ X 1 , …, X n ], n ≥ 2, are extended from R if and only if this holds for n = 1, where R is an arithmetical ring with finite Krull dimension (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)