NYLL
Module

EmptySupportCohomologicalH1KernelDual.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.EmptySupportCohomologicalH1KernelDual
13 declarations indexed from sourceView source ↗

Module documentation

The kernel-dual model of the self-dual cohomological cokernel

Dualizing the global-to-local ramified-character map and taking its cokernel is canonically equivalent to the dual of the kernel of the original map. Thus a subsequent self-dual arithmetic comparison can be reduced to identifying the corresponding primal kernels.

As in EmptySupportCohomologicalH1Cokernel, this is an intermediate self-dual F_p model. The general arithmetic B_∅ uses the Tate-dual coefficient μ_p; connecting the two models remains a separate local Tate/Kummer comparison.

Imports2
Imported by1

Declarations

theorem

dualRange_eq_ker_kernelDualRestriction

L31 ↗
ClassFieldTower.Martinet.Shafarevich.dualRange_eq_ker_kernelDualRestriction
Source context 5 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
Lean source · statement
theorem dualRange_eq_ker_kernelDualRestriction
    {q : ℕ} [Fact q.Prime]
    {V W : Type*}
    [AddCommGroup V] [Module (ZMod q) V]
    [AddCommGroup W] [Module (ZMod q) W]
    (f : V →ₗ[ZMod q] W) :
    LinearMap.range f.dualMap =
      LinearMap.ker (LinearMap.ker f).subtype.dualMap
instance

emptySupportCohomologicalKernelZModAddCommGroup

L46 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalKernelZModAddCommGroup
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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p)
instance

emptySupportCohomologicalKernelH1Module

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

finitePlaceRamifiedCharacterQuotientAddCommGroup

L54 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientAddCommGroup
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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v)
instance

finitePlaceRamifiedCharacterQuotientModule

L59 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceRamifiedCharacterQuotientModule
Source context 10 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
Lean source · statement
instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v)
abbrev

EmptySupportCohomologicalH1Kernel

L65 ↗
ClassFieldTower.Martinet.Shafarevich.EmptySupportCohomologicalH1Kernel
Documentation

Global continuous characters whose restriction at every finite place is unramified.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
abbrev EmptySupportCohomologicalH1Kernel : ModuleCat (ZMod p)
def

emptySupportCohomologicalH1KernelInclusion

L70 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1KernelInclusion
Documentation

Inclusion of the empty-support cohomological kernel into global absolute characters.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
def emptySupportCohomologicalH1KernelInclusion :
    EmptySupportCohomologicalH1Kernel F p →ₗ[ZMod p]
      absoluteContinuousZModCharacterModP F p
theorem

emptySupportCohomologicalH1KernelInclusion_apply

L76 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1KernelInclusion_apply
Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
theorem emptySupportCohomologicalH1KernelInclusion_apply
    (x : EmptySupportCohomologicalH1Kernel F p) :
    emptySupportCohomologicalH1KernelInclusion F p x = x.1
def

emptySupportCohomologicalH1KernelDualRestriction

L82 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1KernelDualRestriction
Documentation

Restriction of global-character functionals to the empty-support cohomological kernel.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
def emptySupportCohomologicalH1KernelDualRestriction :
    Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP F p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (EmptySupportCohomologicalH1Kernel F p)
theorem

emptySupportCohomologicalH1KernelDualRestriction_surjective

L88 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1KernelDualRestriction_surjective
Documentation

Every functional on the cohomological kernel extends to the full global-character space.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
theorem emptySupportCohomologicalH1KernelDualRestriction_surjective :
    Function.Surjective (emptySupportCohomologicalH1KernelDualRestriction F p)
theorem

finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_range

L94 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_range
Documentation

The dual global-to-local range is exactly the kernel of restriction to the cohomological kernel.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
theorem finitePlaceAbsoluteH1RamifiedQuotientFamilyDual_range :
    LinearMap.range (finitePlaceAbsoluteH1RamifiedQuotientFamilyDual F p) =
      LinearMap.ker (emptySupportCohomologicalH1KernelDualRestriction F p)
def

emptySupportCohomologicalH1CokernelEquivKernelDual

L108 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelEquivKernelDual
Documentation

The cohomological empty-support cokernel is canonically the dual of the kernel of the primal global-to-local ramified-character map.

Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
def emptySupportCohomologicalH1CokernelEquivKernelDual :
    EmptySupportCohomologicalH1Cokernel F p ≃ₗ[ZMod p]
      Module.Dual (ZMod p) (EmptySupportCohomologicalH1Kernel F p)
theorem

emptySupportCohomologicalH1CokernelEquivKernelDual_mk

L119 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportCohomologicalH1CokernelEquivKernelDual_mk
Source context 11 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 emptySupportCohomologicalKernelZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance emptySupportCohomologicalKernelH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
local instance finitePlaceRamifiedCharacterQuotientAddCommGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AddCommGroup (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isAddCommGroup
local instance finitePlaceRamifiedCharacterQuotientModule
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Module (ZMod p) (FinitePlaceRamifiedCharacterQuotient F p v) :=
  (FinitePlaceRamifiedCharacterQuotient F p v).isModule
Lean source · statement
theorem emptySupportCohomologicalH1CokernelEquivKernelDual_mk
    (phi : Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP F p)) :
    emptySupportCohomologicalH1CokernelEquivKernelDual F p
        (Submodule.Quotient.mk phi) =
      emptySupportCohomologicalH1KernelDualRestriction F p phi

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