Complete DVR containing a field isomorphic to residue field

The injectivity: Assume that two different formal series $f=sum f_n T^n$, and $g=sum g_n T^n$ are mapped into the same element in $R$. Consider the difference $h=f-g=sum h_nT^nne 0$, which is mapped to $0in R$. Let $n_0$ be the minimal value of $n$ for which $h_nin k$ is not zero, so $h_nin R^times$. Then $hto 0$ means that the two elements $-h_{n_0}T^n_0$ and $sum_{n>n_0} h_nT^n$ are mapped into the same result in $R$. But $-h_{n_0}pi^n_0$ and $sum_{n>n_0} h_npi^n$ have different valuations.

Contradiction to the made assumption. So we have injectivity.

---

The surjectivity: Let $r$ be an element in $R$. Assume the discrete valuation $v$ has as image the integers $ge 0$. Let $n=v(r)$. We immediately set $r_0=r_1=dots=r_{n-1}=0$.

From $n=v(r)$, by definition, $rin (pi)^n=(pi^n)$, a principal ideal, so we can write $r=upi^n$ for a unit $uin R^times$. Consider $r_nin R^times$ (a special lift from $k$, if $k$ is not already coming with a structural morphism into $R$) with the same image as $u$ in $k$, which is $R$ modulo $(pi)$. This implies $r=r_npi^n+r'$. Apply the same procedure for $r'$. If its valuation is not $(n+1)$ set $r_{n+1}=0$, else define $r_{n+1}in R^times$ as above. This determines a sequence $(r_n)$. Then $r$ is the image of $sum r_n T^n$.

Let $X subset R$ be a set of coset representatives for $R/mathfrak{m}$, such that $0 in X$. Now recall a result which holds for any complete DVR:

An element of $a in R$ admits a unique (convergent) $pi$-adic expansion $$a = sum_{i=0}^{infty} a_i pi^i$$ where the $a_i in X$.

Moreover any such expansion converges and hence defines an element of $R$.

In our case $R$ contains $k cong R/mathfrak{m}$, so it suffices to show that we may take $X = k$, since then we have the natural map $$k[[T]] to R$$ $$ sum_{i=0}^infty a_i T^i mapsto sum_{i=0}^infty a_i pi^i$$ and it is well-defined by the moreover part. The existence part of the result shows that the map is surjective, and the uniqueness part shows that it is injective.

But $mathfrak{m} cap k = {0}$, so the quotient injects $k$ into $R/mathfrak{m}$ and so we may take $k = X$.