13.1. The setup
- No associated Lean code or declarations.
Let F be a number field. A \Zp-extension of F is a Galois extension
F_\infty / F with \Gal(F_\infty / F) \cong \Zp. Writing \Gamma := \Gal(F_\infty/F),
the closed subgroups of \Zp are p^n\Zp, so for each n there is a unique
subextension F_n with \Gal(F_n/F) \cong \Z/p^n\Z, and F_\infty = \bigcup_n F_n.
- No associated Lean code or declarations.
Every number field F admits at least one \Zp-extension, the cyclotomic
\Zp-extension, contained in F(\mu_{p^\infty}).
By Galois theory \Gal(F(\mu_{p^\infty})/F) is an open subgroup of
\Gal(\Q(\mu_{p^\infty})/\Q) \cong \Zpx. Now \Zpx \cong \mu_{p-1} \times (1 + p\Zp)
(for p odd) has a maximal quotient isomorphic to \Zp, namely the quotient by
the finite torsion subgroup \mu_{p-1}. Pulling this quotient back to the open
subgroup and taking the fixed field gives a \Zp-extension of F. For
F = \Q(\mu_p) this is F_\infty = \Q(\mu_{p^\infty}), with F_n = \Q(\mu_{p^{n+1}}).
Leopoldt's conjecture predicts that the number of independent \Zp-extensions
of F is exactly r_2 + 1, where r_2 is the number of complex places; in
particular a totally real field should have only the cyclotomic \Zp-extension.
This is known for F abelian over \Q or over an imaginary quadratic field.