The representation norm on the ideles

Let L/K be a Galois extension of number fields. The norm ∑_σ σ x of the representation idelesRep K L of Gal(L/K) on I_L is the idele norm N_{L/K}(x), extended back to L (idelesRep_norm_apply). This is TauCeti.GlobalNumberFields.ideleExtension_ideleNormMap read on the representation. By Galois descent of ideles, an idele of K, extended to L, is then a representation norm exactly when it is an idele norm from L (ideleExtension_mem_range_idelesRep_norm_iff).

Main results

• TauCeti.ClassFieldTheory.idelesRep_norm_apply: the norm of the representation of Gal(L/K) on I_L is the idele norm, extended back to L.
• TauCeti.ClassFieldTheory.ideleExtension_mem_range_idelesRep_norm_iff: an idele of K, extended to L, is a representation norm exactly when it is an idele norm from L.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.

theorem TauCeti.ClassFieldTheory.idelesRep_norm_apply {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (x : ↑(idelesRep K L)) : Rep.toAdditive ((Rep.Hom.hom (idelesRep K L).norm.asHom) x) = Additive.ofMul ((GlobalNumberFields.ideleExtension K L) ((GlobalNumberFields.ideleNormMap K L) (Additive.toMul (Rep.toAdditive x))))

The representation norm on ideles is the idele norm. For L/K Galois, the norm ∑_σ σ x of the representation of Gal(L/K) on I_L is the idele norm N_{L/K}(x), extended back to L.

theorem TauCeti.ClassFieldTheory.ideleExtension_mem_range_idelesRep_norm_iff {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : Rep.toAdditive.symm (Additive.ofMul ((GlobalNumberFields.ideleExtension K L) x)) ∈ (Rep.Hom.hom (idelesRep K L).norm.asHom).range ↔ x ∈ (GlobalNumberFields.ideleNormMap K L).range

An idele of K, extended to L, lies in the image of the representation norm on I_L exactly when it is an idele norm from L.