NYLL
Module

RationalCyclotomicPrincipalAwayProduct.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalCyclotomicPrincipalAwayProduct
29 declarations indexed from sourceView source ↗

Module documentation

Away-from-p factors of a rational cyclotomic principal idele

For the cyclotomic level p ^ k, this file reindexes the actual chosen finite-place Artin characters over rational primes. Away from p, the unramified formula makes the multiplicative support lie in the ordinary finite prime factorization support of the principal rational number.

The final theorem separates the genuine p-factor from the explicit away-from-p finite product. The construction also applies to k = 0.

Imports2
Imported by2

Declarations

instance

(anonymous instance)

L34 ↗
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
open Function
Lean source · statement
instance (q : Nat.Primes) : Fact q.1.Prime
instance

(anonymous instance)

L37 ↗
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
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
Lean source · statement
instance (m : ℕ+) : NeZero (m : ℕ)
instance

rationalCyclotomicPrincipalPrimePowerNumberField

L40 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalPrimePowerNumberField
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
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
Lean source · statement
instance rationalCyclotomicPrincipalPrimePowerNumberField
    (p : Nat.Primes) (k : ℕ) :
    NumberField (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

rationalCyclotomicPrincipalPrimePowerFiniteDimensional

L47 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalPrimePowerFiniteDimensional
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
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (p : Nat.Primes) (k : ℕ) :
    FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

rationalCyclotomicPrincipalPrimePowerIsGalois

L54 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalPrimePowerIsGalois
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
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

rationalCyclotomicPrincipalPrimePowerIsAbelianGalois

L61 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
Source context 11 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
Lean source · statement
instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
instance

rationalCyclotomicPrincipalLevelFiniteDimensional

L69 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalLevelFiniteDimensional
Source context 12 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
Lean source · statement
instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m)
instance

rationalCyclotomicPrincipalLevelIsAbelianGalois

L76 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalLevelIsAbelianGalois
Source context 13 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
Lean source · statement
instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m)
def

rationalCyclotomicPrincipalHeightOneArtinInput

L83 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneArtinInput
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
def rationalCyclotomicPrincipalHeightOneArtinInput
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩ ≃ₐ[ℚ]
      KummerTheory.rationalCyclotomicLevel
        ⟨p.1 ^ k, pow_pos p.2.pos k⟩
theorem

rationalCyclotomicPrincipalHeightOneArtinInput_spec

L99 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneArtinInput_spec
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalHeightOneArtinInput_spec
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    rationalCyclotomicPrincipalHeightOneArtinInput p k x v =
      chosenFinitePlaceArtinMonoidHom
        (K := ℚ)
        (L :=
          KummerTheory.rationalCyclotomicLevel
            ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
        v
        (IdeleGroup.finiteComponent v
          (IdeleGroup.principalIdele ℚ x))
def

rationalCyclotomicPrincipalHeightOneCharacter

L113 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneCharacter
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
def rationalCyclotomicPrincipalHeightOneCharacter
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    (ZMod (p.1 ^ k))ˣ
theorem

rationalCyclotomicPrincipalHeightOneCharacter_spec

L128 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneCharacter_spec
Documentation

The named height-one character is the cyclotomic coordinate of the chosen finite-place Artin symbol.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalHeightOneCharacter_spec
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ)
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    rationalCyclotomicPrincipalHeightOneCharacter p k x v =
      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)))
def

rationalCyclotomicPrincipalFinitePlaceCharacter

L153 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter
Documentation

The genuine chosen finite-place Artin character of the rational principal idele at the prime q, evaluated in the p ^ k cyclotomic coordinate.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
def rationalCyclotomicPrincipalFinitePlaceCharacter
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes) :
    (ZMod (p.1 ^ k))ˣ
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_spec

L160 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_spec
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalFinitePlaceCharacter_spec
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x q =
      rationalCyclotomicPrincipalHeightOneCharacter p k x
        ((Rat.HeightOneSpectrum.primesEquiv
          (R := 𝓞 ℚ)).symm q)
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_chosenArtin_spec

L170 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_chosenArtin_spec
Documentation

The named rational-prime character is exactly the cyclotomic coordinate of the chosen finite-place Artin symbol.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacter_chosenArtin_spec
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x q =
      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⟩)
          ((Rat.HeightOneSpectrum.primesEquiv
            (R := 𝓞 ℚ)).symm q)
          (IdeleGroup.finiteComponent
            ((Rat.HeightOneSpectrum.primesEquiv
              (R := 𝓞 ℚ)).symm q)
            (IdeleGroup.principalIdele ℚ x)))
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_at_prime_succ_formula

