Lemma about completion

Thanks to Kestutis Cesnavicius

formal-spaces.tex

@@ -801,6 +801,37 @@ \section{Topological rings and modules}
 Then $b$ and $c$ are mutually inverse as they are on a dense subset.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-completion-adic-star}
+Let $R$ be a topological ring. Let $M$ be a topological $R$-module.
+Let $I \subset R$ be a finitely generated ideal. Assume $M$
+has an open submodule whose topology is $I$-adic. Then $M^\wedge$
+has an open submodule whose topology is $I$-adic and we have
+$M^\wedge/I^n M^\wedge = M/I^nM$ for all $n \geq 1$.
+\end{lemma}
+
+\begin{proof}
+Let $M' \subset M$ be an open submodule whose topology is $I$-adic.
+Then $\{I^nM'\}_{n \geq 1}$ is a fundamental system of open submodules
+of $M$. Thus $M^\wedge = \lim M/I^nM'$ contains
+$(M')^\wedge = \lim M'/I^nM'$
+as an open submodule and the topology on $(M')^\wedge$ is
+$I$-adic by Algebra, Lemma \ref{algebra-lemma-hathat-finitely-generated}.
+Since $I$ is finitely generated, $I^n$ is finitely generated,
+say by $f_1, \ldots, f_r$. Observe that the surjection
+$(f_1, \ldots, f_r) : M^{\oplus r} \to I^n M$ is continuous
+and open by our description of the topology on $M$ above.
+By Lemma \ref{lemma-ses} applied to this surjection and to the
+short exact sequence $0 \to I^nM \to M \to M/I^nM \to 0$
+we conclude that
+$$
+(f_1, \ldots, f_r) :
+(M^\wedge)^{\oplus r} \longrightarrow M^\wedge
+$$
+surjects onto the kernel of the surjection $M^\wedge \to M/I^nM$.
+Since $f_1, \ldots, f_r$ generate $I^n$ we conclude.
+\end{proof}
+
 \begin{definition}
 \label{definition-toplogy-tensor-product}
 Let $R$ be a topological ring. Let $M$ and $N$ be linearly