Module

FiniteUnramifiedAbsoluteH2Vanishing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FiniteUnramifiedAbsoluteH2Vanishing

3 declarations indexed from sourceView source ↗

Module documentation

Absolute H² vanishing from any embedded unramified p-extension

The supported-idele primitive and the Hilbert-90 correction apply to an actual finite everywhere-unramified p-extension, independently of how it was obtained as a finite stage. This form also applies to the mapped cyclotomic base change. No primitive or comparison assumption is added.

Imports4

Imported by2

def

finiteUnramifiedExtensionFiniteGaloisField

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finiteUnramifiedExtensionFiniteGaloisField

Documentation

The same embedded field, retaining its finite Galois certificates.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (E : FiniteEverywhereUnramifiedProPExtension F (n : ℕ))

Lean source · full declaration

def finiteUnramifiedExtensionFiniteGaloisField :
    FiniteGaloisIntermediateField F (AlgebraicClosure F) where
  toIntermediateField := E.field
  finiteDimensional := E.finiteDimensional
  isGalois := E.isGalois

def

finiteUnramifiedExtensionAbsoluteRestriction

L39 ↗

ClassFieldTower.Martinet.Shafarevich.finiteUnramifiedExtensionAbsoluteRestriction

Documentation

Actual absolute restriction to the embedded unramified extension.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (E : FiniteEverywhereUnramifiedProPExtension F (n : ℕ))

Lean source · statement

def finiteUnramifiedExtensionAbsoluteRestriction :
    Field.absoluteGaloisGroup F →ₜ* Gal(E.field/F)

theorem

finiteUnramifiedExtension_absoluteH2Map_eq_zero

L45 ↗

ClassFieldTower.Martinet.Shafarevich.finiteUnramifiedExtension_absoluteH2Map_eq_zero

Documentation

Every degree-two class from this unramified p-extension becomes zero on the absolute Galois group of a base containing a primitive p-th root.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (E : FiniteEverywhereUnramifiedProPExtension F (n : ℕ))

Lean source · statement

theorem finiteUnramifiedExtension_absoluteH2Map_eq_zero
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (x : Cohomology.continuousCohomologyZModPLifted (n : ℕ) Gal(E.field/F) 2) :
    (Cohomology.continuousCohomologyZModPMapLifted (n : ℕ)
      (finiteUnramifiedExtensionAbsoluteRestriction F n E) 2).hom x = 0

Module documentation

Absolute H² vanishing from any embedded unramified p-extension

Declarations

finiteUnramifiedExtensionFiniteGaloisField

finiteUnramifiedExtensionAbsoluteRestriction

finiteUnramifiedExtension_absoluteH2Map_eq_zero