Module

ArithmeticStageH2RadicalKernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2RadicalKernel

3 declarations indexed from sourceView source ↗

Module documentation

The actual radical functional detects stage inflation

A zero radical functional supplies a global character agreeing with the chosen lift's inertia defects. Correcting the lift by this character kills every finite inertia group. The actual maximal-unramified factor therefore lifts the stage quotient, forcing its inflated degree-two class to vanish.

Imports4

Imported by2

instance

arithmeticRadicalKernelTopology

L36 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalKernelTopology

Source context 10 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 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 arithmeticRadicalKernelTopology : TopologicalSpace (ZMod (n : ℕ))

instance

arithmeticRadicalKernelDiscrete

L37 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticRadicalKernelDiscrete

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 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 arithmeticRadicalKernelTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

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

theorem

arithmeticStageH2RadicalFunctional_eq_zero_imp_inflation_eq_zero

L42 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalFunctional_eq_zero_imp_inflation_eq_zero

Documentation

Vanishing of the actual ideal-radical functional forces the stage class to vanish in the maximal everywhere-unramified pro-p group.

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 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 arithmeticRadicalKernelTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance arithmeticRadicalKernelDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

theorem arithmeticStageH2RadicalFunctional_eq_zero_imp_inflation_eq_zero
    (x : StageH2) (hx : arithmeticStageH2RadicalFunctional F n hpOdd U x = 0) :
    (continuousCohomologyZModPMapLifted (n : ℕ)
      (quotientProjection (U : Subgroup
        (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))) 2).hom x = 0

Module documentation

The actual radical functional detects stage inflation

Declarations

arithmeticRadicalKernelTopology

arithmeticRadicalKernelDiscrete

arithmeticStageH2RadicalFunctional_eq_zero_imp_inflation_eq_zero