Module

FinitePlaceAdicHilbertComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FinitePlaceAdicHilbertComparison

3 declarations indexed from sourceView source ↗

Module documentation

Comparison of finite-place Hilbert factors

The finite-place factor of the transported adic pairing agrees with the established finite-place Hilbert symbol.

Imports2

Imported by3

theorem

globalFinitePlaceHilbertSymbol_map_eq_local

L26 ↗

ClassFieldTheory.globalFinitePlaceHilbertSymbol_map_eq_local

Documentation

The established finite-place symbol becomes the local Mathlib-facing Hilbert symbol after mapping to the absolute-value completion.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · full declaration

theorem globalFinitePlaceHilbertSymbol_map_eq_local
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (v : HeightOneSpectrum (𝓞 F)) (a b : Fˣ) :
    let C := (HeightOneSpectrum.adicAbv F v).Completion
    letI : ValuativeRel C :=
      GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
    let eFC : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) C :=
      letI : NeZero (n : ℕ) := ⟨n.ne_zero⟩
      rootsOfUnityEquivOfPrimitiveRoots (algebraMap F C).injective hmu
    eFC (globalFinitePlaceHilbertSymbol F n hnF hmu v a b) =
      localHilbertSymbol C n
        (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_natCast_ne_zero
          F n hnF v)
        (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_primitiveRoots_nonempty
          F n hmu v)
        (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_completionUnit F v a)
        (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_completionUnit F v b) := by
  let C := (HeightOneSpectrum.adicAbv F v).Completion
  let : ValuativeRel C :=
    GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
  let : NeZero (n : ℕ) := ⟨n.ne_zero⟩
  let eFC : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) C :=
    rootsOfUnityEquivOfPrimitiveRoots (algebraMap F C).injective hmu
  change eFC
    (KummerTheory.nthRootsSubgroupEquivRootsOfUnity F (n : ℕ)
      (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol
        F n hnF hmu v a b)) =
    KummerTheory.nthRootsSubgroupEquivRootsOfUnity C (n : ℕ)
      (GlobalClassFieldTheory.Reciprocity.finitePlaceLocalHilbertSymbol
        F n hnF hmu v a b)
  apply Subtype.ext
  have h := congrArg Subtype.val
    (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_map_eq_localHilbertSymbol
      F n hnF hmu v a b)
  change Units.map (algebraMap F C).toMonoidHom
      (GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol
        F n hnF hmu v a b) =
    GlobalClassFieldTheory.Reciprocity.finitePlaceLocalHilbertSymbol
      F n hnF hmu v a b
  exact h

theorem

rootsOfUnity_finiteCompletion_comp

L71 ↗

ClassFieldTheory.rootsOfUnity_finiteCompletion_comp

Documentation

Mapping roots of unity from the number field to the adic completion agrees with mapping first to the absolute-value completion.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · full declaration

theorem rootsOfUnity_finiteCompletion_comp
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (v : HeightOneSpectrum (𝓞 F))
    (hmuC : (primitiveRoots (n : ℕ)
      (HeightOneSpectrum.adicAbv F v).Completion).Nonempty)
    (z : rootsOfUnity (n : ℕ) F) :
    let C := (HeightOneSpectrum.adicAbv F v).Completion
    let D := v.adicCompletion F
    letI : NeZero (n : ℕ) := ⟨n.ne_zero⟩
    let eFC : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) C :=
      rootsOfUnityEquivOfPrimitiveRoots (algebraMap F C).injective hmu
    let eFD : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) D :=
      rootsOfUnityEquivOfPrimitiveRoots (algebraMap F D).injective hmu
    let eCD : rootsOfUnity (n : ℕ) C ≃* rootsOfUnity (n : ℕ) D :=
      rootsOfUnityEquivOfRingEquiv
        (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv n hmuC
    eFD z = eCD (eFC z) := by
  let C := (HeightOneSpectrum.adicAbv F v).Completion
  let D := v.adicCompletion F
  let : NeZero (n : ℕ) := ⟨n.ne_zero⟩
  let eFC : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) C :=
    rootsOfUnityEquivOfPrimitiveRoots (algebraMap F C).injective hmu
  let eFD : rootsOfUnity (n : ℕ) F ≃* rootsOfUnity (n : ℕ) D :=
    rootsOfUnityEquivOfPrimitiveRoots (algebraMap F D).injective hmu
  let eCD : rootsOfUnity (n : ℕ) C ≃* rootsOfUnity (n : ℕ) D :=
    rootsOfUnityEquivOfRingEquiv
      (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv n hmuC
  apply Subtype.ext
  apply Units.ext
  change algebraMap F D ((z : Fˣ) : F) =
    (relativeFinitePlaceCompletionAlgEquiv v)
      (algebraMap F C ((z : Fˣ) : F))
  exact (relativeFinitePlaceCompletionAlgEquiv v).commutes ((z : Fˣ) : F) |>.symm

theorem

finitePlaceAdicHilbertPairingFamily_finiteFactor

L108 ↗

ClassFieldTheory.finitePlaceAdicHilbertPairingFamily_finiteFactor

Documentation

The finite factor of the adic local Hilbert family is the established global finite-place Hilbert symbol.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem finitePlaceAdicHilbertPairingFamily_finiteFactor
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (v : HeightOneSpectrum (𝓞 F)) (a b : Fˣ) :
    GlobalHilbertPairingFamily.finiteFactor F
      (finitePlaceAdicHilbertPairingFamily F n hmu) hmu v a b =
        globalFinitePlaceHilbertSymbol F n hnF hmu v a b

Module documentation

Comparison of finite-place Hilbert factors

Declarations

globalFinitePlaceHilbertSymbol_map_eq_local

rootsOfUnity_finiteCompletion_comp

finitePlaceAdicHilbertPairingFamily_finiteFactor