8.1. The minus class-number criterion
The analytic and p-adic work on the relative class number gives the following
criterion.
Minus class-number criterion. Let p be an odd prime and let K be a
cyclotomic field of conductor p. Then
p\mid h^-(K) \quad\Longleftrightarrow\quad \exists k,\ 1\le k,\ 2k\le p-3,\quad p\mid (B_{2k})_{\mathrm{num}}.
Theorem 6.1.3.2 Theorem 3.4.3.1 Theorem 3.4.1.1 Corollary 3.4.1.2
Lean code for Theorem8.1.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/HMinus/HMinusCriterion.leancomplete
theorem BernoulliRegular.p_dvd_hMinus_iff_p_dvd_some_bernoulli.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd' : p ≠ 2) : p ∣ BernoulliRegular.hMinus K ↔ ∃ k, 1 ≤ k ∧ 2 * k ≤ p - 3 ∧ ↑p ∣ (bernoulli (2 * k)).num
theorem BernoulliRegular.p_dvd_hMinus_iff_p_dvd_some_bernoulli.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd' : p ≠ 2) : p ∣ BernoulliRegular.hMinus K ↔ ∃ k, 1 ≤ k ∧ 2 * k ≤ p - 3 ∧ ↑p ∣ (bernoulli (2 * k)).num
Diekmann Theorem 42: `p` divides the relative class number iff it divides the numerator of one of the relevant even Bernoulli numbers.
Starting from the analytic class-number formula for h^-, one rewrites the
odd-character product in terms of Teichmuller characters. The boundary character
contributes the unique factor containing the pole at p-1; after the explicit
leading factor 2p is included, that boundary contribution is congruent to 1
modulo p. The remaining factors are
-\frac12 B_{1,\omega^j} (1\le j\le p-4, j odd). Kummer congruences replace
these factors modulo p by -\frac12\,\frac{B_{j+1}}{j+1}. Writing j+1=2k, the
range becomes exactly 1\le k and 2k\le p-3. For these indices the denominator of
B_{2k} is prime to p, and so is 2k. Hence the corresponding p-adic factor
is a unit if and only if p does not divide the numerator of B_{2k}. A finite
product in \mathbb{Z}_p is a non-unit if and only if one of its factors is a
non-unit. This identifies p\mid h^-(K) with the existence of a Bernoulli numerator
in the displayed range divisible by p.
We shall also use the contrapositive form of this criterion.
Non-divisibility of h^- gives Bernoulli non-divisibility. If
p\nmid h^-(K), then for every j with 1\le j and 2j\le p-3,
p\nmid (B_{2j})_{\mathrm{num}}.
Lean code for Corollary8.1.2●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/CyclotomicUnits/HMinusCriterion.leancomplete
theorem BernoulliRegular.bernoulli_nonzero_of_not_dvd_hMinus.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) (hminus : ¬p ∣ BernoulliRegular.hMinus K) (k : ℕ) : 1 ≤ k → 2 * k ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * k)).num
theorem BernoulliRegular.bernoulli_nonzero_of_not_dvd_hMinus.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) (hminus : ¬p ∣ BernoulliRegular.hMinus K) (k : ℕ) : 1 ≤ k → 2 * k ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * k)).num
Contrapositive form of `p_dvd_hMinus_iff_p_dvd_some_bernoulli`. For the concrete model `CyclotomicField p ℚ`, use this theorem with `K := CyclotomicField p ℚ` after installing the CM-field instance from `isCMField_of_cyclotomic`. The divisibility statements already have the needed casts: `hMinus` uses `(p : ℕ)`, while Bernoulli numerators use `(p : ℤ)`.
This is the contrapositive of Theorem 8.1.1. If some
Bernoulli numerator in the range were divisible by p, the right-hand side of the
criterion would hold, and therefore p\mid h^-(K).