10.2. The ideal generated by the p-adic zeta function🔗

It is natural to ask about the zeros of \zeta_p. As multiplying a measure by a unit does not change its zeros, studying the zeros of a measure on \GG is the same as studying the ideal it generates in \Lam(\GG). Although \zeta_p is only a pseudo-measure, and hence not itself an element of \Lam(\GG), it still generates a natural ideal.

Recall the augmentation ideal I(\GG) = \ker\big(\Lam(\GG) \to \Zp\big), where the augmentation map \Lam(\GG) \twoheadrightarrow \Zp is induced by [g] \mapsto 1 for every g \in \GG; equivalently, I(\GG) is the topological ideal generated by the elements [g] - [1], g \in \GG. The ideal I(\GG^+) is defined the same way. By the defining property of a pseudo-measure, ([g]-[1])\zeta_p \in \Lam(\GG) for every g \in \GG.

Proposition10.2.1

Statement uses 3

Statement dependency previews

Preview

Definition 3.6.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

Used by 3

Reverse dependency previews

Preview

Theorem 10.3.4

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

The module I(\GG)\,\zeta_p is an ideal of \Lam(\GG), and likewise I(\GG^+)\,\zeta_p is an ideal of \Lam(\GG^+). This uses the pseudo-measure property of \zeta_p and Corollary 10.1.4.

Lean code for Proposition10.2.1●5 declarations

defdefined in PadicLFunctions/Iwasawa/ZetaGalois.lean

complete

def PadicMeasure.zetaIdeal (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) :
  Ideal (PadicMeasure p ℤ_[p]ˣ)

def PadicMeasure.zetaIdeal (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  Ideal (PadicMeasure p ℤ_[p]ˣ)

**`I(𝒢)ζ_p`** (RJW Proposition, TeX 3052): the set of measures of the form
`λ·ζ_p` with `λ` in the augmentation ideal — an ideal of `Λ(𝒢)` by the
pseudo-measure property (the ideal axioms hold directly; the `Ideal.span`
description below is the computational form).

defdefined in PadicLFunctions/Iwasawa/ZetaGalois.lean

complete

def PadicMeasure.zetaIdealPlus (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) : Ideal (PadicMeasure p (PadicMeasure.GPlus p))

def PadicMeasure.zetaIdealPlus (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  Ideal
    (PadicMeasure p
      (PadicMeasure.GPlus p))

**`I(𝒢⁺)ζ_p`** (RJW Proposition, TeX 3052, plus half): the corresponding ideal
of `Λ(𝒢⁺)` — the right-hand side of Iwasawa's theorem (`thm:iwasawa`, stated on the
§12 board).

theoremdefined in PadicLFunctions/Iwasawa/ZetaGalois.lean

complete

theorem PadicMeasure.zetaIdeal_eq_span (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {b : ℤ_[p]ˣ}
  (hb :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) b) = ⊤)
  {ν : PadicMeasure p ℤ_[p]ˣ}
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
          (PadicMeasure.dirac p b - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  PadicMeasure.zetaIdeal p hp2 = Ideal.span {ν}

theorem PadicMeasure.zetaIdeal_eq_span (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2)
  {b : ℤ_[p]ˣ}
  (hb :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            b) =
        ⊤)
  {ν : PadicMeasure p ℤ_[p]ˣ}
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ)
            (PadicMeasure.QuotientField
              p))
          (PadicMeasure.dirac p b - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  PadicMeasure.zetaIdeal p hp2 =
    Ideal.span {ν}

The computational description: `I(𝒢)ζ_p` is the principal ideal generated by any
witness of `([b]−[1])·ζ_p` at a topological generator `b` (via the principality
`augmentationIdeal_eq_span`).

theoremdefined in PadicLFunctions/Iwasawa/ZetaGalois.lean

complete

theorem PadicMeasure.zetaIdealPlus_eq_span (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤)
  {ν : PadicMeasure p ℤ_[p]ˣ}
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
          (PadicMeasure.dirac p a - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  PadicMeasure.zetaIdealPlus p hp2 =
    Ideal.span {(PadicMeasure.projPlus p) ν}

theorem PadicMeasure.zetaIdealPlus_eq_span (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2)
  {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤)
  {ν : PadicMeasure p ℤ_[p]ˣ}
  (hν :
    (algebraMap (PadicMeasure p ℤ_[p]ˣ)
            (PadicMeasure.QuotientField
              p))
          (PadicMeasure.dirac p a - 1) *
        PadicMeasure.padicZeta p hp2 =
      (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        ν) :
  PadicMeasure.zetaIdealPlus p hp2 =
    Ideal.span
      {(PadicMeasure.projPlus p) ν}

theoremdefined in PadicLFunctions/Iwasawa/ZetaGalois.lean

complete

theorem PadicMeasure.augmentationIdealPlus_eq_span (p : ℕ)
  [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers ((PadicMeasure.unitsToZModPow p n) a) = ⊤) :
  PadicMeasure.augmentationIdeal p =
    Ideal.span {PadicMeasure.dirac p ↑a - 1}

theorem PadicMeasure.augmentationIdealPlus_eq_span
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) {a : ℤ_[p]ˣ}
  (ha :
    ∀ (n : ℕ),
      Subgroup.zpowers
          ((PadicMeasure.unitsToZModPow p
              n)
            a) =
        ⊤) :
  PadicMeasure.augmentationIdeal p =
    Ideal.span
      {PadicMeasure.dirac p ↑a - 1}

The image `ā` of a topological generator generates the augmentation ideal of
`Λ(𝒢⁺)`: `I(𝒢⁺) = ([ā]−[1])·Λ(𝒢⁺)` (transport of `augmentationIdeal_eq_span`
along the surjection `π_*`, using `deg⁺ ∘ π_* = deg`).

Proof for Proposition 10.2.1

uses 0

Since \zeta_p is a pseudo-measure, each product ([g]-[1])\zeta_p lies in \Lam(\GG). As I(\GG) is the topological ideal generated by the elements [g]-[1], the set I(\GG)\zeta_p is closed under multiplication by \Lam(\GG) and is therefore an ideal. The identical argument over \GG^+, using that \zeta_p is a pseudo-measure on \GG^+, shows I(\GG^+)\zeta_p is an ideal of \Lam(\GG^+).