NYLL
Module

RationalQuadraticPowerResidueReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalQuadraticPowerResidueReciprocity
41 declarations indexed from sourceView source ↗

Module documentation

Rational quadratic reciprocity from global class field theory

The dyadic correction specializes power-residue reciprocity over ℚ and derives Gauss's quadratic reciprocity law.

Dyadic correction and Gauss reciprocity

Imports1
Imported by1

Declarations

instance

(anonymous instance)

L27 ↗
Source context 5 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
Lean source · statement
instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion
def

rationalQuadraticRootValuePNatMonoidHom

L48 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValuePNatMonoidHom
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalQuadraticRootValuePNatMonoidHom :
    rootsOfUnity (((2 : ℕ+) : ℕ)) (𝓞 ℚ) →* ℤ
def

rationalTwoPrime

L56 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoPrime
Documentation

The rational prime above two, used throughout the dyadic specialization.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalTwoPrime : Nat.Primes
def

rationalTwoAdicCompletionToIndexedPadic

L58 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicCompletionToIndexedPadic
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalTwoAdicCompletionToIndexedPadic :
    (RayClass.rationalPrime rationalTwoPrime).adicCompletion ℚ ≃+*
      ℚ_[Rat.HeightOneSpectrum.primesEquiv
        (RayClass.rationalPrime rationalTwoPrime)]
def

rationalTwoAdicCompletionEquivPadic

L80 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicCompletionEquivPadic
Documentation

The absolute-value completion at the rational prime above two is canonically the usual field of 2-adic numbers.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalTwoAdicCompletionEquivPadic :
    (HeightOneSpectrum.adicAbv ℚ
        (RayClass.rationalPrime rationalTwoPrime)).Completion ≃+* ℚ_[2]
def

rationalNatInteger

L95 ↗
GlobalClassFieldTheory.Reciprocity.rationalNatInteger
Documentation

A natural number in the rational ring of integers.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalNatInteger (m : ℕ) : 𝓞 ℚ
theorem

rationalNatInteger_equiv

L99 ↗
GlobalClassFieldTheory.Reciprocity.rationalNatInteger_equiv
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalNatInteger_equiv (m : ℕ) :
    Rat.ringOfIntegersEquiv (rationalNatInteger m) = (m : ℤ)
theorem

rationalNatInteger_coe

L104 ↗
GlobalClassFieldTheory.Reciprocity.rationalNatInteger_coe
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalNatInteger_coe (m : ℕ) :
    (rationalNatInteger m : ℚ) = (m : ℚ)
def

rationalNaturalFieldUnit

L109 ↗
GlobalClassFieldTheory.Reciprocity.rationalNaturalFieldUnit
Documentation

A positive natural number, regarded canonically as a rational 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalNaturalFieldUnit
    (m : ℕ) (hm : m ≠ 0) : ℚˣ
theorem

rationalNaturalFieldUnit_coe

L118 ↗
GlobalClassFieldTheory.Reciprocity.rationalNaturalFieldUnit_coe
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalNaturalFieldUnit_coe
    (m : ℕ) (hm : m ≠ 0) :
    (rationalNaturalFieldUnit m hm : ℚ) = (m : ℚ)
def

rationalQuadraticNegOneRoot

L124 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticNegOneRoot
Documentation

The negative quadratic integral root of unity over ℚ.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalQuadraticNegOneRoot : rootsOfUnity 2 (𝓞 ℚ)
theorem

rationalQuadraticRootValue_negOneRoot

L128 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticRootValue_negOneRoot
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalQuadraticRootValue_negOneRoot :
    rationalQuadraticRootValue rationalQuadraticNegOneRoot = -1
theorem

powerResidueExponentIdeal_rational_two

L134 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueExponentIdeal_rational_two
Documentation

For exponent two, the exponent ideal is the rational principal ideal generated by two.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem powerResidueExponentIdeal_rational_two :
    powerResidueExponentIdeal ℚ (2 : ℕ+) = rationalPrincipalIdeal 2
theorem

powerResidueExponentFinitePlaces_rational_two

L143 ↗
GlobalClassFieldTheory.Reciprocity.powerResidueExponentFinitePlaces_rational_two
Documentation

The only finite exponent place in the rational quadratic specialization is the prime above two.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem powerResidueExponentFinitePlaces_rational_two :
    powerResidueExponentFinitePlaces ℚ (2 : ℕ+) =
      {RayClass.rationalPrime rationalTwoPrime}
def

rationalTwoAdicSignedOddUnit

L173 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicSignedOddUnit
Documentation

The sign-normalized odd integer used in the dyadic square-class calculation, regarded as a unit of ℚ₂.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalTwoAdicSignedOddUnit
    (m : ℕ) (hm : Odd m) : ℚ_[2]ˣ
theorem

rationalTwoAdicSignedOddUnit_coe

L185 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicSignedOddUnit_coe
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalTwoAdicSignedOddUnit_coe
    (m : ℕ) (hm : Odd m) :
    (rationalTwoAdicSignedOddUnit m hm : ℚ_[2]) =
      (((-1 : ℤ) ^ (m / 2) * (m : ℤ) : ℤ) : ℚ_[2])
theorem

rationalTwoAdicSignedOddUnit_squareClass

L194 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicSignedOddUnit_squareClass
Documentation

