NYLL
Module

PowerResidueReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.PowerResidueReciprocity
93 declarations indexed from sourceView source ↗

Module documentation

Bad-place support and correction for power-residue reciprocity

For two global units a and b, the local Kummer factor can be nontrivial only where a, b, or the exponent fails to be a valuation-ring unit. This file records that concrete finite set, proves triviality outside it from the unramified simple-Kummer criterion and the local norm kernel, and constructs the exponent-place and infinite-place correction in the common field-valued group of roots of unity.

Quadratic specialization over the rational field

Rational principal-ideal factorization

Imports16
Imported by3

Declarations

theorem

canonicalValuation_eq_of_valuation_eq

L53 ↗
GlobalClassFieldTheory.Reciprocity.canonicalValuation_eq_of_valuation_eq
Documentation

Equality for the valuation used to define a valuative relation transports to equality in the relation's canonical value group.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem canonicalValuation_eq_of_valuation_eq
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation R Γ) (x y : R) (hxy : v x = v y) :
    letI : ValuativeRel R := ValuativeRel.ofValuation v
    ValuativeRel.valuation R x = ValuativeRel.valuation R y := by
  let : ValuativeRel R := ValuativeRel.ofValuation v
  change
    ValuativeRel.ValueGroupWithZero.mk x 1 =
      ValuativeRel.ValueGroupWithZero.mk y 1
  rw [ValuativeRel.ValueGroupWithZero.mk_eq_mk]
  constructor
  · change v (x * (1 : R)) ≤ v (y * (1 : R))
    simpa only [mul_one] using hxy.le
  · change v (y * (1 : R)) ≤ v (x * (1 : R))
    simpa only [mul_one] using hxy.ge
theorem

finitePlaceAdicAbv_nonarchimedeanAbsoluteValue

L72 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceAdicAbv_nonarchimedeanAbsoluteValue
Documentation

The bounded-natural-number form of nonarchimedeanness for a finite-place absolute value. Naming this bridge keeps all completion residue constructions on one proof-irrelevant provider.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceAdicAbv_nonarchimedeanAbsoluteValue
    (v : HeightOneSpectrum (𝓞 K)) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (HeightOneSpectrum.adicAbv K v)
theorem

finiteFieldPowerResidueSymbol_unitsMap_ringEquiv

L83 ↗
GlobalClassFieldTheory.Reciprocity.finiteFieldPowerResidueSymbol_unitsMap_ringEquiv
Documentation

Finite-field power-residue symbols commute with a field equivalence. The statement is made on underlying units so it can be reused with every roots-of-unity transport occurring below.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finiteFieldPowerResidueSymbol_unitsMap_ringEquiv
    {k l : Type*} [Field k] [Field l] [Fintype k] [Fintype l]
    (e : k ≃+* l) (n : ℕ+)
    (hnk : (n : ℕ) ∣ Fintype.card k - 1)
    (hnl : (n : ℕ) ∣ Fintype.card l - 1)
    (u : kˣ) :
    Units.map e.toMonoidHom
        ((AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol
            k n hnk u :
            rootsOfUnity (n : ℕ) k) : kˣ) =
      ((AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol
          l n hnl
          (Units.map e.toMonoidHom u) :
            rootsOfUnity (n : ℕ) l) : lˣ)
def

finitePlacePrimeResidueEquivLocalResidue

L106 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeResidueEquivLocalResidue
Documentation

The residue field of a finite-place completion is canonically the prime-ideal residue field. The construction passes through the localization at the prime and then through the residue equivalence induced by completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def finitePlacePrimeResidueEquivLocalResidue
    (v : HeightOneSpectrum (𝓞 K)) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    (𝓞 K ⧸ v.asIdeal) ≃+* 𝓀[C] := by
  let a := HeightOneSpectrum.adicAbv K v
  let ha : LubinTate.Valuations.NonarchimedeanAbsoluteValue a :=
    finitePlaceAdicAbv_nonarchimedeanAbsoluteValue K v
  let C := a.Completion
  letI : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v
  letI : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  let V := LubinTate.Valuations.exponentialValuationSubring
    (AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation a ha)
  let aC := AbsoluteValue.completionAbsoluteValue a
  let haC : LubinTate.Valuations.NonarchimedeanAbsoluteValue aC :=
    (AbsoluteValue.isNonarchimedean_iff_bounded_nat aC).1
      (AbsoluteValue.completionAbsoluteValue_isNonarchimedean a
        ((AbsoluteValue.isNonarchimedean_iff_bounded_nat a).2 ha))
  let VC := LubinTate.Valuations.exponentialValuationSubring
    (AlgebraicNumberTheory.Valuations.absoluteValueExponentialValuation aC haC)
  let Rv := v.valuationSubringAtPrime K
  letI : IsLocalRing Rv :=
    IsLocalization.AtPrime.isLocalRing Rv v.asIdeal
  have hBase : Rv.toSubring = V := by
    ext x
    rw [AlgebraicNumberTheory.Valuations.mem_absoluteValueExponentialSubring_iff]
    change x ∈ v.valuationSubringAtPrime K ↔ _
    rw [v.valuationSubringAtPrime_eq_valuationSubring]
    change v.valuation K x ≤ 1 ↔ a x ≤ 1
    rw [HeightOneSpectrum.adicAbv_def]
    exact_mod_cast
      (WithZeroMulInt.toNNReal_le_one_iff
        (HeightOneSpectrum.one_lt_absNorm_nnreal v)).symm
  let eBase : Rv ≃+* V := RingEquiv.subringCongr hBase
  have hCompletion : VC = 𝒪[C] := by
    ext x
    rw [AlgebraicNumberTheory.Valuations.mem_absoluteValueExponentialSubring_iff]
    change ‖x‖ ≤ 1 ↔ x ∈ 𝒪[C]
    exact
      (finitePlaceCompletion_mem_integers_iff_norm_le_one
        a (HeightOneSpectrum.isNonarchimedean_adicAbv K v) x).symm
  let eCompletionRing : VC ≃+* 𝒪[C] :=
    RingEquiv.subringCongr hCompletion
  let eIdeal : (𝓞 K ⧸ v.asIdeal) ≃+* v.asIdeal.ResidueField :=
    RingEquiv.ofBijective
      (algebraMap (𝓞 K ⧸ v.asIdeal) v.asIdeal.ResidueField)
      v.asIdeal.bijective_algebraMap_quotient_residueField
  let eLocalization : Localization.AtPrime v.asIdeal ≃ₐ[𝓞 K] Rv :=
    IsLocalization.algEquiv v.asIdeal.primeCompl _ _
  exact
    eIdeal |>.trans
      (IsLocalRing.ResidueField.mapEquiv eLocalization.toRingEquiv) |>.trans
      (IsLocalRing.ResidueField.mapEquiv eBase) |>.trans
      (AlgebraicNumberTheory.Valuations.completionResidueEquiv a ha) |>.trans
      (IsLocalRing.ResidueField.mapEquiv eCompletionRing)
def

finitePlaceIntegralCompletionElement

L169 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceIntegralCompletionElement
Documentation

The image of an algebraic integer in the valuation ring of a finite-place completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def finitePlaceIntegralCompletionElement
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    𝒪[C] := by
  let C := (HeightOneSpectrum.adicAbv K v).Completion
  letI : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v
  letI : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  exact ⟨algebraMap K C (x : K), by
    rw [finitePlaceCompletion_mem_integers_iff_norm_le_one
      (HeightOneSpectrum.adicAbv K v)
      (HeightOneSpectrum.isNonarchimedean_adicAbv K v)]
    calc
      ‖algebraMap K C (x : K)‖ =
          HeightOneSpectrum.adicAbv K v (x : K) :=
        AbsoluteValue.completionAbsoluteValue_coe
          (HeightOneSpectrum.adicAbv K v) (x : K)
      _ ≤ 1 :=
        v.adicAbv_coe_le_one
          (HeightOneSpectrum.one_lt_absNorm_nnreal v) x⟩
theorem

finitePlaceIntegralCompletionElement_coe

L198 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceIntegralCompletionElement_coe
Documentation

The finite-place integral element has the expected underlying completion value.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlaceIntegralCompletionElement_coe
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    (finitePlaceIntegralCompletionElement K v x : C) =
      algebraMap K C (x : K) :=
  rfl
theorem

finitePlacePrimeResidueEquivLocalResidue_mk

L212 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeResidueEquivLocalResidue_mk
Documentation

