The representation norm on units of a Galois extension

For a finite Galois extension L/K, the norm of the representation of Gal(L/K) on Lˣ agrees with the field norm. This file records the resulting identification between the range of the representation norm on elements from Kˣ and the field-theoretic norm group N_{L/K}(Lˣ).

Main results

• TauCeti.mem_range_rep_norm_iff_mem_normGroup: the representation norm on Lˣ has the same range on elements of Kˣ as the field norm.

theorem TauCeti.mem_range_rep_norm_iff_mem_normGroup {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a : Kˣ) : Rep.toAdditive.symm (Additive.ofMul ((Units.map ↑(algebraMap K L)) a)) ∈ (Rep.Hom.hom (Rep.ofMulDistribMulAction Gal(L/K) Lˣ).norm).range ↔ a ∈ normGroup K L

The image of a ∈ Kˣ in Lˣ lies in the range of the representation norm for Gal(L/K) exactly when a lies in the field norm group N_{L/K}(Lˣ).