7.1. Real cyclotomic units🔗

Let u_a = \frac{1-\zeta_p^a}{1-\zeta_p} (a \in \mathbb{Z}, (a,p)=1) be the usual cyclotomic unit in \mathcal{O}_K^\times. For the real subfield one uses the conjugation-fixed unit \varepsilon_a = u_a\,\overline{u_a} = \zeta_p^{\,1-a} \left(\frac{1-\zeta_p^a}{1-\zeta_p}\right)^2 . It lies in K^+ because complex conjugation fixes it, and it is a unit because both u_a and \overline{u_a} are units. The range used for prime conductor is 2 \le a \le \frac{p-1}{2}. In that range 0<a<p, so a prime p cannot divide a; hence (a,p)=1 and the above cyclotomic unit is defined.

Lemma7.1.1

uses 1used by 1✓L∃∀N

Coprimality of the standard indices. Let 2 \le a \le (p-1)/2. Then a is coprime to p.

Definition 2.1.1

Lean code for Lemma7.1.1●1 theorem

theoremdefined in BernoulliRegular/CyclotomicUnits/Basic.lean

complete

theorem BernoulliRegular.realCyclotomicUnit_index_coprime {p : ℕ}
  [Fact (Nat.Prime p)] {a : ℕ} (ha_two : 2 ≤ a)
  (ha_le : a ≤ (p - 1) / 2) : a.Coprime p

theorem BernoulliRegular.realCyclotomicUnit_index_coprime
  {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ}
  (ha_two : 2 ≤ a)
  (ha_le : a ≤ (p - 1) / 2) : a.Coprime p

Indices `2 ≤ a ≤ (p - 1) / 2` are automatically coprime to the prime
conductor `p`.

Proof for Lemma 7.1.1

uses 0

The lower bound gives a>0. The upper bound gives a \le (p-1)/2 < p, so a<p. If p divided a, then since a is positive we would have p \le a, contradicting a<p. Because p is prime, not being divisible by p is equivalent to being coprime to p.

Definition7.1.2

Statement uses 2

Statement dependency previews

Preview

Definition 1.1.1

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Definition 7.2.1

Loading preview

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

✓L∃∀N

Real cyclotomic unit. For 2 \le a \le (p-1)/2, the unit \varepsilon_a \in E^+ is the unique real unit whose image in \mathcal{O}_K^\times is the conjugation-fixed product u_a\overline{u_a}.

Definition 1.1.1 Lemma 7.1.1

Lean code for Definition7.1.2●1 definition

defdefined in BernoulliRegular/CyclotomicUnits/Basic.lean

complete

def BernoulliRegular.realCyclotomicUnit.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] (a : ℕ)
  (ha_two : 2 ≤ a) (ha_le : a ≤ (p - 1) / 2) :
  (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K))ˣ

def BernoulliRegular.realCyclotomicUnit.{u_1}
  {p : ℕ} [Fact (Nat.Prime p)]
  {K : Type u_1} [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  [NumberField.IsCMField K] (a : ℕ)
  (ha_two : 2 ≤ a)
  (ha_le : a ≤ (p - 1) / 2) :
  (NumberField.RingOfIntegers
      ↥(NumberField.maximalRealSubfield
          K))ˣ

The real cyclotomic unit in `𝓞 K⁺` attached to
`2 ≤ a ≤ (p - 1) / 2`.

This wraps the existing descended unit
`FLT37.realCyclotomicUnitPlusUnit p K a`, with the index coprimality proved
from the standard prime-conductor range.

After extension of scalars from \mathcal{O}_{K^+} to \mathcal{O}_K, this unit is exactly the standard conjugation-fixed product u_a\overline{u_a}, and is fixed by complex conjugation.