A sign-normalized odd rational integer is, in ℚ₂, either a square or five times a square. This is the exact dyadic square-class input needed for the quadratic Hilbert 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicSignedOddUnit_squareClass
    (m : ℕ) (hm : Odd m) :
    let five : ℚ_[2]ˣ := Units.mk0 (5 : ℚ_[2]) (by norm_num)
    ∃ r : ℚ_[2]ˣ,
      rationalTwoAdicSignedOddUnit m hm = r ^ 2 ∨
        rationalTwoAdicSignedOddUnit m hm = five * r ^ 2 := by
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let q : ℤ := (-1 : ℤ) ^ (m / 2) * (m : ℤ)
  have hmInt : Odd (m : ℤ) := by exact_mod_cast hm
  have hqData : Odd q ∧ ∃ k : ℤ, q - 1 = 4 * k := by
    have hmMod : m % 4 = 1 ∨ m % 4 = 3 := by
      have hmTwo := Nat.odd_iff.mp hm
      omega
    rcases hmMod with hm1 | hm3
    · have hsign : (-1 : ℤ) ^ (m / 2) = 1 :=
        by
          have hdiv : m / 2 = 2 * (m / 4) := by omega
          rw [hdiv, pow_mul]
          norm_num
      have hmForm : m = 4 * (m / 4) + 1 := by
        have hdiv := Nat.mod_add_div m 4
        omega
      constructor
      · simpa only [q, hsign, one_mul] using hmInt
      · refine ⟨(m / 4 : ℕ), ?_⟩
        simp only [q, hsign, one_mul]
        exact_mod_cast (by omega : (m : ℤ) - 1 = 4 * (m / 4 : ℕ))
    · have hsign : (-1 : ℤ) ^ (m / 2) = -1 :=
        by
          have hdiv : m / 2 = 2 * (m / 4) + 1 := by omega
          rw [hdiv, pow_add, pow_mul]
          norm_num
      have hmForm : m = 4 * (m / 4) + 3 := by
        have hdiv := Nat.mod_add_div m 4
        omega
      constructor
      · simpa only [q, hsign, neg_one_mul] using hmInt.neg
      · refine ⟨-((m / 4 : ℤ) + 1), ?_⟩
        simp only [q, hsign, neg_one_mul]
        omega
  have hqCoprime : IsCoprime q (2 : ℤ) := by
    obtain ⟨k, hk⟩ := hqData.2
    refine ⟨1, -2 * k, ?_⟩
    omega
  have hqPadicUnit : IsUnit (q : ℤ_[2]) := by
    rw [PadicInt.isUnit_iff, PadicInt.norm_intCast_eq_one_iff]
    exact hqCoprime
  let qZ : ℤ_[2]ˣ := hqPadicUnit.unit
  let F :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
  let eO : ℤ_[2] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring 2
  let qO : F.valuationSubringˣ := Units.mapEquiv eO.toMulEquiv qZ
  have hqMaximal :
      (q : ℤ_[2]) - 1 ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ 2 := by
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow,
      Ideal.mem_span_singleton]
    obtain ⟨k, hk⟩ := hqData.2
    refine ⟨(k : ℤ_[2]), ?_⟩
    calc
      (q : ℤ_[2]) - 1 = ((q - 1 : ℤ) : ℤ_[2]) := by norm_num
      _ = ((4 * k : ℤ) : ℤ_[2]) := by rw [hk]
      _ = (2 : ℤ_[2]) ^ 2 * (k : ℤ_[2]) := by norm_num
  have hqO2 :
      qO ∈ LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2 := by
    rw [LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_iff]
    have hqOVal : (qO : F.valuationSubring) = eO (q : ℤ_[2]) := by
      simp [qO, qZ]
    rw [hqOVal, ← map_one eO, ← map_sub]
    exact
      (ValuationTheory.ringEquiv_mem_maximalIdeal_pow_iff
        eO 2 ((q : ℤ_[2]) - 1)).2 hqMaximal
  let u : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2 :=
    ⟨qO, hqO2⟩
  obtain ⟨rD, hrD⟩ :=
    LocalClassFieldTheory.padicDVR_U2_square_class u
  let toField : F.valuationSubringˣ →* ℚ_[2]ˣ :=
    Units.map F.valuation.valuationSubring.subtype.toMonoidHom
  let r : ℚ_[2]ˣ := toField (rD : F.valuationSubringˣ)
  let five : ℚ_[2]ˣ := Units.mk0 (5 : ℚ_[2]) (by norm_num)
  have hbase : toField qO = rationalTwoAdicSignedOddUnit m hm := by
    apply Units.ext
    dsimp [toField, qO, qZ, eO, F, q]
    rfl
  have hfive :
      toField
          ((LocalClassFieldTheory.padicDVR_five :
              LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2) :
            F.valuationSubringˣ) =
        five := by
    apply Units.ext
    dsimp [toField, five, F]
    exact LocalClassFieldTheory.padicDVR_five_val
  refine ⟨r, ?_⟩
  rcases hrD with hrD | hrD
  · left
    calc
      rationalTwoAdicSignedOddUnit m hm = toField qO := hbase.symm
      _ = toField ((rD : F.valuationSubringˣ) ^ 2) :=
        congrArg toField hrD
      _ = r ^ 2 := by rw [map_pow]
  · right
    calc
      rationalTwoAdicSignedOddUnit m hm = toField qO := hbase.symm
      _ = toField
          ((LocalClassFieldTheory.padicDVR_five :
              LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2) *
            (rD : F.valuationSubringˣ) ^ 2) :=
        congrArg toField hrD
      _ = five * r ^ 2 := by rw [map_mul, map_pow, hfive]
theorem

rationalTwoAdicOddUnit_squareClass

L307 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicOddUnit_squareClass
Documentation

