NYLL
Module

Ideal.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.PowerResidueSymbols.Ideal
27 declarations indexed from sourceView source β†—

Module documentation

Power-residue symbols at prime ideals and integral ideals

Let K contain the n-th roots of unity and let P be a prime ideal whose absolute norm is coprime to n. Reduction identifies ΞΌβ‚™(π“ž K) with ΞΌβ‚™(π“ž K / P). Pulling the finite-field symbol back along this identification gives (a/P).

For a nonzero integral ideal I, (a/I) is the finite product of (a/P) raised to the multiplicity of P in I.

Imports3
Imported by2

Declarations

instance

primeIdealResidueFintype

L35 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealResidueFintype
Source context 7 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
Lean source Β· statement
instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal)
def

rootsOfUnityReduction

L41 β†—
AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReduction
Documentation

Reduction of n-th roots of unity modulo an integral prime ideal.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
def rootsOfUnityReduction
    (P : HeightOneSpectrum (π“ž K)) (n : β„•) :
    rootsOfUnity n (π“ž K) β†’*
      rootsOfUnity n (π“ž K β§Έ P.asIdeal) where
  toFun z :=
    ⟨Ideal.rootsOfUnityMapQuot P.asIdeal n z, by
      change Ideal.rootsOfUnityMapQuot P.asIdeal n (z ^ n) = 1
      rw [show z ^ n = 1 by exact Subtype.ext z.2, map_one]⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (Ideal.rootsOfUnityMapQuot P.asIdeal n)
  map_mul' z w := by
    apply Subtype.ext
    exact map_mul (Ideal.rootsOfUnityMapQuot P.asIdeal n) z w
theorem

rootsOfUnityReduction_injective

L57 β†—
AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReduction_injective
Documentation

Reduction on ΞΌβ‚™ is injective away from n.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem rootsOfUnityReduction_injective
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•)) :
    Function.Injective (rootsOfUnityReduction K P (n : β„•))
theorem

dvd_absNorm_sub_one_of_primitiveRoots

L72 β†—
AlgebraicNumberTheory.PowerResidueSymbols.dvd_absNorm_sub_one_of_primitiveRoots
Documentation

If K contains ΞΌβ‚™, then n divides N(P)-1 at every prime P ∀ n.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem dvd_absNorm_sub_one_of_primitiveRoots
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•)) :
    (n : β„•) ∣ Ideal.absNorm P.asIdeal - 1
def

rootsOfUnityReductionEquiv

L100 β†—
AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReductionEquiv
Documentation

Away from n, reduction identifies the global integral n-th roots of unity with the residue-field n-th roots of unity.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def rootsOfUnityReductionEquiv
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•)) :
    rootsOfUnity (n : β„•) (π“ž K) ≃*
      rootsOfUnity (n : β„•) (π“ž K β§Έ P.asIdeal)
theorem

rootsOfUnityReductionEquiv_apply

L140 β†—
AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReductionEquiv_apply
Documentation

The reduction equivalence acts by the canonical reduction homomorphism.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem rootsOfUnityReductionEquiv_apply
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (zeta : rootsOfUnity (n : β„•) (π“ž K)) :
    rootsOfUnityReductionEquiv K P n hmu hcoprime zeta =
      rootsOfUnityReduction K P (n : β„•) zeta
theorem

card_primeIdealResidueField

L151 β†—
AlgebraicNumberTheory.PowerResidueSymbols.card_primeIdealResidueField
Documentation

The cardinality of the residue field is the absolute norm of the prime ideal.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem card_primeIdealResidueField
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype.card (π“ž K β§Έ P.asIdeal) = Ideal.absNorm P.asIdeal
def

primeIdealResidueUnit

L159 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealResidueUnit
Documentation

An algebraic integer prime to P, regarded as a unit of the residue field.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def primeIdealResidueUnit
    (P : HeightOneSpectrum (π“ž K))
    (a : π“ž K) (ha : a βˆ‰ P.asIdeal) :
    (π“ž K β§Έ P.asIdeal)Λ£
theorem

primeIdealResidueUnit_mul

