Module

HilbertFamilyAlgEquiv.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.HilbertFamilyAlgEquiv

5 declarations indexed from sourceView source ↗

Module documentation

Hilbert-pairing families under equivalences of number fields

A number-field equivalence permutes finite places and identifies the corresponding adic completions. The local pairings and their finite factors can therefore be transported without changing their normalization.

Imports3

Imported by2

theorem

primitiveRoots_nonempty_adicCompletion

L30 ↗

ClassFieldTheory.primitiveRoots_nonempty_adicCompletion

Documentation

A primitive root in the number field remains primitive in every finite adic completion.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem primitiveRoots_nonempty_adicCompletion
    (F : Type u) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (v : HeightOneSpectrum (𝓞 F)) :
    (primitiveRoots (n : ℕ) (v.adicCompletion F)).Nonempty

def

globalHilbertPairingFamilyCongr

L43 ↗

ClassFieldTheory.globalHilbertPairingFamilyCongr

Documentation

Transport a global family through the finite-place and adic-completion equivalences induced by an equivalence of number fields.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def globalHilbertPairingFamilyCongr
    {F : Type u} {G : Type v}
    [Field F] [NumberField F] [Field G] [NumberField G]
    (e : F ≃ₐ[ℚ] G) (n : ℕ+)
    (hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
    (BF : GlobalHilbertPairingFamily F n) :
    GlobalHilbertPairingFamily G n

theorem

globalHilbertPairingFamilyCongr_isLocallyHilbert

L57 ↗

ClassFieldTheory.globalHilbertPairingFamilyCongr_isLocallyHilbert

Documentation

Local Hilbert-pairing laws survive transport of the global family.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem globalHilbertPairingFamilyCongr_isLocallyHilbert
    {F : Type u} {G : Type v}
    [Field F] [NumberField F] [Field G] [NumberField G]
    (e : F ≃ₐ[ℚ] G) (n : ℕ+)
    (hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
    (BF : GlobalHilbertPairingFamily F n)
    (hBF : GlobalHilbertPairingFamily.IsLocallyHilbert F BF) :
    GlobalHilbertPairingFamily.IsLocallyHilbert G
      (globalHilbertPairingFamilyCongr e n hmuF BF)

theorem

globalHilbertPairingFamilyCongr_finiteFactor

L76 ↗

ClassFieldTheory.globalHilbertPairingFamilyCongr_finiteFactor

Documentation

At corresponding places, finite factors of the transported family are related by the equivalence of global roots of unity.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem globalHilbertPairingFamilyCongr_finiteFactor
    {F : Type u} {G : Type v}
    [Field F] [NumberField F] [Field G] [NumberField G]
    (e : F ≃ₐ[ℚ] G) (n : ℕ+)
    (hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
    (hmuG : (primitiveRoots (n : ℕ) G).Nonempty)
    (BF : GlobalHilbertPairingFamily F n)
    (W : HeightOneSpectrum (𝓞 G)) (a b : Fˣ) :
    rootsOfUnityEquivOfRingEquiv e.toRingEquiv n hmuF
        (GlobalHilbertPairingFamily.finiteFactor F BF hmuF
          ((finitePlaceCongr e).symm W) a b) =
      GlobalHilbertPairingFamily.finiteFactor G
        (globalHilbertPairingFamilyCongr e n hmuF BF) hmuG W
        (Units.mapEquiv e.toRingEquiv.toMulEquiv a)
        (Units.mapEquiv e.toRingEquiv.toMulEquiv b)

theorem

globalHilbertPairingFamilyCongr_hasFiniteSupport

L113 ↗

ClassFieldTheory.globalHilbertPairingFamilyCongr_hasFiniteSupport

Documentation

Finite support of global evaluations is invariant under an equivalence of number fields.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem globalHilbertPairingFamilyCongr_hasFiniteSupport
    {F : Type u} {G : Type v}
    [Field F] [NumberField F] [Field G] [NumberField G]
    (e : F ≃ₐ[ℚ] G) (n : ℕ+)
    (hmuF : (primitiveRoots (n : ℕ) F).Nonempty)
    (hmuG : (primitiveRoots (n : ℕ) G).Nonempty)
    (BF : GlobalHilbertPairingFamily F n)
    (hBF : GlobalHilbertPairingFamily.HasFiniteSupport F BF hmuF) :
    GlobalHilbertPairingFamily.HasFiniteSupport G
      (globalHilbertPairingFamilyCongr e n hmuF BF) hmuG

Module documentation

Hilbert-pairing families under equivalences of number fields

Declarations

primitiveRoots_nonempty_adicCompletion

globalHilbertPairingFamilyCongr

globalHilbertPairingFamilyCongr_isLocallyHilbert

globalHilbertPairingFamilyCongr_finiteFactor

globalHilbertPairingFamilyCongr_hasFiniteSupport