NYLL
Module

RationalCyclotomicArithmeticProduct.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalCyclotomicArithmeticProduct
19 declarations indexed from sourceView source ↗

Module documentation

The rational cyclotomic product formula in arithmetic normalization

The arithmetic norm-residue symbol sends an ordinary unramified uniformizer to arithmetic Frobenius. At the ramified prime of a prime-power cyclotomic layer, a local unit u therefore acts by u⁻¹. This file records those two signs on the actual chosen local Artin maps and proves the finite principal-idèle product formula in that normalization.

Imports2
Imported by1

Declarations

instance

(anonymous instance)

L29 ↗
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
Lean source · statement
instance (q : Nat.Primes) : Fact q.1.Prime
instance

(anonymous instance)

L32 ↗
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
Lean source · statement
instance (m : ℕ+) : NeZero (m : ℕ)
instance

rationalCyclotomicArithmeticLevelFiniteDimensional

L37 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticLevelFiniteDimensional
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
section ArbitraryCyclotomicLevel
Lean source · statement
instance
    rationalCyclotomicArithmeticLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m)
instance

rationalCyclotomicArithmeticLevelIsAbelianGalois

L45 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticLevelIsAbelianGalois
Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
section ArbitraryCyclotomicLevel
noncomputable local instance
    rationalCyclotomicArithmeticLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  IsCyclotomicExtension.finiteDimensional
    {(m : ℕ)} ℚ (KummerTheory.rationalCyclotomicLevel m)
Lean source · statement
instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m)
theorem

galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_eq_inv

L56 ↗
GlobalClassFieldTheory.Reciprocity.galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_eq_inv
Documentation

Mapping an arithmetic chosen local symbol to a cyclotomic coordinate only inverts the corresponding geometric coordinate. This small opaque boundary keeps the full chosen-Artin expressions out of the finite-product congruence below.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
section ArbitraryCyclotomicLevel
noncomputable local instance
    rationalCyclotomicArithmeticLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  IsCyclotomicExtension.finiteDimensional
    {(m : ℕ)} ℚ (KummerTheory.rationalCyclotomicLevel m)
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicLevelIsAbelianGalois m
Lean source · statement
theorem
    galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_eq_inv
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ))
    (x : (v.adicCompletion ℚ)ˣ) :
    IsCyclotomicExtension.Rat.galEquivZMod
        (m : ℕ)
        (KummerTheory.rationalCyclotomicLevel m)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension m)
        (arithmeticChosenFinitePlaceArtinMonoidHom
          ℚ (KummerTheory.rationalCyclotomicLevel m) v x) =
      (IsCyclotomicExtension.Rat.galEquivZMod
        (m : ℕ)
        (KummerTheory.rationalCyclotomicLevel m)
        (hK :=
          KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension m)
        (chosenFinitePlaceArtinMonoidHom
          (K := ℚ)
          (L := KummerTheory.rationalCyclotomicLevel m)
          v x))⁻¹
theorem

galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_of_not_dvd

L82 ↗
GlobalClassFieldTheory.Reciprocity.galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_of_not_dvd
Documentation

For an arbitrary chosen local input away from the conductor, the arithmetic cyclotomic character is q raised to the negative of the absolute-value logarithmic valuation. Thus an ordinary DVR uniformizer, whose logarithmic value is -1, maps to q.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
section ArbitraryCyclotomicLevel
noncomputable local instance
    rationalCyclotomicArithmeticLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  IsCyclotomicExtension.finiteDimensional
    {(m : ℕ)} ℚ (KummerTheory.rationalCyclotomicLevel m)
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicLevelIsAbelianGalois m
Lean source · statement
theorem
    galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_of_not_dvd
    (m : ℕ+) (q : Nat.Primes)
    (hq : ¬ q.1 ∣ (m : ℕ))
    (x : ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ) :
    IsCyclotomicExtension.Rat.galEquivZMod
        (m : ℕ)
        (KummerTheory.rationalCyclotomicLevel m)
        (arithmeticChosenFinitePlaceArtinMonoidHom
          ℚ (KummerTheory.rationalCyclotomicLevel m)
          (RayClass.rationalPrime q) x) =
      (ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)) ^
        (-
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap
            (HeightOneSpectrum.adicAbv ℚ
              (RayClass.rationalPrime q)).Completion
            (Additive.ofMul
              ((finitePlaceCompletionUnitsContinuousMulEquiv
                (RayClass.rationalPrime q)).symm x)))
theorem

galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_principal_of_not_dvd

L111 ↗
GlobalClassFieldTheory.Reciprocity.galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_principal_of_not_dvd
Documentation

