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



A technical question about affine grassmanian
I am being told it is better not to leave answers in comments. So:


I think you can find more details in Martin Kreidl's thesis, available at [uni-due.de/~hx0051/Dissertation.pdf](http://uni-due.de/~hx0051/Dissertation.pdf).


