Limit of quotients by $p^n$-th powers in $p$-adic fields Let $K/\mathbb{Q}_p$ be a finite extension with normalized valuation $v_K$, let $\mathcal O_K$ be its ring of integers, and let $\mathfrak m_K$ be the maximal ideal of $\mathcal O_K$. Denote $U^N=1+\mathfrak m^N$. I want to prove that the natural map $$U^1\to\varprojlim U^1/(U^1)^{p^n}$$ is an isomorphism. 
The map is injective if I show that for each $N$ there exists $n$ such that $(U^1)^{p^n}\subset U^N$. I fix some $N$. The valuations of the non trivial terms of $(1+m)^{p^n}$ are $v_K(p)\cdot n-v_K(k)+k\cdot v_K(m)$ with $1\leq k\leq p^{n}$. The smallest of these valuations is when $k=p^d$ and $v_K(m)=1$, so I assume that. I need to find $n$ such that $v_K(p)\cdot n-v_K(p)\cdot d+p^d\geq N$ for all $1\leq d\leq n$. The minimum of the function $d\mapsto -v_K(p)\cdot d+p^d$ is independent of $n$, so an $n$ large enough will satisfy the needed condition. 
For surjectivity, I observe that the image is dense and that the profinite group $U^1$ is compact. 
Can someone please verify that the above is correct? 
 A: I think this looks correct.
Another way to proceed could be to show the following:
Lemma: if $x\in\mathcal{O}_K$ is such that $x-1\in\mathfrak{m}$, then 
$$x^{p^n}-1\in\mathfrak{m}^{n+1}$$
for all $n\ge 1$.
You can proceed by induction on $n$, after noticing that $p\in\mathfrak{m}$.
This shows that $(U^1)^{p^n}\subset U^{n+1}$ and $\cap_{n\ge 1}(U^1)^{p^n}=\{1\}$.
Edit: this lemma can be found as "Lemma 1" one Serre's "Corps locaux" (French version, page 35)
For the surjectivity, I think one can also proceed directly: let $(x_n)_n$ be an element of $\varprojlim_{n\ge 1}U^1/(U^1)^{p^n}$. We can find a family $(\tilde{x}_n)_n$ of elements of $U^1$ such that $\tilde{x}_n\mod (U^1)^{p^n}=x_n$. This means that
$\tilde{x}_{n+1}\equiv \tilde{x}_n\mod (U^1)^{p^n},$ i.e. $\tilde{x}_{n+1}\tilde{x}_n^{-1}\in (U^1)^{p^n}\subset U^{n+1}$,
i.e. $\tilde{x}_{n+1}-\tilde{x}_n\in\mathfrak{m}^{n+1}$,
which shows that the sequence $(\tilde{x}_n)$ converges to some $\tilde{x}\in\mathcal{O}_K$.
As $v_K(\tilde{x}_{n}-1)\ge 1$ for all $n$, we get $v_K(\tilde{x}-1)\ge 1$, 
i.e. $\tilde{x}\in U^1$.
As we had $\tilde{x}_{n+1}\tilde{x}_n\in(U^1)^{p^n}$ for each $n$, we have 
$\tilde{x}_k\tilde{x}_n^{-1}\in (U^1)^{p^n}$ for all $k\ge n$, 
then $\tilde{x}\tilde{x}_n^{-1}\in (U^1)^{p^n}$, which means that
$\tilde{x}\mod (U^1)^{p^n}=x_n$, which terminates the surjectivity.
What do you think Lukas ?
