Module

LocalUnramifiedArtinKummerAnnihilator.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalUnramifiedArtinKummerAnnihilator

8 declarations indexed from sourceView source ↗

Module documentation

The annihilator of intrinsic unramified local H¹

The actual Artin--Kummer pairing, restricted to unramified classes in its first argument, vanishes on precisely the valuation-zero Kummer classes. This is the local kernel statement needed to assemble the empty-support unramified local-to-global dual map.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalUnramifiedArtinKummerRange

Imported by2

instance

localUnramifiedArtinKummerAnnihilatorTopology

L28 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerAnnihilatorTopology

Source context 6 commands

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

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

Lean source · statement

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

instance

localUnramifiedArtinKummerAnnihilatorDiscreteTopology

L30 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerAnnihilatorDiscreteTopology

Source context 7 commands

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

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

Lean source · statement

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

instance

localUnramifiedArtinKummerAnnihilatorModule

L32 ↗

ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerAnnihilatorModule

Source context 8 commands

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

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

Lean source · statement

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

def

localArtinKummerUnramifiedDualRestriction

L39 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerUnramifiedDualRestriction

Documentation

Pair a local class against intrinsic unramified H¹ using the actual local Artin--Kummer pairing.

Source context 9 commands

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

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

Lean source · statement

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

theorem

localArtinKummerUnramifiedDualRestriction_apply

L47 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerUnramifiedDualRestriction_apply

Source context 9 commands

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

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

Lean source · statement

theorem localArtinKummerUnramifiedDualRestriction_apply
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
    (u : localStandardUnramifiedH1 K n) :
    localArtinKummerUnramifiedDualRestriction K n hmu chi u =
      localArtinKummerH1DualEmbedding K n hmu u.1 chi

theorem

localArtinKummerUnramifiedDualRestriction_eq_zero_iff

L56 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerUnramifiedDualRestriction_eq_zero_iff

Documentation

Annihilating every unramified local class is equivalent to having zero Kummer valuation.

Source context 9 commands

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

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

Lean source · statement

theorem localArtinKummerUnramifiedDualRestriction_eq_zero_iff
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :
    localArtinKummerUnramifiedDualRestriction K n hmu chi = 0 ↔
      localStandardH1Valuation K n hmu chi = 0

theorem

localArtinKummerUnramifiedDualRestriction_ker

L86 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerUnramifiedDualRestriction_ker

Documentation

The unramified Artin--Kummer annihilator is the valuation-zero subspace.

Source context 9 commands

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

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

Lean source · statement

theorem localArtinKummerUnramifiedDualRestriction_ker
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    LinearMap.ker (localArtinKummerUnramifiedDualRestriction K n hmu) =
      LinearMap.ker (localStandardH1Valuation K n hmu)

theorem

localArtinKummerUnramifiedDualRestriction_kummer_eq_zero_iff

L95 ↗

ClassFieldTower.Martinet.Shafarevich.localArtinKummerUnramifiedDualRestriction_kummer_eq_zero_iff

Documentation

Under Kummer theory, the local unramified annihilator condition is exactly zero normalized valuation on power classes.

Source context 9 commands

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

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

Lean source · statement

theorem localArtinKummerUnramifiedDualRestriction_kummer_eq_zero_iff
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : absolutePowerClassModP K (n : ℕ)) :
    localArtinKummerUnramifiedDualRestriction K n hmu
        (absoluteKummerContinuousH1LinearEquiv K (n : ℕ) hmu x) = 0 ↔
      localPowerClassValuation K (n : ℕ) x = 0

Module documentation

The annihilator of intrinsic unramified local H¹

Declarations