Module

ArithmeticStageAbsoluteH2Vanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageAbsoluteH2Vanishing

4 declarations indexed from sourceView source ↗

Module documentation

Absolute degree-two vanishing at the unramified arithmetic stage

Over a base containing mu_p, the actual finite unramified stage supplies a field-unit primitive through the supported-idele construction. Hilbert 90 and the root correction turn this into an actual continuous lift of the absolute Galois restriction to the cocycle extension.

Consequently every continuous degree-two class of the finite arithmetic stage inflates to zero on the absolute Galois group. The statements have only the original arithmetic stage and primitive-root data as inputs. A single local compactness proof unfolds the public absolute-group wrapper; no data-bearing or global instance is introduced.

Imports2

Imported by2

def

openNormalArithmeticStageFiniteGaloisField

L37 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStageFiniteGaloisField

Documentation

The actual arithmetic stage, repackaged as a finite Galois intermediate field of the same chosen algebraic closure.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))

Lean source · full declaration

def openNormalArithmeticStageFiniteGaloisField :
    FiniteGaloisIntermediateField F (AlgebraicClosure F) where
  toIntermediateField := (openNormalArithmeticStage F (n : ℕ) hpOdd U).field
  finiteDimensional := (openNormalArithmeticStage F (n : ℕ) hpOdd U).finiteDimensional
  isGalois := (openNormalArithmeticStage F (n : ℕ) hpOdd U).isGalois

def

openNormalArithmeticStageAbsoluteRestriction

L47 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStageAbsoluteRestriction

Documentation

Actual absolute-Galois restriction to the arithmetic stage.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)

Lean source · statement

def openNormalArithmeticStageAbsoluteRestriction :
    Field.absoluteGaloisGroup F →ₜ* Gal(StageField/F)

theorem

openNormalArithmeticStage_exists_absoluteLift

L54 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_exists_absoluteLift

Documentation

Every central mod-p cocycle extension at the unramified arithmetic stage admits an actual continuous absolute-Galois lift.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)

Lean source · statement

theorem openNormalArithmeticStage_exists_absoluteLift
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (z : Cohomology.trivialZModPCocyclesLifted (n : ℕ) Gal(StageField/F) 2) :
    ∃ s : Field.absoluteGaloisGroup F →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s =
        openNormalArithmeticStageAbsoluteRestriction F n hpOdd U

theorem

openNormalArithmeticStage_absoluteH2Map_eq_zero

L68 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_absoluteH2Map_eq_zero

Documentation

Every degree-two class at the finite unramified arithmetic stage vanishes after inflation to the absolute Galois group.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.ProP ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F (n : ℕ)))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F (n : ℕ) hpOdd U)

Lean source · statement

theorem openNormalArithmeticStage_absoluteH2Map_eq_zero
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x : Cohomology.continuousCohomologyZModPLifted (n : ℕ) Gal(StageField/F) 2) :
    (Cohomology.continuousCohomologyZModPMapLifted (n : ℕ)
      (openNormalArithmeticStageAbsoluteRestriction F n hpOdd U) 2).hom x = 0

Module documentation

Absolute degree-two vanishing at the unramified arithmetic stage

Declarations

openNormalArithmeticStageFiniteGaloisField

openNormalArithmeticStageAbsoluteRestriction

openNormalArithmeticStage_exists_absoluteLift

openNormalArithmeticStage_absoluteH2Map_eq_zero