4.3. Herbrand's theorem🔗

Herbrand's theorem converts Stickelberger annihilation into a divisibility statement for generalised Bernoulli numbers.

Theorem4.3.1

Statement uses 3

Statement dependency previews

Preview

Definition 2.3.1

Loading preview

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

used by 0✓L∃∀N

Herbrand bridge. Let \chi be an odd Dirichlet character modulo p. If the \chi-eigenspace \mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)})[p]^\chi of the p-part of the class group is non-trivial, then p \mid B_{1,\chi}.

Theorem 4.2.2 Definition 3.1.1 Definition 2.3.1

Lean code for Theorem4.3.1●1 theorem

theoremdefined in BernoulliRegular/Herbrand/Basic.lean

complete

theorem BernoulliRegular.generalizedBernoulliPDivisible_of_nontrivial_oddComponent.{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) {χ : MulChar (ZMod p)ˣ ℚ}
  (hχ_odd : BernoulliRegular.IsOddUnitCharacter p χ)
  (C : BernoulliRegular.CyclotomicClassGroupPSylowComponent p L)
  (hC : C.character = χ)
  (bridge : BernoulliRegular.OddComponentHerbrandBridge p L hp_odd χ C)
  (hC_nontrivial : BernoulliRegular.OddComponentNontrivial p L C) :
  BernoulliRegular.GeneralizedBernoulliPDivisible p χ

theorem BernoulliRegular.generalizedBernoulliPDivisible_of_nontrivial_oddComponent.{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)
  {χ : MulChar (ZMod p)ˣ ℚ}
  (hχ_odd :
    BernoulliRegular.IsOddUnitCharacter p
      χ)
  (C :
    BernoulliRegular.CyclotomicClassGroupPSylowComponent
      p L)
  (hC : C.character = χ)
  (bridge :
    BernoulliRegular.OddComponentHerbrandBridge
      p L hp_odd χ C)
  (hC_nontrivial :
    BernoulliRegular.OddComponentNontrivial
      p L C) :
  BernoulliRegular.GeneralizedBernoulliPDivisible
    p χ

`T035a`: for a declared odd component, the Herbrand bridge turns the
`T034c` Bernoulli annihilation certificate and nontriviality of the component
into `p`-adic divisibility of `B_{1,χ⁻¹}`.

Proof for Theorem 4.3.1

uses 0

Project the Stickelberger annihilation relation to the \chi-eigenspace. On that eigenspace the Stickelberger element acts by the scalar B_{1,\chi}, up to the standard nonzero normalising factor. If the \chi-component of the p-class group is non-trivial, a scalar that annihilates it must be divisible by p; otherwise it would be a unit on the \mathbb{F}_p-component and could not kill a nonzero element. Hence p\mid B_{1,\chi}.