Krull-Schmidt holds for finite-rank OH-lattices

Let $M$ be such a lattice and put $E={\mathrm{End}}_{\mathcal{O}H}(M)$. As an $\mathcal{O}$-submodule of the finite free module ${\mathrm{End}}_{\mathcal{O}}(M)$, the module $E$ is finite free and $\mathfrak{m}$-adically complete. Also $\mathfrak{m}E\subseteq J(E)$: for $x\in \mathfrak{m}E$ and $y\in E$, the geometric series ${\sum }_{n\ge 0}(yx{)}^n$ converges and inverts $1-yx$.

The algebra $\bar{E}=E\mathrm{/}\mathfrak{m}E$ is finite-dimensional over $k$, so its Jacobson radical $J(\bar{E})$ is nilpotent and $\bar{E}\mathrm{/}J(\bar{E})$ is semisimple Artinian. Because $\mathfrak{m}E\subseteq J(E)$ by step 1.1, the standard quotient identity gives $J(E\mathrm{/}\mathfrak{m}E)=J(E)\mathrm{/}\mathfrak{m}E\mathrm{.}$ For completeness, if $x+\mathfrak{m}E$ lies in the radical of the quotient, then for every $y\in E$ the element $1-yx$ is a unit modulo $\mathfrak{m}E$; lifting a two-sided inverse leaves errors in $\mathfrak{m}E\subseteq J(E)$, and multiplying by the inverses of $1$ minus those errors gives a two-sided inverse in $E$. Thus $x\in J(E)$ by the Jacobson-radical test. The reverse inclusion follows by passing units to the quotient. Consequently $E\mathrm{/}J(E)\cong \bar{E}\mathrm{/}J(\bar{E})$ is semisimple Artinian.

Idempotents lift from $E\mathrm{/}J(E)$ to $E$. First lift through the nilpotent ideal $J(\bar{E})$: successively through its powers, the polynomial Newton correction to $e^2-e$ turns an error in $J(\bar{E}{)}^n$ into one in $J(\bar{E}{)}^{2n}$, so the finite nilpotence filtration terminates. Then lift the resulting idempotent of $E\mathrm{/}\mathfrak{m}E$ by the same corrections in $E$; completeness makes the corrections converge. Therefore $E$ is semiperfect.

A nontrivial idempotent of $E$ is exactly a nontrivial direct-sum decomposition of $M$. Repeatedly splitting such an idempotent terminates, because the positive $\mathcal{O}$-ranks of both summands are smaller; direct summands remain finite free over the DVR. This proves existence of a finite indecomposable decomposition. If $M$ is indecomposable, $E$ has no nontrivial idempotent. By step 3.1, every idempotent of the semisimple Artinian ring $E\mathrm{/}J(E)$ lifts, so that quotient also has no nontrivial idempotent. It must therefore be a division ring. Hence the nonunits of $E$ are exactly $J(E)$, and $E$ is local.

Suppose $M={⨁}_{i=1}^r{M}_i={⨁}_{j=1}^s{N}_j$ are two indecomposable decompositions. Restrict the identity of $M$ to $M_1$ through the second decomposition. It becomes a finite sum of composites $M_1\to N_j\to M_1$. In the local ring ${\mathrm{End}}_{\mathcal{O}H}(M_1)$, a sum of nonunits cannot be $1$; therefore one composite is a unit. Write that composite as $ab$, where $b:M_1\to N_j$ is the second-decomposition projection restricted to $M_1$ and $a:N_j\to M_1$ is the first-decomposition projection restricted to $N_j$. Replacing $b$ by $b(ab{)}^{-1}$ gives $ab=1_{M_1}$. Hence $N_j=b(M_1)\oplus \ker a$; indecomposability and $b(M_1)\mathrm{\ne }0$ force $\ker a=0$, so $a$ is an isomorphism. Relative to $M=M_1\oplus M^{\mathrm{\prime }}$ with $M^{\mathrm{\prime }}={⨁}_{i>1}{M}_i$, the summand $N_j$ is therefore the graph of a map $M_1\to M^{\mathrm{\prime }}$. Subtracting that graph map is an automorphism of $M$ which fixes $M^{\mathrm{\prime }}$ and carries $N_j$ to $M_1$. Thus $M=N_j\oplus M^{\mathrm{\prime }}$, and quotienting by $N_j$ identifies $M^{\mathrm{\prime }}$ with the sum of the remaining $N$-summands. Induction on the rank matches all summands and their multiplicities. The zero lattice has the empty decomposition, while the local ring assertion was stated only for nonzero indecomposables. Every selection is from a finite decomposition, so no choice principle is used.