11.5. End of the proof
We can now assemble the pieces and prove Iwasawa's theorem.
The Coleman map induces: (i) a short exact sequence of \Lam(\GGam)-modules
0 \to \sU_{\infty,1}/\CC_{\infty,1} \to \Lam(\GGam)/I(\GGam)\zeta_p \to \Zp(1) \to 0;
and (ii) an isomorphism of \Lam(\GGam^+)-modules
\sU^+_{\infty,1}/\CC^+_{\infty,1} \xrightarrow{\sim} \Lam(\GGam^+)/I(\GGam^+)\zeta_p.
Part (ii) is the statement of Iwasawa's theorem.
Lean code for Theorem11.5.1●2 theorems
Associated Lean declarations
-
theoremdefined in PadicLFunctions/IwasawaProof/Main.leancomplete
theorem PadicLFunctions.Coleman.iwasawa_theorem (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Nonempty (Additive (↥(PadicLFunctions.Coleman.unitsTower1Plus p) ⧸ (PadicLFunctions.Coleman.cycloTower1Plus p).subgroupOf (PadicLFunctions.Coleman.unitsTower1Plus p)) ≃+ PadicMeasure p (PadicMeasure.GPlus p) ⧸ PadicMeasure.zetaIdealPlus p hp2)
theorem PadicLFunctions.Coleman.iwasawa_theorem (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Nonempty (Additive (↥(PadicLFunctions.Coleman.unitsTower1Plus p) ⧸ (PadicLFunctions.Coleman.cycloTower1Plus p).subgroupOf (PadicLFunctions.Coleman.unitsTower1Plus p)) ≃+ PadicMeasure p (PadicMeasure.GPlus p) ⧸ PadicMeasure.zetaIdealPlus p hp2)
**RJW thm:iwasawa 2 (ii) — THE MILESTONE (TeX 3592–3593)**: the Coleman map induces an isomorphism of `Λ(𝒢^+)`-modules `𝒰_{∞,1}^+/𝒞_{∞,1}^+ ≅ Λ(𝒢^+)/I(𝒢^+)ζ_p`. This is `thm:iwasawa` (stated, then unwired, in the §11 chapter), now proved. Stated as the existence of a `Λ(𝒢^+)`-linear (here `ℤ_[p]`-linear placeholder; the `Λ(𝒢^+)`-structure on the quotient is wired at execution) isomorphism between the two quotients. -
theoremdefined in PadicLFunctions/IwasawaProof/Main.leancomplete
theorem PadicLFunctions.Coleman.iwasawa_exact_sequence (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Nonempty (Additive (↥(PadicLFunctions.Coleman.unitsTower1 p) ⧸ (PadicLFunctions.Coleman.cycloTower1 p).subgroupOf (PadicLFunctions.Coleman.unitsTower1 p)) →+ PadicMeasure p ℤ_[p]ˣ ⧸ PadicMeasure.zetaIdeal p hp2)
theorem PadicLFunctions.Coleman.iwasawa_exact_sequence (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Nonempty (Additive (↥(PadicLFunctions.Coleman.unitsTower1 p) ⧸ (PadicLFunctions.Coleman.cycloTower1 p).subgroupOf (PadicLFunctions.Coleman.unitsTower1 p)) →+ PadicMeasure p ℤ_[p]ˣ ⧸ PadicMeasure.zetaIdeal p hp2)
**RJW thm:iwasawa 2 (i) (TeX 3590–3591)**: the `Λ(𝒢)`-module short exact sequence `0 → 𝒰_{∞,1}/𝒞_{∞,1} → Λ(𝒢)/I(𝒢)ζ_p → ℤ_p(1) → 0`. Stated as the injection `𝒰_{∞,1}/𝒞_{∞,1} ↪ Λ(𝒢)/I(𝒢)ζ_p` with cokernel `ℤ_p(1)` (the `χ`-moment).
Start from the fundamental exact sequence
0\to\Zp(1)\to\sU_{\infty,1}\xrightarrow{\Col}\Lam(\GGam)\to\Zp(1)\to 0 of
Theorem 11.2.10. It remains to compute the image of the
cyclotomic units. By Lemma 11.4.3 it suffices to evaluate \Col on
(\xi_{p^n}^b\gamma_{n,a})_n for a,b\in\Zpx. Since \xi_{p^n}^b lies in the
kernel of \Col (it sits in the \mu_{p-1}\times\Zp(1) factor) and
\gamma_{n,a}=\xi_{p^n}^{(1-a)/2}c_n(a), this reduces to \Col(c(a)), which by the
Coleman computation of \zeta_p equals ([\sigma_a]-[1])\zeta_p, depending on
Definition 4.3.2. As a ranges over \Zpx, the elements
[\sigma_a]-[1] generate the augmentation ideal, so the image of \CC_{\infty,1}
(resp. \CC_{\infty,1}^+) is I(\GGam)\zeta_p (resp. I(\GGam^+)\zeta_p), depending
on Proposition 10.2.1. Quotienting the fundamental sequence by this image
gives the exact sequence
0\to\sU_{\infty,1}/\CC_{\infty,1}\to\Lam(\GGam)/I(\GGam)\zeta_p\to\Zp(1)\to 0,
which is (i). For (ii), take invariants under the order-two group
\ang{c}\subset\GGam generated by complex conjugation. As p is odd this functor
is exact, and c acts on \Zp(1) by -1, so \Zp(1)^{\ang c}=0; the sequence
collapses to the isomorphism
\sU_{\infty,1}^+/\CC_{\infty,1}^+\xrightarrow{\sim}\Lam(\GGam^+)/I(\GGam^+)\zeta_p.