NYLL
Module

FiniteKummerContinuousKernel.lean

Nyll.SawinTotallyRealTowers.FiniteKummerContinuousKernel
3 declarations indexed from sourceView source ↗

Module documentation

The finite Kummer coefficient kernel lies in the absolute inflation kernel

The finite coefficient map is composed with the established discrete continuous-to-ordinary H² comparison. Normalization changes a representative by the boundary of a constant one-cochain. The representative-level Hilbert-90 result therefore proves kernel containment for every finite continuous H² class, with no assumption about a chosen representative.

Imports18
Imported by3

Declarations

theorem

normalizedFiniteKummerTwoCocycle_H2π

L45 ↗
ClassFieldTower.Sawin.normalizedFiniteKummerTwoCocycle_H2π
Documentation

Normalizing a dehomogenized cocycle changes it by an explicit constant one-cochain boundary and leaves its ordinary cohomology class unchanged.

Source context 4 commands

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

namespace ClassFieldTower.Sawin
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
noncomputable section
Lean source · statement
theorem normalizedFiniteKummerTwoCocycle_H2π
    (K : Type) [Field K] (p : ℕ+) [Fact (p : ℕ).Prime]
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (z : trivialZModPCocyclesLifted (p : ℕ) Gal(E/K) 2) :
    groupCohomology.H2π
      (Rep.trivial ℤ Gal(E/K) (ULift.{0} (ZMod (p : ℕ))))
      (normalizedFiniteKummerTwoCocycle K p E z) =
    discreteContinuousH2AddEquiv
      (ContinuousCohomology.π (trivialZModPLifted (p : ℕ) Gal(E/K)) 2 z)
def

finiteKummerContinuousH2Map

L68 ↗
ClassFieldTower.Sawin.finiteKummerContinuousH2Map
Documentation

The actual finite Kummer coefficient map on lifted continuous H², using the existing discrete comparison. Its target retains its natural additive group structure; no mod-p module is imposed on field-unit H².

Source context 4 commands

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

namespace ClassFieldTower.Sawin
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
noncomputable section
Lean source · statement
def finiteKummerContinuousH2Map
    (K : Type) [Field K] (p : ℕ+)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    continuousCohomologyZModPLifted (p : ℕ) Gal(E/K) 2 →+
      groupCohomology (Rep.ofAlgebraAutOnUnits K E) 2
theorem

finiteKummerContinuousH2Map_ker_le_absoluteInflation_ker

L79 ↗
ClassFieldTower.Sawin.finiteKummerContinuousH2Map_ker_le_absoluteInflation_ker
Documentation

The kernel of finite Kummer coefficient change is contained in the kernel of actual absolute inflation, for every finite continuous H² class.

Source context 4 commands

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

namespace ClassFieldTower.Sawin
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
noncomputable section
Lean source · statement
theorem finiteKummerContinuousH2Map_ker_le_absoluteInflation_ker
    (K : Type) [Field K] [CharZero K] (p : ℕ+) [Fact (p : ℕ).Prime]
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    (finiteKummerContinuousH2Map K p E hmu).ker ≤
      (continuousCohomologyZModPMapLifted (p : ℕ)
        (absoluteFiniteGaloisRestriction K E) 2).hom.toLinearMap.toAddMonoidHom.ker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.