Explain why maps are surjective

Often used statement: A ---> B map of Noetherian complete local
rings such that m_A B = m_B and iso on residue fields, then this
map is surjective.

algebra.tex

@@ -41624,16 +41624,18 @@ \section{The Cohen structure theorem}
 gives a map whose image is the desired coefficient ring.
 
 \medskip\noindent
-The final statement of the theorem is now clear. Namely, if
+The final statement of the theorem follows readily. Namely, if
 $y_1, \ldots, y_n$ are generators of the ideal $\mathfrak m$,
 then we can use the map $\Lambda \to R$ just constructed
 to get a map
 $$
 \Lambda[[x_1, \ldots, x_n]] \longrightarrow R,
 \quad x_i \longmapsto y_i.
 $$
-This map is surjective on each $R/\mathfrak m^n$ and hence
-is surjective as $R$ is complete. Some details omitted.
+Since both sides are $(x_1, \ldots, x_n)$-adically complete
+this map is surjective by Lemma \ref{lemma-completion-generalities}
+as it is surjective modulo $(x_1, \ldots, x_n)$ by
+construction.
 \end{proof}
 
 \begin{remark}
@@ -41657,26 +41659,25 @@ \section{The Cohen structure theorem}
 \item If $R$ contains either $\mathbf{F}_p$ or $\mathbf{Q}$, then $R$
 is isomorphic to a power series ring over its residue field.
 \item If $k$ is a field and $k \to R$ is a ring map inducing
-an isomrphism $k \to R/\mathfrak m$, then $R$ is isomorphic
+an isomorphism $k \to R/\mathfrak m$, then $R$ is isomorphic
 as a $k$-algebra to a power series ring over $k$.
 \end{enumerate}
 \end{lemma}
 
 \begin{proof}
-By the Cohen structure theorem (Theorem \ref{theorem-cohen-structure-theorem})
-there exists a coefficient ring, which reduces (1) to (2).
-In case (2) we pick $f_1, \ldots, f_d \in \mathfrak m$ which
+In case (1), by the Cohen structure theorem
+(Theorem \ref{theorem-cohen-structure-theorem})
+there exists a coefficient ring which must be a field
+mapping isomorphically to the residue field. Thus
+it suffices to prove (2). In case (2) we pick
+$f_1, \ldots, f_d \in \mathfrak m$ which
 map to a basis of $\mathfrak m/\mathfrak m^2$ and we consider
 the continuous $k$-algebra map $k[[x_1, \ldots, x_d]] \to R$
-sending $x_i$ to $f_i$. This map is an isomorphism because
-it induces an isomorphism
-$$
-(x_1, \ldots, x_d)^n/(x_1, \ldots, x_d)^{n + 1}
-\longrightarrow
-\mathfrak m^n/\mathfrak m^{n + 1}
-$$
-for all $n \geq 1$ by Lemma \ref{lemma-regular-graded}. Some details
-omitted.
+sending $x_i$ to $f_i$. As both source and target are
+$(x_1, \ldots, x_d)$-adically complete, this map is surjective by
+Lemma \ref{lemma-completion-generalities}. On the other hand, it
+has to be injective because otherwise the dimension of
+$R$ would be $< d$ by Lemma \ref{lemma-one-equation}.
 \end{proof}
 
 \begin{lemma}