The finite-place residue equivalence sends the class of an algebraic integer to the residue of its canonical image in the completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlacePrimeResidueEquivLocalResidue_mk
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    finitePlacePrimeResidueEquivLocalResidue K v
        (Ideal.Quotient.mk v.asIdeal x) =
      IsLocalRing.residue 𝒪[C]
        (finitePlaceIntegralCompletionElement K v x) := by
  simp only [finitePlacePrimeResidueEquivLocalResidue,
    finitePlaceIntegralCompletionElement, RingEquiv.trans_apply]
  rw [RingEquiv.ofBijective_apply,
    Ideal.algebraMap_quotient_residueField_mk]
  rw [IsScalarTower.algebraMap_apply
    (NumberField.RingOfIntegers K) (Localization.AtPrime v.asIdeal)]
  rw [IsLocalRing.ResidueField.algebraMap_eq]
  simp only [IsLocalRing.ResidueField.mapEquiv_apply,
    IsLocalRing.ResidueField.map_residue]
  rw [AlgebraicNumberTheory.Valuations.completionResidueEquiv_residue]
  simp only [IsLocalRing.ResidueField.map_residue]
  congr 1
  apply Subtype.ext
  change
    algebraMap K (HeightOneSpectrum.adicAbv K v).Completion
        (((IsLocalization.algEquiv v.asIdeal.primeCompl
            (Localization.AtPrime v.asIdeal)
            (v.valuationSubringAtPrime K))
          (algebraMap (𝓞 K) (Localization.AtPrime v.asIdeal) x) :
        v.valuationSubringAtPrime K) : K) =
      algebraMap K (HeightOneSpectrum.adicAbv K v).Completion (x : K)
  rw [AlgEquiv.commutes]
  rw [IsScalarTower.algebraMap_apply
    (NumberField.RingOfIntegers K) (v.valuationSubringAtPrime K)]
  rfl
def

nonzeroIntegralFieldUnit

L250 ↗
GlobalClassFieldTheory.Reciprocity.nonzeroIntegralFieldUnit
Documentation

A nonzero algebraic integer, regarded as a global field unit.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def nonzeroIntegralFieldUnit (x : 𝓞 K) (hx : x ≠ 0) : Kˣ
theorem

nonzeroIntegralFieldUnit_coe

L259 ↗
GlobalClassFieldTheory.Reciprocity.nonzeroIntegralFieldUnit_coe
Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem nonzeroIntegralFieldUnit_coe (x : 𝓞 K) (hx : x ≠ 0) :
    ((nonzeroIntegralFieldUnit K x hx : Kˣ) : K) = (x : K)
def

primeAvoidingIntegralFieldUnit

L265 ↗
GlobalClassFieldTheory.Reciprocity.primeAvoidingIntegralFieldUnit
Documentation

An algebraic integer avoiding a prime ideal, regarded as a nonzero element of the global field.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def primeAvoidingIntegralFieldUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) : Kˣ
theorem

primeAvoidingIntegralFieldUnit_coe

L276 ↗
GlobalClassFieldTheory.Reciprocity.primeAvoidingIntegralFieldUnit_coe
Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem primeAvoidingIntegralFieldUnit_coe
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    ((primeAvoidingIntegralFieldUnit K v x hx : Kˣ) : K) = (x : K)
def

finitePlaceIntegralCompletionUnit

L284 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceIntegralCompletionUnit
Documentation

An algebraic integer nonzero modulo v, regarded as a unit of the valuation ring of the finite-place completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def finitePlaceIntegralCompletionUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    𝒪[C]ˣ := by
  let a := HeightOneSpectrum.adicAbv K v
  let C := a.Completion
  letI : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v
  letI : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  let y : C := algebraMap K C (x : K)
  have hyNorm : ‖y‖ = 1 := by
    calc
      ‖y‖ = a (x : K) :=
        AbsoluteValue.completionAbsoluteValue_coe a (x : K)
      _ = ‖NumberField.FinitePlace.embedding v (x : K)‖ :=
        (NumberField.FinitePlace.norm_embedding v (x : K)).symm
      _ = 1 :=
        (NumberField.FinitePlace.norm_eq_one_iff_notMem K v x).2 hx
  have hyNe : y ≠ 0 := by
    intro hy
    rw [hy, norm_zero] at hyNorm
    exact zero_ne_one hyNorm
  let yIntegral : 𝒪[C] := ⟨y, by
    rw [finitePlaceCompletion_mem_integers_iff_norm_le_one
      a (HeightOneSpectrum.isNonarchimedean_adicAbv K v)]
    exact hyNorm.le⟩
  let yInvIntegral : 𝒪[C] := ⟨y⁻¹, by
    rw [finitePlaceCompletion_mem_integers_iff_norm_le_one
      a (HeightOneSpectrum.isNonarchimedean_adicAbv K v),
      norm_inv, hyNorm, inv_one]⟩
  exact {
    val := yIntegral
    inv := yInvIntegral
    val_inv := by
      apply Subtype.ext
      exact mul_inv_cancel₀ hyNe
    inv_val := by
      apply Subtype.ext
      exact inv_mul_cancel₀ hyNe }
theorem

finitePlaceIntegralCompletionUnit_coe

L333 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceIntegralCompletionUnit_coe
Documentation

Forgetting the integral-unit structure recovers the ordinary image of the algebraic integer in the finite-place completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlaceIntegralCompletionUnit_coe
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    (((finitePlaceIntegralCompletionUnit K v x hx : 𝒪[C]ˣ) : 𝒪[C]) : C) =
      algebraMap K C (x : K) := by
  rfl
theorem

finitePlaceHilbert_completionUnit_primeAvoidingIntegralFieldUnit

L347 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_completionUnit_primeAvoidingIntegralFieldUnit
Documentation

The completion image of a prime-avoiding algebraic integer is the field unit underlying its canonical valuation-ring unit.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlaceHilbert_completionUnit_primeAvoidingIntegralFieldUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    finitePlaceHilbert_completionUnit K v
        (primeAvoidingIntegralFieldUnit K v x hx) =
      integerUnitsToFieldUnits C
        (finitePlaceIntegralCompletionUnit K v x hx) := by
  let C := (HeightOneSpectrum.adicAbv K v).Completion
  let : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v
  let : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  dsimp only
  apply Units.ext
  change
    algebraMap K C (x : K) =
      (((finitePlaceIntegralCompletionUnit K v x hx : 𝒪[C]ˣ) :
        𝒪[C]) : C)
  exact (finitePlaceIntegralCompletionUnit_coe K v x hx).symm
theorem

finitePlaceIntegralCompletionUnit_val

L375 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceIntegralCompletionUnit_val
Documentation

As an element of the completion valuation ring, the lifted unit is the canonical lifted algebraic integer.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlaceIntegralCompletionUnit_val
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    (finitePlaceIntegralCompletionUnit K v x hx : 𝒪[C]) =
      finitePlaceIntegralCompletionElement K v x := by
  dsimp only
  apply Subtype.ext
  exact finitePlaceIntegralCompletionUnit_coe K v x hx
theorem

finitePlace_integerUnitsToResidueUnits_integralUnit

L391 ↗
GlobalClassFieldTheory.Reciprocity.finitePlace_integerUnitsToResidueUnits_integralUnit
Documentation

Reduction of the canonical completion unit agrees with reduction modulo the corresponding global prime ideal.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlace_integerUnitsToResidueUnits_integralUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    integerUnitsToResidueUnits C
        (finitePlaceIntegralCompletionUnit K v x hx) =
      Units.map
        (finitePlacePrimeResidueEquivLocalResidue K v).toMonoidHom
        (AlgebraicNumberTheory.PowerResidueSymbols.primeIdealResidueUnit
          K v x hx) := by
  dsimp only
  apply Units.ext
  change
    IsLocalRing.residue 𝒪[(HeightOneSpectrum.adicAbv K v).Completion]
        (finitePlaceIntegralCompletionUnit K v x hx :
          𝒪[(HeightOneSpectrum.adicAbv K v).Completion]) =
      finitePlacePrimeResidueEquivLocalResidue K v
        (Ideal.Quotient.mk v.asIdeal x)
  simpa only [finitePlaceIntegralCompletionUnit_val] using
    (finitePlacePrimeResidueEquivLocalResidue_mk K v x).symm
def

integralRootsOfUnityToNthRoots

L418 ↗
GlobalClassFieldTheory.Reciprocity.integralRootsOfUnityToNthRoots
Documentation

