Module

UnitsCohomologyRestrictScalars.lean

Nyll.GaloisCohomology.Kummer.UnitsCohomologyRestrictScalars

1 declaration indexed from sourceView source ↗

Module documentation

Unit cohomology under surjective scalar restriction

When F → E is surjective, restricting an E-automorphism of N to F is a group isomorphism. Its action on Nˣ is unchanged.

Imports4

Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Module.Equiv.Defs
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Imported by2

def

unitsCohomologyRestrictScalarsIso

L25 ↗

ClassFieldTower.Cohomology.unitsCohomologyRestrictScalarsIso

Documentation

Restricting scalars along a surjective base-field map preserves unit cohomology, with identity coefficients in the unchanged top field.

Source context 2 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology

Lean source · statement

def unitsCohomologyRestrictScalarsIso
    (F E N : Type) [Field F] [Field E] [Field N]
    [Algebra F E] [Algebra E N] [Algebra F N] [IsScalarTower F E N]
    (h : Function.Surjective (algebraMap F E)) (n : ℕ) :
    groupCohomology (Rep.ofAlgebraAutOnUnits E N) n ≅
      groupCohomology (Rep.ofAlgebraAutOnUnits F N) n

Module documentation

Unit cohomology under surjective scalar restriction

Declarations

unitsCohomologyRestrictScalarsIso