[proofplan] We fix a Lubin--Tate polynomial $e \in \mathcal{E}_\pi$ and work with the formal group $F = F_e$. The proof proceeds in four stages: (1) show that $\phi_n(X) = e^n(X)/e^{n-1}(X)$ is Eisenstein of the correct degree, so any $\lambda_n \in F(n) \setminus F(n-1)$ generates a totally ramified extension $K(\lambda_n)/K$ of degree $q^{n-1}(q-1)$; (2) show that Galois automorphisms act on $F(n)$ as $\mathcal{O}_K$-module automorphisms, giving an injection $\operatorname{Gal}(L_n/K) \hookrightarrow \mathrm{Aut}_{\mathcal{O}_K}(F(n))$; (3) identify $\mathrm{Aut}_{\mathcal{O}_K}(F(n)) \cong U_K/U_K^{(n)}$; (4) conclude by a degree count that the injection is a bijection and $L_n = K(\lambda_n)$. [/proofplan] [step:Show $\phi_n(X) = e^n(X)/e^{n-1}(X)$ is Eisenstein of degree $q^{n-1}(q-1)$] Choose $e(X) = X^q + \pi(a_{q-1} X^{q-1} + \cdots + a_2 X^2) + \pi X$, a Lubin--Tate polynomial. The iterates $e^k$ (composition $k$ times) satisfy $\deg(e^k) = q^k$. The polynomial $\phi_n(X) = e^n(X)/e^{n-1}(X)$ has degree $q^n - q^{n-1} = q^{n-1}(q-1)$. To verify the Eisenstein property, note that the roots of $e^n(X)$ are exactly the elements of $F(n) = \ker([\pi^n]_F)$, and the roots of $e^{n-1}(X)$ are the elements of $F(n-1)$. So the roots of $\phi_n$ are $F(n) \setminus F(n-1)$. Since $e(X) \equiv \pi X \pmod{X^2}$ and $e(X) \equiv X^q \pmod{\pi}$, the iterate $e^n(X) \equiv \pi^n X \pmod{X^2}$ and $e^n(X) \equiv X^{q^n} \pmod{\pi}$. The constant term of $\phi_n$ is $e^n(0)/e^{n-1}(0)$; since $e^k(0) = 0$ for all $k$, we compute instead: $\phi_n(X) = \prod_{\lambda \in F(n) \setminus F(n-1)} (X - \lambda)$, and the constant term is $(-1)^{q^{n-1}(q-1)} \prod_\lambda \lambda$. The product of all roots of $e^n$ is $(-1)^{q^n} \pi$ (the constant term of $e^n$ divided by the leading coefficient), and similarly for $e^{n-1}$, giving the constant term of $\phi_n$ valuation $v_K = 1$. All intermediate coefficients of $\phi_n$ are divisible by $\pi$ (since the Newton polygon of $\phi_n$ has a single slope, determined by the fact that all roots have the same valuation). Therefore $\phi_n$ is Eisenstein over $\mathcal{O}_K$. [/step] [step:Deduce that $K(\lambda_n)/K$ is totally ramified with $\lambda_n$ a uniformizer] Let $\lambda_n \in F(n) \setminus F(n-1)$. Since $\lambda_n$ is a root of the Eisenstein polynomial $\phi_n$ of degree $q^{n-1}(q - 1)$ over $K$, the [Eisenstein criterion for totally ramified extensions](/theorems/2383) gives: - $[K(\lambda_n) : K] = q^{n-1}(q - 1)$, - $K(\lambda_n)/K$ is totally ramified, - $\lambda_n$ is a uniformizer of $K(\lambda_n)$. The norm $N_{K(\lambda_n)/K}(-\lambda_n)$ equals the constant term of $\phi_n$ (up to sign). Since $\phi_n$ is Eisenstein with constant term having $v_K$-valuation $1$ and the constant term is $\pi$ (from the recursive structure of $e^n$), we obtain $N_{K(\lambda_n)/K}(-\lambda_n) = \pi$. [/step] [step:Show Galois automorphisms act as $\mathcal{O}_K$-linear maps on $F(n)$] Any $\sigma \in \operatorname{Gal}(L_n/K)$ permutes the roots of $e^n(X)$, hence permutes $F(n)$. The formal group law $F_e(X, Y)$ and the endomorphisms $[a]_e(X)$ for $a \in \mathcal{O}_K$ have coefficients in $\mathcal{O}_K \subseteq K$, so they are fixed by $\sigma$. Applying $\sigma$ to the identities $x +_F y = F_e(x, y)$ and $a \cdot x = [a]_e(x)$ for $x, y \in F(n)$: \begin{align*} \sigma(x +_F y) &= F_e(\sigma(x), \sigma(y)) = \sigma(x) +_F \sigma(y), \\ \sigma(a \cdot x) &= [a]_e(\sigma(x)) = a \cdot \sigma(x). \end{align*} Therefore $\sigma$ acts as an $\mathcal{O}_K$-module automorphism of $(F(n), +_F, [\cdot]_e)$. [guided] Why does $\sigma$ preserve the formal group operations? The formal group law $F_e(X, Y) = \sum c_{ij} X^i Y^j$ has coefficients $c_{ij} \in \mathcal{O}_K$. When we evaluate at elements $x, y$ of the splitting field $L_n$, the operation $x +_F y = F_e(x, y)$ is a polynomial in $x$ and $y$ with $K$-rational coefficients. Since $\sigma$ fixes $K$ pointwise, $\sigma(F_e(x, y)) = F_e(\sigma(x), \sigma(y))$. The same argument applies to the endomorphisms $[a]_e$. This shows that $\sigma$ is an $\mathcal{O}_K$-module automorphism of $F(n)$, so we obtain a group homomorphism \begin{align*} \Phi: \operatorname{Gal}(L_n/K) &\to \mathrm{Aut}_{\mathcal{O}_K}(F(n)), \\ \sigma &\mapsto \sigma|_{F(n)}. \end{align*} The map $\Phi$ is injective because $L_n$ is generated over $K$ by the elements of $F(n)$ (it is the splitting field of $e^n$), so an automorphism acting directly on $F(n)$ is the identity. [/guided] [/step] [step:Identify $\mathrm{Aut}_{\mathcal{O}_K}(F(n))$ with $U_K / U_K^{(n)}$] The module $F(n) = \ker([\pi^n]_F)$ is a finite $\mathcal{O}_K$-module annihilated by $\pi^n$. Since $F(n)$ has $|F(n)| = q^n$ elements (as $e^n$ has degree $q^n$ and is separable — its derivative $\pi^n \not\equiv 0$ ensures separability in characteristic $0$, and in equal characteristic separability follows from the formal group structure), and $F(n)/F(n-1) \cong F(1)$ has $q$ elements, the module $F(n)$ is isomorphic to $\mathcal{O}_K / \pi^n \mathcal{O}_K$ as an $\mathcal{O}_K$-module. An $\mathcal{O}_K$-module automorphism of $\mathcal{O}_K / \pi^n \mathcal{O}_K$ is determined by the image of a generator, which must be a unit in $\mathcal{O}_K / \pi^n \mathcal{O}_K$. Therefore \begin{align*} \mathrm{Aut}_{\mathcal{O}_K}(F(n)) \cong (\mathcal{O}_K / \pi^n \mathcal{O}_K)^\times \cong U_K / U_K^{(n)}, \end{align*} where $U_K^{(n)} = 1 + \pi^n \mathcal{O}_K$ is the $n$-th unit group. [guided] The group $(\mathcal{O}_K / \pi^n \mathcal{O}_K)^\times$ has order $q^n - q^{n-1} = q^{n-1}(q - 1)$: there are $q^n$ elements total, and $q^{n-1}$ are divisible by $\pi$ (i.e., non-units). So \begin{align*} |U_K / U_K^{(n)}| = q^{n-1}(q - 1). \end{align*} The identification sends a unit $u \in U_K$ to the automorphism $\lambda \mapsto [u]_F(\lambda)$. Two units $u_1, u_2$ give the same automorphism if and only if $[u_1]_F(\lambda) = [u_2]_F(\lambda)$ for all $\lambda \in F(n)$, i.e., $[u_1 - u_2]_F$ annihilates $F(n)$. Since $F(n) = \ker([\pi^n]_F)$ and $\mathcal{O}_K / \pi^n \mathcal{O}_K$ is a principal ideal ring, $[u_1 - u_2]_F$ annihilates $F(n)$ if and only if $\pi^n \mid (u_1 - u_2)$ in $\mathcal{O}_K$, i.e., $u_1 \equiv u_2 \pmod{\pi^n}$, i.e., $u_1 u_2^{-1} \in U_K^{(n)}$. [/guided] [/step] [step:Conclude the isomorphism by a degree count] From the previous steps, we have an injection \begin{align*} \operatorname{Gal}(L_n/K) \hookrightarrow \mathrm{Aut}_{\mathcal{O}_K}(F(n)) \cong U_K / U_K^{(n)}, \end{align*} and $|U_K / U_K^{(n)}| = q^{n-1}(q - 1) = [K(\lambda_n) : K] \leq [L_n : K] = |\operatorname{Gal}(L_n/K)|$. Since the injection maps a group of order $|\operatorname{Gal}(L_n/K)|$ into a group of order $q^{n-1}(q-1)$, and $|\operatorname{Gal}(L_n/K)| \geq q^{n-1}(q-1) \geq |\mathrm{Aut}_{\mathcal{O}_K}(F(n))|$, the injection must be a bijection. Hence \begin{align*} \operatorname{Gal}(L_n/K) \cong \mathrm{Aut}_{\mathcal{O}_K}(F(n)) \cong U_K / U_K^{(n)}, \end{align*} and $[L_n : K] = q^{n-1}(q - 1) = [K(\lambda_n) : K]$, which forces $L_n = K(\lambda_n)$. The extension $L_n/K$ is abelian (since $U_K/U_K^{(n)}$ is abelian) and totally ramified (since $K(\lambda_n)/K$ is totally ramified by the Eisenstein property). [/step] [step:Identify the subgroups $\operatorname{Gal}(L_m/L_n)$ for $m \geq n$] For $m \geq n$, the restriction map $\operatorname{Gal}(L_m/K) \to \operatorname{Gal}(L_n/K)$ corresponds, under the isomorphism $\operatorname{Gal}(L_m/K) \cong U_K/U_K^{(m)}$, to the natural quotient map $U_K/U_K^{(m)} \twoheadrightarrow U_K/U_K^{(n)}$. This is because a unit $u \in U_K$ acts on $F(m)$ via $[u]_F$, and its restriction to $F(n) \subseteq F(m)$ is $[u]_F|_{F(n)}$, which corresponds to $u \bmod U_K^{(n)}$. The kernel of this restriction map is $\operatorname{Gal}(L_m/L_n)$, which corresponds to the kernel of $U_K/U_K^{(m)} \to U_K/U_K^{(n)}$, namely $U_K^{(n)}/U_K^{(m)}$: \begin{align*} \operatorname{Gal}(L_m/L_n) \cong U_K^{(n)} / U_K^{(m)}. \end{align*} [/step]