2.1. The Galois group🔗

Definition2.1.1

uses 0used by 1✓L∃∀N

The extension \mathbb{Q}(\zeta_p)/\mathbb{Q} is Galois of degree p-1. The assignment \sigma_a(\zeta_p)=\zeta_p^a \qquad (a\in (\mathbb{Z}/p\mathbb{Z})^\times) identifies \operatorname{Gal}(\mathbb{Q}(\zeta_p)/\mathbb{Q}) with (\mathbb{Z}/p\mathbb{Z})^\times.

Lean code for Definition2.1.1●4 declarations

abbrevdefined in BernoulliRegular/UnitQuotient/DeltaAction.lean

complete

abbrev BernoulliRegular.cyclotomicGalEquivZMod.{u_1} (p : ℕ)
  [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] :
  Gal(K/ℚ) ≃* BernoulliRegular.CyclotomicUnitDelta p

abbrev BernoulliRegular.cyclotomicGalEquivZMod.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K] :
  Gal(K/ℚ) ≃*
    BernoulliRegular.CyclotomicUnitDelta p

The standard cyclotomic Galois equivalence
`Gal(K / Q) ≃ (ZMod p)^*`.

defdefined in BernoulliRegular/UnitQuotient/DeltaAction.lean

complete

def BernoulliRegular.cyclotomicSigmaOfUnit.{u_1} (p : ℕ)
  [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a : BernoulliRegular.CyclotomicUnitDelta p) : Gal(K/ℚ)

def BernoulliRegular.cyclotomicSigmaOfUnit.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a :
    BernoulliRegular.CyclotomicUnitDelta
      p) :
  Gal(K/ℚ)

The Galois automorphism indexed by `a : (ZMod p)^*`.

theoremdefined in BernoulliRegular/UnitQuotient/DeltaAction.lean

complete

theorem BernoulliRegular.cyclotomicGalEquivZMod_sigmaOfUnit.{u_1} (p : ℕ)
  [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a : BernoulliRegular.CyclotomicUnitDelta p) :
  (BernoulliRegular.cyclotomicGalEquivZMod p K)
      (BernoulliRegular.cyclotomicSigmaOfUnit p K a) =
    a

theorem BernoulliRegular.cyclotomicGalEquivZMod_sigmaOfUnit.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a :
    BernoulliRegular.CyclotomicUnitDelta
      p) :
  (BernoulliRegular.cyclotomicGalEquivZMod
        p K)
      (BernoulliRegular.cyclotomicSigmaOfUnit
        p K a) =
    a

theoremdefined in BernoulliRegular/UnitQuotient/DeltaAction.lean

complete

theorem BernoulliRegular.cyclotomicSigmaOfUnit_apply_zeta.{u_1} (p : ℕ)
  [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a : BernoulliRegular.CyclotomicUnitDelta p) :
  (BernoulliRegular.cyclotomicSigmaOfUnit p K a)
      (IsCyclotomicExtension.zeta p ℚ K) =
    IsCyclotomicExtension.zeta p ℚ K ^ (↑a).val

theorem BernoulliRegular.cyclotomicSigmaOfUnit_apply_zeta.{u_1}
  (p : ℕ) [Fact (Nat.Prime p)]
  (K : Type u_1) [Field K] [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  (a :
    BernoulliRegular.CyclotomicUnitDelta
      p) :
  (BernoulliRegular.cyclotomicSigmaOfUnit
        p K a)
      (IsCyclotomicExtension.zeta p ℚ K) =
    IsCyclotomicExtension.zeta p ℚ K ^
      (↑a).val