NYLL
Module

EmptySupportCohomologicalH1Cokernel.lean

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

Module documentation

Self-dual empty-support cohomological H¹ cokernel

Absolute continuous mod-p characters restrict at every finite place and then pass to the quotient by unramified characters. The empty-support object is the cokernel of the dual of this global-to-local map, not the cokernel of the primal map.

This is the self-dual F_p model. Over a general number field, the Tate-dual coefficient of trivial F_p is μ_p, so identifying this object with the arithmetic B_∅ additionally requires the cyclotomic coefficient comparison and local Tate duality. No such identification is asserted in this file.

Imports2
Imported by2

Declarations

instance

emptySupportCohomologicalH1ZModAddCommGroup

L35 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1ZModAddCommGroup
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 : ℕ) [Fact p.Prime]
Lean source · statement
instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p)
instance

emptySupportCohomologicalH1Module

L38 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1Module
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 : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
def

finitePlaceAbsoluteH1RamifiedQuotient

L44 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotient
Documentation

Restriction at v, followed by passage to the ramified local character quotient.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1RamifiedQuotient
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      FinitePlaceRamifiedCharacterQuotient F p v
theorem

finitePlaceAbsoluteH1RamifiedQuotient_apply

L52 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotient_apply
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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1RamifiedQuotient_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p) :
    finitePlaceAbsoluteH1RamifiedQuotient F p v chi =
      Submodule.Quotient.mk
        (finitePlaceAbsoluteH1DecompositionRestriction F p v chi)
abbrev

FinitePlaceRamifiedCharacterLocalizationTarget

L61 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceRamifiedCharacterLocalizationTarget
Documentation

The dependent product of ramified local character quotients at all finite places.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev FinitePlaceRamifiedCharacterLocalizationTarget
def

finitePlaceAbsoluteH1RamifiedQuotientFamily

L66 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotientFamily
Documentation

The primal global-to-local map into all ramified local character quotients.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1RamifiedQuotientFamily :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      FinitePlaceRamifiedCharacterLocalizationTarget F p
theorem

finitePlaceAbsoluteH1RamifiedQuotientFamily_apply

L72 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotientFamily_apply
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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1RamifiedQuotientFamily_apply
    (chi : absoluteContinuousZModCharacterModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteH1RamifiedQuotientFamily F p chi v =
      finitePlaceAbsoluteH1RamifiedQuotient F p v chi
def

finitePlaceAbsoluteH1RamifiedQuotientFamilyDual

L80 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotientFamilyDual
Documentation

The dual local-to-global map whose cokernel is the cohomological empty-support object.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1RamifiedQuotientFamilyDual :
    Module.Dual (ZMod p) (FinitePlaceRamifiedCharacterLocalizationTarget F p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP F p)
theorem

finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_apply

L86 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_apply
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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_apply
    (phi : Module.Dual (ZMod p) (FinitePlaceRamifiedCharacterLocalizationTarget F p))
    (chi : absoluteContinuousZModCharacterModP F p) :
    finitePlaceAbsoluteH1RamifiedQuotientFamilyDual F p phi chi =
      phi (finitePlaceAbsoluteH1RamifiedQuotientFamily F p chi)
abbrev

EmptySupportCohomologicalH1Cokernel

L95 ↗
ClassFieldTower.Martinet.Shafarevich.EmptySupportCohomologicalH1Cokernel
Documentation

The self-dual cohomological empty-support H¹ cokernel: the cokernel of the dual local-to-global map on trivial mod-p characters.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev EmptySupportCohomologicalH1Cokernel : ModuleCat (ZMod p)
def

emptySupportCohomologicalH1CokernelMap

L101 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelMap
Documentation

The canonical projection onto the cohomological empty-support cokernel.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def emptySupportCohomologicalH1CokernelMap :
    Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP F p) →ₗ[ZMod p]
      EmptySupportCohomologicalH1Cokernel F p
theorem

emptySupportCohomologicalH1CokernelMap_apply

L107 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelMap_apply
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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem emptySupportCohomologicalH1CokernelMap_apply
    (phi : Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP F p)) :
    emptySupportCohomologicalH1CokernelMap F p phi =
      Submodule.Quotient.mk phi
theorem

emptySupportCohomologicalH1CokernelMap_ker

L114 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelMap_ker
Documentation

The kernel of the cokernel projection is the range of the dual local-to-global map.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem emptySupportCohomologicalH1CokernelMap_ker :
    LinearMap.ker (emptySupportCohomologicalH1CokernelMap F p) =
      LinearMap.range (finitePlaceAbsoluteH1RamifiedQuotientFamilyDual F p)
theorem

emptySupportCohomologicalH1CokernelMap_surjective

L120 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelMap_surjective
Documentation

The canonical projection onto the cohomological empty-support cokernel is surjective.

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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance emptySupportCohomologicalH1ZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem emptySupportCohomologicalH1CokernelMap_surjective :
    Function.Surjective (emptySupportCohomologicalH1CokernelMap F p)

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