Pull the signed odd square-class decomposition back from ℚ₂ to the canonical absolute-value completion used by 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicOddUnit_squareClass
    (m : ℕ) (hm : Odd m) :
    let v₂ := RayClass.rationalPrime rationalTwoPrime
    let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
    let aC := finitePlaceHilbert_completionUnit ℚ v₂
      (rationalNaturalFieldUnit m (by
        intro hm0
        subst m
        norm_num at hm))
    let fiveC : Cˣ := Units.mk0 (5 : C)
      (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+) (by norm_num) v₂)
    ∃ r : Cˣ,
      aC = (-1 : Cˣ) ^ (m / 2) * r ^ 2 ∨
        aC = (-1 : Cˣ) ^ (m / 2) * (fiveC * r ^ 2) := by
  dsimp only
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
  let e : C ≃+* ℚ_[2] := rationalTwoAdicCompletionEquivPadic
  have hm0 : m ≠ 0 := by
    intro hm0
    subst m
    norm_num at hm
  let aC : Cˣ := finitePlaceHilbert_completionUnit ℚ v₂
    (rationalNaturalFieldUnit m hm0)
  have haC :
      (aC : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) =
        (m : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) := by
    simp only [aC, C, finitePlaceHilbert_completionUnit, Units.coe_map,
      rationalNaturalFieldUnit_coe]
    exact map_natCast
      (algebraMap ℚ (HeightOneSpectrum.adicAbv ℚ v₂).Completion) m
  let fiveC : Cˣ := Units.mk0 (5 : C)
    (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+) (by norm_num) v₂)
  let fiveQ : ℚ_[2]ˣ := Units.mk0 (5 : ℚ_[2]) (by norm_num)
  obtain ⟨rQ, hrQ⟩ :=
    rationalTwoAdicSignedOddUnit_squareClass m hm
  let rC : Cˣ := Units.map e.symm.toMonoidHom rQ
  have hsigned :
      Units.map e.symm.toMonoidHom
          (rationalTwoAdicSignedOddUnit m hm) =
        (-1 : Cˣ) ^ (m / 2) * aC := by
    apply Units.ext
    simp only [Units.coe_map, Units.val_mul, Units.val_pow_eq_pow_val,
      rationalTwoAdicSignedOddUnit_coe]
    rw [haC]
    change
      e.symm ((((-1 : ℤ) ^ (m / 2) * (m : ℤ) : ℤ) : ℚ_[2])) =
        (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) ^ (m / 2) *
          (m : (HeightOneSpectrum.adicAbv ℚ v₂).Completion)
    calc
      e.symm ((((-1 : ℤ) ^ (m / 2) * (m : ℤ) : ℤ) : ℚ_[2])) =
          (((-1 : ℤ) ^ (m / 2) * (m : ℤ) : ℤ) :
            (HeightOneSpectrum.adicAbv ℚ v₂).Completion) :=
        map_intCast e.symm.toRingHom _
      _ = (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) ^ (m / 2) *
          (m : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) := by norm_num
  have hqSq : (((-1 : Cˣ) ^ (m / 2)) ^ 2) = 1 := by
    calc
      (((-1 : Cˣ) ^ (m / 2)) ^ 2) = ((-1 : Cˣ) ^ 2) ^ (m / 2) := by
        rw [← pow_mul, Nat.mul_comm, pow_mul]
      _ = 1 := by rw [neg_one_sq, one_pow]
  refine ⟨rC, ?_⟩
  rcases hrQ with hrQ | hrQ
  · left
    have hmapped := congrArg
      (Units.map e.symm.toMonoidHom) hrQ
    have hsignedEq :
        (-1 : Cˣ) ^ (m / 2) * aC = rC ^ 2 := by
      simpa only [hsigned, map_pow, rC] using hmapped
    calc
      aC = 1 * aC := (one_mul aC).symm
      _ = (((-1 : Cˣ) ^ (m / 2)) ^ 2) * aC := by rw [hqSq]
      _ = (-1 : Cˣ) ^ (m / 2) *
          (((-1 : Cˣ) ^ (m / 2)) * aC) := by
        rw [pow_two, mul_assoc]
      _ = (-1 : Cˣ) ^ (m / 2) * rC ^ 2 := by rw [hsignedEq]
  · right
    have hmapped := congrArg
      (Units.map e.symm.toMonoidHom) hrQ
    have hfiveMapped :
        Units.map e.symm.toMonoidHom fiveQ = fiveC := by
      apply Units.ext
      change e.symm (5 : ℚ_[2]) = (5 : C)
      simpa using map_natCast e.symm 5
    have hsignedEq :
        (-1 : Cˣ) ^ (m / 2) * aC = fiveC * rC ^ 2 := by
      simpa only [hsigned, map_mul, map_pow, hfiveMapped, rC, fiveQ]
        using hmapped
    calc
      aC = 1 * aC := (one_mul aC).symm
      _ = (((-1 : Cˣ) ^ (m / 2)) ^ 2) * aC := by rw [hqSq]
      _ = (-1 : Cˣ) ^ (m / 2) *
          (((-1 : Cˣ) ^ (m / 2)) * aC) := by
        rw [pow_two, mul_assoc]
      _ = (-1 : Cˣ) ^ (m / 2) * (fiveC * rC ^ 2) :=
        congrArg (fun z => (-1 : Cˣ) ^ (m / 2) * z) hsignedEq
theorem

localHilbertSymbol_pow_left

L404 ↗
GlobalClassFieldTheory.Reciprocity.localHilbertSymbol_pow_left
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localHilbertSymbol_pow_left
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x y : Fˣ) (e : ℕ) :
    localHilbertSymbol F n hnF hmu (x ^ e) y =
      localHilbertSymbol F n hnF hmu x y ^ e
theorem

localHilbertSymbol_pow_right

L417 ↗
GlobalClassFieldTheory.Reciprocity.localHilbertSymbol_pow_right
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localHilbertSymbol_pow_right
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x y : Fˣ) (e : ℕ) :
    localHilbertSymbol F n hnF hmu x (y ^ e) =
      localHilbertSymbol F n hnF hmu x y ^ e
theorem

localHilbertSymbol_mul_left

L429 ↗
GlobalClassFieldTheory.Reciprocity.localHilbertSymbol_mul_left
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localHilbertSymbol_mul_left
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x y z : Fˣ) :
    localHilbertSymbol F n hnF hmu (x * y) z =
      localHilbertSymbol F n hnF hmu x z *
        localHilbertSymbol F n hnF hmu y z
theorem

localHilbertSymbol_pow_pow

L444 ↗
GlobalClassFieldTheory.Reciprocity.localHilbertSymbol_pow_pow
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localHilbertSymbol_pow_pow
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x y : Fˣ) (a b : ℕ) :
    localHilbertSymbol F n hnF hmu (x ^ a) (y ^ b) =
      localHilbertSymbol F n hnF hmu x y ^ (a * b)
theorem

localQuadraticHilbertSymbol_square_left_eq_one

L455 ↗
GlobalClassFieldTheory.Reciprocity.localQuadraticHilbertSymbol_square_left_eq_one
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localQuadraticHilbertSymbol_square_left_eq_one
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (h2F : ((((2 : ℕ+) : ℕ)) : F) ≠ 0)
    (hmu : (primitiveRoots (((2 : ℕ+) : ℕ)) F).Nonempty)
    (x y : Fˣ) :
    localHilbertSymbol F (2 : ℕ+) h2F hmu (x ^ 2) y = 1