The canonical inclusion from integral roots of unity into the common field-valued group used by the global Hilbert symbols.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def integralRootsOfUnityToNthRoots
    (n : ℕ) :
    rootsOfUnity n (𝓞 K) →* nthRootsSubgroup K n where
  toFun z :=
    ⟨Units.map (algebraMap (𝓞 K) K).toMonoidHom z.1, by
      calc
        Units.map (algebraMap (𝓞 K) K).toMonoidHom z.1 ^ n =
            Units.map (algebraMap (𝓞 K) K).toMonoidHom (z.1 ^ n) :=
          (map_pow
            (Units.map (algebraMap (𝓞 K) K).toMonoidHom) z.1 n).symm
        _ = 1 := by rw [z.2, map_one]⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (Units.map (algebraMap (𝓞 K) K).toMonoidHom)
  map_mul' := by
    intro z w
    apply Subtype.ext
    exact map_mul
      (Units.map (algebraMap (𝓞 K) K).toMonoidHom) z.1 w.1
theorem

integralRootsOfUnityToNthRoots_apply

L441 ↗
GlobalClassFieldTheory.Reciprocity.integralRootsOfUnityToNthRoots_apply
Documentation

The integral-root inclusion is the underlying unit map.

Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem integralRootsOfUnityToNthRoots_apply
    (n : ℕ) (z : rootsOfUnity n (𝓞 K)) :
    (integralRootsOfUnityToNthRoots K n z).1 =
      Units.map (algebraMap (𝓞 K) K).toMonoidHom z.1
theorem

integralRootsOfUnityToNthRoots_injective

L449 ↗
GlobalClassFieldTheory.Reciprocity.integralRootsOfUnityToNthRoots_injective
Documentation

The integral-to-field inclusion is injective on roots of unity.

Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem integralRootsOfUnityToNthRoots_injective
    (n : ℕ) :
    Function.Injective (integralRootsOfUnityToNthRoots K n)
theorem

finitePlace_localNthRootsReduction_integralRoots

L463 ↗
GlobalClassFieldTheory.Reciprocity.finitePlace_localNthRootsReduction_integralRoots
Documentation

Reduction after embedding an integral global root of unity into a finite-place completion is the transport of reduction modulo the corresponding prime ideal.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlace_localNthRootsReduction_integralRoots
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (z : rootsOfUnity (n : ℕ) (𝓞 K)) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    (localNthRootsReduction C n
        (nthRootsSubgroupMap K C (n : ℕ)
          (integralRootsOfUnityToNthRoots K (n : ℕ) z))).1 =
      Units.map
        (finitePlacePrimeResidueEquivLocalResidue K v).toMonoidHom
        (AlgebraicNumberTheory.PowerResidueSymbols.rootsOfUnityReduction
          K v (n : ℕ) z).1 := by
  dsimp only
  apply Units.ext
  change
    IsLocalRing.residue 𝒪[(HeightOneSpectrum.adicAbv K v).Completion]
        (nthRootIntegerUnit
          (HeightOneSpectrum.adicAbv K v).Completion n
          (nthRootsSubgroupMap K
            (HeightOneSpectrum.adicAbv K v).Completion (n : ℕ)
            (integralRootsOfUnityToNthRoots K (n : ℕ) z)) :
          𝒪[(HeightOneSpectrum.adicAbv K v).Completion]) =
      finitePlacePrimeResidueEquivLocalResidue K v
        (Ideal.Quotient.mk v.asIdeal (z.1 : 𝓞 K))
  rw [finitePlacePrimeResidueEquivLocalResidue_mk]
  congr 1
def

powerResidueExponentIdeal

L494 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueExponentIdeal
Documentation

The integral principal ideal generated by the exponent.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def powerResidueExponentIdeal (n : ℕ+) : Ideal (𝓞 K)
theorem

powerResidueExponentIdeal_ne_zero

L498 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueExponentIdeal_ne_zero
Documentation

The exponent ideal is nonzero in a number field.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem powerResidueExponentIdeal_ne_zero (n : ℕ+) :
    powerResidueExponentIdeal K n ≠ 0
theorem

ideal_span_singleton_ne_zero

L505 ↗
GlobalClassFieldTheory.Reciprocity.ideal_span_singleton_ne_zero
Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem ideal_span_singleton_ne_zero
    {x : 𝓞 K} (hx : x ≠ 0) : Ideal.span {x} ≠ 0
def

powerResidueExponentFinitePlaces

L512 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueExponentFinitePlaces
Documentation

The finite places dividing the exponent. These, together with all infinite places, are precisely the correction places in the reciprocity formula once the two principal denominator supports are removed.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def powerResidueExponentFinitePlaces
    (n : ℕ+) : Finset (HeightOneSpectrum (𝓞 K))
theorem

mem_powerResidueExponentFinitePlaces_iff

L520 ↗
GlobalClassFieldTheory.Reciprocity.mem_powerResidueExponentFinitePlaces_iff
Documentation

Membership in the exponent-place support is divisibility by the exponent ideal.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem mem_powerResidueExponentFinitePlaces_iff
    (n : ℕ+) (v : HeightOneSpectrum (𝓞 K)) :
    v ∈ powerResidueExponentFinitePlaces K n ↔
      v.asIdeal ∣ powerResidueExponentIdeal K n
theorem

finitePlace_natCast_valuation_eq_one_of_not_mem_exponent

L530 ↗
GlobalClassFieldTheory.Reciprocity.finitePlace_natCast_valuation_eq_one_of_not_mem_exponent
Documentation

At a finite place not dividing the exponent, the exponent is a unit in the canonical completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlace_natCast_valuation_eq_one_of_not_mem_exponent
    (n : ℕ+) (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueExponentFinitePlaces K n) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    ValuativeRel.valuation C ((n : ℕ) : C) = 1 := by
  dsimp only
  let : IsUltrametricDist
      (HeightOneSpectrum.adicAbv K v).Completion :=
    finitePlaceArtinCompletionIsUltrametricDist
      (HeightOneSpectrum.adicAbv K v)
      (HeightOneSpectrum.isNonarchimedean_adicAbv K v)
  have hvNotDvd :
      ¬ v.asIdeal ∣ powerResidueExponentIdeal K n := by
    simpa only [mem_powerResidueExponentFinitePlaces_iff] using hv
  have hvNotMem : ((n : ℕ) : 𝓞 K) ∉ v.asIdeal := by
    intro hvMem
    apply hvNotDvd
    rw [powerResidueExponentIdeal, Ideal.dvd_span_singleton]
    exact hvMem
  let C := (HeightOneSpectrum.adicAbv K v).Completion
  have hNorm : ‖((n : ℕ) : C)‖ = 1 := by
    calc
      ‖((n : ℕ) : C)‖ =
          ‖algebraMap K C (((n : ℕ) : K))‖ := by rw [map_natCast]
      _ = HeightOneSpectrum.adicAbv K v (((n : ℕ) : K)) :=
        AbsoluteValue.completionAbsoluteValue_coe
          (HeightOneSpectrum.adicAbv K v) (((n : ℕ) : K))
      _ = ‖NumberField.FinitePlace.embedding v (((n : ℕ) : K))‖ :=
        (NumberField.FinitePlace.norm_embedding v (((n : ℕ) : K))).symm
      _ = 1 :=
        (NumberField.FinitePlace.norm_eq_one_iff_notMem K v
          (((n : ℕ) : 𝓞 K))).2 hvNotMem
  let vCNorm := NormedField.valuation (K := C)
  let : vCNorm.Compatible := Valuation.Compatible.ofValuation vCNorm
  have hnCNorm : vCNorm ((n : ℕ) : C) = 1 := by
    change ‖((n : ℕ) : C)‖₊ = 1
    exact NNReal.eq (by simpa using hNorm)
  exact
    (ValuativeRel.isEquiv vCNorm (ValuativeRel.valuation C))
      |>.eq_one_iff_eq_one.mp hnCNorm
def

finitePlaceLocalTamePowerResidueSymbolValue

L575 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalTamePowerResidueSymbolValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceLocalTamePowerResidueSymbolValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    nthRootsSubgroup (HeightOneSpectrum.adicAbv K v).Completion (n : ℕ)
def

finitePlaceLocalTamePowerResidueSymbolFieldValue

L591 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalTamePowerResidueSymbolFieldValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceLocalTamePowerResidueSymbolFieldValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    (HeightOneSpectrum.adicAbv K v).Completion
def

finitePlacePrimeIdealPowerResidueIntegralRoot

L607 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeIdealPowerResidueIntegralRoot
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlacePrimeIdealPowerResidueIntegralRoot
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    rootsOfUnity (n : ℕ) (𝓞 K)
def

finitePlacePrimeIdealPowerResidueGlobalRoot

L616 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeIdealPowerResidueGlobalRoot
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlacePrimeIdealPowerResidueGlobalRoot
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) : nthRootsSubgroup K (n : ℕ)
def

finitePlacePrimeIdealPowerResidueFactorValue

L624 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeIdealPowerResidueFactorValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlacePrimeIdealPowerResidueFactorValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    nthRootsSubgroup (HeightOneSpectrum.adicAbv K v).Completion (n : ℕ)
def

finitePlacePrimeIdealPowerResidueFactorFieldValue

L633 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeIdealPowerResidueFactorFieldValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlacePrimeIdealPowerResidueFactorFieldValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    (HeightOneSpectrum.adicAbv K v).Completion
def

finitePlaceLocalTamePowerResidueSymbolResidueValue

L644 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalTamePowerResidueSymbolResidueValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def finitePlaceLocalTamePowerResidueSymbolResidueValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C := finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    𝓀[C] := by
  dsimp only
  let C := (HeightOneSpectrum.adicAbv K v).Completion
  letI : ValuativeRel C := finitePlaceLocalArtinCompletionValuativeRel v
  letI : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  letI : Fintype 𝓀[C] := Fintype.ofFinite _
  have hnLocal : (n : ℕ) ∣ Fintype.card 𝓀[C] - 1 := by
    rw [← Nat.card_eq_fintype_card]
    exact dvd_residueCard_sub_one_of_primitiveRoots C n
      (finitePlace_natCast_valuation_eq_one_of_not_mem_exponent K n v hv)
      (finitePlaceHilbert_primitiveRoots_nonempty K n hmu v)
  exact
    (((AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol
        𝓀[C] n hnLocal
        (integerUnitsToResidueUnits C
          (finitePlaceIntegralCompletionUnit K v a ha)) :
      rootsOfUnity (n : ℕ) 𝓀[C]).1 : 𝓀[C]ˣ) : 𝓀[C])
def

finitePlacePrimeIdealPowerResidueFactorResidueValue

L672 ↗
GlobalClassFieldTheory.Reciprocity.finitePlacePrimeIdealPowerResidueFactorResidueValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
def finitePlacePrimeIdealPowerResidueFactorResidueValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    let C := (HeightOneSpectrum.adicAbv K v).Completion
    letI : ValuativeRel C := finitePlaceLocalArtinCompletionValuativeRel v
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
    𝓀[C] := by
  dsimp only
  let C := (HeightOneSpectrum.adicAbv K v).Completion
  letI : ValuativeRel C := finitePlaceLocalArtinCompletionValuativeRel v
  letI : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
  exact
    (((localNthRootsReduction C n
        (nthRootsSubgroupMap K C (n : ℕ)
          (integralRootsOfUnityToNthRoots K (n : ℕ)
            (AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol
              K v n hmu hcoprime a ha)))).1 : 𝓀[C]ˣ) : 𝓀[C])
theorem

finitePlaceLocalTamePowerResidueSymbol_residueValue_eq

L697 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalTamePowerResidueSymbol_residueValue_eq
Documentation

The tame symbol in a finite-place completion is the image of the prime-ideal power-residue symbol. All comparisons are canonical: the only place hypothesis says that the place does not divide the exponent.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceLocalTamePowerResidueSymbol_residueValue_eq
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    finitePlaceLocalTamePowerResidueSymbolResidueValue K v n hmu hv a ha =
      finitePlacePrimeIdealPowerResidueFactorResidueValue
        K v n hmu hcoprime a ha
theorem

finitePlaceLocalTamePowerResidueSymbolFieldValue_eq_primeIdealValue

L740 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalTamePowerResidueSymbolFieldValue_eq_primeIdealValue
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceLocalTamePowerResidueSymbolFieldValue_eq_primeIdealValue
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) :
    @Eq (HeightOneSpectrum.adicAbv K v).Completion
      (finitePlaceLocalTamePowerResidueSymbolFieldValue K v n hmu hv a ha)
      (finitePlacePrimeIdealPowerResidueFactorFieldValue
        K v n hmu hcoprime a ha)
def

finitePlaceNormalizedValuation

L783 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormalizedValuation
Documentation

The normalized additive valuation of a global field unit in the canonical completion at a finite place.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceNormalizedValuation
    (v : HeightOneSpectrum (𝓞 K)) (x : Kˣ) : ℤ
theorem

finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor_zpow

L796 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor_zpow
Documentation

Away from the exponent, a finite-place Hilbert factor with integral-unit first entry is the prime-ideal power-residue symbol raised to the negative normalized valuation of the second entry.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor_zpow
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) (b : Kˣ) :
    finitePlaceHilbertSymbol K n hnK hmu v
        (primeAvoidingIntegralFieldUnit K v a ha) b =
      integralRootsOfUnityToNthRoots K (n : ℕ)
          (AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol
              K v n hmu hcoprime a ha) ^
        (-finitePlaceNormalizedValuation K v b)
theorem

finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor

L854 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor
Documentation

Endpoint form of the finite-place local/global power-residue comparison.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_eq_primeIdealPowerResidueFactor
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a : 𝓞 K) (ha : a ∉ v.asIdeal) (b : Kˣ) :
    finitePlaceHilbertSymbol K n hnK hmu v
        (primeAvoidingIntegralFieldUnit K v a ha) b =
      integralRootsOfUnityToNthRoots K (n : ℕ)
          (AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol
              K v n hmu hcoprime a ha) ^
        (-finitePlaceNormalizedValuation K v b)
theorem

intValuation_eq_exp_neg_idealPrimeMultiplicity

L872 ↗
GlobalClassFieldTheory.Reciprocity.intValuation_eq_exp_neg_idealPrimeMultiplicity
Documentation

The Dedekind prime multiplicity is the exponent occurring in the integer-valued adic valuation.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem intValuation_eq_exp_neg_idealPrimeMultiplicity
    (v : HeightOneSpectrum (𝓞 K)) (x : 𝓞 K) (hx : x ≠ 0) :
    v.intValuation x =
      WithZero.exp
        (-(AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity
          K v (Ideal.span {x}) : ℤ))
theorem

finitePlaceNormalizedValuation_nonzeroIntegralFieldUnit

L884 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormalizedValuation_nonzeroIntegralFieldUnit
Documentation

For an integral element, the normalized valuation in the canonical finite-place completion is the negative multiplicity of the prime in its principal ideal.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceNormalizedValuation_nonzeroIntegralFieldUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ≠ 0) :
    finitePlaceNormalizedValuation K v
        (nonzeroIntegralFieldUnit K x hx) =
      -(AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity
        K v (Ideal.span {x}) : ℤ)
theorem

finitePlaceNormalizedValuation_primeAvoidingIntegralFieldUnit

L1009 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormalizedValuation_primeAvoidingIntegralFieldUnit
Documentation

Prime avoidance is the common special case of the integral valuation formula used for numerator units.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceNormalizedValuation_primeAvoidingIntegralFieldUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : 𝓞 K) (hx : x ∉ v.asIdeal) :
    finitePlaceNormalizedValuation K v
        (primeAvoidingIntegralFieldUnit K v x hx) =
      -(AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity
        K v (Ideal.span {x}) : ℤ)
theorem

finitePlaceHilbertSymbol_integral_eq_primeIdealPowerResidueFactor

L1027 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_integral_eq_primeIdealPowerResidueFactor
Documentation

Integral form of the finite-place comparison: the exponent is the Dedekind multiplicity in the principal denominator ideal.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_integral_eq_primeIdealPowerResidueFactor
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (hcoprime : (Ideal.absNorm v.asIdeal).Coprime (n : ℕ))
    (a b : 𝓞 K) (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (ha : a ∉ v.asIdeal) :
    finitePlaceHilbertSymbol K n hnK hmu v
        (nonzeroIntegralFieldUnit K a ha0)
        (nonzeroIntegralFieldUnit K b hb0) =
      integralRootsOfUnityToNthRoots K (n : ℕ)
          (AlgebraicNumberTheory.PowerResidueSymbols.primeIdealPowerResidueSymbol
              K v n hmu hcoprime a ha) ^
        AlgebraicNumberTheory.PowerResidueSymbols.idealPrimeMultiplicity K v (Ideal.span {b})
theorem

finitePlaceHilbertSymbol_skew

L1056 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_skew
Documentation

Finite-place Hilbert symbols inherit skew symmetry from the local Hilbert symbol in the canonical completion.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_skew
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ) :
    finitePlaceHilbertSymbol K n hnK hmu v a b =
      (finitePlaceHilbertSymbol K n hnK hmu v b a)⁻¹
theorem

finitePlaceHilbertSymbol_integral_units_eq_one

L1080 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_integral_units_eq_one
Documentation

If two nonzero algebraic integers are both units at a finite place, the corresponding finite-place Hilbert symbol is trivial.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_integral_units_eq_one
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueExponentFinitePlaces K n)
    (a b : 𝓞 K) (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (ha : a ∉ v.asIdeal) (hb : b ∉ v.asIdeal) :
    finitePlaceHilbertSymbol K n hnK hmu v
        (nonzeroIntegralFieldUnit K a ha0)
        (nonzeroIntegralFieldUnit K b hb0) = 1
theorem

powerResidueAwayFromExponentFiniteFactor_integral_eq_idealFactors

L1131 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueAwayFromExponentFiniteFactor_integral_eq_idealFactors
Documentation

Primewise comparison between the tame finite-place Hilbert factor and the quotient of the two ideal power-residue factors.

Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open scoped Classical in
Lean source · full declaration
theorem powerResidueAwayFromExponentFiniteFactor_integral_eq_idealFactors
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : 𝓞 K) (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (hcoprimeA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (hcoprimeB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (haB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} → a ∉ P.asIdeal)
    (hbA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} → b ∉ P.asIdeal)
    (hAwayA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          P ∉ powerResidueExponentFinitePlaces K n)
    (hAwayB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          P ∉ powerResidueExponentFinitePlaces K n)
    (P : HeightOneSpectrum (𝓞 K)) :
    (if P ∈ powerResidueExponentFinitePlaces K n then
        1
      else
        finitePlaceHilbertSymbol K n hnK hmu P
          (nonzeroIntegralFieldUnit K a ha0)
          (nonzeroIntegralFieldUnit K b hb0)) =
      integralRootsOfUnityToNthRoots K (n : ℕ)
          (idealPowerResidueFactor K (Ideal.span {b}) n hmu a
            hcoprimeB haB P) *
        (integralRootsOfUnityToNthRoots K (n : ℕ)
          (idealPowerResidueFactor K (Ideal.span {a}) n hmu b
            hcoprimeA hbA P))⁻¹ := by
  by_cases hPExponent : P ∈ powerResidueExponentFinitePlaces K n
  · have hPA : ¬ P.asIdeal ∣ Ideal.span {a} := by
      intro hPA
      exact (hAwayA P hPA) hPExponent
    have hPB : ¬ P.asIdeal ∣ Ideal.span {b} := by
      intro hPB
      exact (hAwayB P hPB) hPExponent
    simp only [ite_eq_left hPExponent, idealPowerResidueFactor,
      dite_eq_right hPA, dite_eq_right hPB, map_one, inv_one, mul_one]
  · rw [ite_eq_right hPExponent]
    by_cases hPB : P.asIdeal ∣ Ideal.span {b}
    · have haP : a ∉ P.asIdeal := haB P hPB
      have hPA : ¬ P.asIdeal ∣ Ideal.span {a} := by
        intro hPA
        apply haP
        rw [← Ideal.dvd_span_singleton]
        exact hPA
      rw [finitePlaceHilbertSymbol_integral_eq_primeIdealPowerResidueFactor
        K n hnK hmu P (hAwayB P hPB) (hcoprimeB P hPB)
          a b ha0 hb0 haP]
      simp only [idealPowerResidueFactor, dite_eq_left hPB, dite_eq_right hPA,
        map_pow, map_one, inv_one, mul_one]
    · by_cases hPA : P.asIdeal ∣ Ideal.span {a}
      · have hbP : b ∉ P.asIdeal := hbA P hPA
        rw [finitePlaceHilbertSymbol_skew K n hnK hmu]
        rw [finitePlaceHilbertSymbol_integral_eq_primeIdealPowerResidueFactor
          K n hnK hmu P (hAwayA P hPA) (hcoprimeA P hPA)
            b a hb0 ha0 hbP]
        simp only [idealPowerResidueFactor, dite_eq_right hPB, dite_eq_left hPA,
          map_pow, map_one, one_mul]
      · have haP : a ∉ P.asIdeal := by
          intro haMem
          apply hPA
          rw [Ideal.dvd_span_singleton]
          exact haMem
        have hbP : b ∉ P.asIdeal := by
          intro hbMem
          apply hPB
          rw [Ideal.dvd_span_singleton]
          exact hbMem
        rw [finitePlaceHilbertSymbol_integral_units_eq_one
          K n hnK hmu P hPExponent a b ha0 hb0 haP hbP]
        simp only [idealPowerResidueFactor, dite_eq_right hPB, dite_eq_right hPA,
          map_one, inv_one, mul_one]
def

powerResidueBadFinitePlaces

L1219 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueBadFinitePlaces
Documentation

A concrete finite set containing every finite place where a local power-residue factor of a and b may be nontrivial. Its exponent part is the exact set of prime divisors of (n).

Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def powerResidueBadFinitePlaces
    (n : ℕ+) (a b : Kˣ) :
    Finset (HeightOneSpectrum (𝓞 K))
def

powerResidueBadPlaceCorrection

L1228 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueBadPlaceCorrection
Documentation

The explicit bad-place correction in power-residue reciprocity. Every factor already lies in the common group nthRootsSubgroup K n.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def powerResidueBadPlaceCorrection
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)
theorem

valuation_eq_one_of_not_mem_chosenUnitFiniteSupport

L1238 ↗
GlobalClassFieldTheory.Reciprocity.valuation_eq_one_of_not_mem_chosenUnitFiniteSupport
Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem valuation_eq_one_of_not_mem_chosenUnitFiniteSupport
    (x : Kˣ) (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ chosenUnitFiniteSupport (K := K) x) :
    v.valuation K (x : K) = 1
theorem

finitePlaceHilbertSymbol_eq_one_of_valuation_eq_one

L1248 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_eq_one_of_valuation_eq_one
Documentation

The finite-place Hilbert symbol is trivial when the exponent and both global arguments are units at this place.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_eq_one_of_valuation_eq_one
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) (v : HeightOneSpectrum (𝓞 K))
    (hva : v.valuation K (a : K) = 1)
    (hvb : v.valuation K (b : K) = 1)
    (hvn : v.valuation K ((n : ℕ) : K) = 1) :
    finitePlaceHilbertSymbol K n hnK hmu v a b = 1
theorem

finitePlaceHilbertSymbol_eq_one_of_not_mem_powerResidueBadFinitePlaces

L1313 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_eq_one_of_not_mem_powerResidueBadFinitePlaces
Documentation

Outside the concrete bad-place set, the finite-place Hilbert factor is trivial.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_eq_one_of_not_mem_powerResidueBadFinitePlaces
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ powerResidueBadFinitePlaces K n a b) :
    finitePlaceHilbertSymbol K n hnK hmu v a b = 1
theorem

finitePlaceHilbertSymbol_mulSupport_subset_powerResidueBadFinitePlaces

L1354 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_mulSupport_subset_powerResidueBadFinitePlaces
Documentation

The multiplicative support of the finite-place Hilbert factors is contained in the explicit power-residue bad-place set.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · full declaration
theorem finitePlaceHilbertSymbol_mulSupport_subset_powerResidueBadFinitePlaces
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    Function.mulSupport
        (fun v : HeightOneSpectrum (𝓞 K) =>
          finitePlaceHilbertSymbol K n hnK hmu v a b) ⊆
      (powerResidueBadFinitePlaces K n a b :
        Set (HeightOneSpectrum (𝓞 K))) := by
  intro v hv
  change finitePlaceHilbertSymbol K n hnK hmu v a b ≠ 1 at hv
  change v ∈ powerResidueBadFinitePlaces K n a b
  by_contra hvBad
  exact hv
    (finitePlaceHilbertSymbol_eq_one_of_not_mem_powerResidueBadFinitePlaces
      K n hnK hmu a b v hvBad)
theorem

finitePlaceHilbertSymbol_finprod_eq_prod_powerResidueBadFinitePlaces

L1373 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_finprod_eq_prod_powerResidueBadFinitePlaces
Documentation

The finite-place Hilbert finprod is the ordinary product over the explicit bad-place set.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_finprod_eq_prod_powerResidueBadFinitePlaces
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    (∏ᶠ v : HeightOneSpectrum (𝓞 K),
        finitePlaceHilbertSymbol K n hnK hmu v a b) =
      ∏ v ∈ powerResidueBadFinitePlaces K n a b,
        finitePlaceHilbertSymbol K n hnK hmu v a b
theorem

powerResidueBadFinitePlaces_product_eq_infinitePlaceProduct_inv

L1387 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueBadFinitePlaces_product_eq_infinitePlaceProduct_inv
Documentation

Finite-set form of the Hilbert product formula: the product over all explicitly bad finite places is the inverse of the infinite-place product.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem powerResidueBadFinitePlaces_product_eq_infinitePlaceProduct_inv
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    (∏ v ∈ powerResidueBadFinitePlaces K n a b,
        finitePlaceHilbertSymbol K n hnK hmu v a b) =
      (∏ v : InfinitePlace K,
        infinitePlaceHilbertSymbol K n v a b)⁻¹
def

powerResidueAwayFromExponentFiniteProduct

L1407 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueAwayFromExponentFiniteProduct
Documentation

The product of the finite-place Hilbert factors away from primes dividing the exponent. C1 identifies this term with the quotient of the two ideal power-residue symbols; the remaining factors are exactly the correction.

Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def powerResidueAwayFromExponentFiniteProduct
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)
theorem

powerResidueAwayFromExponentFiniteProduct_integral_eq_idealSymbol_div

L1420 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueAwayFromExponentFiniteProduct_integral_eq_idealSymbol_div
Documentation

The complete tame finite-place product for two nonzero algebraic integers is the quotient of the two ideal power-residue symbols.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem powerResidueAwayFromExponentFiniteProduct_integral_eq_idealSymbol_div
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : 𝓞 K) (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (hcoprimeA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (hcoprimeB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (haB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} → a ∉ P.asIdeal)
    (hbA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} → b ∉ P.asIdeal)
    (hAwayA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          P ∉ powerResidueExponentFinitePlaces K n)
    (hAwayB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          P ∉ powerResidueExponentFinitePlaces K n) :
    powerResidueAwayFromExponentFiniteProduct K n hnK hmu
        (nonzeroIntegralFieldUnit K a ha0)
        (nonzeroIntegralFieldUnit K b hb0) =
      integralRootsOfUnityToNthRoots K (n : ℕ)
          (idealPowerResidueSymbol K (Ideal.span {b})
            (ideal_span_singleton_ne_zero K hb0)
            n hmu a hcoprimeB haB) *
        (integralRootsOfUnityToNthRoots K (n : ℕ)
          (idealPowerResidueSymbol K (Ideal.span {a})
            (ideal_span_singleton_ne_zero K ha0)
            n hmu b hcoprimeA hbA))⁻¹
theorem

finitePlaceHilbertSymbol_finprod_eq_exponent_product_mul_away

L1546 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_finprod_eq_exponent_product_mul_away
Documentation

Split the full finite-place product into exponent-prime factors and the product away from the exponent.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_finprod_eq_exponent_product_mul_away
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    (∏ᶠ v : HeightOneSpectrum (𝓞 K),
        finitePlaceHilbertSymbol K n hnK hmu v a b) =
      (∏ v ∈ powerResidueExponentFinitePlaces K n,
          finitePlaceHilbertSymbol K n hnK hmu v a b) *
        powerResidueAwayFromExponentFiniteProduct K n hnK hmu a b
theorem

powerResidueAwayFromExponentFiniteProduct_eq_badPlaceCorrection_inv

L1629 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueAwayFromExponentFiniteProduct_eq_badPlaceCorrection_inv
Documentation

General Hilbert-product core of power-residue reciprocity. The complete finite product away from the exponent is the inverse of the explicit product of all infinite-place factors and all exponent-prime factors.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem powerResidueAwayFromExponentFiniteProduct_eq_badPlaceCorrection_inv
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    powerResidueAwayFromExponentFiniteProduct K n hnK hmu a b =
      (powerResidueBadPlaceCorrection K n hnK hmu a b)⁻¹
theorem

idealPowerResidueSymbol_reciprocity_with_bad_place_correction

L1645 ↗
GlobalClassFieldTheory.Reciprocity.idealPowerResidueSymbol_reciprocity_with_bad_place_correction
Documentation

General ideal power-residue reciprocity with the explicit product of infinite and exponent-prime Hilbert factors as correction.

Source context 11 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem idealPowerResidueSymbol_reciprocity_with_bad_place_correction
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : 𝓞 K) (ha0 : a ≠ 0) (hb0 : b ≠ 0)
    (hcoprimeA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (hcoprimeB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          (Ideal.absNorm P.asIdeal).Coprime (n : ℕ))
    (haB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} → a ∉ P.asIdeal)
    (hbA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} → b ∉ P.asIdeal)
    (hAwayA :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {a} →
          P ∉ powerResidueExponentFinitePlaces K n)
    (hAwayB :
      ∀ P : HeightOneSpectrum (𝓞 K),
        P.asIdeal ∣ Ideal.span {b} →
          P ∉ powerResidueExponentFinitePlaces K n) :
    integralRootsOfUnityToNthRoots K (n : ℕ)
        (idealPowerResidueSymbol K (Ideal.span {b})
          (ideal_span_singleton_ne_zero K hb0)
          n hmu a hcoprimeB haB) =
      (powerResidueBadPlaceCorrection K n hnK hmu
        (nonzeroIntegralFieldUnit K a ha0)
        (nonzeroIntegralFieldUnit K b hb0))⁻¹ *
      integralRootsOfUnityToNthRoots K (n : ℕ)
        (idealPowerResidueSymbol K (Ideal.span {a})
          (ideal_span_singleton_ne_zero K ha0)
          n hmu b hcoprimeA hbA)
instance

rationalPrimeFact

L1714 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeFact
Source context 12 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
Lean source · statement
instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime
theorem

rationalQuadraticPrimitiveRoots_nonempty

L1720 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticPrimitiveRoots_nonempty
Documentation

The rational field contains the primitive square root of unity -1. This is the canonical source of the primitive-root input in the quadratic specialization; no root is chosen downstream.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticPrimitiveRoots_nonempty :
    (primitiveRoots 2 ℚ).Nonempty
def

rationalPrimeResidueEquivZMod

L1728 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeResidueEquivZMod
Documentation

The residue field at the rational prime over p is canonically ZMod p. The construction first transports the prime ideal through Rat.ringOfIntegersEquiv and then uses the standard integer quotient.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalPrimeResidueEquivZMod
    (p : Nat.Primes) :
    (𝓞 ℚ ⧸ (RayClass.rationalPrime p).asIdeal) ≃+* ZMod p.1
theorem

rationalPrimeResidueEquivZMod_mk

L1753 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeResidueEquivZMod_mk
Documentation

The rational residue-field equivalence sends an integral residue class to the corresponding integer class modulo p.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrimeResidueEquivZMod_mk
    (p : Nat.Primes) (a : 𝓞 ℚ) :
    rationalPrimeResidueEquivZMod p
      (Ideal.Quotient.mk (RayClass.rationalPrime p).asIdeal a) =
      (Rat.ringOfIntegersEquiv a : ZMod p.1)
theorem

absNorm_rationalPrime

L1792 ↗
GlobalClassFieldTheory.Reciprocity.absNorm_rationalPrime
Documentation

The absolute norm of the rational prime ideal attached to p is p. This follows from the explicit residue-field equivalence rather than from a cardinality assumption supplied by a consumer.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem absNorm_rationalPrime (p : Nat.Primes) :
    Ideal.absNorm (RayClass.rationalPrime p).asIdeal = p.1
theorem

absNorm_rationalPrime_coprime_two

L1803 ↗
GlobalClassFieldTheory.Reciprocity.absNorm_rationalPrime_coprime_two
Documentation

An odd rational prime has residue characteristic coprime to the quadratic exponent.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem absNorm_rationalPrime_coprime_two
    (p : Nat.Primes) (hp : p.1 ≠ 2) :
    (Ideal.absNorm (RayClass.rationalPrime p).asIdeal).Coprime 2
def

rationalQuadraticRootValue

L1811 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValue
Documentation

Evaluate a quadratic integral root of unity as the corresponding integer sign.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalQuadraticRootValue
    (z : rootsOfUnity 2 (𝓞 ℚ)) : ℤ
theorem

rationalQuadraticRootValue_one

L1817 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValue_one
Documentation

The identity quadratic root evaluates to the positive integer sign.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticRootValue_one :
    rationalQuadraticRootValue (1 : rootsOfUnity 2 (𝓞 ℚ)) = 1
def

rationalQuadraticRootValueMonoidHom

L1822 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValueMonoidHom
Documentation

Integer evaluation of quadratic roots of unity is multiplicative.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · full declaration
def rationalQuadraticRootValueMonoidHom :
    rootsOfUnity 2 (𝓞 ℚ) →* ℤ where
  toFun := rationalQuadraticRootValue
  map_one' := rationalQuadraticRootValue_one
  map_mul' := by
    intro z w
    simp [rationalQuadraticRootValue]
theorem

rationalQuadraticRootValueMonoidHom_apply

L1832 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValueMonoidHom_apply
Documentation

The multiplicative sign evaluation has the expected underlying function.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticRootValueMonoidHom_apply
    (z : rootsOfUnity 2 (𝓞 ℚ)) :
    rationalQuadraticRootValueMonoidHom z =
      rationalQuadraticRootValue z
theorem

rationalQuadraticRootValue_eq_one_iff

L1839 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValue_eq_one_iff
Documentation

