1 Introduction
1.1 Iwasawa’s theorem on growth of class groups
The first goal of this project is formalize the proof of Iwasawa’s theorem on growth of class groups in a \({\mathbb {Z}}_p\)-extension tower in LꓱꓯN.
Let \(K\) be a field, \(p\) be a prime.
(i) An extension \(K_\infty /K\) is called a \({\mathbb {Z}}_p\)-extension, if it is Galois with \(\Gamma ={\mathrm{Gal}}(K_\infty /K)\cong {\mathbb {Z}}_p\) as topological groups.
(ii) If \(K_\infty /K\) is a \({\mathbb {Z}}_p\)-extension, then for any \(n\geq 0\), define \(K_n:=K_\infty ^{\Gamma ^{p^n}}\).
Let \(K\) be a number field, \(p\) be a prime, \(K_\infty /K\) be a \({\mathbb {Z}}_p\)-extension. Then there exist integers \(\lambda \geq 0,\mu \geq 0,\nu \) such that for all sufficiently large \(n\), \(\operatorname{ord}_p(\# {\mathrm{Cl}}(K_n))=\mu p^n+\lambda n+\nu \).
For each \(n\) let \(L_n\) be the maximal unramified abelian extension of \(K_n\) of exponent \(p\), and let \(X_n:={\mathrm{Gal}}(L_n/K_n)\). Then by class field theory, \(\operatorname{ord}_p(\# {\mathrm{Cl}}(K_n))=\operatorname{ord}_p(\# X_n)\). Let \(L_\infty =\bigcup _n K_n\) and \(X_\infty ={\mathrm{Gal}}(L_\infty /K_\infty )=\varprojlim _n X_n\), then \(X_\infty \) is a \(\Lambda \)-module, where \(\Lambda :={\mathbb {Z}}_p[[\Gamma ]]\). Theorem 5.20 asserts that \(X_\infty \) is a finitely generated torsion \(\Lambda \)-module and each \(X_n\) is isomorphic to certain quotient of \(X_\infty \). Proposition 4.18 asserts the growth of such quotient is of form \(\mu p^n+\lambda n+\nu \).