L169 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealResidueUnit_mul
Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem primeIdealResidueUnit_mul
    (P : HeightOneSpectrum (π“ž K))
    (a b : π“ž K) (ha : a βˆ‰ P.asIdeal) (hb : b βˆ‰ P.asIdeal)
    (hab : a * b βˆ‰ P.asIdeal) :
    primeIdealResidueUnit K P (a * b) hab =
      primeIdealResidueUnit K P a ha *
        primeIdealResidueUnit K P b hb
def

primeIdealPowerResidueSymbol

L181 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol
Documentation

The n-th power-residue symbol (a/P), valued in the common group ΞΌβ‚™(π“ž K).

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def primeIdealPowerResidueSymbol
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (a : π“ž K) (ha : a βˆ‰ P.asIdeal) :
    rootsOfUnity (n : β„•) (π“ž K)
theorem

rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol

L197 β†—
AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol
Documentation

Reduction sends (a/P) to the finite-field formula a^((N(P)-1)/n).

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (a : π“ž K) (ha : a βˆ‰ P.asIdeal) :
    let hn : (n : β„•) ∣ Fintype.card (π“ž K β§Έ P.asIdeal) - 1 := by
      rw [card_primeIdealResidueField K P]
      exact dvd_absNorm_sub_one_of_primitiveRoots K P n hmu hcoprime
    rootsOfUnityReductionEquiv K P n hmu hcoprime
        (primeIdealPowerResidueSymbol K P n hmu hcoprime a ha) =
      finiteFieldPowerResidueSymbol
        (π“ž K β§Έ P.asIdeal) n hn
        (primeIdealResidueUnit K P a ha) := by
  dsimp only [primeIdealPowerResidueSymbol]
  exact (rootsOfUnityReductionEquiv K P n hmu hcoprime).apply_symm_apply _
theorem

primeIdealPowerResidueSymbol_eq_one_iff

L215 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol_eq_one_iff
Documentation

The prime-ideal symbol is one exactly when a is an n-th power modulo P.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem primeIdealPowerResidueSymbol_eq_one_iff
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (a : π“ž K) (ha : a βˆ‰ P.asIdeal) :
    primeIdealPowerResidueSymbol K P n hmu hcoprime a ha = 1 ↔
      βˆƒ u : (π“ž K β§Έ P.asIdeal)Λ£,
        u ^ (n : β„•) = primeIdealResidueUnit K P a ha
theorem

primeIdealPowerResidueSymbol_mul

L245 β†—
AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol_mul
Documentation