The integer sign evaluation detects the identity root.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticRootValue_eq_one_iff
    (z : rootsOfUnity 2 (𝓞 ℚ)) :
    rationalQuadraticRootValue z = 1 ↔ z = 1
theorem

rationalQuadraticRootValue_eq_one_or_neg_one

L1855 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValue_eq_one_or_neg_one
Documentation

A quadratic root evaluates to one of the two integer signs.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticRootValue_eq_one_or_neg_one
    (z : rootsOfUnity 2 (𝓞 ℚ)) :
    rationalQuadraticRootValue z = 1 ∨
      rationalQuadraticRootValue z = -1
theorem

rationalPrimeResidue_intCast_ne_zero

L1869 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeResidue_intCast_ne_zero
Documentation

The chosen integral numerator remains nonzero after passing to the standard residue field ZMod p.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrimeResidue_intCast_ne_zero
    (p : Nat.Primes) (a : 𝓞 ℚ)
    (ha : a ∉ (RayClass.rationalPrime p).asIdeal) :
    (Rat.ringOfIntegersEquiv a : ZMod p.1) ≠ 0
theorem

rationalPrimeResidueUnit_sq_iff_isSquare

L1882 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeResidueUnit_sq_iff_isSquare
Documentation

A square among residue units is exactly a square in the standard rational prime residue field. The reverse implication constructs the unit from the nonzero square root.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrimeResidueUnit_sq_iff_isSquare
    (p : Nat.Primes) (a : 𝓞 ℚ)
    (ha : a ∉ (RayClass.rationalPrime p).asIdeal) :
    (∃ u : (𝓞 ℚ ⧸ (RayClass.rationalPrime p).asIdeal)ˣ,
        u ^ 2 = primeIdealResidueUnit ℚ (RayClass.rationalPrime p) a ha) ↔
      IsSquare (Rat.ringOfIntegersEquiv a : ZMod p.1)
theorem

rationalPrimeIdealPowerResidueSymbol_two_eq_legendre

L1914 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrimeIdealPowerResidueSymbol_two_eq_legendre
Documentation

The quadratic prime-ideal power-residue symbol over ℚ, evaluated as an integer sign, is the classical Legendre symbol.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrimeIdealPowerResidueSymbol_two_eq_legendre
    (p : Nat.Primes) (hp : p.1 ≠ 2)
    (a : 𝓞 ℚ) (ha : a ∉ (RayClass.rationalPrime p).asIdeal) :
    rationalQuadraticRootValue
        (primeIdealPowerResidueSymbol ℚ (RayClass.rationalPrime p)
          (2 : ℕ+) rationalQuadraticPrimitiveRoots_nonempty
          (absNorm_rationalPrime_coprime_two p hp) a ha) =
      legendreSym p.1 (Rat.ringOfIntegersEquiv a)
def

rationalPrincipalIdeal

L1961 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdeal
Documentation

The principal ideal of 𝓞 ℚ generated by a natural number, expressed through the canonical equivalence 𝓞 ℚ ≃+* ℤ.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalPrincipalIdeal (b : ℕ) : Ideal (𝓞 ℚ)
theorem

rationalPrincipalIdeal_ne_zero

L1965 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdeal_ne_zero
Documentation

A positive rational principal ideal is nonzero.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrincipalIdeal_ne_zero
    (b : ℕ) (hb : b ≠ 0) :
    rationalPrincipalIdeal b ≠ 0
theorem

rationalPrime_asIdeal_eq_span

L1976 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrime_asIdeal_eq_span
Documentation

The height-one prime of 𝓞 ℚ attached to p is generated by the corresponding rational integer.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrime_asIdeal_eq_span
    (p : Nat.Primes) :
    (RayClass.rationalPrime p).asIdeal =
      Ideal.span {Rat.ringOfIntegersEquiv.symm (p.1 : ℤ)}
theorem

rationalPrime_dvd_rationalPrincipalIdeal_iff

L2012 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrime_dvd_rationalPrincipalIdeal_iff
Documentation

Divisibility of a rational principal ideal by the prime over p is exactly natural-number divisibility by p.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrime_dvd_rationalPrincipalIdeal_iff
    (p : Nat.Primes) (b : ℕ) :
    (RayClass.rationalPrime p).asIdeal ∣ rationalPrincipalIdeal b ↔
      p.1 ∣ b
theorem

rationalPrincipalIdeal_absNorm_coprime_two_of_odd

L2023 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdeal_absNorm_coprime_two_of_odd
Documentation

Every prime divisor of an odd rational principal ideal has odd residue characteristic. Thus its norm is coprime to the quadratic exponent.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrincipalIdeal_absNorm_coprime_two_of_odd
    (b : ℕ) (hbOdd : Odd b)
    (P : HeightOneSpectrum (𝓞 ℚ))
    (hP : P.asIdeal ∣ rationalPrincipalIdeal b) :
    (Ideal.absNorm P.asIdeal).Coprime 2
theorem

rationalPrincipalIdeal_numerator_not_mem_of_coprime

L2051 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdeal_numerator_not_mem_of_coprime
Documentation

Coprimality of the integer numerator and the natural denominator excludes the numerator from every prime ideal dividing the denominator ideal.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrincipalIdeal_numerator_not_mem_of_coprime
    (a : 𝓞 ℚ) (b : ℕ)
    (hab : Nat.Coprime
      (Rat.ringOfIntegersEquiv a).natAbs b)
    (P : HeightOneSpectrum (𝓞 ℚ))
    (hP : P.asIdeal ∣ rationalPrincipalIdeal b) :
    a ∉ P.asIdeal
theorem

idealPrimeMultiplicity_rationalPrincipalIdeal

L2094 ↗
GlobalClassFieldTheory.Reciprocity.idealPrimeMultiplicity_rationalPrincipalIdeal
Documentation

The multiplicity of the rational prime ideal over p in (b) is the usual p-adic exponent in the natural-number factorization of b.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem idealPrimeMultiplicity_rationalPrincipalIdeal
    (p : Nat.Primes) (b : ℕ) (hb : b ≠ 0) :
    idealPrimeMultiplicity ℚ (RayClass.rationalPrime p)
        (rationalPrincipalIdeal b) =
      b.factorization p.1
def

rationalPrincipalIdealPrimeDivisorsEquiv

L2131 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdealPrimeDivisorsEquiv
Documentation

Prime divisors of the rational principal ideal (b) are canonically the natural prime factors of b.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · full declaration
def rationalPrincipalIdealPrimeDivisorsEquiv
    (b : ℕ) (hb : b ≠ 0) :
    idealPrimeDivisors ℚ (rationalPrincipalIdeal b) ≃
      b.primeFactors where
  toFun P :=
    ⟨Rat.HeightOneSpectrum.natGenerator P.1,
      (Nat.mem_primeFactors_of_ne_zero hb).mpr
        ⟨Rat.HeightOneSpectrum.prime_natGenerator P.1,
            (rationalPrime_dvd_rationalPrincipalIdeal_iff
            ⟨Rat.HeightOneSpectrum.natGenerator P.1,
              Rat.HeightOneSpectrum.prime_natGenerator P.1⟩ b).mp
            (by
              have hprimeEq :
                  RayClass.rationalPrime
                      ⟨Rat.HeightOneSpectrum.natGenerator P.1,
                        Rat.HeightOneSpectrum.prime_natGenerator P.1⟩ =
                    P.1 :=
                (Rat.HeightOneSpectrum.primesEquiv
                  (R := 𝓞 ℚ)).symm_apply_apply P.1
              rw [hprimeEq]
              exact P.2)⟩⟩
  invFun p :=
    ⟨RayClass.rationalPrime
        ⟨p.1, Nat.prime_of_mem_primeFactors p.2⟩,
      (rationalPrime_dvd_rationalPrincipalIdeal_iff
        ⟨p.1, Nat.prime_of_mem_primeFactors p.2⟩ b).mpr
        (Nat.dvd_of_mem_primeFactors p.2)⟩
  left_inv P := by
    apply Subtype.ext
    have hq :
        (⟨Rat.HeightOneSpectrum.natGenerator P.1,
          Rat.HeightOneSpectrum.prime_natGenerator P.1⟩ : Nat.Primes) =
          Rat.HeightOneSpectrum.primesEquiv P.1 :=
      Subtype.ext rfl
    simpa only [RayClass.rationalPrime, hq] using
      (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm_apply_apply P.1
  right_inv p := by
    apply Subtype.ext
    exact
      RayClass.natGenerator_rationalPrime
        ⟨p.1, Nat.prime_of_mem_primeFactors p.2⟩
theorem

rationalPrincipalIdealPrimeDivisorsEquiv_symm_apply_val

L2176 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdealPrimeDivisorsEquiv_symm_apply_val
Documentation

Reindexing a natural prime factor back to a height-one prime gives the standard rational prime above it.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalPrincipalIdealPrimeDivisorsEquiv_symm_apply_val
    (b : ℕ) (hb : b ≠ 0) (p : b.primeFactors) :
    ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p).1 =
      RayClass.rationalPrime
        ⟨p.1, Nat.prime_of_mem_primeFactors p.2⟩
