Module

Main.lean

Nyll.GaloisCohomology.Cyclic.TateH0.Main

1 declaration indexed from sourceView source ↗

Module documentation

Degree-zero Tate cohomology and the norm quotient

This module identifies degree-zero Tate cohomology of the multiplicative group of a finite Galois extension with the corresponding field norm quotient.

Imports1

Nyll.GaloisCohomology.Cyclic.TateH0.NormImage

Imported by5

def

H0TateUnitsIsoNormQuotient

L25 ↗

CyclicCohomology.H0TateUnitsIsoNormQuotient

Documentation

The canonical comparison between mathlib's degree-zero Tate cohomology of Lˣ and the field norm quotient Kˣ / N_{L/K}(Lˣ) for a finite Galois extension.

Source context 3 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section

Lean source · statement

def H0TateUnitsIsoNormQuotient (K L : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
    CategoryTheory.Iso (tateCohomology (Rep.ofAlgebraAutOnUnits K L) 0)
      (ModuleCat.of Int (Additive (NormQuotient K L)))

Module documentation

Degree-zero Tate cohomology and the norm quotient

Declarations

H0TateUnitsIsoNormQuotient