Module

FiniteKummerAbsoluteKernel.lean

Nyll.SawinTotallyRealTowers.FiniteKummerAbsoluteKernel

1 declaration indexed from sourceView source ↗

Module documentation

Finite Kummer zero classes vanish after absolute inflation

A vanishing finite field-unit class gives an actual field-unit primitive. The existing Hilbert-90 correction then gives a continuous lift of the normalized central extension over the absolute Galois group. Thus its inflated mod-p class is zero. The finite coefficient map is not asserted to be injective. This is the representative-level kernel comparison and uses neither a local-field nor an unramified-extension assumption.

Imports12

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteKummerAbsoluteLift
Nyll.GaloisCohomology.Kummer.FiniteKummerCoefficientH2
Nyll.GaloisCohomology.ProP.H2CocycleExtensionPullback
Nyll.GaloisCohomology.ProP.TrivialZModP
Mathlib.FieldTheory.AbsoluteGaloisGroup
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.Galois.Profinite
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
Mathlib.RepresentationTheory.Rep.Basic

Imported by2

theorem

absoluteInflation_eq_zero_of_finiteKummerH2_eq_zero

L38 ↗

ClassFieldTower.Sawin.absoluteInflation_eq_zero_of_finiteKummerH2_eq_zero

Documentation

A finite Kummer coefficient class in the kernel maps to zero under actual absolute inflation of the original lifted class.

Source context 3 commands

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

namespace ClassFieldTower.Sawin
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

theorem absoluteInflation_eq_zero_of_finiteKummerH2_eq_zero
    (K : Type) [Field K] [CharZero K]
    (p : ℕ+) [Fact (p : ℕ).Prime]
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : trivialZModPCocyclesLifted (p : ℕ) Gal(E/K) 2)
    (hZero : (finiteKummerCoefficientH2Map K E p hmu).hom
      (groupCohomology.H2π
        (Rep.trivial ℤ Gal(E/K) (ULift.{0} (ZMod (p : ℕ))))
        (normalizedFiniteKummerTwoCocycle K p E z)) = 0) :
    (continuousCohomologyZModPMapLifted (p : ℕ)
      (absoluteFiniteGaloisRestriction K E) 2).hom
      (ContinuousCohomology.π (trivialZModPLifted (p : ℕ) Gal(E/K)) 2 z) = 0

Module documentation

Finite Kummer zero classes vanish after absolute inflation

Declarations

absoluteInflation_eq_zero_of_finiteKummerH2_eq_zero