Module

LocalValuationKummerDual.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.LocalValuationKummerDual

11 declarations indexed from sourceView source ↗

Module documentation

Finite-place valuation defects and local Kummer duality

At a finite place of a number field, normalized valuation modulo p descends to a surjective linear map from local p-power classes to ZMod p. Its dual embeds the one-dimensional valuation-defect space into the dual of the local power-class module.

The resulting dual map is the local object that must eventually be compared with the coordinate maps in finiteValuationLocalizationDual and, through local Hilbert duality, with local Kummer classes.

Imports4

Imported by5

def

finitePlaceAdicCompletionValuativeRel

L38 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicCompletionValuativeRel

Documentation

The valuation relation induced by the distinguished integer-valued valuation on an adic completion.

Source context 6 commands

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

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

Lean source · statement

def finitePlaceAdicCompletionValuativeRel
    (v : HeightOneSpectrum (𝓞 K)) : ValuativeRel (v.adicCompletion K)

theorem

finitePlaceAdicCompletionIsNonarchimedeanLocalField

L45 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicCompletionIsNonarchimedeanLocalField

Documentation

A number-field completion, equipped with its distinguished adic valuation, is a nonarchimedean local field.

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (v : HeightOneSpectrum (𝓞 K)) :
    @IsNonarchimedeanLocalField (v.adicCompletion K) inferInstance
      (finitePlaceAdicCompletionValuativeRel K v) inferInstance

abbrev

FinitePlaceLocalPowerClassModP

L66 ↗

ClassFieldTower.Martinet.Shafarevich.FinitePlaceLocalPowerClassModP

Documentation

Local p-power classes at the finite place v, with their canonical ZMod p-module structure.

Source context 6 commands

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

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

Lean source · statement

abbrev FinitePlaceLocalPowerClassModP
    (v : HeightOneSpectrum (𝓞 K)) : ModuleCat (ZMod p)

def

finitePlaceLocalPowerClassValuationMonoidHom

L71 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuationMonoidHom

Documentation

Normalized valuation modulo p, descended to local p-power classes.

Source context 6 commands

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

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

Lean source · statement

def finitePlaceLocalPowerClassValuationMonoidHom
    (v : HeightOneSpectrum (𝓞 K)) :
    ((v.adicCompletion K)ˣ ⧸
        (powMonoidHom p : (v.adicCompletion K)ˣ →* (v.adicCompletion K)ˣ).range) →*
      Multiplicative (ZMod p)

theorem

finitePlaceLocalPowerClassValuationMonoidHom_surjective

L92 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuationMonoidHom_surjective

Documentation

The finite-place local valuation on power classes is surjective.

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceLocalPowerClassValuationMonoidHom_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    Function.Surjective
      (finitePlaceLocalPowerClassValuationMonoidHom K p v)

def

finitePlaceLocalPowerClassValuation

L108 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuation

Documentation

Normalized valuation modulo p as a linear map on local power classes.

Source context 6 commands

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

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

Lean source · statement

def finitePlaceLocalPowerClassValuation
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceLocalPowerClassModP K p v →ₗ[ZMod p] ZMod p

theorem

finitePlaceLocalPowerClassValuation_apply

L142 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuation_apply

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceLocalPowerClassValuation_apply
    (v : HeightOneSpectrum (𝓞 K))
    (x : FinitePlaceLocalPowerClassModP K p v) :
    Multiplicative.ofAdd (finitePlaceLocalPowerClassValuation K p v x) =
      finitePlaceLocalPowerClassValuationMonoidHom K p v (Additive.toMul x)

theorem

finitePlaceLocalPowerClassValuation_surjective

L150 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuation_surjective

Documentation

The linear local valuation on power classes is surjective.

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceLocalPowerClassValuation_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    Function.Surjective (finitePlaceLocalPowerClassValuation K p v)

def

finitePlaceValuationDefectDualEmbedding

L162 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceValuationDefectDualEmbedding

Documentation

The one-dimensional valuation-defect space inside the dual of local power classes.

Source context 6 commands

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

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

Lean source · statement

def finitePlaceValuationDefectDualEmbedding
    (v : HeightOneSpectrum (𝓞 K)) :
    ZMod p →ₗ[ZMod p]
      Module.Dual (ZMod p) (FinitePlaceLocalPowerClassModP K p v)

theorem

finitePlaceValuationDefectDualEmbedding_apply

L170 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceValuationDefectDualEmbedding_apply

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceValuationDefectDualEmbedding_apply
    (v : HeightOneSpectrum (𝓞 K))
    (a : ZMod p) (x : FinitePlaceLocalPowerClassModP K p v) :
    finitePlaceValuationDefectDualEmbedding K p v a x =
      a * finitePlaceLocalPowerClassValuation K p v x

theorem

finitePlaceValuationDefectDualEmbedding_injective

L178 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceValuationDefectDualEmbedding_injective

Documentation

The dualized valuation-defect map is injective.

Source context 6 commands

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

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

Lean source · statement

theorem finitePlaceValuationDefectDualEmbedding_injective
    (v : HeightOneSpectrum (𝓞 K)) :
    Function.Injective (finitePlaceValuationDefectDualEmbedding K p v)

Module documentation

Finite-place valuation defects and local Kummer duality

Declarations