4.2. The Stickelberger element🔗

Definition4.2.1

uses 1used by 1✓L∃∀N

The Stickelberger element is \theta \;=\; \sum_{a \in (\mathbb{Z}/p\mathbb{Z})^\times} \Bigl\langle \frac{a}{p} \Bigr\rangle\,\sigma_a^{-1} \;\in\; \mathbb{Q}\bigl[(\mathbb{Z}/p\mathbb{Z})^\times\bigr], where \langle x \rangle = x-\lfloor x\rfloor denotes the fractional part, and \sigma_a is the automorphism sending \zeta_p\mapsto\zeta_p^a. Multiplying by the appropriate denominator gives the usual integral Stickelberger ideal.

Definition 2.2.1

Lean code for Definition4.2.1●1 definition

defdefined in BernoulliRegular/Stickelberger.lean

complete

def BernoulliRegular.stickelbergerElement (p : ℕ)
  [hp : Fact (Nat.Prime p)] : MonoidAlgebra ℚ (ZMod p)ˣ

def BernoulliRegular.stickelbergerElement
  (p : ℕ) [hp : Fact (Nat.Prime p)] :
  MonoidAlgebra ℚ (ZMod p)ˣ

The Stickelberger element `θ_p ∈ ℚ[(ZMod p)ˣ]`:
`θ_p := (1/p) · ∑_{a ∈ (ZMod p)ˣ} (a.val : ℚ) • single a⁻¹ 1`.

Theorem4.2.2

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

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

used by 1✓L∃∀N

Stickelberger's theorem. The integral Stickelberger ideal I_\theta \subset \mathbb{Z}[(\mathbb{Z}/p\mathbb{Z})^\times] annihilates the class group of \mathbb{Q}(\zeta_p): for any prime \mathfrak l \nmid p and any \beta \in I_\theta, the ideal \mathfrak l^\beta is principal.

Definition 4.2.1 Definition 4.1.1

Lean code for Theorem4.2.2●1 theorem

theoremdefined in BernoulliRegular/Stickelberger/Annihilation.lean

complete

theorem BernoulliRegular.stickelbergerCharacterCoefficientGroupRingTarget_annihilates_primeClass.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L]
  [NumberField L] [IsCyclotomicExtension {p * (p - 1)} ℚ L]
  (hp_odd : p ≠ 2) {χ : DirichletCharacter ℂ p} (hχ : χ ≠ 1) :
  BernoulliRegular.characterSideStickelbergerClassAction p L
      (BernoulliRegular.stickelbergerCharacterCoefficientGroupRingTarget
        p L χ) =
    1

theorem BernoulliRegular.stickelbergerCharacterCoefficientGroupRingTarget_annihilates_primeClass.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (L : Type u_1) [Field L] [NumberField L]
  [IsCyclotomicExtension {p * (p - 1)} ℚ
      L]
  (hp_odd : p ≠ 2)
  {χ : DirichletCharacter ℂ p}
  (hχ : χ ≠ 1) :
  BernoulliRegular.characterSideStickelbergerClassAction
      p L
      (BernoulliRegular.stickelbergerCharacterCoefficientGroupRingTarget
        p L χ) =
    1

`T032c`: the character-side Stickelberger exponent supplied by the
Gauss-sum factorisation annihilates the distinguished-prime class.

Proof for Theorem 4.2.2

uses 0

One first proves the ideal factorisation of Gauss sums: for a non-trivial character \chi, the principal ideal generated by \tau(\chi) has factorisation prescribed by the Stickelberger exponent. Since a principal ideal represents the trivial class, the corresponding group-ring exponent annihilates the class of every prime above a rational prime \ell\ne p. Such prime classes generate the ideal class group, so every element of the integral Stickelberger ideal annihilates the full class group.