Module

LocalReciprocityUnramifiedUnits.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalReciprocityUnramifiedUnits

6 declarations indexed from sourceView source ↗

Module documentation

Integral-unit triviality detects unramified local characters

The actual unit/uniformizer decomposition shows that an Artin character trivial on all integer units has a valuation-line power-class functional. The roots-of-unity-free reciprocity range theorem and pairing injectivity then identify it with the intrinsic unramified H¹ submodule. Neither characteristic zero nor a primitive root in the local field is assumed.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalReciprocityUnramifiedValuation

Imported by2

instance

localReciprocityUnitsTopology

L32 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitsTopology

Source context 7 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]

Lean source · statement

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

instance

localReciprocityUnitsDiscrete

L33 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitsDiscrete

Source context 8 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

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

instance

localReciprocityUnitsH1Module

L35 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitsH1Module

Source context 9 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

instance localReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))

theorem

localReciprocityH1PowerClassPairing_eq_valuation_of_integerUnits

L42 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_eq_valuation_of_integerUnits

Documentation

An Artin character trivial on integer units is its normalized uniformizer coordinate times valuation.

Source context 10 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule

Lean source · statement

theorem localReciprocityH1PowerClassPairing_eq_valuation_of_integerUnits
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
    (hchi : ∀ u : 𝒪[K]ˣ,
      localReciprocityUnitCharacter K (n : ℕ) chi (integerUnitsToFieldUnits K u) = 1) :
    localReciprocityH1PowerClassPairing K (n : ℕ) chi =
      localPowerClassValuationDualEmbedding K (n : ℕ) (localReciprocityPrimeScalar K n chi)

theorem

localReciprocityUnitCharacter_integerUnits_iff_unramified

L97 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitCharacter_integerUnits_iff_unramified

Documentation

A local Artin character kills every integer unit exactly when its continuous H¹ class is intrinsically unramified.

Source context 10 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule

Lean source · statement

theorem localReciprocityUnitCharacter_integerUnits_iff_unramified
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :
    (∀ u : 𝒪[K]ˣ,
      localReciprocityUnitCharacter K (n : ℕ) chi (integerUnitsToFieldUnits K u) = 1) ↔
      chi ∈ localStandardUnramifiedH1 K n

theorem

localReciprocityUnitCharacter_valuationZero_iff_unramified

L128 ↗

ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitCharacter_valuationZero_iff_unramified

Documentation

Equivalent valuation-zero formulation, convenient for comparing actual integral-unit subgroups under completion normalizations.

Source context 10 commands

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

open scoped Topology ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localReciprocityUnitsTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnitsDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnitsH1Module :
    Module (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule

Lean source · statement

theorem localReciprocityUnitCharacter_valuationZero_iff_unramified
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :
    (∀ a : Kˣ, valuationMap K (Additive.ofMul a) = 0 →
      localReciprocityUnitCharacter K (n : ℕ) chi a = 1) ↔
      chi ∈ localStandardUnramifiedH1 K n

Module documentation

Integral-unit triviality detects unramified local characters

Declarations

localReciprocityUnitsTopology

localReciprocityUnitsDiscrete

localReciprocityUnitsH1Module

localReciprocityH1PowerClassPairing_eq_valuation_of_integerUnits

localReciprocityUnitCharacter_integerUnits_iff_unramified

localReciprocityUnitCharacter_valuationZero_iff_unramified