7.6. Bernoulli non-divisibility and the plus index
The previous sections combine into the theorem used by the final proof.
Bernoulli non-divisibility implies index non-divisibility. Assume p is odd and
\forall j,\quad 1\le j,\ 2j\le p-3 \Longrightarrow p\nmid (B_{2j})_{\mathrm{num}}.
Then p\nmid [E^+:C^+_{\mathrm{sq}}].
Lean code for Theorem7.6.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/CyclotomicUnits/UnitsReflection.leancomplete
theorem BernoulliRegular.not_dvd_cyclotomicUnitIndex_of_bernoulli_nonzero {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) (hB : ∀ (j : ℕ), 1 ≤ j → 2 * j ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * j)).num) : ¬p ∣ (BernoulliRegular.CPlus ⋯).index
theorem BernoulliRegular.not_dvd_cyclotomicUnitIndex_of_bernoulli_nonzero {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_odd : p ≠ 2) (hB : ∀ (j : ℕ), 1 ≤ j → 2 * j ≤ p - 3 → ¬↑p ∣ (bernoulli (2 * j)).num) : ¬p ∣ (BernoulliRegular.CPlus ⋯).index
CU-16: Bernoulli numerator nonvanishing in the classical range implies that `p` does not divide the real cyclotomic-unit index.
If p=3, then the generator range is empty. The real subfield of
\mathbb{Q}(\zeta_3) is \mathbb{Q}, so its unit group is generated by -1.
Hence C^+_{\mathrm{sq}}=E^+ and the index is 1, which is not divisible by p.
Now assume p\ge5. The Bernoulli non-divisibility hypothesis makes the Kummer
logarithm determinant nonzero by Theorem 7.5.1. The
determinant non-vanishing theorem Theorem 7.5.2 gives
p-saturation of C^+_{\mathrm{sq}} in E^+. Finally
Theorem 7.4.1 converts this saturation into
p\nmid [E^+:C^+_{\mathrm{sq}}].