Module

FiniteCyclicLocalUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicLocalUnitsH2

3 declarations indexed from sourceView source ↗

Module documentation

Degree-two cohomology of cyclic local unit representations

For a finite cyclic Galois extension, degree-two cohomology of the actual unit representation is identified first with the field norm quotient. Over a nonarchimedean local base this is then transported by finite local reciprocity to the abelianized Galois group, and hence to the cyclic Galois group itself.

The periodicity comparison is normalized by the supplied cyclic generator. The norm-quotient and Artin comparisons are the existing canonical ones.

Imports5

Imported by6

def

finiteCyclicUnitsH2IsoNormQuotient

L40 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2IsoNormQuotient

Documentation

For a finite cyclic Galois extension, degree-two cohomology of its unit representation is the actual field norm quotient.

The generator is used only for the finite-cyclic periodic resolution.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalClassFieldTheory LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicUnitsH2IsoNormQuotient
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 ≅
      ModuleCat.of Int (Additive (NormQuotient K L))

def

finiteCyclicLocalUnitsH2IsoAbelianizedArtin

L59 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicLocalUnitsH2IsoAbelianizedArtin

Documentation

Over a nonarchimedean local field, finite local reciprocity sends the cyclic unit H² object to the abelianized local Galois group.

This is the Artin interface before using cyclic commutativity to remove the abelianization wrapper.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalClassFieldTheory LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicLocalUnitsH2IsoAbelianizedArtin
    (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 ≅
      ModuleCat.of Int (Additive (Abelianization (Gal(L / K))))

def

finiteCyclicLocalUnitsH2AddEquivGalois

L79 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicLocalUnitsH2AddEquivGalois

Documentation

The cyclic form of the local Artin interface, with target the actual Galois group. It retains its natural additive-group structure; a ZMod n coordinate would require a further normalized choice of cyclic coordinate.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalClassFieldTheory LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicLocalUnitsH2AddEquivGalois
    (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ x : Gal(L / K), x ∈ Subgroup.zpowers g) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) 2 ≃+
      Additive (Gal(L / K))

Module documentation

Degree-two cohomology of cyclic local unit representations

Declarations

finiteCyclicUnitsH2IsoNormQuotient

finiteCyclicLocalUnitsH2IsoAbelianizedArtin

finiteCyclicLocalUnitsH2AddEquivGalois