Theorems · Theorem · group theory

groupCohomology.norm_ofAlgebraAutOnUnits_eq

∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L]
  [IsGalois K L] (x : Lˣ),
  ↑(Additive.toMul
        (Rep.toAdditive ((Rep.Hom.hom (Rep.ofAlgebraAutOnUnits K L).norm) (Rep.toAdditive.symm (Additive.ofMul x))))) =
    (algebraMap K L) ((Algebra.norm K) ↑x)

Given L/K finite and Galois, and x : Lˣ, this essentially says (∏ σ) • x = N_{L/K}(x), where the product is over σ ∈ Gal(L/K).

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Cited by

1 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFiniteDimensionalIsGalois