NYLL
Module

ArithmeticStageH2RadicalLinearMap.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2RadicalLinearMap
8 declarations indexed from sourceView source ↗

Module documentation

Linearity of the actual arithmetic-stage radical obstruction

The local additivity defect agrees on inertia with one actual global character. Global reciprocity annihilates that character on the ideal radical, while unramified local changes do not affect the pairing. Thus the chosen lifts give an additive obstruction. Additivity over the prime field supplies scalar compatibility without any additional choices.

Imports5
Imported by2

Declarations

instance

stageRadicalLinearCanonicalZModAddCommGroup

L34 ↗
ClassFieldTower.Martinet.Shafarevich.stageRadicalLinearCanonicalZModAddCommGroup
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
Lean source · statement
instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ))
instance

stageRadicalLinearTopology

L42 ↗
ClassFieldTower.Martinet.Shafarevich.stageRadicalLinearTopology
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
Lean source · statement
instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ))
instance

stageRadicalLinearDiscrete

L43 ↗
ClassFieldTower.Martinet.Shafarevich.stageRadicalLinearDiscrete
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ))
instance

stageRadicalLinearH1Module

L45 ↗
ClassFieldTower.Martinet.Shafarevich.stageRadicalLinearH1Module
Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance stageRadicalLinearH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))
theorem

arithmeticStageH2RadicalFunctional_add

L50 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalFunctional_add
Documentation

The actual chosen-lift radical obstruction is additive.

Source context 14 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance stageRadicalLinearH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem arithmeticStageH2RadicalFunctional_add (x y : StageH2) :
    arithmeticStageH2RadicalFunctional F n hpOdd U (x + y) =
      arithmeticStageH2RadicalFunctional F n hpOdd U x +
        arithmeticStageH2RadicalFunctional F n hpOdd U y
theorem

arithmeticStageH2RadicalFunctional_zero

L81 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalFunctional_zero
Documentation

The zero class has zero radical obstruction.

Source context 14 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance stageRadicalLinearH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem arithmeticStageH2RadicalFunctional_zero :
    arithmeticStageH2RadicalFunctional F n hpOdd U 0 = 0
def

arithmeticStageH2RadicalLinearMap

L88 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalLinearMap
Documentation

The source-produced linear map from finite-stage H² to the ideal-radical dual.

Source context 14 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance stageRadicalLinearH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
def arithmeticStageH2RadicalLinearMap :
    StageH2 →ₗ[ZMod (n : ℕ)] Module.Dual (ZMod (n : ℕ)) (idealPowerRadicalModP F (n : ℕ))
theorem

arithmeticStageH2RadicalLinearMap_apply

L96 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalLinearMap_apply
Source context 14 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local instance stageRadicalLinearCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance stageRadicalLinearTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance stageRadicalLinearDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance stageRadicalLinearH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem arithmeticStageH2RadicalLinearMap_apply (x : StageH2) :
    arithmeticStageH2RadicalLinearMap F n hpOdd U x =
      arithmeticStageH2RadicalFunctional F n hpOdd U x

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