theorem

idealPrimeMultiplicity_rationalPrincipalIdeal_reindexed

L2186 ↗
GlobalClassFieldTheory.Reciprocity.idealPrimeMultiplicity_rationalPrincipalIdeal_reindexed
Documentation

Under the prime-factor reindexing, ideal multiplicity becomes the corresponding entry of Nat.factorization.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem idealPrimeMultiplicity_rationalPrincipalIdeal_reindexed
    (b : ℕ) (hb : b ≠ 0) (p : b.primeFactors) :
    idealPrimeMultiplicity ℚ
        ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p).1
        (rationalPrincipalIdeal b) =
      b.factorization p.1
theorem

prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors

L2198 ↗
GlobalClassFieldTheory.Reciprocity.prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors
Documentation

Reindex a product over the prime divisors of (b) by the ordinary natural prime factors of b.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · full declaration
theorem prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors
    {M : Type*} [CommMonoid M]
    (b : ℕ) (hb : b ≠ 0)
    (f : HeightOneSpectrum (𝓞 ℚ) → M) :
    letI : Fintype
        (idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) :=
      (idealPrimeDivisors_finite ℚ (rationalPrincipalIdeal b)
        (rationalPrincipalIdeal_ne_zero b hb)).fintype
    (∏ P : idealPrimeDivisors ℚ (rationalPrincipalIdeal b), f P.1) =
      ∏ p : b.primeFactors,
        f ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p).1 := by
  let : Fintype
      (idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) :=
    (idealPrimeDivisors_finite ℚ (rationalPrincipalIdeal b)
      (rationalPrincipalIdeal_ne_zero b hb)).fintype
  exact
    Fintype.prod_equiv
      (rationalPrincipalIdealPrimeDivisorsEquiv b hb)
      (fun P => f P.1)
      (fun p => f ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p).1)
      (fun P => by
        rw [(rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm_apply_apply])
theorem

prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors_subtype

L2224 ↗
GlobalClassFieldTheory.Reciprocity.prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors_subtype
Documentation

Reindex a product whose factor also depends on the divisibility witness. This is the subtype-valued form used by the defining product of the ideal power-residue symbol.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · full declaration
theorem prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors_subtype
    {M : Type*} [CommMonoid M]
    (b : ℕ) (hb : b ≠ 0)
    (f : idealPrimeDivisors ℚ (rationalPrincipalIdeal b) → M) :
    letI : Fintype
        (idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) :=
      (idealPrimeDivisors_finite ℚ (rationalPrincipalIdeal b)
        (rationalPrincipalIdeal_ne_zero b hb)).fintype
    (∏ P : idealPrimeDivisors ℚ (rationalPrincipalIdeal b), f P) =
      ∏ p : b.primeFactors,
        f ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p) := by
  let : Fintype
      (idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) :=
    (idealPrimeDivisors_finite ℚ (rationalPrincipalIdeal b)
      (rationalPrincipalIdeal_ne_zero b hb)).fintype
  exact
    Fintype.prod_equiv
      (rationalPrincipalIdealPrimeDivisorsEquiv b hb)
      f
      (fun p =>
        f ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p))
      (fun P => by
        rw [(rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm_apply_apply])
theorem

jacobiSym_eq_prod_primeFactors_factorization

L2250 ↗
GlobalClassFieldTheory.Reciprocity.jacobiSym_eq_prod_primeFactors_factorization
Documentation

The list-based Jacobi symbol is the product over distinct prime factors, with the usual natural factorization multiplicity as exponent.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem jacobiSym_eq_prod_primeFactors_factorization
    (a : ℤ) (b : ℕ) :
    jacobiSym a b =
      ∏ p : b.primeFactors,
        (@legendreSym p.1
          ⟨Nat.prime_of_mem_primeFactors p.2⟩ a) ^
          b.factorization p.1
theorem

rationalQuadraticPrimitiveRoots_nonempty_pnat

L2294 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticPrimitiveRoots_nonempty_pnat
Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalQuadraticPrimitiveRoots_nonempty_pnat :
    (primitiveRoots (((2 : ℕ+) : ℕ)) ℚ).Nonempty
def

rationalQuadraticRootValuePNatMonoidHom

L2299 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValuePNatMonoidHom
Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalQuadraticRootValuePNatMonoidHom :
    rootsOfUnity (((2 : ℕ+) : ℕ)) (𝓞 ℚ) →* ℤ
def

rationalIdealQuadraticSourceFactor

L2304 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdealQuadraticSourceFactor
Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalIdealQuadraticSourceFactor
    (a : 𝓞 ℚ) (b : ℕ) (hbOdd : Odd b)
    (hab : Nat.Coprime (Rat.ringOfIntegersEquiv a).natAbs b)
    (P : idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) : ℤ
def

rationalJacobiPrimeFactor

L2323 ↗
GlobalClassFieldTheory.Reciprocity.rationalJacobiPrimeFactor
Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def rationalJacobiPrimeFactor
    (a : 𝓞 ℚ) (b : ℕ) (p : b.primeFactors) : ℤ
theorem

rationalIdealQuadraticSourceFactor_reindexed

L2328 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdealQuadraticSourceFactor_reindexed
Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem rationalIdealQuadraticSourceFactor_reindexed
    (a : 𝓞 ℚ) (b : ℕ) (hb : b ≠ 0) (hbOdd : Odd b)
    (hab : Nat.Coprime (Rat.ringOfIntegersEquiv a).natAbs b)
    (p : b.primeFactors) :
    rationalIdealQuadraticSourceFactor a b hbOdd hab
        ((rationalPrincipalIdealPrimeDivisorsEquiv b hb).symm p) =
      rationalJacobiPrimeFactor a b p
theorem

rationalIdealPowerResidueSymbol_two_eq_jacobiSym

L2355 ↗
GlobalClassFieldTheory.Reciprocity.rationalIdealPowerResidueSymbol_two_eq_jacobiSym
Documentation

The quadratic ideal power-residue symbol of a positive rational principal ideal is the classical Jacobi symbol. Oddness supplies the residue-characteristic condition at every denominator prime, while ordinary natural coprimality supplies numerator nonvanishing.

Source context 13 commands

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

open scoped BigOperators NumberField NumberTheorySymbols ValuativeRel WithZero
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [NumberField K]
open AlgebraicNumberTheory.PowerResidueSymbols
local instance rationalPrimeFact (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · full declaration
theorem rationalIdealPowerResidueSymbol_two_eq_jacobiSym
    (a : 𝓞 ℚ) (b : ℕ) (hb : b ≠ 0)
    (hbOdd : Odd b)
    (hab : Nat.Coprime
      (Rat.ringOfIntegersEquiv a).natAbs b) :
    rationalQuadraticRootValue
        (idealPowerResidueSymbol ℚ
          (rationalPrincipalIdeal b)
          (rationalPrincipalIdeal_ne_zero b hb)
          (2 : ℕ+) rationalQuadraticPrimitiveRoots_nonempty_pnat a
          (by
            intro P hP
            change (Ideal.absNorm P.asIdeal).Coprime 2
            exact rationalPrincipalIdeal_absNorm_coprime_two_of_odd
              b hbOdd P hP)
          (rationalPrincipalIdeal_numerator_not_mem_of_coprime a b hab)) =
      jacobiSym (Rat.ringOfIntegersEquiv a) b := by
  let : Fintype
      (idealPrimeDivisors ℚ (rationalPrincipalIdeal b)) :=
    (idealPrimeDivisors_finite ℚ (rationalPrincipalIdeal b)
      (rationalPrincipalIdeal_ne_zero b hb)).fintype
  rw [idealPowerResidueSymbol_eq_prod]
  change rationalQuadraticRootValuePNatMonoidHom _ = _
  rw [map_prod]
  change
    (∏ P : idealPrimeDivisors ℚ (rationalPrincipalIdeal b),
      rationalIdealQuadraticSourceFactor a b hbOdd hab P) = _
  rw [
    prod_rationalPrincipalIdealPrimeDivisors_eq_prod_primeFactors_subtype
      b hb (rationalIdealQuadraticSourceFactor a b hbOdd hab),
    jacobiSym_eq_prod_primeFactors_factorization]
  apply Fintype.prod_congr
  intro p
  exact rationalIdealQuadraticSourceFactor_reindexed
    a b hb hbOdd hab p

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