7.2. The cyclotomic-unit subgroups🔗

There are two closely related real cyclotomic-unit subgroups. The logarithmic saturation argument is most convenient for the squared family \varepsilon_a. The index theorem is naturally stated for the normalised family \eta_a = \zeta_p^{(1-a)/2}\frac{1-\zeta_p^a}{1-\zeta_p}, \qquad \eta_a^2=\varepsilon_a . Here (1-a)/2 is understood modulo p, using that 2 is invertible modulo the odd prime p.

Definition7.2.1

uses 1

Used by 8

Reverse dependency previews

Preview

Lemma 7.2.3

Loading preview

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

✓L∃∀N

The squared cyclotomic-unit subgroup. Let g=(p-3)/2. The subgroup C^+_{\mathrm{sq}}\le E^+ is generated by -1 and by the units \varepsilon_2,\varepsilon_3,\ldots,\varepsilon_{(p-1)/2}. Equivalently, C^+_{\mathrm{sq}} = \left\langle -1,\ \varepsilon_a\ (2\le a\le (p-1)/2) \right\rangle .

Definition 7.1.2

Lean code for Definition7.2.1●1 definition

defdefined in BernoulliRegular/CyclotomicUnits/Subgroup.lean

complete

def BernoulliRegular.CPlus.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1}
  [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))ˣ

def BernoulliRegular.CPlus.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {K : Type u_1}
  [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K))ˣ

The real cyclotomic-unit subgroup `C⁺`, generated by `-1` and the
standard real cyclotomic units.

The finite index set may be written as i\in \operatorname{Fin}((p-3)/2), a=i+2. Thus the listed units are precisely the nontrivial real cyclotomic generators in the prime-conductor range, together with the torsion unit -1.

Definition7.2.2

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 7.2.3

Loading preview

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

✓L∃∀N

The normalised cyclotomic-unit subgroup. The subgroup C^+_{\mathrm{norm}}\le E^+ is generated by -1 and by the normalised real cyclotomic units \eta_2,\eta_3,\ldots,\eta_{(p-1)/2}.

Definition 7.1.2

Lean code for Definition7.2.2●1 definition

defdefined in BernoulliRegular/CyclotomicUnits/NormalizedSubgroup.lean

complete

def BernoulliRegular.normalizedCPlus.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))ˣ

def BernoulliRegular.normalizedCPlus.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  Subgroup
    (NumberField.RingOfIntegers
        ↥(NumberField.maximalRealSubfield
            K))ˣ

The TeX normalized subgroup
`C⁺ = <-1, ε₂, ..., ε_g> ≤ (𝓞 K⁺)ˣ`.

The relation between the two families is exactly the relation \eta_a^2=\varepsilon_a.

Lemma7.2.3

Statement uses 2

Statement dependency previews

Preview

Definition 7.2.1

Loading preview

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

used by 1✓L∃∀N

Squares of normalised generators. For each standard generator index a, \eta_a^2=\varepsilon_a.

Definition 7.2.1 Definition 7.2.2

Lean code for Lemma7.2.3●1 theorem

theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedSubgroup.lean

complete

theorem BernoulliRegular.normalizedCPlusGenerator_sq_eq_CPlusGenerator.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) (i : Fin ((p - 3) / 2)) :
  BernoulliRegular.normalizedCPlusGenerator hp_odd hp_three i ^ 2 =
    BernoulliRegular.CPlusGenerator hp_three i

theorem BernoulliRegular.normalizedCPlusGenerator_sq_eq_CPlusGenerator.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p)
  (i : Fin ((p - 3) / 2)) :
  BernoulliRegular.normalizedCPlusGenerator
        hp_odd hp_three i ^
      2 =
    BernoulliRegular.CPlusGenerator
      hp_three i

Proof for Lemma 7.2.3

uses 0

This is the elementary identity \left( \zeta_p^{(1-a)/2}\frac{1-\zeta_p^a}{1-\zeta_p} \right)^2 = \zeta_p^{1-a} \left(\frac{1-\zeta_p^a}{1-\zeta_p}\right)^2 = u_a\overline{u_a}. The last equality is the standard computation \overline{u_a} = \frac{1-\zeta_p^{-a}}{1-\zeta_p^{-1}} = \zeta_p^{1-a}\frac{1-\zeta_p^a}{1-\zeta_p}.

Lemma7.2.4

Statement uses 3

Statement dependency previews

Preview

Definition 7.2.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 7.7.6

Loading preview

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

✓L∃∀N

Odd-primary comparison of the two indices. For odd p, p \mid [E^+ : C^+_{\mathrm{sq}}] \quad\Longleftrightarrow\quad p \mid [E^+ : C^+_{\mathrm{norm}}].

Definition 7.2.1 Definition 7.2.2 Lemma 7.2.3

Lean code for Lemma7.2.4●2 theorems

theoremdefined in BernoulliRegular/CyclotomicUnits/NormalizedSubgroup.lean

complete

theorem BernoulliRegular.CPlus_index_prime_dvd_iff_normalizedCPlus_index_prime_dvd.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  p ∣ (BernoulliRegular.CPlus hp_three).index ↔
    p ∣ (BernoulliRegular.normalizedCPlus hp_odd hp_three).index

theorem BernoulliRegular.CPlus_index_prime_dvd_iff_normalizedCPlus_index_prime_dvd.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K]
  (hp_odd : p ≠ 2) (hp_three : 3 ≤ p) :
  p ∣
      (BernoulliRegular.CPlus
          hp_three).index ↔
    p ∣
      (BernoulliRegular.normalizedCPlus
          hp_odd hp_three).index

theoremdefined in BernoulliRegular/CyclotomicUnits/IndexComparison.lean

complete

theorem BernoulliRegular.subgroup_index_prime_dvd_iff_of_relIndex_dvd_two_pow.{u_1}
  {G : Type u_1} [Group G] {H K : Subgroup G} (hHK : H ≤ K) {p r : ℕ}
  (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hrel : H.relIndex K ∣ 2 ^ r) :
  p ∣ H.index ↔ p ∣ K.index

theorem BernoulliRegular.subgroup_index_prime_dvd_iff_of_relIndex_dvd_two_pow.{u_1}
  {G : Type u_1} [Group G]
  {H K : Subgroup G} (hHK : H ≤ K)
  {p r : ℕ} (hp : Nat.Prime p)
  (hp_odd : p ≠ 2)
  (hrel : H.relIndex K ∣ 2 ^ r) :
  p ∣ H.index ↔ p ∣ K.index

Proof for Lemma 7.2.4

uses 0

The subgroup C^+_{\mathrm{sq}} is contained in C^+_{\mathrm{norm}}, because -1 is a normalised generator and each squared generator \varepsilon_a is the square of the normalised generator \eta_a. Conversely, every class in C^+_{\mathrm{norm}}/C^+_{\mathrm{sq}} has square one: it is enough to check this on the generators, and it follows from \eta_a^2=\varepsilon_a and (-1)^2=1. Hence the relative index [C^+_{\mathrm{norm}}:C^+_{\mathrm{sq}}] divides a power of 2. The two ambient indices differ by this relative index. Since p is odd, p does not divide any power of 2. Therefore the p-primary divisibility of [E^+ : C^+_{\mathrm{sq}}] and [E^+ : C^+_{\mathrm{norm}}] is the same.