Module

RationalCyclotomicCharacter.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.RationalCyclotomicCharacter

8 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic character of the rational cyclotomic field

This file assembles mathlib's p-adic cyclotomic characters of the actual extension rationalCyclotomicField / ℚ. Their product takes values in the canonical product of the local unit groups, and the topological Chinese-remainder equivalence identifies that product with ZHatˣ.

No abstract copy of either the Galois group or its expected target is introduced here.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.RationalCyclotomicField
Nyll.GaloisCohomology.ProfiniteIntegers.ProfiniteIntegerUnits
Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Imported by2

instance

rationalCyclotomicField_hasEnoughRootsOfUnity

L35 ↗

KummerTheory.rationalCyclotomicField_hasEnoughRootsOfUnity

Documentation

The actual rational cyclotomic field contains primitive roots of unity of every nonzero order.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation

Lean source · full declaration

instance rationalCyclotomicField_hasEnoughRootsOfUnity
    (n : ℕ) [NeZero n] :
    HasEnoughRootsOfUnity rationalCyclotomicField n where
  prim :=
    IsCyclotomicExtension.exists_isPrimitiveRoot
      (S := (Set.univ : Set ℕ))
      ℚ rationalCyclotomicField (Set.mem_univ n) (NeZero.ne n)
  cyc := rootsOfUnity.isCyclic rationalCyclotomicField n

instance

(anonymous instance)

L44 ↗

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation

Lean source · statement

instance (p : Nat.Primes) : Fact p.1.Prime

def

rationalCyclotomicCharacterPrimeProduct

L49 ↗

KummerTheory.rationalCyclotomicCharacterPrimeProduct

Documentation

The product, over all rational primes, of mathlib's p-adic cyclotomic characters of Gal(rationalCyclotomicField / ℚ).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · full declaration

def rationalCyclotomicCharacterPrimeProduct :
    (rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField) →ₜ*
      ((p : Nat.Primes) → ℤ_[p.1]ˣ) where
  toMonoidHom :=
    MonoidHom.pi fun p =>
      (cyclotomicCharacter rationalCyclotomicField p.1).comp
        (MulSemiringAction.toRingAut
          (rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField)
          rationalCyclotomicField)
  continuous_toFun :=
    continuous_pi fun p =>
      cyclotomicCharacter.continuous
        p.1 ℚ rationalCyclotomicField

theorem

rationalCyclotomicCharacterPrimeProduct_apply

L66 ↗

KummerTheory.rationalCyclotomicCharacterPrimeProduct_apply

Documentation

Evaluation at a prime is the corresponding mathlib cyclotomic character.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem rationalCyclotomicCharacterPrimeProduct_apply
    (σ : rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField)
    (p : Nat.Primes) :
    rationalCyclotomicCharacterPrimeProduct σ p =
      cyclotomicCharacter rationalCyclotomicField p.1
        (MulSemiringAction.toRingAut
          (rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField)
          rationalCyclotomicField σ)

instance

primePowerLevelNumberField

L80 ↗

KummerTheory.primePowerLevelNumberField

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
section PrimePowerCharacter

-- Expose the exact prime-power index to instance synthesis. Both
-- proposition-valued instances are supplied by the existing canonical factories.

Lean source · statement

instance primePowerLevelNumberField (p : Nat.Primes) (k : ℕ) :
    NumberField (rationalCyclotomicLevel ⟨p.1 ^ k, pow_pos p.2.pos k⟩)

instance

primePowerLevelIsGalois

L84 ↗

KummerTheory.primePowerLevelIsGalois

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
section PrimePowerCharacter

-- Expose the exact prime-power index to instance synthesis. Both
-- proposition-valued instances are supplied by the existing canonical factories.
local instance primePowerLevelNumberField (p : Nat.Primes) (k : ℕ) :
    NumberField (rationalCyclotomicLevel ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevel_numberField ⟨p.1 ^ k, pow_pos p.2.pos k⟩

Lean source · statement

instance primePowerLevelIsGalois (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (rationalCyclotomicLevel ⟨p.1 ^ k, pow_pos p.2.pos k⟩)

theorem

rationalCyclotomicCharacterPrimeProduct_toZModPow

L90 ↗

KummerTheory.rationalCyclotomicCharacterPrimeProduct_toZModPow

Documentation

Reduction of the p-coordinate modulo p ^ k is the standard mathlib character of the finite internal cyclotomic level.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
section PrimePowerCharacter

-- Expose the exact prime-power index to instance synthesis. Both
-- proposition-valued instances are supplied by the existing canonical factories.
local instance primePowerLevelNumberField (p : Nat.Primes) (k : ℕ) :
    NumberField (rationalCyclotomicLevel ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevel_numberField ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance primePowerLevelIsGalois (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (rationalCyclotomicLevel ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevel_isGalois ⟨p.1 ^ k, pow_pos p.2.pos k⟩

Lean source · statement

theorem rationalCyclotomicCharacterPrimeProduct_toZModPow
    (σ : rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField)
    (p : Nat.Primes) (k : ℕ) :
    Units.map (PadicInt.toZModPow k).toMonoidHom
        (rationalCyclotomicCharacterPrimeProduct σ p) =
      IsCyclotomicExtension.Rat.galEquivZMod
        (p.1 ^ k)
        (rationalCyclotomicLevel
          ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (hK :=
          rationalCyclotomicLevel_isCyclotomicExtension
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        (σ.restrictNormal
          (rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩))

def