Module

LocalArtinKummerH1Duality.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalArtinKummerH1Duality

8 declarations indexed from sourceView source ↗

Module documentation

Local Artin--Kummer duality on continuous H¹

The maximal local Kummer extension and the local Artin map give the local Hilbert pairing on power classes. This file transports that pairing across the absolute Kummer equivalence to continuous additive ZMod p characters.

This is an Artin--Kummer duality statement. It does not identify the pairing with a cup product followed by a local invariant map.

Imports2

Imported by3

instance

localArtinKummerH1Topology

L32 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1Topology

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]

Lean source · statement

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

instance

localArtinKummerH1DiscreteTopology

L34 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DiscreteTopology

Source context 8 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

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

instance

localArtinKummerH1Module

L37 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1Module

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))

def

localArtinKummerH1DualEmbedding

L44 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding

Documentation

The maximal-local-Artin Kummer pairing, transported to continuous H¹ in both variables.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def localArtinKummerH1DualEmbedding
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup L) →ₗ[ZMod (n : ℕ)]
      Module.Dual (ZMod (n : ℕ))
        (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup L))

theorem

localArtinKummerH1DualEmbedding_apply

L55 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_apply

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem localArtinKummerH1DualEmbedding_apply
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty)
    (chi psi : ContinuousH1ZMod
      (p := (n : ℕ)) (G := Field.absoluteGaloisGroup L)) :
    localArtinKummerH1DualEmbedding L n hmu chi psi =
      localHilbertDualEmbedding L n hmu
        ((absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu).symm chi)
        ((absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu).symm psi)

theorem

localArtinKummerH1DualEmbedding_kummer

L68 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_kummer

Documentation

On Kummer classes, the transported pairing is the original local Hilbert pairing on power classes.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem localArtinKummerH1DualEmbedding_kummer
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty)
    (a b : absolutePowerClassModP L (n : ℕ)) :
    localArtinKummerH1DualEmbedding L n hmu
        (absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu a)
        (absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu b) =
      localHilbertDualEmbedding L n hmu a b

theorem

localArtinKummerH1DualEmbedding_mk

L81 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_mk

Documentation

Representative formula: the Artin--Kummer H¹ pairing is the local Hilbert symbol, written additively using the chosen primitive root.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem localArtinKummerH1DualEmbedding_mk
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) (a b : Lˣ) :
    localArtinKummerH1DualEmbedding L n hmu
        (absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range a)))
        (absoluteKummerContinuousH1LinearEquiv L (n : ℕ) hmu
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range b))) =
      ((localNthRootsEquivMultiplicativeZMod L n hmu)
        (localHilbertSymbol L n
          (Nat.cast_ne_zero.mpr n.ne_zero) hmu a b)).toAdd

theorem

localArtinKummerH1DualEmbedding_injective

L117 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_injective

Documentation

Nondegeneracy of the local Hilbert pairing makes the transported Artin--Kummer map injective.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open ClassFieldTower.ProP
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localArtinKummerH1Topology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localArtinKummerH1DiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localArtinKummerH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem localArtinKummerH1DualEmbedding_injective
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    Function.Injective (localArtinKummerH1DualEmbedding L n hmu)

Module documentation

Local Artin--Kummer duality on continuous H¹

Declarations