8.3. The total class number
Recall from Theorem 1.6.4 that h(K)=h^+(K)\,h^-(K). The previous
corollary lets us reduce divisibility of the total class number to divisibility of
the minus class number.
Total class-number divisibility. For odd p, assume that
p\mid h^+(K)\Longrightarrow p\mid h^-(K). Then
p\mid h(K) \quad\Longleftrightarrow\quad p\mid h^-(K).
Lean code for Theorem8.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/CyclotomicUnits/ClassNumber.leancomplete
theorem BernoulliRegular.dvd_h_iff_dvd_hMinus_of_dvd_hPlus_imp.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hplus_to_hminus : p ∣ BernoulliRegular.hPlus K → p ∣ BernoulliRegular.hMinus K) : p ∣ BernoulliRegular.h K ↔ p ∣ BernoulliRegular.hMinus K
theorem BernoulliRegular.dvd_h_iff_dvd_hMinus_of_dvd_hPlus_imp.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hplus_to_hminus : p ∣ BernoulliRegular.hPlus K → p ∣ BernoulliRegular.hMinus K) : p ∣ BernoulliRegular.h K ↔ p ∣ BernoulliRegular.hMinus K
If the cyclotomic-unit route proves `p ∣ hPlus K → p ∣ hMinus K`, then the total class-number divisibility condition is equivalent to relative class-number divisibility. The canonical class-number API used here is: * `h K` from `BernoulliRegular/TotallyRealSubfield/Basic.lean`; * `hPlus K` from `BernoulliRegular/TotallyRealSubfield/Basic.lean`; * `hMinus K` from `BernoulliRegular/TotallyRealSubfield/ClassGroup.lean`; * `h_eq_hPlus_mul_hMinus` from `BernoulliRegular/TotallyRealSubfield/ClassGroup.lean`.
The implication from right to left is immediate from h(K)=h^+(K)h^-(K).
Conversely, suppose p\mid h(K). Since h(K)=h^+(K)h^-(K) and p is prime,
Euclid's lemma gives p\mid h^+(K) or p\mid h^-(K). In the second case we are
done. In the first case, the assumed implication converts p\mid h^+(K) into
p\mid h^-(K). Thus p\mid h^-(K) in all cases.
Total class number and Bernoulli numerators. For odd p,
p\mid h(K) \quad\Longleftrightarrow\quad \exists k,\ 1\le k,\ 2k\le p-3,\quad p\mid (B_{2k})_{\mathrm{num}}.
Lean code for Theorem8.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/CyclotomicUnits/UnitsReflection.leancomplete
theorem BernoulliRegular.dvd_h_iff_exists_dvd_bernoulli_units {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) : p ∣ BernoulliRegular.h K ↔ ∃ k, 1 ≤ k ∧ 2 * k ≤ p - 3 ∧ ↑p ∣ (bernoulli (2 * k)).num
theorem BernoulliRegular.dvd_h_iff_exists_dvd_bernoulli_units {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) : p ∣ BernoulliRegular.h K ↔ ∃ k, 1 ≤ k ∧ 2 * k ≤ p - 3 ∧ ↑p ∣ (bernoulli (2 * k)).num
The total class-number divisibility criterion obtained from the cyclotomic-unit weak-reflection route.
Apply Theorem 8.3.1 with the implication supplied by
Corollary 8.2.2. This replaces p\mid h(K) by p\mid h^-(K).
Then apply the minus class-number criterion Theorem 8.1.1,
which replaces p\mid h^-(K) by the existence of a divisible Bernoulli numerator in
Kummer's range.