12.4. The Iwasawa Main Conjecture for Vandiver primes
Let h_n^+ = \#\Cl(F_n^+) be the class number of F_n^+. The prime p is a
Vandiver prime if p \nmid h_1^+.
We sketch Iwasawa's conditional proof, following the exposition of Coates–Sujatha. We freely use class field theory and some classical results whose proofs we omit.
For n \ge 1 let \sE_n be the p-adic closure of the global units
\sV_n = \cO_{F_n}^\times inside the local units \sU_n, put
\sE_n^+ = \sE_n \cap \sU_n^+, and set
\sE_{n,1} = \sE_n \cap \sU_{n,1}, \qquad \sE_{n,1}^+ = \sE_n^+ \cap \sU_{n,1},
\sE_{\infty,1} = \varprojlim_n \sE_{n,1}, \qquad \sE_{\infty,1}^+ = \varprojlim_n \sE_{n,1}^+,
where \sU_{n,1} denotes the local units congruent to 1 modulo
\mathfrak{p}_n.
Leopoldt's conjecture, known here by a theorem of Brumer, asserts that \sE_n is
a \Zp-module of rank r_1 + r_2 - 1 = p^{n-1}(p-1)/2; equivalently, global
units that are multiplicatively \Z-independent remain \Zp-independent.
There is an exact sequence of \Lam(\GG^+)-modules
0 \to \sE_{\infty,1}^+ \to \sU_{\infty,1}^+ \to \Gal(\sM_\infty^+/\sL_\infty^+) \to 0.
This uses the unit modules Definition 12.4.2 and the Galois extensions
Definition 12.2.1.
Global class field theory identifies, at each finite level n, the Galois group
\Gal(\sM_n^+/\sL_n^+) with the quotient of the local units modulo the closure
of the global units, giving a short exact sequence
0 \to \sE_{n,1}^+ \to \sU_{n,1}^+ \to \Gal(\sM_n^+/\sL_n^+) \to 0.
All three terms are finitely generated \Zp-modules, so the inverse system
satisfies the Mittag-Leffler condition and \varprojlim_n is exact; taking the
limit over n gives the stated sequence.
There is an exact sequence of \Lam(\GG^+)-modules
0 \to \sE_{\infty,1}^+/\sC_{\infty,1}^+ \to \sU_{\infty,1}^+/\sC_{\infty,1}^+ \to \sX_\infty^+ \to \sY_\infty^+ \to 0,
where \sC_{\infty,1}^+ is the module of cyclotomic units. This rests on
Proposition 12.4.3 and Definition 9.3.1.
The fundamental theorem of Galois theory gives a short exact sequence
0 \to \Gal(\sM_\infty^+/\sL_\infty^+) \to \sX_\infty^+ \to \sY_\infty^+ \to 0,
since F_\infty^+ \subseteq \sL_\infty^+ \subseteq \sM_\infty^+. Splice this with
the sequence of Proposition 12.4.3, identifying the kernel term
\Gal(\sM_\infty^+/\sL_\infty^+) \cong \sU_{\infty,1}^+/\sE_{\infty,1}^+. Dividing
numerator and denominator by the cyclotomic units \sC_{\infty,1}^+ \subseteq \sE_{\infty,1}^+
and applying the third isomorphism theorem rewrites this as
(\sU_{\infty,1}^+/\sC_{\infty,1}^+)\big/(\sE_{\infty,1}^+/\sC_{\infty,1}^+),
yielding the four-term exact sequence.
The remaining input is a result from classical Iwasawa theory relating the
coinvariants of \sY_\infty^+ to finite-level class groups. Set
\sY_n^+ = \Gal(\sL_n^+/F_n^+) \cong \Cl(F_n^+)\otimes_\Z \Zp.
For all n \ge 0, the module of coinvariants of \sY_\infty^+ under
\GG_n^+ = \Gal(F_\infty^+/F_n^+) is
(\sY_\infty^+)_{\GG_n^+} = \sY_n^+.
This refers to Definition 12.2.2.
This is a standard fact of Iwasawa theory (proved in the appendix on the
\mu-invariant). The unramified pro-p tower \sL_\infty^+/F_\infty^+
descends layer by layer: taking \GG_n^+-coinvariants of
\sY_\infty^+ = \Gal(\sL_\infty^+/F_\infty^+) recovers the Galois group of the
maximal unramified abelian p-extension of F_n^+ that is split over the
tower, which by class field theory is the p-part of the class group, i.e.
\sY_n^+. See Theorem 13.2.2.
If p is a Vandiver prime, then
(i) \sY_\infty^+ = 0; (ii) p \nmid h_n^+ for every n \ge 1; and
(iii) \sE_{\infty,1}^+/\sC_{\infty,1}^+ = 0. This uses
Definition 12.4.1, Proposition 12.4.5 and
Definition 9.3.1.
By the displayed isomorphism \sY_n^+ \cong \Cl(F_n^+)\otimes_\Z\Zp, the
condition p \nmid h_n^+ is equivalent to \sY_n^+ = 0.
(i) If p \nmid h_1^+ then (\sY_\infty^+)_{\GG_0^+} = \sY_1^+ = 0 by
Proposition 12.4.5. Since \sY_\infty^+ is a finitely generated
\Lam(\GG^+)-module whose coinvariants vanish, Nakayama's lemma forces
\sY_\infty^+ = 0.
(ii) Vanishing of \sY_\infty^+ and Proposition 12.4.5 give
\sY_n^+ = 0 for all n, i.e. p \nmid h_n^+.
(iii) The classical class-number formula gives
[\sV_n^+ : \sD_n^+] = h_n^+, which is prime to p by (ii); the isomorphism
theorem S/(S\cap N) \cong SN/N shows [\sV_{n,1}^+ : \sD_{n,1}^+] divides
h_n^+, so is also prime to p. Hence \sV_{n,1}^+/\sD_{n,1}^+ is finite of
order prime to p, and tensoring the sequence
0 \to \sD_{n,1}^+ \to \sV_{n,1}^+ \to W_n \to 0 with \Zp kills W_n, giving
\sD_{n,1}^+\otimes_\Z\Zp \cong \sV_{n,1}^+\otimes_\Z\Zp. As \sC_{n,1}^+
(resp. \sE_{n,1}^+) is the p-adic closure of \sD_{n,1}^+ (resp.
\sV_{n,1}^+), the surjections
\sD_{n,1}^+\otimes_\Z\Zp \twoheadrightarrow \sC_{n,1}^+ and
\sV_{n,1}^+\otimes_\Z\Zp \twoheadrightarrow \sE_{n,1}^+ make the inclusion
\sC_{n,1}^+ \hookrightarrow \sE_{n,1}^+ surjective, hence an isomorphism.
Passing to the limit gives \sC_{\infty,1}^+ \cong \sE_{\infty,1}^+.
If p is a Vandiver prime, then there is an isomorphism of
\Lam(\GG^+)-modules
\sX_\infty^+ \cong \Lam(\GG^+)/I(\GG^+)\zeta_p.
In particular the Iwasawa Main Conjecture Theorem 12.3.1
holds. This combines Corollary 12.4.4, Corollary 12.4.6
and Theorem 10.3.4.
Insert the Vandiver vanishing Corollary 12.4.6 (i) and (iii)
into the exact sequence Corollary 12.4.4: the outer terms
\sE_{\infty,1}^+/\sC_{\infty,1}^+ and \sY_\infty^+ both vanish, collapsing the
four-term sequence to an isomorphism
\sU_{\infty,1}^+/\sC_{\infty,1}^+ \xrightarrow{\sim} \sX_\infty^+. Iwasawa's
theorem Theorem 10.3.4 identifies the left-hand side with
\Lam(\GG^+)/I(\GG^+)\zeta_p, giving the displayed isomorphism. Taking
characteristic ideals then proves the Main Conjecture in this case.
Conjecturally every prime is a Vandiver prime, so conjecturally the argument above proves the full Main Conjecture. This conditional proof is due to Iwasawa himself; the first unconditional proof was given by Mazur–Wiles, and a later proof using Euler systems is due to Kolyvagin, Rubin and Thaine.