NYLL
Module

EmptySupportKummerCokernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.EmptySupportKummerCokernel
14 declarations indexed from sourceView source ↗

Module documentation

The empty-support Kummer cokernel

The finite valuations give a concrete localization map from global power classes to the product of their valuation defects. Its kernel is exactly the ideal-power radical. Dualizing the localization map therefore gives an actual presentation of the empty-support Kummer cokernel, and the first isomorphism theorem identifies that cokernel with the dual of the ideal-power radical.

This is the algebraic Kummer model of B_∅. Identifying its localization-dual map with the cohomological map assembled from local unramified H¹ still requires local Tate duality and global-to-local restriction maps.

Imports2
Imported by10

Declarations

abbrev

FiniteValuationDefect

L36 ↗
ClassFieldTower.Martinet.Shafarevich.FiniteValuationDefect
Documentation

The multiplicative product of the mod-p finite-valuation defects.

Source context 6 commands

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

open scoped NumberField
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 FiniteValuationDefect
theorem

finiteValuationDefect_pow_eq_one

L41 ↗
ClassFieldTower.Martinet.Shafarevich.finiteValuationDefect_pow_eq_one
Documentation

Every product of mod-p valuation defects has exponent dividing p.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
omit [NumberField K] in
Lean source · statement
theorem finiteValuationDefect_pow_eq_one
    (x : FiniteValuationDefect K p) :
    x ^ p = 1
def

FiniteValuationDefectModP

L50 ↗
ClassFieldTower.Martinet.Shafarevich.FiniteValuationDefectModP
Documentation

The product of the mod-p finite-valuation defects as a ZMod p-module.

Source context 6 commands

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

open scoped NumberField
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 FiniteValuationDefectModP : ModuleCat (ZMod p)
def

absolutePowerClassFiniteValuationLocalizationMonoidHom

L57 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassFiniteValuationLocalizationMonoidHom
Documentation

Multiplicative localization of a global power class at every finite valuation.

Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassFiniteValuationLocalizationMonoidHom :
    (Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) →*
      FiniteValuationDefect K p
def

absolutePowerClassFiniteValuationLocalization

L63 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassFiniteValuationLocalization
Documentation

Localization of a global power class at every finite valuation.

Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassFiniteValuationLocalization :
    absolutePowerClassModP K p →ₗ[ZMod p] FiniteValuationDefectModP K p
theorem

absolutePowerClassFiniteValuationLocalization_apply

L76 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassFiniteValuationLocalization_apply
Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassFiniteValuationLocalization_apply
    (x : absolutePowerClassModP K p)
    (v : HeightOneSpectrum (𝓞 K)) :
    Additive.toMul (absolutePowerClassFiniteValuationLocalization K p x) v =
      v.valuationOfNeZeroMod p (Additive.toMul x)
theorem

absolutePowerClassFiniteValuationLocalization_ker

L84 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassFiniteValuationLocalization_ker
Documentation

The kernel of finite-valuation localization is precisely the embedded ideal-power radical.

Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassFiniteValuationLocalization_ker :
    LinearMap.ker (absolutePowerClassFiniteValuationLocalization K p) =
      LinearMap.range (idealPowerRadicalToAbsolutePowerClassLinearMap K p)
def

finiteValuationLocalizationDual

L133 ↗
ClassFieldTower.Martinet.Shafarevich.finiteValuationLocalizationDual
Documentation

The dual of finite-valuation localization. Its image consists of global Kummer functionals generated by the finite-valuation defects.

Source context 6 commands

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

open scoped NumberField
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 finiteValuationLocalizationDual :
    Module.Dual (ZMod p) (FiniteValuationDefectModP K p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (absolutePowerClassModP K p)
def

absolutePowerClassDualRestriction

L139 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassDualRestriction
Documentation

Restriction of global Kummer functionals to the ideal-power radical.

Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassDualRestriction :
    Module.Dual (ZMod p) (absolutePowerClassModP K p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP K p)
theorem

absolutePowerClassDualRestriction_surjective

L145 ↗
ClassFieldTower.Martinet.Shafarevich.absolutePowerClassDualRestriction_surjective
Documentation

Every functional on the ideal-power radical extends to the full power-class module.

Source context 6 commands

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

open scoped NumberField
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 absolutePowerClassDualRestriction_surjective :
    Function.Surjective (absolutePowerClassDualRestriction K p)
theorem

finiteValuationLocalizationDual_range

L152 ↗
ClassFieldTower.Martinet.Shafarevich.finiteValuationLocalizationDual_range
Documentation

The image of dualized finite-valuation localization is exactly the kernel of restriction to the ideal-power radical.

Source context 6 commands

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

open scoped NumberField
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 finiteValuationLocalizationDual_range :
    LinearMap.range (finiteValuationLocalizationDual K p) =
      LinearMap.ker (absolutePowerClassDualRestriction K p)
abbrev

EmptySupportKummerCokernel

L169 ↗
ClassFieldTower.Martinet.Shafarevich.EmptySupportKummerCokernel
Documentation

The cokernel of dualized finite-valuation localization: the algebraic Kummer model of B_∅.

Source context 6 commands

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

open scoped NumberField
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 EmptySupportKummerCokernel : ModuleCat (ZMod p)
def

emptySupportKummerCokernelEquivIdealPowerRadicalDual

L175 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportKummerCokernelEquivIdealPowerRadicalDual
Documentation

The empty-support Kummer cokernel is the dual of the ideal-power radical.

Source context 6 commands

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

open scoped NumberField
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 emptySupportKummerCokernelEquivIdealPowerRadicalDual :
    EmptySupportKummerCokernel K p ≃ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP K p)
theorem

emptySupportKummerCokernelEquivIdealPowerRadicalDual_mk

L186 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportKummerCokernelEquivIdealPowerRadicalDual_mk
Source context 6 commands

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

open scoped NumberField
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 emptySupportKummerCokernelEquivIdealPowerRadicalDual_mk
    (φ : Module.Dual (ZMod p) (absolutePowerClassModP K p)) :
    emptySupportKummerCokernelEquivIdealPowerRadicalDual K p
        (Submodule.Quotient.mk φ) =
      absolutePowerClassDualRestriction K p φ

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