Multiplicativity of (a/P) in the numerator.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem primeIdealPowerResidueSymbol_mul
    (P : HeightOneSpectrum (π“ž K)) (n : β„•+)
    (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (hcoprime : (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (a b : π“ž K) (ha : a βˆ‰ P.asIdeal) (hb : b βˆ‰ P.asIdeal) :
    primeIdealPowerResidueSymbol K P n hmu hcoprime (a * b)
        (by
          intro hab
          exact (P.isPrime.mem_or_mem hab).elim ha hb) =
      primeIdealPowerResidueSymbol K P n hmu hcoprime a ha *
        primeIdealPowerResidueSymbol K P n hmu hcoprime b hb := by
  let hab : a * b βˆ‰ P.asIdeal := by
    intro h
    exact (P.isPrime.mem_or_mem h).elim ha hb
  let hn : (n : β„•) ∣ Fintype.card (π“ž K β§Έ P.asIdeal) - 1 := by
    rw [card_primeIdealResidueField K P]
    exact dvd_absNorm_sub_one_of_primitiveRoots K P n hmu hcoprime
  apply (rootsOfUnityReductionEquiv K P n hmu hcoprime).injective
  rw [map_mul]
  rw [rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol,
    rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol,
    rootsOfUnityReductionEquiv_primeIdealPowerResidueSymbol]
  rw [primeIdealResidueUnit_mul K P a b ha hb hab, map_mul]
def

idealPrimeMultiplicity

L271 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity
Documentation

Multiplicity of P in the prime factorization of a nonzero integral ideal.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def idealPrimeMultiplicity
    (P : HeightOneSpectrum (π“ž K)) (I : Ideal (π“ž K)) : β„•
theorem

idealPrimeMultiplicity_mul

L277 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity_mul
Documentation

Prime-ideal multiplicities add under multiplication of nonzero integral ideals.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem idealPrimeMultiplicity_mul
    (P : HeightOneSpectrum (π“ž K))
    (I J : Ideal (π“ž K)) (hI : I β‰  0) (hJ : J β‰  0) :
    idealPrimeMultiplicity K P (I * J) =
      idealPrimeMultiplicity K P I +
        idealPrimeMultiplicity K P J
theorem

idealPrimeMultiplicity_eq_zero_of_not_dvd

L293 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity_eq_zero_of_not_dvd
Documentation

A prime not dividing a nonzero ideal has multiplicity zero in its factorization.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem idealPrimeMultiplicity_eq_zero_of_not_dvd
    (P : HeightOneSpectrum (π“ž K))
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (hP : ¬ P.asIdeal ∣ I) :
    idealPrimeMultiplicity K P I = 0
def

idealPrimeDivisors

L307 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeDivisors
Documentation

The finite set of height-one primes dividing a nonzero denominator ideal.

Naming this set keeps every finite-product presentation on the same subtype, instead of asking typeclass inference to reconstruct definitionally equal subtypes from separate predicate expressions.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def idealPrimeDivisors (I : Ideal (π“ž K)) :
    Set (HeightOneSpectrum (π“ž K))
theorem

mem_idealPrimeDivisors

L314 β†—
AlgebraicNumberTheory.PowerResidueSymbols.mem_idealPrimeDivisors
Documentation

Membership in the named prime-divisor set is ordinary ideal divisibility.

Source context 9 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
omit [NumberField K] in
Lean source Β· statement
theorem mem_idealPrimeDivisors
    (I : Ideal (π“ž K)) (P : HeightOneSpectrum (π“ž K)) :
    P ∈ idealPrimeDivisors K I ↔ P.asIdeal ∣ I
theorem

idealPrimeDivisors_finite

L320 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeDivisors_finite
Documentation

The prime divisors of a nonzero ideal form a finite set.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem idealPrimeDivisors_finite
    (I : Ideal (π“ž K)) (hI : I β‰  0) :
    (idealPrimeDivisors K I).Finite
def

idealPowerResidueSymbol

L330 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueSymbol
Documentation

Ideal power residue symbol. For I = ∏ P ^ v_P(I), define

(a/I) = ∏ (a/P) ^ v_P(I).

The hypotheses only concern the finitely many primes dividing I.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
def idealPowerResidueSymbol
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal) :
    rootsOfUnity (n : β„•) (π“ž K)
def

idealPowerResidueFactor

L355 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueFactor
Documentation

The prime-by-prime factor of the ideal power-residue symbol, extended by 1 away from the prime divisors of the denominator.

Source context 9 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
open scoped Classical in
Lean source Β· statement
def idealPowerResidueFactor
    (I : Ideal (π“ž K))
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal)
    (P : HeightOneSpectrum (π“ž K)) :
    rootsOfUnity (n : β„•) (π“ž K)
theorem

idealPowerResidueFactor_hasFiniteMulSupport

L377 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueFactor_hasFiniteMulSupport
Documentation

Only prime divisors of the denominator can contribute a nontrivial factor.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem idealPowerResidueFactor_hasFiniteMulSupport
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal) :
    Function.HasFiniteMulSupport
      (idealPowerResidueFactor K I n hmu a hcoprime ha)
theorem

idealPowerResidueFactor_mul

L398 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueFactor_mul
Documentation