L200 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_at_prime_succ_formula
Documentation

At every positive p-power level, the finite-place character at p is the direct reduction of the rational p-adic unit.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalFinitePlaceCharacter_at_prime_succ_formula
    (p : Nat.Primes) (n : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p (n + 1) x p =
      Units.map
        (PadicInt.toZModPow (p := p.1) (n + 1)).toMonoidHom
        (padicIntUnitOfRat p
          (rationalPrimeUnit x p : ℚ)
          (rationalPrimeUnit x p).ne_zero
          (padicValRat_rationalPrimeUnit x p))
theorem

rationalPrime_not_dvd_pow_of_ne

L309 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrime_not_dvd_pow_of_ne
Documentation

A rational prime distinct from p does not divide any power p ^ k. This includes the level-one case k = 0.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalPrime_not_dvd_pow_of_ne
    (q p : Nat.Primes) (hqp : q ≠ p) (k : ℕ) :
    ¬ q.1 ∣ p.1 ^ k
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_of_ne

L319 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_of_ne
Documentation

Away from p, the chosen finite-place character is the inverse Frobenius power determined by the rational q-adic valuation.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalFinitePlaceCharacter_of_ne
    (p q : Nat.Primes) (hqp : q ≠ p)
    (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalFinitePlaceCharacter 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

padicValRat_eq_zero_of_not_mem_rationalPrimeFactorizationPrimeSupport

L346 ↗
GlobalClassFieldTheory.Reciprocity.padicValRat_eq_zero_of_not_mem_rationalPrimeFactorizationPrimeSupport
Documentation

Outside the finite rational prime-factorization support, the q-adic valuation of the nonzero rational number is zero.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    padicValRat_eq_zero_of_not_mem_rationalPrimeFactorizationPrimeSupport
    (x : ℚˣ) (p q : Nat.Primes)
    (hq :
      q ∉ rationalPrimeFactorizationPrimeSupport x p) :
    padicValRat q.1 (x : ℚ) = 0
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support

L410 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support
Documentation

A chosen finite-place Artin character outside the rational prime-factorization support is genuinely trivial.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacter_eq_one_of_not_mem_support
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) (q : Nat.Primes)
    (hq :
      q ∉ rationalPrimeFactorizationPrimeSupport x p) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x q = 1
theorem

rationalCyclotomicPrincipalFinitePlaceCharacters_hasFiniteMulSupport

L430 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacters_hasFiniteMulSupport
Documentation

The actual rational principal finite-place characters have finite multiplicative support, contained in the ordinary rational prime factorization support.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacters_hasFiniteMulSupport
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    HasFiniteMulSupport
      (rationalCyclotomicPrincipalFinitePlaceCharacter p k x)
theorem

rationalCyclotomicPrincipalAwayFinitePlaceCharacter_finprod_eq_factorizationProduct

L447 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalAwayFinitePlaceCharacter_finprod_eq_factorizationProduct
Documentation

The off-p finprod of the genuine chosen Artin characters is the explicit finite product over the erased rational prime-factorization support.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalAwayFinitePlaceCharacter_finprod_eq_factorizationProduct
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    (∏ᶠ (q : Nat.Primes) (_ : q ≠ p),
      rationalCyclotomicPrincipalFinitePlaceCharacter p k x q) =
      ∏ q :
          ↥((rationalPrimeFactorizationPrimeSupport x p).erase p),
        (ZMod.unitOfCoprime q.1.1
          (q.1.2.coprime_iff_not_dvd.mpr
            (rationalPrime_not_dvd_pow_of_ne
              q.1 p (Finset.ne_of_mem_erase q.2) k))) ^
          (-padicValRat q.1.1 (x : ℚ))
theorem

rationalPrimeUnitCharacter_mul_principalAwayFactorizationProduct_eq_sign

L508 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeUnitCharacter_mul_principalAwayFactorizationProduct_eq_sign
Documentation

The direct rational p-unit character times the explicit inverse away-from-p factorization product is the reduced rational sign.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalPrimeUnitCharacter_mul_principalAwayFactorizationProduct_eq_sign
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    Units.map (PadicInt.toZModPow k).toMonoidHom
          (padicIntUnitOfRat p (rationalPrimeUnit x p : ℚ)
            (rationalPrimeUnit x p).ne_zero
            (padicValRat_rationalPrimeUnit x p)) *
        ∏ q :
            ↥((rationalPrimeFactorizationPrimeSupport x p).erase p),
          (ZMod.unitOfCoprime q.1.1
            (q.1.2.coprime_iff_not_dvd.mpr
              (rationalPrime_not_dvd_pow_of_ne
                q.1 p (Finset.ne_of_mem_erase q.2) k))) ^
            (-padicValRat q.1.1 (x : ℚ)) =
      Units.map (PadicInt.toZModPow k).toMonoidHom
        (rationalSignPadicUnit x p)
def

rationalCyclotomicPrincipalHeightOneCharacterFinprod

L528 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneCharacterFinprod
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
def rationalCyclotomicPrincipalHeightOneCharacterFinprod
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    (ZMod (p.1 ^ k))ˣ
theorem

rationalCyclotomicPrincipalHeightOneCharacterFinprod_eq_finprod

L534 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneCharacterFinprod_eq_finprod
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalHeightOneCharacterFinprod_eq_finprod
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalHeightOneCharacterFinprod p k x =
      ∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        rationalCyclotomicPrincipalHeightOneCharacter p k x v
theorem

rationalCyclotomicPrincipalHeightOneCharacterFinprod_spec

L542 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalHeightOneCharacterFinprod_spec
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem rationalCyclotomicPrincipalHeightOneCharacterFinprod_spec
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalHeightOneCharacterFinprod p 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⟩)
          (chosenFinitePlaceArtinMonoidHom
            (K := ℚ)
            (L :=
              KummerTheory.rationalCyclotomicLevel
                ⟨p.1 ^ k, pow_pos p.2.pos k⟩)
            v
            (IdeleGroup.finiteComponent v
              (IdeleGroup.principalIdele ℚ x)))
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_eq_namedFinprod

