For a commutative ring $R$, consider $R[[t]]$-modules $$t^k R[[t]]^n \subset M \subset t^{-k} R[[t]]^n \subset R((t))^n.$$ It is known that if $t^{-k} R[[t]]^n / M$ is finitely generated projective $R$-module, then $M$ is finitely generated projective $R[[t]]$-module.
One line of proof, as found in http://web.stanford.edu/~tonyfeng/Zhu.pdf and http://www.math.harvard.edu/~gaitsgde/grad_2009/SeminarNotes/Oct13(AffGr).pdf, reduces to a Noetherian $R$, and then to the global situation (basically, replacing power series by polynomials).
Another line of proof is in the chapter "Affine Springer Fibers and Affine Deligne–Lusztig Varieties" by Ulrich Gortz (lemam 2.11).
The problem with the second line is that it is sketchy (for example, I think that it might actually use Noetherness of $R$ when formalized). So, my question is, do you know, or have a reference, to a proof of that fact, which is not along the first line above?
Thank you, Sasha