theorem

localQuadraticHilbertSymbol_square_right_eq_one

L466 ↗
GlobalClassFieldTheory.Reciprocity.localQuadraticHilbertSymbol_square_right_eq_one
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localQuadraticHilbertSymbol_square_right_eq_one
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (h2F : ((((2 : ℕ+) : ℕ)) : F) ≠ 0)
    (hmu : (primitiveRoots (((2 : ℕ+) : ℕ)) F).Nonempty)
    (x y : Fˣ) :
    localHilbertSymbol F (2 : ℕ+) h2F hmu x (y ^ 2) = 1
theorem

localQuadraticHilbertSymbol_value_sq_eq_one

L477 ↗
GlobalClassFieldTheory.Reciprocity.localQuadraticHilbertSymbol_value_sq_eq_one
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localQuadraticHilbertSymbol_value_sq_eq_one
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (h2F : ((((2 : ℕ+) : ℕ)) : F) ≠ 0)
    (hmu : (primitiveRoots (((2 : ℕ+) : ℕ)) F).Nonempty)
    (x y : Fˣ) :
    localHilbertSymbol F (2 : ℕ+) h2F hmu x y ^ 2 = 1
theorem

localQuadraticHilbertSymbol_squareClass_formula

L487 ↗
GlobalClassFieldTheory.Reciprocity.localQuadraticHilbertSymbol_squareClass_formula
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem localQuadraticHilbertSymbol_squareClass_formula
    (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    (h2F : ((((2 : ℕ+) : ℕ)) : F) ≠ 0)
    (hmu : (primitiveRoots (((2 : ℕ+) : ℕ)) F).Nonempty)
    (q five a b r s : Fˣ) (ka kb : ℕ)
    (negRoot : nthRootsSubgroup F (((2 : ℕ+) : ℕ)))
    (hqq : localHilbertSymbol F (2 : ℕ+) h2F hmu q q = negRoot)
    (hqfive :
      localHilbertSymbol F (2 : ℕ+) h2F hmu q five = 1)
    (hfivefive :
      localHilbertSymbol F (2 : ℕ+) h2F hmu five five = 1)
    (ha : a = q ^ ka * r ^ 2 ∨
      a = q ^ ka * (five * r ^ 2))
    (hb : b = q ^ kb * s ^ 2 ∨
      b = q ^ kb * (five * s ^ 2)) :
    localHilbertSymbol F (2 : ℕ+) h2F hmu a b =
      negRoot ^ (ka * kb)
theorem

rationalTwoAdicHilbert_negOne_five_eq_one

L528 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicHilbert_negOne_five_eq_one
Documentation

The dyadic quadratic Hilbert symbol of -1 and 5 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicHilbert_negOne_five_eq_one :
    let v₂ := RayClass.rationalPrime rationalTwoPrime
    let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v₂
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
    localHilbertSymbol C (2 : ℕ+)
        (finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
          (by norm_num) v₂)
        (finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
          rationalQuadraticPrimitiveRoots_nonempty v₂)
        (-1 : Cˣ) (Units.mk0 (5 : C)
          (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+)
            (by norm_num) v₂)) = 1 := by
  dsimp only
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
  let : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v₂
  let : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
  let h2C := finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
    (by norm_num) v₂
  let hmuC := finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
    rationalQuadraticPrimitiveRoots_nonempty v₂
  let two : Cˣ := Units.mk0 (2 : C)
    (finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+) (by norm_num) v₂)
  let negFour : Cˣ := Units.mk0 (-4 : C)
    (neg_ne_zero.mpr
      (finitePlaceHilbert_natCast_ne_zero ℚ (4 : ℕ+) (by norm_num) v₂))
  let five : Cˣ := Units.mk0 (5 : C)
    (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+) (by norm_num) v₂)
  have hnegFour : negFour = (-1 : Cˣ) * two ^ 2 := by
    apply Units.ext
    change
      (-4 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) =
        (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) *
          (2 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) ^ 2
    norm_num
  have hstein :
      localHilbertSymbol C (2 : ℕ+) h2C hmuC negFour five = 1 := by
    have hcomp : 1 - (negFour : C) ≠ 0 := by
      have hval : 1 - (negFour : C) = (5 : C) := by
        dsimp only [negFour]
        change
          1 - (-4 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) = 5
        norm_num
      rw [hval]
      exact finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+)
        (by norm_num) v₂
    have hs := localHilbertSymbol_steinberg C (2 : ℕ+) h2C hmuC negFour hcomp
    have hfiveComp : five = Units.mk0 (1 - (negFour : C)) hcomp := by
      apply Units.ext
      dsimp only [negFour, five]
      change
        (5 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) = 1 - (-4)
      norm_num
    rw [hfiveComp]
    exact hs
  rw [hnegFour] at hstein
  change
    localHilbertSymbolHom C (2 : ℕ+) h2C hmuC five
        ((-1 : Cˣ) * two ^ 2) = 1 at hstein
  rw [map_mul] at hstein
  change
    localHilbertSymbol C (2 : ℕ+) h2C hmuC (-1 : Cˣ) five *
        localHilbertSymbol C (2 : ℕ+) h2C hmuC (two ^ 2) five = 1
      at hstein
  rw [localQuadraticHilbertSymbol_square_left_eq_one, mul_one] at hstein
  exact hstein
theorem

rationalTwoAdicHilbert_five_five_eq_one

L601 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicHilbert_five_five_eq_one
Documentation

