Module

ArithmeticStageKummerFieldUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageKummerFieldUnitsH2

2 declarations indexed from sourceView source ↗

Module documentation

Field-unit primitives for Kummer classes at the arithmetic stage

The actual stage supplies its p-group Galois group and unramifiedness at every place. The proved supported-idele construction and field-unit H² injection therefore kill its Kummer H² classes and produce field-unit primitives, ready for the Hilbert-90 and Kummer correction.

Imports2

Imported by2

theorem

openNormalArithmeticStage_kummerH2_eq_zero

L35 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_kummerH2_eq_zero

Documentation

Every Kummer H² class at the actual arithmetic stage vanishes in the field-unit representation.

Source context 8 commands

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

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

Lean source · statement

theorem openNormalArithmeticStage_kummerH2_eq_zero
    (x : groupCohomology
      (Rep.trivial ℤ Gal(StageField/F) (ULift (ZMod (n : ℕ)))) 2) :
    (finiteKummerCoefficientH2Map F StageField n hmu).hom x = 0

theorem

openNormalArithmeticStage_kummerTwoCocycle_isFieldUnitsCoboundary

L47 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_kummerTwoCocycle_isFieldUnitsCoboundary