7.4. From saturation to index non-divisibility
Saturation forbids p in the index. If C^+_{\mathrm{sq}} is p-saturated in
E^+, then p\nmid [E^+:C^+_{\mathrm{sq}}].
Lean code for Theorem7.4.1●3 theorems
Associated Lean declarations
-
theoremdefined in BernoulliRegular/CyclotomicUnits/SaturationIndex.leancomplete
theorem BernoulliRegular.not_dvd_index_of_pSaturated {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_three : 3 ≤ p) (hsat : BernoulliRegular.pSaturated (BernoulliRegular.CPlus hp_three) BernoulliRegular.EPlus p) : ¬p ∣ (BernoulliRegular.CPlus hp_three).index
theorem BernoulliRegular.not_dvd_index_of_pSaturated {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_three : 3 ≤ p) (hsat : BernoulliRegular.pSaturated (BernoulliRegular.CPlus hp_three) BernoulliRegular.EPlus p) : ¬p ∣ (BernoulliRegular.CPlus hp_three).index
CU-15: p-saturation of the cyclotomic units in the full plus-side unit group forces p not to divide the cyclotomic-unit index.
-
theoremdefined in BernoulliRegular/CyclotomicUnits/SaturationIndex.leancomplete
theorem BernoulliRegular.subgroup_not_dvd_index_of_pSaturated_top_of_pow_eq_one_mem.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [CommGroup G] {H : Subgroup G} [H.FiniteIndex] (hsat : BernoulliRegular.pSaturated H ⊤ p) (htorsion : ∀ (g : G), g ^ p = 1 → g ∈ H) : ¬p ∣ H.index
theorem BernoulliRegular.subgroup_not_dvd_index_of_pSaturated_top_of_pow_eq_one_mem.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [CommGroup G] {H : Subgroup G} [H.FiniteIndex] (hsat : BernoulliRegular.pSaturated H ⊤ p) (htorsion : ∀ (g : G), g ^ p = 1 → g ∈ H) : ¬p ∣ H.index
A finite-index subgroup of a commutative group has p-prime-to index if it is p-saturated in the whole group and contains every element killed by `p`. The proof is Cauchy's theorem on `G / H`: a p-divisor of the index gives a nontrivial quotient class with p-th power one. Saturation lifts the p-th power equality into `H`, and the torsion hypothesis forces the representative itself back into `H`, contradiction.
-
theoremdefined in BernoulliRegular/CyclotomicUnits/SaturationIndex.leancomplete
theorem BernoulliRegular.CPlus_index_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_three : 3 ≤ p) : (BernoulliRegular.CPlus hp_three).index ≠ 0
theorem BernoulliRegular.CPlus_index_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (hp_three : 3 ≤ p) : (BernoulliRegular.CPlus hp_three).index ≠ 0
The real cyclotomic-unit subgroup has finite index in the full plus-side unit group for prime conductor.
The proof is purely group-theoretic once one knows that C^+_{\mathrm{sq}} has
finite index in E^+ and contains the torsion of E^+. Suppose for contradiction
that p divides [E^+:C^+_{\mathrm{sq}}]. By Cauchy's theorem applied to the
finite quotient E^+/C^+_{\mathrm{sq}}, there is a non-trivial quotient class of
order p. Choose a representative g\in E^+. The order condition says
g^p\in C^+_{\mathrm{sq}}. Of course g^p is a p-th power in E^+. By
p-saturation, there is h\in C^+_{\mathrm{sq}} with h^p=g^p. Then
(gh^{-1})^p=1. Thus gh^{-1} is p-torsion in E^+. The only torsion units in
the real cyclotomic field are \pm1, and both belong to C^+_{\mathrm{sq}}. Hence
gh^{-1}\in C^+_{\mathrm{sq}}, and since h\in C^+_{\mathrm{sq}}, also
g\in C^+_{\mathrm{sq}}. This means the quotient class of g was trivial,
contradicting its order p.