The dyadic quadratic Hilbert symbol of 5 with itself 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicHilbert_five_five_eq_one :
    let v₂ := RayClass.rationalPrime rationalTwoPrime
    let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v₂
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
    localHilbertSymbol C (2 : ℕ+)
        (finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
          (by norm_num) v₂)
        (finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
          rationalQuadraticPrimitiveRoots_nonempty v₂)
        (Units.mk0 (5 : C)
          (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+)
            (by norm_num) v₂))
        (Units.mk0 (5 : C)
          (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+)
            (by norm_num) v₂)) = 1 := by
  dsimp only
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
  let : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v₂
  let : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
  let h2C := finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
    (by norm_num) v₂
  let hmuC := finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
    rationalQuadraticPrimitiveRoots_nonempty v₂
  let five : Cˣ := Units.mk0 (5 : C)
    (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+) (by norm_num) v₂)
  have hneg :
      localHilbertSymbol C (2 : ℕ+) h2C hmuC five (-five) = 1 :=
    localHilbertSymbol_neg_self C (2 : ℕ+) h2C hmuC five
  have hdecomp : -five = (-1 : Cˣ) * five := by
    apply Units.ext
    change
      -(5 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) =
        (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completion) * 5
    ring
  rw [hdecomp, localHilbertSymbol_mul_right] at hneg
  have hskew :
      localHilbertSymbol C (2 : ℕ+) h2C hmuC five (-1 : Cˣ) = 1 := by
    rw [localHilbertSymbol_skew,
      rationalTwoAdicHilbert_negOne_five_eq_one, inv_one]
  rw [hskew, one_mul] at hneg
  exact hneg
def

rationalQuadraticNegOneFieldUnit

L650 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticNegOneFieldUnit
Documentation

The rational global field unit represented by -1.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def rationalQuadraticNegOneFieldUnit : ℚˣ
theorem

rationalQuadraticNegOneFieldUnit_coe

L654 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticNegOneFieldUnit_coe
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalQuadraticNegOneFieldUnit_coe :
    (rationalQuadraticNegOneFieldUnit : ℚ) = -1
theorem

rationalQuadraticNegOne_not_mem

L658 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticNegOne_not_mem
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalQuadraticNegOne_not_mem
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    (-1 : 𝓞 ℚ) ∉ v.asIdeal
theorem

rationalFinitePlaceHilbert_negOne_negOne_eq_one_of_ne_two

L666 ↗
GlobalClassFieldTheory.Reciprocity.rationalFinitePlaceHilbert_negOne_negOne_eq_one_of_ne_two
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalFinitePlaceHilbert_negOne_negOne_eq_one_of_ne_two
    (v : HeightOneSpectrum (𝓞 ℚ))
    (hv : v ≠ RayClass.rationalPrime rationalTwoPrime) :
    finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
        rationalQuadraticPrimitiveRoots_nonempty v
        rationalQuadraticNegOneFieldUnit
        rationalQuadraticNegOneFieldUnit = 1 := by
  apply finitePlaceHilbertSymbol_integral_units_eq_one
      ℚ (2 : ℕ+) (by norm_num)
        rationalQuadraticPrimitiveRoots_nonempty v
  · rw [powerResidueExponentFinitePlaces_rational_two]
    simpa only [Finset.mem_singleton]
  · exact rationalQuadraticNegOne_not_mem v
  · exact rationalQuadraticNegOne_not_mem v
theorem

rationalFinitePlaceHilbert_negOne_negOne_eq_negOne

L684 ↗
GlobalClassFieldTheory.Reciprocity.rationalFinitePlaceHilbert_negOne_negOne_eq_negOne
Documentation

The finite-place Hilbert factor of (-1,-1) at the prime above two is the negative quadratic root. The proof uses the global product formula; all odd finite factors are trivial and the unique real factor is -1.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalFinitePlaceHilbert_negOne_negOne_eq_negOne :
    finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
        rationalQuadraticPrimitiveRoots_nonempty
        (RayClass.rationalPrime rationalTwoPrime)
        rationalQuadraticNegOneFieldUnit
        rationalQuadraticNegOneFieldUnit =
      integralRootsOfUnityToNthRoots ℚ 2
        rationalQuadraticNegOneRoot := by
  let negRoot : nthRootsSubgroup ℚ (((2 : ℕ+) : ℕ)) :=
    integralRootsOfUnityToNthRoots ℚ (((2 : ℕ+) : ℕ))
      rationalQuadraticNegOneRoot
  have hinfinite :
      (∏ v : InfinitePlace ℚ,
        infinitePlaceHilbertSymbol ℚ (2 : ℕ+)
          v rationalQuadraticNegOneFieldUnit
            rationalQuadraticNegOneFieldUnit) = negRoot := by
    rw [Fintype.prod_unique,
      show (default : InfinitePlace ℚ) = Rat.infinitePlace by
        exact Subsingleton.elim _ _]
    apply Subtype.ext
    have hreal := infinitePlaceHilbertSymbol_real_apply
      ℚ (2 : ℕ+) Rat.infinitePlace
        rationalQuadraticNegOneFieldUnit rationalQuadraticNegOneFieldUnit
          rfl Rat.isReal_infinitePlace
    have hneg :
        InfinitePlace.embedding_of_isReal Rat.isReal_infinitePlace
          (rationalQuadraticNegOneFieldUnit : ℚ) < 0 := by
      rw [rationalQuadraticNegOneFieldUnit_coe, map_neg, map_one]
      norm_num
    rw [ite_eq_left ⟨hneg, hneg⟩] at hreal
    have hreal' :
        (infinitePlaceHilbertSymbol ℚ (2 : ℕ+) Rat.infinitePlace
          rationalQuadraticNegOneFieldUnit
            rationalQuadraticNegOneFieldUnit).1 = (-1 : ℚˣ) := by
      simpa [rationalQuadraticNegOneFieldUnit] using hreal
    have hnegRootVal : negRoot.1 = (-1 : ℚˣ) := by
      apply Units.ext
      change algebraMap (𝓞 ℚ) ℚ (-1 : 𝓞 ℚ) = (-1 : ℚ)
      rw [map_neg, map_one]
    exact hreal'.trans hnegRootVal.symm
  have hfinite :
      (∏ᶠ v : HeightOneSpectrum (𝓞 ℚ),
        finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
          rationalQuadraticPrimitiveRoots_nonempty v
          rationalQuadraticNegOneFieldUnit
          rationalQuadraticNegOneFieldUnit) =
        finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
          rationalQuadraticPrimitiveRoots_nonempty
          (RayClass.rationalPrime rationalTwoPrime)
          rationalQuadraticNegOneFieldUnit
          rationalQuadraticNegOneFieldUnit := by
    apply finprod_eq_single
    intro v hv
    exact
      rationalFinitePlaceHilbert_negOne_negOne_eq_one_of_ne_two v hv
  have hproduct := hilbertSymbol_allPlaces_product_eq_one
    ℚ (2 : ℕ+) (by norm_num)
      rationalQuadraticPrimitiveRoots_nonempty
        rationalQuadraticNegOneFieldUnit
          rationalQuadraticNegOneFieldUnit
  rw [hinfinite, hfinite] at hproduct
  have hnegRootSquare : negRoot * negRoot = 1 := by
    have hroot : negRoot.1 ^ (((2 : ℕ+) : ℕ)) = (1 : ℚˣ) :=
      (KummerTheory.mem_nthRootsSubgroup_iff ℚ).mp negRoot.2
    change negRoot.1 ^ 2 = (1 : ℚˣ) at hroot
    apply Subtype.ext
    change negRoot.1 * negRoot.1 = (1 : ℚˣ)
    simpa only [pow_two] using hroot
  let twoFactor :=
    finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
      rationalQuadraticPrimitiveRoots_nonempty
      (RayClass.rationalPrime rationalTwoPrime)
      rationalQuadraticNegOneFieldUnit rationalQuadraticNegOneFieldUnit
  change twoFactor = negRoot
  calc
    twoFactor = 1 * twoFactor := (one_mul twoFactor).symm
    _ = (negRoot * negRoot) * twoFactor := by rw [hnegRootSquare]
    _ = negRoot * (negRoot * twoFactor) := mul_assoc _ _ _
    _ = negRoot := by rw [hproduct, mul_one]
