10.4. From reflection to class numbers🔗

Theorem10.4.1

uses 1used by 0✓L∃∀N

Reflection-route plus-to-minus implication. For an odd prime p, p\mid h^+(K)\Longrightarrow p\mid h^-(K).

Lean code for Theorem10.4.1●1 theorem

theoremdefined in BernoulliRegular/Reflection/FinalReflection/Part2.lean

complete

theorem BernoulliRegular.weakReflection_dvd_hMinus_of_dvd_hPlus.{u} (p : ℕ)
  [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] (hplus : p ∣ BernoulliRegular.hPlus K) :
  p ∣ BernoulliRegular.hMinus K

theorem BernoulliRegular.weakReflection_dvd_hMinus_of_dvd_hPlus.{u}
  (p : ℕ) [Fact (Nat.Prime p)]
  (hp_odd : p ≠ 2) (K : Type u) [Field K]
  [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hplus : p ∣ BernoulliRegular.hPlus K) :
  p ∣ BernoulliRegular.hMinus K

**Weak reflection, class-number consequence.**

For the cyclotomic field `K = Q(zeta_p)`, divisibility of the plus relative
class number by `p` forces divisibility of the minus relative class number by
`p`. This is the form consumed by Kummer's criterion.
The only reflection input is `weakReflection_componentNontrivial`.

Proof for Theorem 10.4.1

uses 0

Assume p\mid h^+(K) and p\nmid h^-(K). Since h(K)=h^+(K)h^-(K), the first assumption implies p\mid h(K), so the group A is nonzero. Decompose A into character components and choose a nonzero component A_k. The assumption p\nmid h^-(K) says that complex conjugation acts trivially on the relevant mod-p class group. Therefore no odd component can be nonzero. The zero component is also trivial, as in the boundary argument above. Hence the chosen nonzero component is even and nonzero. Component reflection gives a nonzero reflected component, but the reflected index is odd, contradicting the trivial action of complex conjugation. Thus p\nmid h^-(K) is impossible.

Once the plus-to-minus implication is known, the reflection route also recovers the same class-number criterion as the main proof: (p:\mathbb{N})\mid h(K) \quad\Longleftrightarrow\quad \exists k,\ 1\le k,\ 2k\le p-3,\quad (p:\mathbb{Z})\mid (B_{2k})_{\mathrm{num}}. Indeed, by the factorisation h(K)=h^+(K)h^-(K), divisibility of h(K) by the prime p means that p divides either h^+(K) or h^-(K). The plus-to-minus implication transfers the first case to the second. Thus p\mid h(K)\Longleftrightarrow p\mid h^-(K). The minus class-number criterion identifies the latter condition with Bernoulli numerator divisibility in Kummer's range.