Prime-by-prime multiplicativity in the denominator.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem idealPowerResidueFactor_mul
    (I J : Ideal (π“ž K)) (hI : I β‰  0) (hJ : J β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I ∨ P.asIdeal ∣ J β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I ∨ P.asIdeal ∣ J β†’ a βˆ‰ P.asIdeal)
    (P : HeightOneSpectrum (π“ž K)) :
    let hcoprimeI :=
      fun P hP => hcoprime P (Or.inl hP)
    let hcoprimeJ :=
      fun P hP => hcoprime P (Or.inr hP)
    let hcoprimeIJ :=
      fun P hP => hcoprime P (P.prime.dvd_mul.mp hP)
    let haI :=
      fun P hP => ha P (Or.inl hP)
    let haJ :=
      fun P hP => ha P (Or.inr hP)
    let haIJ :=
      fun P hP => ha P (P.prime.dvd_mul.mp hP)
    idealPowerResidueFactor K (I * J) n hmu a
        hcoprimeIJ haIJ P =
      idealPowerResidueFactor K I n hmu a
          hcoprimeI haI P *
        idealPowerResidueFactor K J n hmu a
          hcoprimeJ haJ P := by
  classical
  dsimp only
  by_cases hPI : P.asIdeal ∣ I
  · have hPIJ : P.asIdeal ∣ I * J :=
      dvd_mul_of_dvd_left hPI J
    by_cases hPJ : P.asIdeal ∣ J
    Β· rw [idealPowerResidueFactor, dite_eq_left hPIJ,
        idealPowerResidueFactor, dite_eq_left hPI,
        idealPowerResidueFactor, dite_eq_left hPJ,
        idealPrimeMultiplicity_mul K P I J hI hJ,
        pow_add]
    Β· have hmJ :
          idealPrimeMultiplicity K P J = 0 :=
        idealPrimeMultiplicity_eq_zero_of_not_dvd
          K P J hJ hPJ
      rw [idealPowerResidueFactor, dite_eq_left hPIJ,
        idealPowerResidueFactor, dite_eq_left hPI,
        idealPowerResidueFactor, dite_eq_right hPJ,
        idealPrimeMultiplicity_mul K P I J hI hJ,
        hmJ, add_zero, mul_one]
  · by_cases hPJ : P.asIdeal ∣ J
    · have hPIJ : P.asIdeal ∣ I * J :=
        dvd_mul_of_dvd_right hPJ I
      have hmI :
          idealPrimeMultiplicity K P I = 0 :=
        idealPrimeMultiplicity_eq_zero_of_not_dvd
          K P I hI hPI
      rw [idealPowerResidueFactor, dite_eq_left hPIJ,
        idealPowerResidueFactor, dite_eq_right hPI,
        idealPowerResidueFactor, dite_eq_left hPJ,
        idealPrimeMultiplicity_mul K P I J hI hJ,
        hmI, zero_add, one_mul]
    · have hPIJ : ¬ P.asIdeal ∣ I * J := by
        intro h
        exact (P.prime.dvd_mul.mp h).elim hPI hPJ
      rw [idealPowerResidueFactor, dite_eq_right hPIJ,
        idealPowerResidueFactor, dite_eq_right hPI,
        idealPowerResidueFactor, dite_eq_right hPJ, one_mul]
theorem

idealPowerResidueSymbol_eq_finprod

L469 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueSymbol_eq_finprod
Documentation

The subtype product defining the ideal symbol is equivalently the finite product over all finite primes, with factor 1 away from the denominator.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· statement
theorem idealPowerResidueSymbol_eq_finprod
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal) :
    idealPowerResidueSymbol K I hI n hmu a hcoprime ha =
      ∏ᢠ P : HeightOneSpectrum (π“ž K),
        idealPowerResidueFactor K I n hmu a hcoprime ha P
theorem

idealPowerResidueSymbol_mul_denominator

L512 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueSymbol_mul_denominator
Documentation

