NYLL
Module

LocalReciprocityUnramifiedValuation.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalReciprocityUnramifiedValuation
8 declarations indexed from sourceView source ↗

Module documentation

Unramified local reciprocity and the valuation line

The roots-of-unity-free reciprocity pairing sends the intrinsic unramified character space onto the valuation line in the dual of actual power classes. The proof evaluates finite Artin reciprocity in the character's own unramified fixed field.

Imports2
Imported by3

Declarations

instance

localReciprocityUnramifiedTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnramifiedTopology
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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ))
instance

localReciprocityUnramifiedDiscreteTopology

L33 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnramifiedDiscreteTopology
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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ))
instance

localReciprocityUnramifiedZModAddCommGroup

L35 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnramifiedZModAddCommGroup
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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ))
instance

localReciprocityUnramifiedH1Module

L37 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnramifiedH1Module
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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
Lean source · statement
instance localReciprocityUnramifiedH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))
theorem

localReciprocityH1PowerClassPairing_mem_valuation_range

L44 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_mem_valuation_range
Documentation

Every unramified character evaluates through normalized valuation. The scalar is the finite character's actual arithmetic Frobenius value.

Source context 11 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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
local instance localReciprocityUnramifiedH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityH1PowerClassPairing_mem_valuation_range
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
    (hchi : chi ∈ localStandardUnramifiedH1 K n) :
    localReciprocityH1PowerClassPairing K (n : ℕ) chi ∈
      LinearMap.range (localPowerClassValuationDualEmbedding K (n : ℕ))
def

localReciprocityPrimeScalar

L94 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityPrimeScalar
Documentation

Evaluation on the normalized inverse uniformizer. For an unramified character this is its arithmetic Frobenius coordinate.

Source context 11 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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
local instance localReciprocityUnramifiedH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityPrimeScalar
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :
    ZMod (n : ℕ)
theorem

localReciprocityH1PowerClassPairing_eq_primeScalar_valuation

L103 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_eq_primeScalar_valuation
Documentation

The unramified reciprocity functional is its normalized Frobenius coordinate times valuation modulo the coefficient prime.

Source context 11 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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
local instance localReciprocityUnramifiedH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityH1PowerClassPairing_eq_primeScalar_valuation
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
    (hchi : chi ∈ localStandardUnramifiedH1 K n) :
    localReciprocityH1PowerClassPairing K (n : ℕ) chi =
      localPowerClassValuationDualEmbedding K (n : ℕ)
        (localReciprocityPrimeScalar K n chi)
theorem

localReciprocityH1PowerClassPairing_unramified_range

L129 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_unramified_range
Documentation

The unramified character space corresponds exactly to the valuation line under local reciprocity, without a roots-of-unity hypothesis.

Source context 11 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 localReciprocityUnramifiedTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localReciprocityUnramifiedDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localReciprocityUnramifiedZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
local instance localReciprocityUnramifiedH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityH1PowerClassPairing_unramified_range :
    LinearMap.range
      ((localReciprocityH1PowerClassPairing K (n : ℕ)).comp
        (localStandardUnramifiedH1 K n).subtype) =
      LinearMap.range (localPowerClassValuationDualEmbedding K (n : ℕ))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.