Module

UnitsCohomologyCongr.lean

Nyll.GaloisCohomology.Kummer.UnitsCohomologyCongr

1 declaration indexed from sourceView source ↗

Module documentation

Unit cohomology under a field isomorphism

Conjugation identifies the automorphism groups, while the same field isomorphism identifies their actual unit representations.

Imports5

Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Group.Units.Equiv
Mathlib.Algebra.Module.Equiv.Basic
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Imported by3

def

unitsCohomologyCongrTop

L25 ↗

ClassFieldTower.Cohomology.unitsCohomologyCongrTop

Documentation

An actual algebra equivalence transports field-unit cohomology in every degree.

Source context 2 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology

Lean source · statement

def unitsCohomologyCongrTop
    (K L M : Type) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M]
    (e : L ≃ₐ[K] M) (n : ℕ) :
    groupCohomology (Rep.ofAlgebraAutOnUnits K L) n ≅
      groupCohomology (Rep.ofAlgebraAutOnUnits K M) n

Module documentation

Unit cohomology under a field isomorphism

Declarations

unitsCohomologyCongrTop