Module

ArithmeticStageH2RadicalFunctional.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2RadicalFunctional

11 declarations indexed from sourceView source ↗

Module documentation

The actual radical functional of an arithmetic-stage degree-two class

Finite-stage mod-p H² is a finite set. The union of the ramification supports of all its chosen global lifts is consequently one fixed finite set. On this set the actual local lift differences, transported to the adic absolute Galois groups, pair with localized global power classes. Restriction to the ideal-power radical gives a concrete functional for every stage class. Its linearity and kernel are proved in the subsequent comparison leaves.

Imports5

Imported by3

instance

arithmeticRadicalFunctionalH2Finite

L41 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalFunctionalH2Finite

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2

Lean source · statement

instance arithmeticRadicalFunctionalH2Finite : Finite StageH2

instance

arithmeticRadicalFunctionalTopology

L46 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalFunctionalTopology

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))

Lean source · statement

instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ))

instance

arithmeticRadicalFunctionalDiscreteTopology

L47 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalFunctionalDiscreteTopology

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ))

instance

arithmeticRadicalFunctionalH1Module

L49 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalFunctionalH1Module

Source context 14 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

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

theorem

arithmeticStageH2RamifiedPlaces_family_finite

L54 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RamifiedPlaces_family_finite

Documentation

All chosen stage lifts ramify inside one finite set, since the stage H² itself is finite.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem arithmeticStageH2RamifiedPlaces_family_finite :
    (⋃ x : StageH2, (arithmeticStageH2GlobalRamifiedPlaces F n hpOdd U x :
      Set (HeightOneSpectrum (𝓞 F)))).Finite

def

arithmeticStageH2UniformRamifiedPlaces

L60 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2UniformRamifiedPlaces

Documentation

A single finite support valid for the chosen global lift of every stage class.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

def arithmeticStageH2UniformRamifiedPlaces : Finset (HeightOneSpectrum (𝓞 F))

theorem

arithmeticStageH2GlobalRamifiedPlaces_subset_uniform

L64 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalRamifiedPlaces_subset_uniform

Documentation

Each individual chosen lift's ramified set lies in the common support.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem arithmeticStageH2GlobalRamifiedPlaces_subset_uniform (x : StageH2) :
    arithmeticStageH2GlobalRamifiedPlaces F n hpOdd U x ⊆
      arithmeticStageH2UniformRamifiedPlaces F n hpOdd U

theorem

arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem_uniform

L72 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem_uniform

Documentation

Every chosen stage lift is unramified outside the fixed support.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem arithmeticStageH2GlobalLiftAtFinitePlace_inertia_le_ker_of_not_mem_uniform
    (x : StageH2) (v : HeightOneSpectrum (𝓞 F))
    (hv : v ∉ arithmeticStageH2UniformRamifiedPlaces F n hpOdd U) :
    finitePlaceAbsoluteInertiaSubgroup F v ≤
      (arithmeticStageH2GlobalLiftAtFinitePlace F n hpOdd U x v).toMonoidHom.ker

def

arithmeticStageH2AdicLocalDifference

L81 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AdicLocalDifference

Documentation

The actual local difference character, in the adic absolute Galois model.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

def arithmeticStageH2AdicLocalDifference (x : StageH2) (v : HeightOneSpectrum (𝓞 F)) :
    ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup (v.adicCompletion F))

def

arithmeticStageH2PowerClassFunctional

L87 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2PowerClassFunctional

Documentation

The finite local reciprocity functional on global power classes.

Source context 15 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageQuotient" => MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ) ⧸
  (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageH2" => continuousCohomologyZModPLifted (n : ℕ) StageQuotient 2
local instance arithmeticRadicalFunctionalH2Finite : Finite StageH2 := by
  let : FiniteDimensional (ZMod (n : ℕ)) StageH2 :=
    finiteDimensional_degree_two_of_finite (p := (n : ℕ)) (inferInstance : Finite StageQuotient)
  exact Module.finite_of_finite (ZMod (n : ℕ))
local instance arithmeticRadicalFunctionalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalFunctionalDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance arithmeticRadicalFunctionalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

def arithmeticStageH2PowerClassFunctional (x : StageH2) :
    Module.Dual (ZMod (n : ℕ)) (absolutePowerClassModP F (n : ℕ))

def