8.2. The plus-to-minus divisibility step🔗

The cyclotomic-unit theorem from the previous chapter turns the contrapositive of the minus criterion into a statement about h^+.

Theorem8.2.1

Statement uses 4

Statement dependency previews

Preview

Lemma 7.2.4

Loading preview

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

used by 1✓L∃∀N

Contrapositive plus-to-minus divisibility. Let p be an odd prime and let K be a cyclotomic field of conductor p. If p\nmid h^-(K), then p\nmid h^+(K).

Corollary 8.1.2 Theorem 7.6.1 Theorem 7.7.6 Lemma 7.2.4

Lean code for Theorem8.2.1●1 theorem

theoremdefined in BernoulliRegular/CyclotomicUnits/UnitsReflection.lean

complete

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

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

CU-17: contrapositive weak reflection from the cyclotomic-unit route.

Proof for Theorem 8.2.1

uses 0

Assume p\nmid h^-(K). By Corollary 8.1.2, all Bernoulli numerators (B_{2j})_{\mathrm{num}} in Kummer's range are prime to p. The cyclotomic-unit theorem Theorem 7.6.1 therefore gives p\nmid [E^+:C^+_{\mathrm{sq}}]. Suppose, for contradiction, that p\mid h^+(K). The prime-conductor cyclotomic-unit index theorem Theorem 7.7.6 gives p\mid [E^+:C^+_{\mathrm{norm}}]. By the odd-primary comparison of the two cyclotomic-unit subgroups, Lemma 7.2.4, this is equivalent to p\mid [E^+:C^+_{\mathrm{sq}}], contradicting the index non-divisibility already obtained. Hence p\nmid h^+(K).

Corollary8.2.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 8.3.1

Loading preview

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

✓L∃∀N

Plus divisibility implies minus divisibility. If p\mid h^+(K), then p\mid h^-(K).

Theorem 8.2.1

Lean code for Corollary8.2.2●1 theorem

theoremdefined in BernoulliRegular/CyclotomicUnits/UnitsReflection.lean

complete

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

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

CU-18: weak reflection by contrapositive from the cyclotomic-unit route.

Proof for Corollary 8.2.2

uses 0

Argue by contradiction. If p\nmid h^-(K), then Theorem 8.2.1 gives p\nmid h^+(K), contradicting the hypothesis. Therefore p\mid h^-(K).