An introduction to p-adic L-functions — Lean blueprint

10.3. Cyclotomic units and Iwasawa's theorem🔗

Iwasawa's theorem describes the ideal I(\GG)\zeta_p in terms of the module of cyclotomic units. We recall this module and its classical link to class numbers, and then state the theorem.

Definition10.3.1
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 10.3.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

For n \ge 1, the group \DD_n of cyclotomic units of F_n is the intersection of \cO_{F_n}^\times with the multiplicative subgroup of F_n^\times generated by \set{\pm\xi_{p^n},\ \xi_{p^n}^a - 1 : 1 \le a \le p^n - 1}, where \xi_{p^n} is a primitive p^n-th root of unity. We set \DD_n^+ = \DD_n \cap F_n^+.

Lean code for Definition10.3.1●5 definitions
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.Fglobal (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : IntermediateField ℚ ℂ_[p]
    def PadicLFunctions.Coleman.Fglobal (p : ℕ)
  [hp : Fact (Nat.Prime p)] (n : ℕ) :
  IntermediateField ℚ ℂ_[p]
    `F_n = ℚ(μ_{p^n})`, inside `ℂ_[p]` (RJW TeX 2471).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.FglobalPlus (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : IntermediateField ℚ ℂ_[p]
    def PadicLFunctions.Coleman.FglobalPlus
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : IntermediateField ℚ ℂ_[p]
    `F_n⁺ = ℚ(ξ_{p^n} + ξ_{p^n}⁻¹)`: the maximal totally real subfield, rendered by
its standard concrete generator (RJW TeX 2471/2475).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.globalUnits (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.globalUnits
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    `𝒱_n = 𝒪_{F_n}^×`: the global units — units of `ℂ_[p]` lying in `F_n`,
integral over `ℤ` together with their inverses (RJW TeX 2472).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloUnits (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.cycloUnits (p : ℕ)
  [hp : Fact (Nat.Prime p)] (n : ℕ) :
  Subgroup ℂ_[p]ˣ
    **RJW Definition (TeX 3065–3067)**: the group `𝒟_n` of cyclotomic units of
`F_n` — the intersection of `𝒪_{F_n}^×` with the multiplicative subgroup of `F_n^×`
generated by `±ξ_{p^n}` and the `ξ_{p^n}^a − 1` (the generators all lie in `F_n`,
so closing inside `ℂ_[p]ˣ` is the same as closing inside `F_n^×`).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloUnitsPlus (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.cycloUnitsPlus
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    `𝒟_n⁺ = 𝒟_n ∩ F_n⁺` (RJW TeX 3066).

The cyclotomic units are connected to class numbers as follows.

Theorem10.3.2
uses 1used by 0XL∃∀N

Let n \ge 1. The group \DD_n (resp. \DD_n^+) has finite index in the unit group \VV_n (resp. \VV_n^+) of F_n (resp. F_n^+), and h_n^+ = [\VV_n : \DD_n] = [\VV_n^+ : \DD_n^+], where h_n^+ = \#\Cl(F_n^+) is the class number of F_n^+. This uses Definition 10.3.1.

Proof for Theorem 10.3.2
uses 1

We do not reprove this here; see (Washington, 1997, Theorem 8.2). The argument computes the regulator of the cyclotomic units \DD_n^+ as a determinant of logarithms of 1-\xi_{p^n}^a, which by Dirichlet's class number formula is expressed through the special values at s = 1 of the Dirichlet L-functions of the even characters of \Gal(F_n^+/\Q). Comparing this with the analytic class number formula for F_n^+, whose regulator is that of the full unit group \VV_n^+, the two regulators differ exactly by the index [\VV_n^+ : \DD_n^+], which therefore equals the class number h_n^+.

As explained in the construction of the Coleman map, the cyclotomic units c_n(a) used to build \zeta_p are naturally elements of \DD_n, hence global; one then takes their image in the local units and applies the (purely local) Coleman map. In the same spirit we now pass from the global modules \DD_n, \DD_n^+ to their closures inside the local units. (Formalised: the \DD_n-membership of c_n(a) is PadicLFunctions.Coleman.cyclo_elems_mem_cycloUnits, unconditional in a coprime to p; its norm-compatible tower lies in \CC_{\infty,1} — PadicLFunctions.Coleman.cyclo_mem_cycloTower1 — under the additional hypothesis a \equiv 1 \bmod p, since c_n(a) \equiv a \bmod \pri_n is a principal unit only then; the principal-unit normalisation for general a is part of the next chapter's fundamental exact sequence.) Recall that \UU_{\infty,1}^+ denotes the group of norm-compatible local units congruent to 1 \bmod p.

Definition10.3.3
uses 1used by 1✓L∃∀N

For n \ge 1, let \CC_n be the p-adic closure of \DD_n inside the local units \UU_n, set \CC_n^+ = \CC_n \cap \UU_n^+, and define \CC_{n,1} = \CC_n \cap \UU_{n,1}, \qquad \CC_{n,1}^+ = \CC_n^+ \cap \UU_{n,1}. Passing to the inverse limit over the norm maps, set \CC_{\infty,1} = \varprojlim_{n \ge 1}\CC_{n,1}, \qquad \CC_{\infty,1}^+ = \varprojlim_{n \ge 1}\CC_{n,1}^+. This is the local avatar of Definition 10.3.1.

Lean code for Definition10.3.3●6 definitions
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloClosure (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.cycloClosure
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    **RJW Definition (TeX 3090)**: `𝒞_n` — the p-adic closure of `𝒟_n` inside the
local units `𝒰_n` (topological closure in the topological group `ℂ_[p]ˣ`,
intersected into `𝒰_n`; since `𝒟_n ≤ 𝒰_n` and `𝒰_n` is closed, this is the honest
subspace closure — the explicit description is `lem:closure`, §12).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloClosureOne (p : ℕ)
  [hp : Fact (Nat.Prime p)] (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.cycloClosureOne
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    `𝒞_{n,1} = 𝒞_n ∩ 𝒰_{n,1}` (RJW TeX 3091).
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloTower1 (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Subgroup (PadicLFunctions.Coleman.NormCompatUnits p)
    def PadicLFunctions.Coleman.cycloTower1
  (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Subgroup
    (PadicLFunctions.Coleman.NormCompatUnits
      p)
    `𝒞_{∞,1} = lim←_{n≥1} 𝒞_{n,1}` (RJW TeX 3092), as a subgroup of `𝒰_∞`.
  • defdefined in PadicLFunctions/Iwasawa/CyclotomicUnits.lean
    complete
    def PadicLFunctions.Coleman.cycloTower1Plus (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  Subgroup (PadicLFunctions.Coleman.NormCompatUnits p)
    def PadicLFunctions.Coleman.cycloTower1Plus
  (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Subgroup
    (PadicLFunctions.Coleman.NormCompatUnits
      p)
    `𝒞⁺_{∞,1} = lim←_{n≥1} 𝒞⁺_{n,1}` (RJW TeX 3092).
  • defdefined in PadicLFunctions/Iwasawa/LocalUnits.lean
    complete
    def PadicLFunctions.Coleman.unitsTower1 (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Subgroup (PadicLFunctions.Coleman.NormCompatUnits p)
    def PadicLFunctions.Coleman.unitsTower1
  (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Subgroup
    (PadicLFunctions.Coleman.NormCompatUnits
      p)
    `𝒰_{∞,1} = lim←_{n≥1} 𝒰_{n,1}`: the norm-compatible systems through the
principal units (RJW Eq. (`eq:Uinfty 1`), TeX 2503; the `n ≥ 1` convention matches
the `compat` field's).
  • defdefined in PadicLFunctions/Iwasawa/LocalUnits.lean
    complete
    def PadicLFunctions.Coleman.localUnitsOne (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    def PadicLFunctions.Coleman.localUnitsOne
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (n : ℕ) : Subgroup ℂ_[p]ˣ
    `𝒰_{n,1} = {u ∈ 𝒰_n : u ≡ 1 (mod 𝔭_n)}`: the principal units, with the
congruence rendered as `‖u − 1‖ < 1` (replan R11.6). RJW Eq. (`eq:U1`), TeX 2494.

The module \UU_{\infty,1}^+, and its quotient \UU_{\infty,1}^+/\CC_{\infty,1}^+, carry natural \Lam(\GG^+)-module structures. Iwasawa related this quotient explicitly to the p-adic zeta function: the cyclotomic units capture exactly the zeros of \zeta_p. This is the theorem that ultimately motivated his Main Conjecture.

Theorem10.3.4
Statement uses 3
Statement dependency previews
Preview
Definition 9.5.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Theorem 11.5.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

The Coleman map induces an isomorphism of \Lam(\GG^+)-modules \UU_{\infty,1}^+ / \CC_{\infty,1}^+ \xrightarrow{\sim} \Lam(\GG^+) / I(\GG^+)\,\zeta_p. This rests on the Coleman map, the ideal I(\GG^+)\zeta_p, and the local cyclotomic units Definition 10.3.3.

Lean code for Theorem10.3.4●1 theorem
  • theoremdefined in PadicLFunctions/IwasawaProof/Main.lean
    complete
    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.
Proof for Theorem 10.3.4
Proof uses 5
Proof dependency previews
Preview
Definition 9.3.1
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

The proof is carried out in the next chapter; we sketch its spine. By equivariance of the Coleman map the map \Col : \UU_{\infty,1} \to \Lam(\GG) is a homomorphism of \Lam(\GG)-modules, where the \GG-equivariance hinges on the renormalising twist by 1 built into \zeta_p. The fundamental exact sequence 0 \to \Zp(1) \to \UU_{\infty,1} \xrightarrow{\Col} \Lam(\GG) \to \Zp(1) \to 0 identifies the cokernel of \Col with \Zp(1), the map to it being \mu \mapsto \int_\GG\chi\,d\mu. Passing to the plus parts (legitimate since p is odd, by Lemma 10.1.1) yields an injection \UU_{\infty,1}^+ \hookrightarrow \Lam(\GG^+) whose cokernel is computed by the augmentation map. On the local cyclotomic units the Coleman map reproduces exactly the construction of \zeta_p out of the cyclotomic units c_n(a), so \Col(\CC_{\infty,1}^+) is precisely the ideal I(\GG^+)\zeta_p. Therefore \Col descends to the displayed isomorphism \UU_{\infty,1}^+/\CC_{\infty,1}^+ \xrightarrow{\sim} \Lam(\GG^+)/I(\GG^+)\zeta_p of quotient \Lam(\GG^+)-modules.

The quotient \UU_{\infty,1}^+/\CC_{\infty,1}^+ is the infinite-level local analogue of the cyclotomic units inside the global units, whose indices compute class numbers in the cyclotomic tower. These modules are in turn related to the Galois modules appearing in the Iwasawa Main Conjecture. This theorem is thus the first step towards the deep connection between class groups and the p-adic zeta function expressed by the Main Conjecture.