= Solution
Let $F_n$ be the degree-$p^n$ layer, $\Gamma_n=\Gamma^{p^n}$, and
$$
\Lambda=\mathbb Z_p[[\Gamma]]\cong\mathbb Z_p[[T]],
\qquad \omega_n(T)=(1+T)^{p^n}-1.
$$
Conjugation makes $Y$ a compact $\Lambda$-<module>. The goal is to show that it is finitely generated and has <Iwasawa-module rank> zero. This proof applies to every <Zp-extension>, not only a cyclotomic one, and makes no <Leopoldt conjecture> assumption.
By the ramification argument above, only primes over $p$ ramify in $F_\infty/F$, and at least one does. Every nonzero closed <inertia group> in $\Gamma\cong\mathbb Z_p$ is open. After replacing $F$ by a finite layer, every prime which ramifies is totally ramified in the remaining tower. The number $s\geq1$ of such primes then stays constant. This replacement does not affect whether $Y$ is a <torsion module>: $\mathbb Z_p[[\Gamma]]$ is finite free over the <Iwasawa algebra> of an open subgroup, and the two module ranks vanish together.
Let $\mathcal G_n=\operatorname{Gal}(L_\infty/F_n)$, and let $D_n$ be its maximal abelian quotient. The <abelianization over a Zp-extension> formula gives an <exact sequence>
$$
0\longrightarrow Y_{\Gamma_n}
\longrightarrow D_n
\longrightarrow\Gamma_n
\longrightarrow0,
\qquad
Y_{\Gamma_n}=Y/\omega_nY.
$$
Choose a lift of a generator of $\Gamma_n$ if a splitting is desired. We will bound the $\mathbb Z_p$-rank of the middle term independently of $n$.
At each of the $s$ ramified primes, inertia in $L_\infty/F_n$ maps isomorphically onto $\Gamma_n$: its kernel is inertia in the unramified extension $L_\infty/F_\infty$, hence trivial, and the map onto the totally ramified base inertia is surjective. Thus each image in $D_n$ is procyclic and has $\mathbb Z_p$-rank at most one. No other finite prime contributes inertia. Quotienting $D_n$ by the closed subgroup generated by these $s$ images gives an abelian extension of $F_n$ unramified at all finite primes. Its <Galois group> is finite by <class field theory>, using the ordinary or narrow <ideal class group> according to the treatment of real places. Any infinite-place inertia is finite and does not affect the rank bound. Therefore $D_n$ is finitely generated over $\mathbb Z_p$ and
$$
\operatorname{rank}_{\mathbb Z_p}D_n\leq s.
$$
The preceding <exact sequence> now yields the uniform bound
$$
\boxed{\operatorname{rank}_{\mathbb Z_p}(Y/\omega_nY)\leq s-1.}
$$
It does not assert that these <coinvariant modules> are always finite when several primes ramify.
At $n=0$, $Y/TY$ is finitely generated over $\mathbb Z_p$, so $Y/(p,T)Y$ is finite. Lift a finite basis of this quotient to $Y$. The <Compact Nakayama lemma> shows that these lifts generate $Y$ over $\Lambda$. Briefly, the quotient by their compact generated image satisfies $Q=(p,T)Q$. Every finite continuous $\Lambda$-quotient of $Q$ has nilpotent action by $(p,T)$: $p$ is nilpotent, and modulo $p$ a finite pro-$p$ action makes $\gamma-1$ nilpotent. Such a quotient must be zero. Finite quotients separate points of a compact <pro-p group>, so $Q=0$.
Suppose now that $Y$ had positive $\Lambda$-rank $r$. The <Iwasawa module structure theorem> provides a <pseudo-isomorphism> to
$$
\Lambda^r\oplus E
$$
with $E$ a finitely generated <torsion module>. Passing to $\Gamma_n$-<coinvariant modules> leaves a finite cokernel. But
$$
\Lambda/\omega_n\Lambda\cong\mathbb Z_p[\Gamma/\Gamma_n]
$$
is free of rank $p^n$ over $\mathbb Z_p$. Thus the <coinvariant modules> would have rank at least $r p^n$, contradicting the uniform bound $s-1$. Equivalently their ranks have asymptotic form $r p^n+O(1)$, with the torsion elementary divisors contributing only a bounded rank.
It follows that $r=0$. Since $\Lambda$ is an <integral domain>, rank zero means every element is killed by a nonzero scalar. Therefore
$$
\boxed{Y\text{ is a finitely generated torsion }\mathbb Z_p[[\Gamma]]\text{-module}.}
$$
This is the <unramified Iwasawa torsion theorem>. The crucial arithmetic inputs are finite class fields and the bounded number of ramified primes; neither vanishing of a $\mu$-invariant nor a cyclotomic main conjecture is required.
Back to article page
