[proofplan] We show that every Lubin--Tate $\mathcal{O}_K$-module for $\pi$ has the form $F_e$ for some $e \in \mathcal{E}_\pi$, and that all such modules are isomorphic. The first claim follows by extracting the endomorphism $[\pi]_F$ and verifying it belongs to $\mathcal{E}_\pi$. The isomorphism and homomorphism statements follow from the uniqueness clause of the Lifting Lemma: $[a]_{e_1, e_2}$ is a homomorphism because both $[a]_{e_1, e_2} \circ F_{e_2}$ and $F_{e_1} \circ ([a]_{e_1, e_2}, [a]_{e_1, e_2})$ solve the same lifting problem, and it is an isomorphism when $a \in \mathcal{O}_K^\times$ because $[a^{-1}]_{e_2, e_1}$ is a two-sided inverse. [/proofplan]

[step:Show every Lubin--Tate module for $\pi$ has the form $F_e$] Let $F$ be a Lubin--Tate $\mathcal{O}_K$-module for $\pi$, with $\mathcal{O}_K$-action $a \mapsto [a]_F$. Set $e = [\pi]_F \in \mathcal{O}_K[[X]]$. By definition of a Lubin--Tate module: - $[a]_F(X) \equiv aX \pmod{X^2}$ for all $a \in \mathcal{O}_K$, so $e(X) = [\pi]_F(X) \equiv \pi X \pmod{X^2}$. - The endomorphism $[\pi]_F$ commutes with $F$: $e(F(X, Y)) = F(e(X), e(Y))$. - $e(X) \equiv X^q \pmod{\pi}$ (this is part of the definition of a Lubin--Tate module — the reduction modulo $\pi$ of $[\pi]_F$ is the Frobenius). These three properties are precisely the conditions for $e \in \mathcal{E}_\pi$. Moreover, $F$ satisfies $F(X, Y) \equiv X + Y \pmod{(X,Y)^2}$ and $e(F(X,Y)) = F(e(X), e(Y))$, which is exactly the characterizing property of $F_e$ from the [Formal Group Law](/theorems/2392). By the uniqueness clause of the Lifting Lemma, $F = F_e$. [/step]

[step:Show $[a]_{e_1, e_2}$ is a homomorphism $F_{e_2} \to F_{e_1}$] We must verify $[a]_{e_1, e_2}(F_{e_2}(X, Y)) = F_{e_1}([a]_{e_1, e_2}(X), [a]_{e_1, e_2}(Y))$. Consider both sides as elements of $\mathcal{O}_K[[X, Y]]$. They have the same linear part: the LHS has linear part $a(X + Y)$ (since $[a]_{e_1, e_2}(Z) \equiv aZ$ and $F_{e_2}(X,Y) \equiv X + Y$), and the RHS has linear part $F_{e_1}(aX, aY) \equiv aX + aY = a(X+Y)$. For the intertwining relation, using the defining properties of $[a]_{e_1, e_2}$ and $F_{e_1}$, $F_{e_2}$: \begin{align*} e_1([a]_{e_1, e_2}(F_{e_2}(X, Y))) &= [a]_{e_1, e_2}(e_2(F_{e_2}(X, Y))) = [a]_{e_1, e_2}(F_{e_2}(e_2(X), e_2(Y))), \end{align*} and \begin{align*} e_1(F_{e_1}([a]_{e_1, e_2}(X), [a]_{e_1, e_2}(Y))) &= F_{e_1}(e_1([a]_{e_1, e_2}(X)), e_1([a]_{e_1, e_2}(Y))) \\ &= F_{e_1}([a]_{e_1, e_2}(e_2(X)), [a]_{e_1, e_2}(e_2(Y))). \end{align*} Both sides satisfy the lifting problem with $n = 2$, $L(X,Y) = a(X + Y)$, and intertwining series $e_1$ (on the outside) and $e_2$ (on the variables). By uniqueness in the [Lifting Lemma](/theorems/2391), they are equal. [/step]

[step:Show $[a]_{e_1, e_2}$ is an isomorphism when $a \in \mathcal{O}_K^\times$] When $a \in \mathcal{O}_K^\times$, the power series $[a^{-1}]_{e_2, e_1}$ is a homomorphism $F_{e_1} \to F_{e_2}$ (by the previous step with the roles of $e_1$ and $e_2$ swapped and $a$ replaced by $a^{-1}$). The composition $[a^{-1}]_{e_2, e_1} \circ [a]_{e_1, e_2}$ has linear part $a^{-1} \cdot a \cdot X = X$ and satisfies the intertwining relation $e_2 \circ G = G \circ e_2$. By uniqueness in the Lifting Lemma (with $n = 1$, $L(X) = X$, $e_1 = e_2$), the unique solution is $G(X) = X$. Hence $[a^{-1}]_{e_2, e_1} \circ [a]_{e_1, e_2} = \operatorname{id}$. Symmetrically, $[a]_{e_1, e_2} \circ [a^{-1}]_{e_2, e_1} = \operatorname{id}$. Therefore $[a]_{e_1, e_2}$ is an isomorphism $F_{e_2} \xrightarrow{\sim} F_{e_1}$ with inverse $[a^{-1}]_{e_2, e_1}$. [/step]

[step:Conclude that all Lubin--Tate modules for $\pi$ are isomorphic] For any $e_1, e_2 \in \mathcal{E}_\pi$, choose $a = 1 \in \mathcal{O}_K^\times$. Then $[1]_{e_1, e_2}$ is an isomorphism $F_{e_2} \xrightarrow{\sim} F_{e_1}$. Since every Lubin--Tate module for $\pi$ has the form $F_e$ for some $e \in \mathcal{E}_\pi$ (by the first step), all Lubin--Tate modules for $\pi$ are isomorphic. The remaining compatibility identities — $[a + b]_{e_1, e_2} = F_{e_1}([a]_{e_1, e_2}, [b]_{e_1, e_2})$ and $[ab]_{e_1, e_3} = [a]_{e_1, e_2} \circ [b]_{e_2, e_3}$ — follow by the same uniqueness argument: both sides of each identity satisfy the same lifting problem (same linear part, same intertwining relation). [/step]