theorem

rationalTwoAdicHilbert_negOne_negOne_eq_negOne

L766 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicHilbert_negOne_negOne_eq_negOne
Documentation

In the canonical dyadic completion, the local quadratic Hilbert symbol of (-1,-1) is -1.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicHilbert_negOne_negOne_eq_negOne :
    let v₂ := RayClass.rationalPrime rationalTwoPrime
    let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v₂
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
    localHilbertSymbol C (2 : ℕ+)
        (finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
          (by norm_num) v₂)
        (finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
          rationalQuadraticPrimitiveRoots_nonempty v₂)
        (-1 : Cˣ) (-1 : Cˣ) =
      (⟨(-1 : Cˣ), by
        apply (KummerTheory.mem_nthRootsSubgroup_iff C).mpr
        change
          ((-1 : (HeightOneSpectrum.adicAbv ℚ
            (RayClass.rationalPrime rationalTwoPrime)).Completionˣ)) ^ 2 = 1
        norm_num⟩ : nthRootsSubgroup C 2) := by
  dsimp only
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
  let : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v₂
  let : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
  let hn : ((((2 : ℕ+) : ℕ)) : ℚ) ≠ 0 := by norm_num
  have hmap := finitePlaceHilbertSymbol_map_eq_localHilbertSymbol
    ℚ (2 : ℕ+) hn rationalQuadraticPrimitiveRoots_nonempty
      (RayClass.rationalPrime rationalTwoPrime)
        rationalQuadraticNegOneFieldUnit rationalQuadraticNegOneFieldUnit
  rw [rationalFinitePlaceHilbert_negOne_negOne_eq_negOne] at hmap
  have hmappedNeg :
      nthRootsSubgroupMap ℚ
        (HeightOneSpectrum.adicAbv ℚ
          (RayClass.rationalPrime rationalTwoPrime)).Completion 2
          (integralRootsOfUnityToNthRoots ℚ 2
            rationalQuadraticNegOneRoot) =
        (⟨(-1 : (HeightOneSpectrum.adicAbv ℚ
          (RayClass.rationalPrime rationalTwoPrime)).Completionˣ), by
            apply (KummerTheory.mem_nthRootsSubgroup_iff _).mpr
            norm_num⟩ : nthRootsSubgroup _ 2) := by
    apply Subtype.ext
    apply Units.ext
    change
      algebraMap ℚ (HeightOneSpectrum.adicAbv ℚ
        (RayClass.rationalPrime rationalTwoPrime)).Completion (-1) = -1
    rw [map_neg, map_one]
  have hnegC :
      finitePlaceHilbert_completionUnit ℚ
          (RayClass.rationalPrime rationalTwoPrime)
            rationalQuadraticNegOneFieldUnit =
        (-1 : (HeightOneSpectrum.adicAbv ℚ
          (RayClass.rationalPrime rationalTwoPrime)).Completionˣ) := by
    apply Units.ext
    change
      algebraMap ℚ (HeightOneSpectrum.adicAbv ℚ
        (RayClass.rationalPrime rationalTwoPrime)).Completion (-1) = -1
    rw [map_neg, map_one]
  have hresult := hmap.symm.trans hmappedNeg
  unfold finitePlaceLocalHilbertSymbol at hresult
  rw [hnegC] at hresult
  exact hresult
theorem

rationalTwoAdicHilbert_odd_eq_classicalSign

L832 ↗
GlobalClassFieldTheory.Reciprocity.rationalTwoAdicHilbert_odd_eq_classicalSign
Documentation

