Complete DVR containing a field isomorphic to residue field Let $(R, \mathfrak m, k)$ be a ($\mathfrak m$-adically) complete DVR containing $k\cong R/\mathfrak m$. Also assume $k$ is algebraically closed.
Then, is it true  that we always have a $k$-algebra isomorphism $R \cong k[[T]]$ ?
My try: Let $\mathfrak m=(\pi)$ . Then every element $a$ of $R$ can be uniquely written as $a=u\pi^{v(a)}$ for some $v(a)\ge 0$ where $u \notin \mathfrak m$. Since $R$ is complete, so we can consider the ring homomorphism $k[[T]] \to R$ sending $T \to \pi$ . But I'm not sure if this is either injective or surjective. Please help.
 A: 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^n\ne 0$, which is mapped to $0\in R$. Let $n_0$ be the minimal value of $n$ for which $h_n\in k$ is not zero, so $h_n\in R^\times$. Then $h\to 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_n\pi^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, $r\in (\pi)^n=(\pi^n)$, a principal ideal, so we can write $r=u\pi^n$ for a unit $u\in R^\times$. Consider $r_n\in 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_n\pi^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$.
A: 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$.
