Placewise characterization of idele norms

An idele is a norm precisely when each coordinate is a norm from the corresponding local étale algebra for a number-field extension L/K. No restrictedness hypothesis on local preimages is needed: outside the finitely many ramified places and nonunit target coordinates, preimages can be chosen as integral units by unramified unit-norm surjectivity and assembled into an idele.

This is an arithmetic property of the idele norm map, independent of global reciprocity and of the Hasse norm principle for field elements.

Main results

• TauCeti.GlobalNumberFields.mem_range_ideleNormMap_iff: the purely placewise norm criterion.
• TauCeti.GlobalNumberFields.mem_range_normUnits_ideleFiniteCoord_ideleNormMap and TauCeti.GlobalNumberFields.mem_range_normUnits_ideleInfiniteCoord_ideleNormMap: every coordinate of a relative idele norm is a norm from the local étale algebra.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.
• J. S. Milne, Class Field Theory, Chapter VII, §2.

The assembly uses Mathlib's RestrictedProduct.mkUnit; unit-norm surjectivity is TauCeti.map_normUnits_unitFiltration.

theorem TauCeti.GlobalNumberFields.mem_range_normUnits_ideleFiniteCoord_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : v.ideleFiniteCoord ((ideleNormMap K L) x) ∈ (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range

Every finite coordinate of an idele norm is a norm from the local étale algebra.

theorem TauCeti.GlobalNumberFields.mem_range_normUnits_ideleInfiniteCoord_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) (v : NumberField.InfinitePlace K) : v.ideleInfiniteCoord ((ideleNormMap K L) x) ∈ (Algebra.normUnits v.Completion).range

Every infinite coordinate of an idele norm is a norm from the local étale algebra.

theorem TauCeti.GlobalNumberFields.mem_range_ideleNormMap_iff (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : x ∈ (ideleNormMap K L).range ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.ideleFiniteCoord x ∈ (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range) ∧ ∀ (v : NumberField.InfinitePlace K), v.ideleInfiniteCoord x ∈ (Algebra.normUnits v.Completion).range

An arbitrary idele is a norm exactly when each finite and infinite coordinate is a norm from the actual local étale algebra. No cyclicity or Galois hypothesis is required.