Module

FinitePlaceAdicLocalField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FinitePlaceAdicLocalField

7 declarations indexed from sourceView source ↗

Module documentation

Local-field structure on a finite adic completion

The distinguished integer-valued valuation on a number-field completion provides the valuation relation required by local reciprocity. The valuation relation is passed explicitly, not registered globally.

Imports8

Imported by2

def

finitePlaceCompletionValuativeRel

L36 ↗

ClassFieldTheory.finitePlaceCompletionValuativeRel

Documentation

The valuation relation induced by the canonical discrete valuation on the completion at a finite place.

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

Lean source · statement

def finitePlaceCompletionValuativeRel
    (F : Type u) [Field F] [NumberField F]
    (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F)

theorem

finitePlaceCompletionIsNonarchimedeanLocalField

L45 ↗

ClassFieldTheory.finitePlaceCompletionIsNonarchimedeanLocalField

Documentation

The canonical finite adic completion is a nonarchimedean local field for its distinguished valuation.

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

Lean source · statement

theorem finitePlaceCompletionIsNonarchimedeanLocalField
    (F : Type u) [Field F] [NumberField F]
    (v : HeightOneSpectrum (𝓞 F)) :
    @IsNonarchimedeanLocalField (v.adicCompletion F) inferInstance
      (finitePlaceCompletionValuativeRel F v) inferInstance

instance

finitePlaceCompletionComparisonSourceValuativeRel

L74 ↗

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
section CompletionComparison
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

instance finitePlaceCompletionComparisonSourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion

instance

finitePlaceCompletionComparisonTargetValuativeRel

L78 ↗

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
section CompletionComparison
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceCompletionComparisonSourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v

Lean source · statement

instance finitePlaceCompletionComparisonTargetValuativeRel :
    ValuativeRel (v.adicCompletion F)

theorem

finitePlaceCompletion_semilinearValuationCompatible

L84 ↗

Documentation

The canonical equivalence between the two finite-completion models respects their chosen valuation relations.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
section CompletionComparison
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceCompletionComparisonSourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceCompletionComparisonTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) :=
  ClassFieldTheory.finitePlaceCompletionValuativeRel F v

Lean source · statement

theorem finitePlaceCompletion_semilinearValuationCompatible :
    SemilinearValuationCompatible
      (HeightOneSpectrum.adicAbv F v).Completion
      (v.adicCompletion F)
      (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv

def

finitePlaceAdicHilbertPairingFamily

L113 ↗

ClassFieldTheory.finitePlaceAdicHilbertPairingFamily

Documentation

At each finite place, transport the local Hilbert pairing from the absolute-value completion to Mathlib's adic 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 · statement

def finitePlaceAdicHilbertPairingFamily
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty) :
    GlobalHilbertPairingFamily F n

theorem

finitePlaceAdicHilbertPairingFamily_isLocallyHilbert

L139 ↗

ClassFieldTheory.finitePlaceAdicHilbertPairingFamily_isLocallyHilbert

Documentation

Every finite member of the transported family satisfies the local Steinberg, skew-symmetry, nondegeneracy, and Kummer norm-residue laws.

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_isLocallyHilbert
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty) :
    GlobalHilbertPairingFamily.IsLocallyHilbert F
      (finitePlaceAdicHilbertPairingFamily F n hmu)

Module documentation

Local-field structure on a finite adic completion

Declarations

finitePlaceCompletionValuativeRel

finitePlaceCompletionIsNonarchimedeanLocalField

finitePlaceCompletionComparisonSourceValuativeRel

finitePlaceCompletionComparisonTargetValuativeRel

finitePlaceCompletion_semilinearValuationCompatible

finitePlaceAdicHilbertPairingFamily

finitePlaceAdicHilbertPairingFamily_isLocallyHilbert