The famous Quillen-Suslin theorem (formerly known as Serre's problem/conjecture) states that every projective module over $k[x\_1,\dots, x\_n]$ is free for $k$ a field. Replacing $k$ by a more general ring, we get the Bass-Quillen conjecture:



> 
> Let $R$ be a regular ring and $P$ a projective module over $R[x\_1,\dots, x\_n]$, then $P \cong Q \otimes\_R R[x\_1,\dots, x\_n]$ for a projective $R$-module $Q$.
> 
> 
> 


This has been proven in many cases, for example for $R$ of Krull dimension $\leq 2$ or if $R$ is a localization of an affine $k$-algebra for $k$ a field.


Now one could put forward similar conjectures replacing polynomial variables by power or Laurent series variables:



> 
> (Power) Let $R$ be a regular ring and $P$ a projective module over $R[[x\_1,\dots, x\_n]]$, then $P \cong Q \otimes\_R R[[x\_1,\dots, x\_n]]$ for a projective $R$-module $Q$.
> 
> 
> (Laurent) Let $R$ be a regular ring and $P$ a projective module over $R((x\_1,\dots, x\_n))$, then $P \cong Q \otimes\_R R((x\_1,\dots, x\_n))$ for a projective $R$-module $Q$.
> 
> 
> 


If I understand the (affine) Horrocks Theorem correctly, then the Laurent series version of the conjecture actually implies the original Bass-Serre conjecture for a ring $R$ if $n=1$. Actually, Horrocks proves the Laurent series version for $R$ regular local either of dimension $\leq 1$ or of dimension $\leq 2$ and containing a field already in 1964. My question is now:



> 
> What is known about the power and Laurent series versions of the Bass-Quillen conjecture?
> 
> 
> 



An analogue of the Bass-Quillen conjecture with power or Laurent series
Here is an attempt at the power series question. One can easily reduce to the one variable case. So, I will attempt to prove that if $R$ is any Noetherian ring and $A=R[[x]]$ and $P$ a projective $A$-module, then $P\cong P/xP\otimes\_R A =P'$. First, note that if $K$ is any finitely generated $A$-module, then it is complete with respect to the $x$-adic topology and so if $K=xK$, then $K=0$. Since $P'$ is $A$-projective, we can lift the surjective map $P'\to P/xP$ to a map $P'\to P$ which is an isomorphism mod $x$. Then the cokernel $K$ of $P'\to P$ has the property $K/xK=0$ and thus $K=0$. So, $P'\to P$ is surjective and so it splits. If $C$ is its kernel, then $C/xC=0$ and so $C=0$. Thus the map $P'\to P$ is an isomorphism.