Explicit dyadic quadratic Hilbert-symbol formula for positive odd rational integers.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalTwoAdicHilbert_odd_eq_classicalSign
    (a b : ℕ) (ha : Odd a) (hb : Odd b) :
    let v₂ := RayClass.rationalPrime rationalTwoPrime
    let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
    letI : ValuativeRel C :=
      finitePlaceLocalArtinCompletionValuativeRel v₂
    letI : IsNonarchimedeanLocalField C :=
      finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
    localHilbertSymbol C (2 : ℕ+)
        (finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
          (by norm_num) v₂)
        (finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
          rationalQuadraticPrimitiveRoots_nonempty v₂)
        (finitePlaceHilbert_completionUnit ℚ v₂
          (rationalNaturalFieldUnit a (by
            intro ha0
            subst a
            norm_num at ha)))
        (finitePlaceHilbert_completionUnit ℚ v₂
          (rationalNaturalFieldUnit b (by
            intro hb0
            subst b
            norm_num at hb))) =
      (⟨(-1 : Cˣ), by
        apply (KummerTheory.mem_nthRootsSubgroup_iff C).mpr
        change
          (-1 : (HeightOneSpectrum.adicAbv ℚ
            (RayClass.rationalPrime rationalTwoPrime)).Completionˣ) ^ 2 = 1
        norm_num⟩ : nthRootsSubgroup C 2) ^
        (a / 2 * (b / 2)) := by
  dsimp only
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  let C := (HeightOneSpectrum.adicAbv ℚ v₂).Completion
  let : ValuativeRel C :=
    finitePlaceLocalArtinCompletionValuativeRel v₂
  let : IsNonarchimedeanLocalField C :=
    finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v₂
  let h2C := finitePlaceHilbert_natCast_ne_zero ℚ (2 : ℕ+)
    (by norm_num) v₂
  let hmuC := finitePlaceHilbert_primitiveRoots_nonempty ℚ (2 : ℕ+)
    rationalQuadraticPrimitiveRoots_nonempty v₂
  have ha0 : a ≠ 0 := by
    intro ha0
    subst a
    norm_num at ha
  have hb0 : b ≠ 0 := by
    intro hb0
    subst b
    norm_num at hb
  let aC := finitePlaceHilbert_completionUnit ℚ v₂
    (rationalNaturalFieldUnit a ha0)
  let bC := finitePlaceHilbert_completionUnit ℚ v₂
    (rationalNaturalFieldUnit b hb0)
  let fiveC : Cˣ := Units.mk0 (5 : C)
    (finitePlaceHilbert_natCast_ne_zero ℚ (5 : ℕ+) (by norm_num) v₂)
  let negRootC : nthRootsSubgroup C 2 := ⟨(-1 : Cˣ), by
    apply (KummerTheory.mem_nthRootsSubgroup_iff C).mpr
    change
      (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completionˣ) ^ 2 = 1
    norm_num⟩
  obtain ⟨r, hr⟩ := rationalTwoAdicOddUnit_squareClass a ha
  obtain ⟨s, hs⟩ := rationalTwoAdicOddUnit_squareClass b hb
  exact localQuadraticHilbertSymbol_squareClass_formula
    C h2C hmuC (-1 : Cˣ) fiveC aC bC r s
      (a / 2) (b / 2) negRootC
      rationalTwoAdicHilbert_negOne_negOne_eq_negOne
      rationalTwoAdicHilbert_negOne_five_eq_one
      rationalTwoAdicHilbert_five_five_eq_one hr hs
theorem

rationalFinitePlaceHilbert_odd_eq_classicalSign

L903 ↗
GlobalClassFieldTheory.Reciprocity.rationalFinitePlaceHilbert_odd_eq_classicalSign
Documentation