Multiplicativity of the ideal power residue symbol in the denominator ideal.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem idealPowerResidueSymbol_mul_denominator
    (I J : Ideal (π“ž K)) (hI : I β‰  0) (hJ : J β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I ∨ P.asIdeal ∣ J β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I ∨ P.asIdeal ∣ J β†’ a βˆ‰ P.asIdeal) :
    let hcoprimeI :=
      fun P hP => hcoprime P (Or.inl hP)
    let hcoprimeJ :=
      fun P hP => hcoprime P (Or.inr hP)
    let hcoprimeIJ :=
      fun P hP => hcoprime P (P.prime.dvd_mul.mp hP)
    let haI :=
      fun P hP => ha P (Or.inl hP)
    let haJ :=
      fun P hP => ha P (Or.inr hP)
    let haIJ :=
      fun P hP => ha P (P.prime.dvd_mul.mp hP)
    idealPowerResidueSymbol K (I * J) (mul_ne_zero hI hJ)
        n hmu a hcoprimeIJ haIJ =
      idealPowerResidueSymbol K I hI n hmu a hcoprimeI haI *
        idealPowerResidueSymbol K J hJ n hmu a hcoprimeJ haJ := by
  dsimp only
  rw [idealPowerResidueSymbol_eq_finprod,
    idealPowerResidueSymbol_eq_finprod,
    idealPowerResidueSymbol_eq_finprod]
  rw [← finprod_mul_distrib
    (idealPowerResidueFactor_hasFiniteMulSupport
      K I hI n hmu a _ _)
    (idealPowerResidueFactor_hasFiniteMulSupport
      K J hJ n hmu a _ _)]
  apply finprod_congr
  intro P
  exact idealPowerResidueFactor_mul
    K I J hI hJ n hmu a hcoprime ha P
theorem

idealPowerResidueSymbol_eq_prod

L554 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueSymbol_eq_prod
Documentation

Unfolded finite-product form of the ideal power residue symbol.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem idealPowerResidueSymbol_eq_prod
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal) :
    letI : Fintype
        (idealPrimeDivisors K I) :=
      (idealPrimeDivisors_finite K I hI).fintype
    idealPowerResidueSymbol K I hI n hmu a hcoprime ha =
      ∏ P : idealPrimeDivisors K I,
        primeIdealPowerResidueSymbol K P.1 n hmu
            (hcoprime P.1 ((mem_idealPrimeDivisors K I P.1).mp P.2)) a
            (ha P.1 ((mem_idealPrimeDivisors K I P.1).mp P.2)) ^
          idealPrimeMultiplicity K P.1 I :=
  rfl
theorem

idealPowerResidueSymbol_mul

L577 β†—
AlgebraicNumberTheory.PowerResidueSymbols.idealPowerResidueSymbol_mul
Documentation

Multiplicativity of the ideal power residue symbol in the numerator.

Source context 8 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
noncomputable section
namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
attribute [local instance] Ideal.Quotient.field
variable (K : Type*) [Field K] [NumberField K]
noncomputable local instance primeIdealResidueFintype
    (P : HeightOneSpectrum (π“ž K)) :
    Fintype (π“ž K β§Έ P.asIdeal) :=
  Fintype.ofFinite _
Lean source Β· full declaration
theorem idealPowerResidueSymbol_mul
    (I : Ideal (π“ž K)) (hI : I β‰  0)
    (n : β„•+) (hmu : (primitiveRoots (n : β„•) K).Nonempty)
    (a b : π“ž K)
    (hcoprime :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’
          (Ideal.absNorm P.asIdeal).Coprime (n : β„•))
    (ha :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ a βˆ‰ P.asIdeal)
    (hb :
      βˆ€ P : HeightOneSpectrum (π“ž K),
        P.asIdeal ∣ I β†’ b βˆ‰ P.asIdeal) :
    idealPowerResidueSymbol K I hI n hmu (a * b) hcoprime
        (fun P hP hab =>
          (P.isPrime.mem_or_mem hab).elim (ha P hP) (hb P hP)) =
      idealPowerResidueSymbol K I hI n hmu a hcoprime ha *
        idealPowerResidueSymbol K I hI n hmu b hcoprime hb := by
  classical
  let : Fintype
      (idealPrimeDivisors K I) :=
    (idealPrimeDivisors_finite K I hI).fintype
  unfold idealPowerResidueSymbol
  rw [← Finset.prod_mul_distrib]
  apply Finset.prod_congr rfl
  intro P _
  rw [primeIdealPowerResidueSymbol_mul, mul_pow]

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