NYLL
Module

LocalReciprocityCharacterPairing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalReciprocityCharacterPairing
13 declarations indexed from sourceView source ↗

Module documentation

Local reciprocity pairing without coefficient roots of unity

Evaluate a continuous mod-p Galois character on the absolute local Artin map. The resulting functional descends to actual multiplicative power classes. Dense image of the Artin map makes the pairing faithful in the character variable. No primitive root or Kummer trivialization is used.

Imports9
Imported by5

Declarations

instance

localReciprocityPairingCanonicalZModAddCommGroup

L38 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityPairingCanonicalZModAddCommGroup
Source context 6 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

localReciprocityCharacterTopology

L41 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterTopology
Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p)
instance

localReciprocityCharacterDiscreteTopology

L42 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterDiscreteTopology
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p)
instance

localReciprocityCharacterH1Module

L44 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterH1Module
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
def

localReciprocityAbelianCharacter

L49 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityAbelianCharacter
Documentation

A continuous character descends through the closed commutator subgroup.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityAbelianCharacter
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    Field.absoluteGaloisGroupAbelianization K →ₜ* Multiplicative (ZMod p)
theorem

localReciprocityAbelianCharacter_mk

L60 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityAbelianCharacter_mk
Source context 11 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem localReciprocityAbelianCharacter_mk
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
    (sigma : Field.absoluteGaloisGroup K) :
    localReciprocityAbelianCharacter K p chi (QuotientGroup.mk sigma) =
      Multiplicative.ofAdd (chi (Additive.ofMul sigma))
def

localReciprocityUnitCharacter

L67 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitCharacter
Documentation

Evaluate a local Galois character on the absolute Artin map.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityUnitCharacter
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    Kˣ →ₜ* Multiplicative (ZMod p)
def

localReciprocityPowerClassCharacter

L73 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityPowerClassCharacter
Documentation

The Artin evaluation descends to the quotient by actual p-th powers.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityPowerClassCharacter
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    (Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) →* Multiplicative (ZMod p)
def

localReciprocityPowerClassFunctional

L84 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityPowerClassFunctional
Documentation

The power-class functional attached to a continuous local character.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityPowerClassFunctional
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    Module.Dual (ZMod p) (absolutePowerClassModP K p)
theorem

localReciprocityPowerClassFunctional_mk

L94 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityPowerClassFunctional_mk
Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityPowerClassFunctional_mk
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) (a : Kˣ) :
    localReciprocityPowerClassFunctional K p chi
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)) =
      (localReciprocityAbelianCharacter K p chi (absoluteLocalArtinMap K a)).toAdd
def

localReciprocityH1PowerClassPairing

L102 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing
Documentation

The local reciprocity pairing, linear in the continuous H¹ character and in the actual power class; no roots-of-unity hypothesis is needed.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
def localReciprocityH1PowerClassPairing :
    ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K) →ₗ[ZMod p]
      Module.Dual (ZMod p) (absolutePowerClassModP K p)
theorem

localReciprocityH1PowerClassPairing_mk

L135 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_mk
Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityH1PowerClassPairing_mk
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) (a : Kˣ) :
    localReciprocityH1PowerClassPairing K p chi
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)) =
      (localReciprocityAbelianCharacter K p chi (absoluteLocalArtinMap K a)).toAdd
theorem

localReciprocityH1PowerClassPairing_injective

L142 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityH1PowerClassPairing_injective
Documentation

Dense Artin image detects every continuous local mod-p character.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityPairingCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance localReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityCharacterH1Module :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :=
  continuousH1ZModModule
Lean source · statement
theorem localReciprocityH1PowerClassPairing_injective :
    Function.Injective (localReciprocityH1PowerClassPairing K p)

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