The global finite-place Hilbert factor at two is the classical quadratic sign for positive odd rational integers.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalFinitePlaceHilbert_odd_eq_classicalSign
    (a b : ℕ) (ha : Odd a) (hb : Odd b) :
    finitePlaceHilbertSymbol ℚ (2 : ℕ+) (by norm_num)
        rationalQuadraticPrimitiveRoots_nonempty
        (RayClass.rationalPrime rationalTwoPrime)
        (rationalNaturalFieldUnit a (by
          intro ha0
          subst a
          norm_num at ha))
        (rationalNaturalFieldUnit b (by
          intro hb0
          subst b
          norm_num at hb)) =
      integralRootsOfUnityToNthRoots ℚ 2
        (rationalQuadraticNegOneRoot ^ (a / 2 * (b / 2))) := by
  have ha0 : a ≠ 0 := by
    intro ha0
    subst a
    norm_num at ha
  have hb0 : b ≠ 0 := by
    intro hb0
    subst b
    norm_num at hb
  let hn : ((2 : ℕ) : ℚ) ≠ 0 := by norm_num
  let v₂ := RayClass.rationalPrime rationalTwoPrime
  change finitePlaceHilbertSymbol ℚ (2 : ℕ+) hn
      rationalQuadraticPrimitiveRoots_nonempty v₂
      (rationalNaturalFieldUnit a ha0)
      (rationalNaturalFieldUnit b hb0) = _
  apply nthRootsSubgroupMap_injective ℚ
    (HeightOneSpectrum.adicAbv ℚ v₂).Completion 2
  have hmap := finitePlaceHilbertSymbol_map_eq_localHilbertSymbol
    ℚ (2 : ℕ+) hn rationalQuadraticPrimitiveRoots_nonempty v₂
      (rationalNaturalFieldUnit a ha0) (rationalNaturalFieldUnit b hb0)
  have hlocal := rationalTwoAdicHilbert_odd_eq_classicalSign a b ha hb
  dsimp only at hlocal
  have hrootMap :
      nthRootsSubgroupMap ℚ
          (HeightOneSpectrum.adicAbv ℚ v₂).Completion 2
          (integralRootsOfUnityToNthRoots ℚ 2
            (rationalQuadraticNegOneRoot ^ (a / 2 * (b / 2)))) =
        (⟨(-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completionˣ), by
            apply (KummerTheory.mem_nthRootsSubgroup_iff _).mpr
            norm_num⟩ : nthRootsSubgroup _ 2) ^
          (a / 2 * (b / 2)) := by
    apply Subtype.ext
    change
      Units.map (algebraMap ℚ
        (HeightOneSpectrum.adicAbv ℚ v₂).Completion).toMonoidHom
          (Units.map (algebraMap (𝓞 ℚ) ℚ).toMonoidHom
            ((-1 : (𝓞 ℚ)ˣ) ^ (a / 2 * (b / 2)))) =
        (-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completionˣ) ^
          (a / 2 * (b / 2))
    rw [map_pow, map_pow]
    congr 1
    apply Units.ext
    simp
  have hlocal' :
      finitePlaceLocalHilbertSymbol ℚ (2 : ℕ+) hn
          rationalQuadraticPrimitiveRoots_nonempty v₂
          (rationalNaturalFieldUnit a ha0)
          (rationalNaturalFieldUnit b hb0) =
        (⟨(-1 : (HeightOneSpectrum.adicAbv ℚ v₂).Completionˣ), by
            apply (KummerTheory.mem_nthRootsSubgroup_iff _).mpr
            norm_num⟩ : nthRootsSubgroup _ 2) ^
          (a / 2 * (b / 2)) := by
    unfold finitePlaceLocalHilbertSymbol
    exact hlocal
  exact hmap.trans (hlocal'.trans hrootMap.symm)
theorem

rationalInfinitePlaceHilbert_natural_eq_one

L973 ↗
GlobalClassFieldTheory.Reciprocity.rationalInfinitePlaceHilbert_natural_eq_one
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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalInfinitePlaceHilbert_natural_eq_one
    (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0)
    (v : InfinitePlace ℚ) :
    infinitePlaceHilbertSymbol ℚ (2 : ℕ+) v
        (rationalNaturalFieldUnit a ha)
        (rationalNaturalFieldUnit b hb) = 1
theorem

rationalQuadraticBadPlaceCorrection_eq_classicalSign

L1004 ↗
GlobalClassFieldTheory.Reciprocity.rationalQuadraticBadPlaceCorrection_eq_classicalSign
Documentation

Evaluation of the complete rational quadratic bad-place correction. For positive odd inputs the infinite factor is trivial, and the sole finite bad place is 2, whose wild Hilbert symbol gives the classical sign.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · full declaration
theorem rationalQuadraticBadPlaceCorrection_eq_classicalSign
    (a b : ℕ) (ha : Odd a) (hb : Odd b) :
    powerResidueBadPlaceCorrection ℚ (2 : ℕ+) (by norm_num)
        rationalQuadraticPrimitiveRoots_nonempty
        (rationalNaturalFieldUnit a (by
          intro ha0
          subst a
          norm_num at ha))
        (rationalNaturalFieldUnit b (by
          intro hb0
          subst b
          norm_num at hb)) =
      integralRootsOfUnityToNthRoots ℚ 2
        (rationalQuadraticNegOneRoot ^ (a / 2 * (b / 2))) := by
  have ha0 : a ≠ 0 := by
    intro ha0
    subst a
    norm_num at ha
  have hb0 : b ≠ 0 := by
    intro hb0
    subst b
    norm_num at hb
  let hn : ((((2 : ℕ+) : ℕ)) : ℚ) ≠ 0 := by norm_num
  change powerResidueBadPlaceCorrection ℚ (2 : ℕ+) hn
      rationalQuadraticPrimitiveRoots_nonempty
      (rationalNaturalFieldUnit a ha0)
      (rationalNaturalFieldUnit b hb0) = _
  unfold powerResidueBadPlaceCorrection
  have hinfinite :
      (∏ v : InfinitePlace ℚ,
        infinitePlaceHilbertSymbol ℚ (2 : ℕ+) v
          (rationalNaturalFieldUnit a ha0)
          (rationalNaturalFieldUnit b hb0)) = 1 := by
    apply Finset.prod_eq_one
    intro v _
    exact rationalInfinitePlaceHilbert_natural_eq_one a b ha0 hb0 v
  rw [hinfinite, one_mul,
    powerResidueExponentFinitePlaces_rational_two,
    Finset.prod_singleton,
    rationalFinitePlaceHilbert_odd_eq_classicalSign a b ha hb]
theorem

rationalPrincipalIdeal_primeDivisors_away_from_two

L1047 ↗
GlobalClassFieldTheory.Reciprocity.rationalPrincipalIdeal_primeDivisors_away_from_two
Documentation

Every prime divisor of an odd rational principal ideal is away from the quadratic exponent 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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem rationalPrincipalIdeal_primeDivisors_away_from_two
    (m : ℕ) (hm : Odd m)
    (P : HeightOneSpectrum (𝓞 ℚ))
    (hP : P.asIdeal ∣ rationalPrincipalIdeal m) :
    P ∉ powerResidueExponentFinitePlaces ℚ (2 : ℕ+)
theorem

gaussReciprocity_nat_from_powerResidueReciprocity

L1064 ↗
GlobalClassFieldTheory.Reciprocity.gaussReciprocity_nat_from_powerResidueReciprocity
Documentation

Gauss reciprocity derived from the global power-residue reciprocity theorem, including the explicitly evaluated dyadic correction. The proof does not invoke the pre-existing quadratic-reciprocity theorem.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem gaussReciprocity_nat_from_powerResidueReciprocity
    {a b : ℕ} (ha : Odd a) (hb : Odd b) (hab : a.Coprime b) :
    J((a : ℤ) | b) * J((b : ℤ) | a) =
      (-1 : ℤ) ^ (a / 2 * (b / 2))
theorem

gaussReciprocity_nat_from_powerResidueReciprocity_eq_mathlib

L1226 ↗
GlobalClassFieldTheory.Reciprocity.gaussReciprocity_nat_from_powerResidueReciprocity_eq_mathlib
Documentation

The CFT-derived theorem agrees propositionally with the existing library statement. This comparison is the only place where the pre-existing theorem is mentioned.

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

-- Specializing the generic completion construction to `ℚ` must keep the
-- `Algebra.id` owner fixed.  Otherwise the rational-field algebra path is
-- underdetermined during instance synthesis.
@[reducible] noncomputable local instance
    (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra ℚ (HeightOneSpectrum.adicAbv ℚ v).Completion := by
  letI : Algebra ℚ ℚ := Algebra.id ℚ
  let hWith : Algebra ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instAlgebra _
  let hUniform : UniformContinuousConstSMul ℚ
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) :=
    WithAbs.instUniformContinuousConstSMulReal _
  exact
    @UniformSpace.Completion.algebra
      (WithAbs (HeightOneSpectrum.adicAbv ℚ v)) _ _ _ _
      ℚ _ hWith hUniform
open KummerTheory
open AlgebraicNumberTheory.PowerResidueSymbols
open LocalClassFieldTheory.Kummer
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem gaussReciprocity_nat_from_powerResidueReciprocity_eq_mathlib
    {a b : ℕ} (ha : Odd a) (hb : Odd b) (hab : a.Coprime b) :
    gaussReciprocity_nat_from_powerResidueReciprocity ha hb hab =
      AlgebraicNumberTheory.PowerResidueSymbols.gaussReciprocity_nat
        ha hb hab

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