Away from the conductor, the arithmetic local Artin character of a rational principal component is the usual positive valuation power of arithmetic Frobenius.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
section ArbitraryCyclotomicLevel
noncomputable local instance
    rationalCyclotomicArithmeticLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  IsCyclotomicExtension.finiteDimensional
    {(m : ℕ)} ℚ (KummerTheory.rationalCyclotomicLevel m)
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicLevelIsAbelianGalois m
Lean source · statement
theorem
    galEquivZMod_arithmeticChosenFinitePlaceArtinMonoidHom_principal_of_not_dvd
    (m : ℕ+) (q : Nat.Primes)
    (hq : ¬ q.1 ∣ (m : ℕ)) (x : ℚˣ) :
    IsCyclotomicExtension.Rat.galEquivZMod
        (m : ℕ)
        (KummerTheory.rationalCyclotomicLevel m)
        (arithmeticChosenFinitePlaceArtinMonoidHom
          ℚ (KummerTheory.rationalCyclotomicLevel m)
          (RayClass.rationalPrime q)
          (IdeleGroup.finiteComponent
            (RayClass.rationalPrime q)
            (IdeleGroup.principalIdele ℚ x))) =
      (ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)) ^
          padicValRat q.1 (x : ℚ)
def

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter

L137 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
Documentation

The arithmetic chosen finite-place character of a rational principal idèle at the prime q.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
def
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes) :
    (ZMod (p.1 ^ k))ˣ
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_inv

L146 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_inv
Documentation

Arithmetic and geometric finite-place characters differ exactly by inversion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_inv
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes) :
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
        p k x q =
      (rationalCyclotomicPrincipalFinitePlaceCharacter
        p k x q)⁻¹
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support

L158 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support
Documentation

Outside the ordinary rational prime-factorization support, the arithmetic local factor is trivial.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes)
    (hq :
      q ∉ rationalPrimeFactorizationPrimeSupport x p) :
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
        p k x q =
      1
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacters_hasFiniteMulSupport

L174 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacters_hasFiniteMulSupport
Documentation

The arithmetic rational principal finite-place characters have finite multiplicative support.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacters_hasFiniteMulSupport
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    Function.HasFiniteMulSupport
      (rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
        p k x)
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_of_ne

L191 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_of_ne
Documentation

At a prime away from p, the arithmetic character is the direct Frobenius power q ^ v_q(x).

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_of_ne
    (p q : Nat.Primes) (hqp : q ≠ p)
    (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
        p k x q =
      (ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr
          (rationalPrime_not_dvd_pow_of_ne q p hqp k))) ^
        padicValRat q.1 (x : ℚ)
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_at_prime

L209 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_at_prime
Documentation

At the ramified prime p, the arithmetic character is the inverse of the actual reduced p-adic unit.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter_at_prime
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicArithmeticPrincipalFinitePlaceCharacter
        p k x p =
      (Units.map (PadicInt.toZModPow k).toMonoidHom
        (padicIntUnitOfRat p
          (rationalPrimeUnit x p : ℚ)
          (rationalPrimeUnit x p).ne_zero
          (padicValRat_rationalPrimeUnit x p)))⁻¹
instance

(anonymous instance)

L223 ↗
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

(anonymous instance)

L230 ↗
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
instance (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

(anonymous instance)

L237 ↗
Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
instance (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_inv_geometric

L247 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_inv_geometric
Documentation

Pointwise inversion of the chosen local characters, assembled before the public product formula so that its proof does not unfold the full finite-product expressions during definitional equality checking.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_inv_geometric
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        IsCyclotomicExtension.Rat.galEquivZMod
          (p.1 ^ k)
          (KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (hK :=
            KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (arithmeticChosenFinitePlaceArtinMonoidHom
            ℚ
            (KummerTheory.rationalCyclotomicLevel
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele ℚ x)))) =
      (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        IsCyclotomicExtension.Rat.galEquivZMod
          (p.1 ^ k)
          (KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (hK :=
            KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (chosenFinitePlaceArtinMonoidHom
            (K := ℚ)
            (L :=
              KummerTheory.rationalCyclotomicLevel
                ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele ℚ x))))⁻¹
theorem

rationalSignPadicUnit_toZModPow_inv_eq_self

L340 ↗
GlobalClassFieldTheory.Reciprocity.rationalSignPadicUnit_toZModPow_inv_eq_self
Documentation

The reduction of a rational sign is fixed by inversion.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
theorem rationalSignPadicUnit_toZModPow_inv_eq_self
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    (Units.map (PadicInt.toZModPow k).toMonoidHom
        (rationalSignPadicUnit x p))⁻¹ =
      Units.map (PadicInt.toZModPow k).toMonoidHom
        (rationalSignPadicUnit x p)
theorem

rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_sign

L382 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_sign
Documentation

At every prime-power cyclotomic level, the product of the actual arithmetic finite-place characters of a rational principal idèle is the reduction of its sign.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance (p : Nat.Primes) (k : ℕ) :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
theorem
    rationalCyclotomicArithmeticPrincipalFinitePlaceProduct_eq_sign
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        IsCyclotomicExtension.Rat.galEquivZMod
          (p.1 ^ k)
          (KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (hK :=
            KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
          (arithmeticChosenFinitePlaceArtinMonoidHom
            ℚ
            (KummerTheory.rationalCyclotomicLevel
              ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele ℚ x)))) =
      Units.map (PadicInt.toZModPow k).toMonoidHom
        (rationalSignPadicUnit x p)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.