Module

FinitePlaceReciprocityUnramifiedUnits.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceReciprocityUnramifiedUnits

7 declarations indexed from sourceView source ↗

Module documentation

Adic integral units detect unramified reciprocity characters

Compatibility of the intrinsic normalized valuation with the distinguished adic valuation identifies its zero kernel with the actual completion's integral-unit subgroup. The roots-of-unity-free local reciprocity criterion therefore applies directly to finite-place idele factors.

Imports2

Imported by3

instance

finitePlaceReciprocityUnitsValuativeRel

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityUnitsValuativeRel

Source context 8 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F)

instance

finitePlaceReciprocityUnitsLocalField

L34 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityUnitsLocalField

Source context 9 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v

Lean source · statement

instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F)

instance

finitePlaceReciprocityUnitsTopology

L37 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityUnitsTopology

Source context 10 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v

Lean source · statement

instance finitePlaceReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ))

instance

finitePlaceReciprocityUnitsDiscrete

L38 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityUnitsDiscrete

Source context 11 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

instance finitePlaceReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ))

instance

finitePlaceReciprocityUnitsH1Module

L40 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityUnitsH1Module

Source context 12 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

instance finitePlaceReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ))
        (G := Field.absoluteGaloisGroup (v.adicCompletion F)))

theorem

finitePlaceValuationMap_eq_zero_iff_integralUnit

L47 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceValuationMap_eq_zero_iff_integralUnit

Documentation

Valuation zero is exactly membership in the actual adic integer-unit subgroup.

Source context 13 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ))
        (G := Field.absoluteGaloisGroup (v.adicCompletion F))) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceValuationMap_eq_zero_iff_integralUnit (a : (v.adicCompletion F)ˣ) :
    valuationMap (v.adicCompletion F) (Additive.ofMul a) = 0 ↔
      a ∈ (v.adicCompletionIntegers F).units

theorem

finitePlaceLocalReciprocityUnitCharacter_integralUnits_iff_unramified

L63 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalReciprocityUnitCharacter_integralUnits_iff_unramified

Documentation

An Artin character kills actual adic integral units exactly when its continuous H¹ class is intrinsically unramified.

Source context 13 commands

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

open scoped NumberField ValuativeRel WithZero Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceReciprocityUnitsValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceReciprocityUnitsLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ))
        (G := Field.absoluteGaloisGroup (v.adicCompletion F))) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceLocalReciprocityUnitCharacter_integralUnits_iff_unramified
    (chi : ContinuousH1ZMod (p := (n : ℕ))
      (G := Field.absoluteGaloisGroup (v.adicCompletion F))) :
    (∀ a : (v.adicCompletion F)ˣ, a ∈ (v.adicCompletionIntegers F).units →
      localReciprocityUnitCharacter (v.adicCompletion F) (n : ℕ) chi a = 1) ↔
      chi ∈ localStandardUnramifiedH1 (v.adicCompletion F) n

Module documentation

Adic integral units detect unramified reciprocity characters

Declarations

finitePlaceReciprocityUnitsValuativeRel

finitePlaceReciprocityUnitsLocalField

finitePlaceReciprocityUnitsTopology

finitePlaceReciprocityUnitsDiscrete

finitePlaceReciprocityUnitsH1Module

finitePlaceValuationMap_eq_zero_iff_integralUnit

finitePlaceLocalReciprocityUnitCharacter_integralUnits_iff_unramified