Module

FinitePlaceRamifiedCharacterQuotient.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceRamifiedCharacterQuotient

6 declarations indexed from sourceView source ↗

Module documentation

Ramified local character quotient

Continuous mod-p characters of the chosen decomposition group are quotiented by the characters trivial on absolute inertia.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceUnramifiedH1

Imported by2

instance

finitePlaceRamifiedCharacterH1Module

L28 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterH1Module

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

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

abbrev

FinitePlaceRamifiedCharacterQuotient

L35 ↗

ClassFieldTower.Martinet.Shafarevich.FinitePlaceRamifiedCharacterQuotient

Documentation

The ramified local character quotient H¹(D_v, F_p) / H¹_unr(D_v, F_p) as a ZMod p-module object.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceRamifiedCharacterH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule

Lean source · statement

abbrev FinitePlaceRamifiedCharacterQuotient
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ModuleCat (ZMod p)

def

finitePlaceRamifiedCharacterQuotientMap

L44 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientMap

Documentation

The canonical quotient map from local decomposition-group characters to their ramified classes.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceRamifiedCharacterH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceRamifiedCharacterQuotientMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) →ₗ[ZMod p]
      FinitePlaceRamifiedCharacterQuotient F p v

theorem

finitePlaceRamifiedCharacterQuotientMap_apply

L51 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientMap_apply

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceRamifiedCharacterH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceRamifiedCharacterQuotientMap_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    finitePlaceRamifiedCharacterQuotientMap F p v chi =
      Submodule.Quotient.mk chi

theorem

finitePlaceRamifiedCharacterQuotientMap_ker

L60 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientMap_ker

Documentation

The kernel of the canonical ramified-character quotient map is exactly unramified continuous H¹.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceRamifiedCharacterH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceRamifiedCharacterQuotientMap_ker
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    LinearMap.ker (finitePlaceRamifiedCharacterQuotientMap F p v) =
      finitePlaceUnramifiedH1 F p v

theorem

finitePlaceRamifiedCharacterQuotientMap_surjective

L67 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientMap_surjective

Documentation

Every ramified local character class has a decomposition-group character representative.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceRamifiedCharacterH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceRamifiedCharacterQuotientMap_surjective
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Function.Surjective (finitePlaceRamifiedCharacterQuotientMap F p v)

Module documentation

Ramified local character quotient

Declarations

finitePlaceRamifiedCharacterH1Module

FinitePlaceRamifiedCharacterQuotient

finitePlaceRamifiedCharacterQuotientMap

finitePlaceRamifiedCharacterQuotientMap_apply

finitePlaceRamifiedCharacterQuotientMap_ker

finitePlaceRamifiedCharacterQuotientMap_surjective