Principal ideles that are idele norms

For an extension L/K of number fields, the main result, unitEmbedding_mem_range_ideleNormMap_iff, says that x ∈ Kˣ is a norm at every place (TauCeti.GlobalNumberFields.IsLocalNormEverywhere) exactly when its principal idele is the norm of an idele of L. It is the principal case of the placewise criterion mem_range_ideleNormMap_iff. With the Hasse norm theorem for cyclic extensions, which identifies global norms with principal ideles that are idele norms, it turns the Hasse norm principle into a statement about norm equations in the completions. The easy half of that principle holds for every extension: a global norm is a norm everywhere (isLocalNormEverywhere_normUnits).

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §2.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §2 (norms of ideles) and §4 (the Hasse norm theorem).

theorem TauCeti.GlobalNumberFields.unitEmbedding_mem_range_ideleNormMap_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (x : Kˣ) : (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x ∈ (ideleNormMap K L).range ↔ IsLocalNormEverywhere K L x

Principal idele norms are local norms everywhere. For an extension L/K of number fields, the principal idele of x ∈ Kˣ is the norm of an idele of L exactly when x is a norm from the local étale algebra K_v ⊗[K] L at every finite and every infinite place v of K.

theorem TauCeti.GlobalNumberFields.isLocalNormEverywhere_normUnits {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (y : Lˣ) : IsLocalNormEverywhere K L ((Algebra.normUnits K) y)

A global norm is a local norm everywhere. This is the easy half of the Hasse norm principle, valid for every extension of number fields.