Module

FiniteCyclicKummerH2NormQuotient.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteCyclicKummerH2NormQuotient

2 declarations indexed from sourceView source ↗

Module documentation

Finite cyclic Kummer H² and the norm quotient

For a finite cyclic extension whose base contains a primitive p-th root, the primitive-root coefficient morphism sends ordinary mod-p degree-two cohomology to unit cohomology. Finite-cyclic periodicity then places the result in the field norm quotient.

No assertion is made here that a particular cup class maps to a prescribed norm class or Hilbert symbol.

Imports2

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.All

def

finiteCyclicKummerH2ToNormQuotient

L35 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicKummerH2ToNormQuotient

Documentation

Ordinary mod-p degree-two cohomology mapped to the field norm quotient through the primitive-root coefficient inclusion and the existing finite-cyclic units comparison.

Source context 6 commands

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

open CategoryTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable (p : ℕ+)

Lean source · statement

def finiteCyclicKummerH2ToNormQuotient
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    groupCohomology
        (Rep.trivial ℤ (Gal(L / K)) (ULift (ZMod (p : ℕ)))) 2 ⟶
      ModuleCat.of ℤ (Additive (LocalFieldTheory.NormQuotient K L))

theorem

finiteCyclicKummerH2ToNormQuotient_quotient

L47 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicKummerH2ToNormQuotient_quotient