12.3. The Main Conjecture
Recall the ideal I(\GG^+)\zeta_p \subseteq \Lam(\GG^+) generated by the
Kubota–Leopoldt pseudo-measure — concretely the topological ideal generated by the
elements ([g]-[1])\zeta_p, g \in \GG^+. It encodes the zeros of \zeta_p,
and Iwasawa's theorem already gave it an arithmetic description in terms of
cyclotomic units. The Main Conjecture upgrades this to a statement about the
Galois module \sX_\infty^+.
- No associated Lean code or declarations.
(Iwasawa Main Conjecture.) The module \sX_\infty^+ is a finitely generated
torsion \Lam(\GG^+)-module, and its characteristic ideal equals the ideal of
\zeta_p:
\Ch_{\Lam(\GG^+)}(\sX_\infty^+) = I(\GG^+)\,\zeta_p.
This is a statement about Definition 12.1.4 of the Galois module
Definition 12.2.2 and the ideal Proposition 10.2.1 generated
by the Kubota–Leopoldt p-adic L-function Definition 4.3.2.
For Vandiver primes this follows from the explicit isomorphism
Theorem 12.4.7, which gives
\sX_\infty^+ \cong \Lam(\GG^+)/I(\GG^+)\zeta_p; taking characteristic ideals of
both sides and using that \Ch_{\Lam(\GG^+)}(\Lam(\GG^+)/J) = J for an ideal
J cut out by elementary divisors yields the claim. The conjecture holds
unconditionally by the theorem of Mazur–Wiles (and, via Euler systems, by
Kolyvagin–Rubin–Thaine); in these notes we prove only the Vandiver case.
It is traditional to phrase the Main Conjecture in terms of an even Dirichlet
character of \Gal(\Q(\mu_p)/\Q). The parity of the character produces the
familiar even/odd dichotomy (visible already in the Bernoulli numbers); the
formulation above packages together all even characters. For the odd case one
works with \sY_\infty^+ instead.