1
Introduction
▶
1.1
Iwasawa’s theorem on growth of class groups
2
Preliminaries in commutative algebra
▶
2.1
Random
2.2
Noetherian integrally closed domain
2.3
Semilocal PID
3
Structure of module up to pseudo-isomorphism
▶
3.1
Characteristic ideal
3.2
Pseudo-null module
3.3
Structure theorem
3.4
Noetherian regular domain
4
Structure of Iwasawa module
▶
4.1
Iwasawa algebra
4.2
Weierstrass preparation theorem
4.3
Characteristic ideal
4.4
Growth of coinvariant part
5
Arithmetic of \({\mathbb {Z}}_p\)-extensions
▶
5.1
The class group of \({\mathbb {Z}}_p\)-extension of a number field
5.2
Recover the finite level of class group from infinite level
A
Known results in mathlib
▶
A.1
Rings
A.2
Ideals
A.3
Modules
A.4
Number theory
Dependency graph
Formalization of Iwasawa Theory in LꓱꓯN
Jz Pan
1
Introduction
1.1
Iwasawa’s theorem on growth of class groups
2
Preliminaries in commutative algebra
2.1
Random
2.2
Noetherian integrally closed domain
2.3
Semilocal PID
3
Structure of module up to pseudo-isomorphism
3.1
Characteristic ideal
3.2
Pseudo-null module
3.3
Structure theorem
3.4
Noetherian regular domain
4
Structure of Iwasawa module
4.1
Iwasawa algebra
4.2
Weierstrass preparation theorem
4.3
Characteristic ideal
4.4
Growth of coinvariant part
5
Arithmetic of \({\mathbb {Z}}_p\)-extensions
5.1
The class group of \({\mathbb {Z}}_p\)-extension of a number field
5.2
Recover the finite level of class group from infinite level
A
Known results in mathlib
A.1
Rings
A.2
Ideals
A.3
Modules
A.4
Number theory