L571 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_eq_namedFinprod
Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_eq_namedFinprod
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x p *
        (∏ᶠ (q : Nat.Primes) (_ : q ≠ p),
          rationalCyclotomicPrincipalFinitePlaceCharacter p k x q) =
      rationalCyclotomicPrincipalHeightOneCharacterFinprod p k x
theorem

rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_finprod

L603 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_finprod
Documentation

Reindexing by Rat.HeightOneSpectrum.primesEquiv and separating the distinguished prime identifies the height-one finprod with its genuine p-factor times the off-p prime finprod.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_away_finprod
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x p *
        (∏ᶠ (q : Nat.Primes) (_ : q ≠ p),
          rationalCyclotomicPrincipalFinitePlaceCharacter p k x q) =
      ∏ᶠ 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

rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_factorizationProduct

L633 ↗
GlobalClassFieldTheory.Reciprocity.rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_factorizationProduct
Documentation

Exact source for the final principal-product calculation: the height-one chosen Artin finprod is the genuine p-factor times the explicit away-from-p rational factorization product.

Source context 14 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open Function
local instance (q : Nat.Primes) : Fact q.1.Prime :=
  ⟨q.2⟩
local instance (m : ℕ+) : NeZero (m : ℕ) :=
  ⟨m.ne_zero⟩
local instance rationalCyclotomicPrincipalPrimePowerNumberField
    (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 rationalCyclotomicPrincipalPrimePowerFiniteDimensional
    (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 rationalCyclotomicPrincipalPrimePowerIsGalois
    (p : Nat.Primes) (k : ℕ) :
    IsGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  KummerTheory.rationalCyclotomicLevel_isGalois
    ⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicPrincipalPrimePowerIsAbelianGalois
    (p : Nat.Primes) (k : ℕ) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
  IsAbelianGalois.of_algHom
    (KummerTheory.rationalCyclotomicLevel
      ⟨p.1 ^ k, pow_pos p.2.pos k⟩).val
noncomputable local instance
    rationalCyclotomicPrincipalLevelFiniteDimensional
    (m : ℕ+) :
    FiniteDimensional ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
    rationalCyclotomicPrincipalLevelIsAbelianGalois
    (m : ℕ+) :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel m) :=
  rationalCyclotomicPrincipalPrimeLevelIsAbelianGalois m
Lean source · statement
theorem
    rationalCyclotomicPrincipalFinitePlaceCharacter_prime_mul_factorizationProduct
    (p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
    rationalCyclotomicPrincipalFinitePlaceCharacter p k x p *
        (∏ q :
            ↥((rationalPrimeFactorizationPrimeSupport x p).erase p),
          (ZMod.unitOfCoprime q.1.1
            (q.1.2.coprime_iff_not_dvd.mpr
              (rationalPrime_not_dvd_pow_of_ne
                q.1 p (Finset.ne_of_mem_erase q.2) k))) ^
            (-padicValRat q.1.1 (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)))

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