NYLL
Module

EmptySupportUnramifiedArtinKummerCokernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.EmptySupportUnramifiedArtinKummerCokernel
9 declarations indexed from sourceView source ↗

Module documentation

The empty-support unramified Artin--Kummer cokernel

Over a number field containing the coefficient roots of unity (in particular the chosen cyclotomic base), actual local Artin--Kummer pairing against intrinsic unramified H¹ assembles into a global localization map on Kummer power classes. Its dual has the same image as finite-valuation localization, so its cokernel is canonically the dual of the ideal-power radical.

This uses the dual of the unramified local subspace as localization target; it does not identify the different ramified-quotient model EmptySupportCohomologicalH1Cokernel with the arithmetic cokernel.

Imports3
Imported by1

Declarations

instance

emptySupportArtinKummerCanonicalZModAddCommGroup

L37 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportArtinKummerCanonicalZModAddCommGroup
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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
Lean source · statement
instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ))
theorem

finitePlaceUnramifiedArtinKummerLocalizationFamily_ker_eq_valuation

L43 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamily_ker_eq_valuation
Documentation

The kernel of actual unramified Artin--Kummer localization agrees with the kernel of arithmetic finite-valuation localization.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem finitePlaceUnramifiedArtinKummerLocalizationFamily_ker_eq_valuation
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    LinearMap.ker (finitePlaceUnramifiedArtinKummerLocalizationFamily K n hmu) =
      LinearMap.ker (absolutePowerClassFiniteValuationLocalization K (n : ℕ))
theorem

finitePlaceUnramifiedArtinKummerLocalizationFamily_ker

L66 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamily_ker
Documentation

The global Kummer classes annihilating every intrinsic unramified local class are exactly the ideal-power radical.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem finitePlaceUnramifiedArtinKummerLocalizationFamily_ker
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    LinearMap.ker (finitePlaceUnramifiedArtinKummerLocalizationFamily K n hmu) =
      LinearMap.range (idealPowerRadicalToAbsolutePowerClassLinearMap K (n : ℕ))
def

finitePlaceUnramifiedArtinKummerLocalizationFamilyDual

L75 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamilyDual
Documentation

The dual local-to-global map assembled from the actual unramified local Artin--Kummer pairings.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def finitePlaceUnramifiedArtinKummerLocalizationFamilyDual
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Module.Dual (ZMod (n : ℕ))
        (FinitePlaceUnramifiedArtinKummerLocalizationTarget K n) →ₗ[ZMod (n : ℕ)]
      Module.Dual (ZMod (n : ℕ)) (absolutePowerClassModP K (n : ℕ))
theorem

finitePlaceUnramifiedArtinKummerLocalizationFamilyDual_range

L84 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedArtinKummerLocalizationFamilyDual_range
Documentation

The dual of the actual unramified local pairing family has exactly the same image as the arithmetic finite-valuation dual map.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem finitePlaceUnramifiedArtinKummerLocalizationFamilyDual_range
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    LinearMap.range (finitePlaceUnramifiedArtinKummerLocalizationFamilyDual K n hmu) =
      LinearMap.range (finiteValuationLocalizationDual K (n : ℕ))
abbrev

EmptySupportUnramifiedArtinKummerCokernel

L97 ↗
ClassFieldTower.Martinet.Shafarevich.EmptySupportUnramifiedArtinKummerCokernel
Documentation

The empty-support cokernel obtained by dualizing localization against actual unramified local H¹, with global H¹(μ_n) in its Kummer model.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
abbrev EmptySupportUnramifiedArtinKummerCokernel
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) : ModuleCat (ZMod (n : ℕ))
def

emptySupportUnramifiedArtinKummerCokernelEquivKummer

L105 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportUnramifiedArtinKummerCokernelEquivKummer
Documentation

The actual unramified Artin--Kummer cokernel is the arithmetic empty-support Kummer cokernel.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def emptySupportUnramifiedArtinKummerCokernelEquivKummer
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    EmptySupportUnramifiedArtinKummerCokernel K n hmu ≃ₗ[ZMod (n : ℕ)]
      EmptySupportKummerCokernel K (n : ℕ)
def

emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual

L114 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual
Documentation

Hence the unramified Artin--Kummer cokernel is the linear dual of the ideal-power radical.

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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    EmptySupportUnramifiedArtinKummerCokernel K n hmu ≃ₗ[ZMod (n : ℕ)]
      Module.Dual (ZMod (n : ℕ)) (idealPowerRadicalModP K (n : ℕ))
theorem

emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual_mk

L122 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual_mk
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 KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance emptySupportArtinKummerCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual_mk
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (phi : Module.Dual (ZMod (n : ℕ)) (absolutePowerClassModP K (n : ℕ))) :
    emptySupportUnramifiedArtinKummerCokernelEquivIdealPowerRadicalDual K n hmu
        (Submodule.Quotient.mk phi) =
      absolutePowerClassDualRestriction K (n : ℕ) phi

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