1 Introduction

Notations. A “✓” in a theorem/lemma/definition means that its statement is formalized in LꓱꓯN (but not proof!). A “✓” in a proof means that the proof is also formalized in LꓱꓯN (but it could have dependencies which are not yet formalized).

1.1 Iwasawa’s theorem on growth of class groups

Iwasawa theory is a branch of modern number theory, initiated by Kenkichi Iwasawa in 1959 [ Iwa59 ] , which studies arithmetic objects over infinite towers of number fields. It was motivated by the study of class groups of cyclotomic fields, which are very important in number theory.

Theorem 1.1 Fermat’s Last Theorem, regular prime case

If a prime \(p\geq 3\) does not divide the class number of \({\mathbb {Q}}(\mu _p)\), then \(x^p+y^p=z^p\), \(xyz\neq 0\) does not have integral solution.

The class group of \({\mathbb {Q}}(\mu _p)\) is studied via infinite tower of cyclotomic fields

\[ {\mathbb {Q}}(\mu _p)\subset {\mathbb {Q}}(\mu _{p^2})\subset {\mathbb {Q}}(\mu _{p^3})\subset \cdots \subset {\mathbb {Q}}(\mu _{p^\infty }), \]

which is an example of a \({\mathbb {Z}}_p\)-extension.

Definition 1.2

✓

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}}\).

The \(K_n\) form an infinite tower

\[ K=K_0\subset K_1\subset K_2\subset \cdots \subset K_\infty . \]

Iwasawa in 1959 [ Iwa59 ] studied the growth of class groups of \(K_n\) in a \({\mathbb {Z}}_p\)-extension.

Theorem 1.3 Iwasawa’s theorem, [ Was97 ] , Theorem 13.13, [ Iwa59 ] , Theorem 11

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 \).

Proof ▶

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 \).

The first goal of our project is formalize the proof of the above Iwasawa’s theorem on growth of class groups in a \({\mathbb {Z}}_p\)-extension tower in LꓱꓯN.