Module

FinitePlaceUnramifiedArtinKummerLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceUnramifiedArtinKummerLocalization

13 declarations indexed from sourceView source ↗

Module documentation

Finite-place unramified Artin--Kummer localization

Global power classes are localized to actual adic completions and paired against intrinsic unramified H¹. The local kernel criterion is proved from Artin--Kummer duality, including at primes above the coefficient prime. The product of these local maps is the primal map for the empty-support unramified Artin--Kummer cokernel.

Imports2

Imported by2

instance

finitePlaceUnramifiedArtinKummerTopology

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerTopology

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]

Lean source · statement

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

instance

finitePlaceUnramifiedArtinKummerDiscreteTopology

L34 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerDiscreteTopology

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

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

instance

finitePlaceUnramifiedArtinKummerModule

L36 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerModule

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _

Lean source · statement

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

instance

finitePlaceUnramifiedArtinKummerValuativeRel

L41 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerValuativeRel

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K)

instance

finitePlaceUnramifiedArtinKummerLocalField

L45 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalField

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v

Lean source · statement

instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K)

theorem

finitePlaceCompletion_primitiveRoots_nonempty

L52 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletion_primitiveRoots_nonempty

Documentation

A global primitive root remains primitive in the actual finite-place adic completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v
omit [Fact ((n : ℕ).Prime)] in

Lean source · statement

theorem finitePlaceCompletion_primitiveRoots_nonempty
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) :
    (primitiveRoots (n : ℕ) (v.adicCompletion K)).Nonempty

def

finitePlaceUnramifiedCompletionH1

L63 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedCompletionH1

Documentation

Intrinsic unramified continuous H¹ of the adic completion at v.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

def finitePlaceUnramifiedCompletionH1
    (v : HeightOneSpectrum (𝓞 K)) :
    Submodule (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ))
        (G := Field.absoluteGaloisGroup (v.adicCompletion K)))

def

finitePlaceUnramifiedArtinKummerLocalization

L72 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalization

Documentation

Localize a global Kummer class and pair it against actual unramified local H¹ using the Artin--Kummer pairing.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

def finitePlaceUnramifiedArtinKummerLocalization
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) :
    absolutePowerClassModP K (n : ℕ) →ₗ[ZMod (n : ℕ)]
      Module.Dual (ZMod (n : ℕ)) (finitePlaceUnramifiedCompletionH1 K n v)

theorem

finitePlaceUnramifiedArtinKummerLocalization_eq_zero_iff

L85 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalization_eq_zero_iff

Documentation

The intrinsic unramified annihilator condition on a localized global class is precisely its zero normalized local valuation.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

theorem finitePlaceUnramifiedArtinKummerLocalization_eq_zero_iff
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K))
    (x : absolutePowerClassModP K (n : ℕ)) :
    finitePlaceUnramifiedArtinKummerLocalization K n hmu v x = 0 ↔
      finitePlaceLocalPowerClassValuation K (n : ℕ) v
        (finitePlacePowerClassLocalization K (n : ℕ) v x) = 0

abbrev

FinitePlaceUnramifiedArtinKummerLocalizationTarget

L98 ↗

ClassFieldTower.Martinet.Shafarevich.FinitePlaceUnramifiedArtinKummerLocalizationTarget

Documentation

The product of the duals of intrinsic unramified local H¹ spaces.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

abbrev FinitePlaceUnramifiedArtinKummerLocalizationTarget

def

finitePlaceUnramifiedArtinKummerLocalizationFamily

L103 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamily

Documentation

The actual unramified Artin--Kummer localization map at all finite places.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

def finitePlaceUnramifiedArtinKummerLocalizationFamily
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    absolutePowerClassModP K (n : ℕ) →ₗ[ZMod (n : ℕ)]
      FinitePlaceUnramifiedArtinKummerLocalizationTarget K n

theorem

finitePlaceUnramifiedArtinKummerLocalizationFamily_apply

L110 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamily_apply

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

theorem finitePlaceUnramifiedArtinKummerLocalizationFamily_apply
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : absolutePowerClassModP K (n : ℕ)) (v : HeightOneSpectrum (𝓞 K)) :
    finitePlaceUnramifiedArtinKummerLocalizationFamily K n hmu x v =
      finitePlaceUnramifiedArtinKummerLocalization K n hmu v x

theorem

finitePlaceUnramifiedArtinKummerLocalizationFamily_eq_zero_iff

L118 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamily_eq_zero_iff

Documentation

Membership in the family kernel is the pointwise unramified annihilator condition at every finite place.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance finitePlaceUnramifiedArtinKummerTopology :
    TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedArtinKummerDiscreteTopology :
    DiscreteTopology (ZMod (n : ℕ)) := discreteTopology_bot _
local instance finitePlaceUnramifiedArtinKummerModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
local instance finitePlaceUnramifiedArtinKummerValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K) :=
  finitePlaceAdicCompletionValuativeRel K v
local instance finitePlaceUnramifiedArtinKummerLocalField
    (v : HeightOneSpectrum (𝓞 K)) : IsNonarchimedeanLocalField (v.adicCompletion K) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField K v

Lean source · statement

theorem finitePlaceUnramifiedArtinKummerLocalizationFamily_eq_zero_iff
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : absolutePowerClassModP K (n : ℕ)) :
    finitePlaceUnramifiedArtinKummerLocalizationFamily K n hmu x = 0 ↔
      ∀ v : HeightOneSpectrum (𝓞 K),
        finitePlaceLocalPowerClassValuation K (n : ℕ) v
          (finitePlacePowerClassLocalization K (n : ℕ) v x) = 0

Module documentation

Finite-place unramified Artin--Kummer localization

Declarations