Module

FiniteKummerCoefficientH2.lean

Nyll.GaloisCohomology.Kummer.FiniteKummerCoefficientH2

11 declarations indexed from sourceView source ↗

Module documentation

Finite Kummer coefficients in degree-two group cohomology

A primitive p-th root in the base field gives an equivariant additive map from the trivial ZMod p coefficient group to the unit representation of a finite extension. This file constructs the resulting morphism of Int-representations and its induced map on ordinary degree-two group cohomology.

This is only the coefficient-change bridge. It does not compare ordinary group cohomology with the continuous lifted cup-product model, nor identify the resulting unit class with a Hilbert symbol.

Imports2

Mathlib.FieldTheory.KummerExtension
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Imported by10

def

finiteKummerCoefficientRootUnit

L35 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientRootUnit

Documentation

The chosen primitive root, mapped to the extension field and regarded as a unit.

Source context 5 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 (p : ℕ+)

Lean source · statement

def finiteKummerCoefficientRootUnit
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) : Lˣ

theorem

finiteKummerCoefficientRootUnit_val

L45 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientRootUnit_val

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientRootUnit_val
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    ((finiteKummerCoefficientRootUnit K L p hmu : Lˣ) : L) =
      algebraMap K L hmu.choose

theorem

finiteKummerCoefficientRootUnit_isPrimitiveRoot

L51 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientRootUnit_isPrimitiveRoot

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientRootUnit_isPrimitiveRoot
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    IsPrimitiveRoot (finiteKummerCoefficientRootUnit K L p hmu) (p : ℕ)

def

finiteKummerCoefficientAddHom

L60 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientAddHom

Documentation

Additive ZMod p mapped to the powers of the chosen primitive root in the extension's unit group.

Source context 5 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 (p : ℕ+)

Lean source · statement

def finiteKummerCoefficientAddHom
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    ULift (ZMod (p : ℕ)) →+ Additive Lˣ

theorem

finiteKummerCoefficientAddHom_intCast

L70 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientAddHom_intCast

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientAddHom_intCast
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) (i : ℤ) :
    finiteKummerCoefficientAddHom K L p hmu
        (ULift.up (i : ZMod (p : ℕ))) =
      Additive.ofMul (finiteKummerCoefficientRootUnit K L p hmu ^ i)

theorem

finiteKummerCoefficientAddHom_pow_eq_one

L85 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientAddHom_pow_eq_one

Documentation

Every finite Kummer coefficient is killed by the exponent of its root of unity.

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientAddHom_pow_eq_one
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : ULift (ZMod (p : ℕ))) :
    (finiteKummerCoefficientAddHom K L p hmu z).toMul ^ (p : ℕ) = 1

theorem

finiteKummerCoefficientAddHom_fixed

L103 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientAddHom_fixed

Documentation

The chosen root coefficient is fixed by every automorphism over the base field.

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientAddHom_fixed
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (sigma : Gal(L/K)) (z : ULift (ZMod (p : ℕ))) :
    (Rep.ofAlgebraAutOnUnits K L).ρ sigma
        (finiteKummerCoefficientAddHom K L p hmu z) =
      finiteKummerCoefficientAddHom K L p hmu z

def

finiteKummerCoefficientRepHom

L125 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientRepHom

Documentation

The primitive-root inclusion as a morphism from the trivial Int-linear ZMod p representation to the extension-unit representation.

Source context 5 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 (p : ℕ+)

Lean source · statement

def finiteKummerCoefficientRepHom
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ))) ⟶
      Rep.ofAlgebraAutOnUnits K L

def

finiteKummerCoefficientH2Map

L141 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map

Documentation

Change coefficients from trivial mod-p coefficients to extension units in ordinary degree-two group cohomology.

Source context 5 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 (p : ℕ+)

Lean source · statement

def finiteKummerCoefficientH2Map
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    groupCohomology
        (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2 ⟶
      groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2

theorem

finiteKummerCoefficientCocyclesMap_apply

L151 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientCocyclesMap_apply

Documentation

On an inhomogeneous cocycle representative, coefficient change applies the chosen-root homomorphism pointwise.

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientCocyclesMap_apply
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : groupCohomology.cocycles
      (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2)
    (x : Fin 2 → Gal(L/K)) :
    groupCohomology.iCocycles (Rep.ofAlgebraAutOnUnits K L) 2
        (groupCohomology.cocyclesMap (MonoidHom.id (Gal(L/K)))
          (finiteKummerCoefficientRepHom K L p hmu) 2 z) x =
      finiteKummerCoefficientAddHom K L p hmu
        (groupCohomology.iCocycles
          (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2 z x)

theorem

finiteKummerCoefficientH2Map_quotient

L168 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_quotient

Documentation

Naturality of the quotient map for the finite Kummer coefficient change.

Source context 5 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 (p : ℕ+)

Lean source · statement

theorem finiteKummerCoefficientH2Map_quotient
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty)
    (z : groupCohomology.cocycles
      (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2) :
    finiteKummerCoefficientH2Map K L p hmu
        (groupCohomology.π
          (Rep.trivial ℤ (Gal(L/K)) (ULift (ZMod (p : ℕ)))) 2 z) =
      groupCohomology.π (Rep.ofAlgebraAutOnUnits K L) 2
        (groupCohomology.cocyclesMap (MonoidHom.id (Gal(L/K)))
          (finiteKummerCoefficientRepHom K L p hmu) 2 z)

Module documentation

Finite Kummer coefficients in degree-two group cohomology

Declarations