The idele norm of a number field

An idele of a number field K is a unit x of the adele ring 𝔸_K (NumberField.IdeleGroup (𝓞 K) K). Its coordinate x_v at every place is a unit of the completion K_v, and at all but finitely many finite places it is a unit of the valuation ring. The idele norm is the product of the normalized local absolute values of the coordinates,

‖x‖ = ∏_{w | ∞} |x_w|_w · ∏_{v < ∞} ‖x_v‖_v,

where |·|_w is the absolute value at a real place and its square at a complex place (completionNormalizedAbsValue), and ‖·‖_v is the norm of the v-adic completion, which sends a uniformizer to (N v)⁻¹. Almost every finite factor is 1, so the product is a finite one. The idele norm is a group homomorphism to the positive reals, and the product formula says exactly that it is trivial on the principal ideles, which is what lets it descend to the idele class group.

Main definitions

• TauCeti.GlobalNumberFields.ideleNorm: the idele norm, a homomorphism to ℝ≥0ˣ.
• TauCeti.GlobalNumberFields.ideleNormSection: the continuous section of the idele norm at an infinite place w, the idele whose w-coordinate is t ^ (1 / m_w) and whose other coordinates are 1.

Main results

• TauCeti.GlobalNumberFields.eventually_norm_ideleFiniteCoord_eq_one: the finite coordinates of an idele have norm 1 at all but finitely many places.
• TauCeti.GlobalNumberFields.coe_ideleNorm: the idele norm is the product of the normalized local absolute values of the coordinates.
• TauCeti.GlobalNumberFields.ideleNorm_unitEmbedding: the idele norm of a principal idele is 1; this is the product formula NumberField.prod_abs_eq_one, read on ideles.
• TauCeti.GlobalNumberFields.principalSubgroup_le_ker_ideleNorm: the principal ideles lie in the kernel of the idele norm.
• TauCeti.GlobalNumberFields.coe_ideleNorm_ofAdicCompletion, TauCeti.GlobalNumberFields.coe_ideleNorm_ofCompletion: on an idele concentrated at one place the idele norm is the normalized absolute value at that place.
• TauCeti.GlobalNumberFields.coe_ideleNorm_ofAdicCompletion_of_valued_eq_exp_neg_one: an idele concentrated at a finite place v with a uniformizer as coordinate has idele norm N(v)⁻¹.
• TauCeti.GlobalNumberFields.continuous_ideleNorm: the idele norm is continuous, because the finite factors are locally constant on the idele group.
• TauCeti.GlobalNumberFields.ideleNorm_ideleNormSection: the section is right inverse to the idele norm.
• TauCeti.GlobalNumberFields.ideleNorm_surjective: every positive real number is an idele norm.
• TauCeti.GlobalNumberFields.mixedEmbedding_norm_eq_ideleNorm: for an idele whose finite part is an everywhere-integral unit, its idele norm equals the mixed norm of its infinite part.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• J. Tate, Fourier analysis in number fields and Hecke's zeta-functions, §3.3.

Coordinates of an idele

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_unitEmbedding {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : Kˣ) : v.ideleFiniteCoord ((NumberField.IdeleGroup.unitEmbedding R K) x) = (Units.map ↑(algebraMap K (adicCompletion K v))) x

The finite coordinate of a principal idele is the image of the global element.

theorem IsDedekindDomain.HeightOneSpectrum.valued_ideleFiniteCoord_unitEmbedding_sub_one {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : Kˣ) : Valued.v (↑(v.ideleFiniteCoord ((NumberField.IdeleGroup.unitEmbedding R K) x)) - 1) = (valuation K v) (↑x - 1)

The distance from one of the coordinate at v of a principal idele is measured by the v-adic valuation of x - 1.

@[simp]

theorem NumberField.InfinitePlace.ideleInfiniteCoord_unitEmbedding {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (x : Kˣ) : w.ideleInfiniteCoord ((IdeleGroup.unitEmbedding R K) x) = (Units.map ↑(algebraMap K w.Completion)) x

The infinite coordinate of a principal idele is the image of the global element.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_ofAdicCompletion_self {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (u : (adicCompletion K v)ˣ) : v.ideleFiniteCoord ((NumberField.IdeleGroup.ofAdicCompletion R K v) u) = u

At its own place, the finite coordinate of an idele concentrated at a finite place v is the given unit of K_v.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_ofAdicCompletion_of_ne {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v' : HeightOneSpectrum R) {v : HeightOneSpectrum R} (h : v' ≠ v) (u : (adicCompletion K v)ˣ) : v'.ideleFiniteCoord ((NumberField.IdeleGroup.ofAdicCompletion R K v) u) = 1

Away from its own place, the finite coordinates of an idele concentrated at a finite place are trivial.

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_prod_ofAdicCompletion {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [DecidableEq (HeightOneSpectrum R)] (v' : HeightOneSpectrum R) (S : Finset (HeightOneSpectrum R)) (u : (v : HeightOneSpectrum R) → (adicCompletion K v)ˣ) : v'.ideleFiniteCoord (∏ v ∈ S, (NumberField.IdeleGroup.ofAdicCompletion R K v) (u v)) = if v' ∈ S then u v' else 1

The finite coordinates of a product of ideles, one concentrated at each place of a finite set S of finite places: the prescribed unit at a place of S, and 1 elsewhere.

@[simp]

theorem NumberField.InfinitePlace.ideleInfiniteCoord_ofAdicCompletion {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (v : IsDedekindDomain.HeightOneSpectrum R) (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : w.ideleInfiniteCoord ((IdeleGroup.ofAdicCompletion R K v) u) = 1

The infinite coordinates of an idele concentrated at a finite place are trivial.

@[simp]

theorem NumberField.InfinitePlace.ideleInfiniteCoord_ofCompletion_self {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (u : w.Completionˣ) : w.ideleInfiniteCoord ((IdeleGroup.ofCompletion R K w) u) = u

At its own place, the infinite coordinate of an idele concentrated at an infinite place w is the given unit of K_w.

@[simp]

theorem NumberField.InfinitePlace.ideleInfiniteCoord_ofCompletion_of_ne {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w' : InfinitePlace K) {w : InfinitePlace K} (h : w' ≠ w) (u : w.Completionˣ) : w'.ideleInfiniteCoord ((IdeleGroup.ofCompletion R K w) u) = 1

Away from its own place, the infinite coordinates of an idele concentrated at an infinite place are trivial.

@[simp]

theorem NumberField.InfinitePlace.ideleInfiniteCoord_ofFiniteIdele {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) (a : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) : w.ideleInfiniteCoord ((IdeleGroup.ofFiniteIdele R K) a) = 1

The infinite coordinates of an idele with trivial infinite components are trivial.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_ofFiniteIdele {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : (FiniteAdeleRing R K)ˣ) : v.ideleFiniteCoord ((NumberField.IdeleGroup.ofFiniteIdele R K) a) = (Units.map (RestrictedProduct.evalMonoidHom (adicCompletion K) v)) a

The finite coordinate of an idele built from a finite idele is its original coordinate.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ideleFiniteCoord_ofCompletion {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (w : NumberField.InfinitePlace K) (u : w.Completionˣ) : v.ideleFiniteCoord ((NumberField.IdeleGroup.ofCompletion R K w) u) = 1

The finite coordinates of an idele concentrated at an infinite place are trivial.

theorem NumberField.InfinitePlace.ideleInfiniteCoord_prod_ofCompletion {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [DecidableEq (InfinitePlace K)] (w' : InfinitePlace K) (T : Finset (InfinitePlace K)) (u : (w : InfinitePlace K) → w.Completionˣ) : w'.ideleInfiniteCoord (∏ w ∈ T, (IdeleGroup.ofCompletion R K w) (u w)) = if w' ∈ T then u w' else 1

The infinite coordinates of a product of ideles, one concentrated at each place of a finite set T of infinite places: the prescribed unit at a place of T, and 1 elsewhere.

theorem NumberField.IdeleGroup.exists_mul_eq_coord_ite {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum R)] [DecidableEq (InfinitePlace K)] (x : IdeleGroup R K) (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (T : Finset (InfinitePlace K)) : ∃ (y : IdeleGroup R K) (z : IdeleGroup R K), z * y = x ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.ideleFiniteCoord y = if v ∈ S then v.ideleFiniteCoord x else 1) ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum R), v.ideleFiniteCoord z = if v ∈ S then 1 else v.ideleFiniteCoord x) ∧ (∀ (w : InfinitePlace K), w.ideleInfiniteCoord y = if w ∈ T then w.ideleInfiniteCoord x else 1) ∧ ∀ (w : InfinitePlace K), w.ideleInfiniteCoord z = if w ∈ T then 1 else w.ideleInfiniteCoord x

Splitting an idele coordinatewise: for a finite set S of finite places and a finite set T of infinite places, an idele x is a product z * y where y has the coordinates of x at the places in S and T and is trivial elsewhere, while z is trivial at those places and has the coordinates of x elsewhere.

theorem NumberField.IdeleGroup.prod_ofCompletion_mul_ofFiniteIdele {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [NumberField K] (x : IdeleGroup R K) : (∏ w : InfinitePlace K, (ofCompletion R K w) (w.ideleInfiniteCoord x)) * (ofFiniteIdele R K) ((toFiniteIdele R K) x) = x

An idele is the product of its archimedean components and its finite component: the ideles concentrated at the infinite places, carrying the infinite coordinates of x, times the idele with the finite component of x and trivial infinite components.

theorem TauCeti.GlobalNumberFields.eventually_norm_ideleFiniteCoord_eq_one {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, ‖↑(v.ideleFiniteCoord x)‖ = 1

The finite coordinates of an idele are units of the valuation ring, that is, have norm 1, at all but finitely many places.

theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_norm_ideleFiniteCoord {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ‖↑(v.ideleFiniteCoord x)‖

The norms of the finite coordinates of an idele have finite multiplicative support.

The idele norm

noncomputable def TauCeti.GlobalNumberFields.ideleNorm {K : Type u_1} [Field K] [NumberField K] : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K →* NNRealˣ

The idele norm of a number field: the product over all places of the normalized local absolute values of the coordinates of an idele, a positive real number. At a real place the local factor is the absolute value, at a complex place its square, and at a finite place the norm of the v-adic completion, which is 1 at almost every place.

theorem TauCeti.GlobalNumberFields.coe_ideleNorm {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ↑↑(ideleNorm x) = (∏ w : NumberField.InfinitePlace K, w.completionNormalizedAbsValue ↑(w.ideleInfiniteCoord x)) * ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ‖↑(v.ideleFiniteCoord x)‖

The idele norm is the product of the normalized local absolute values of the coordinates.

theorem TauCeti.GlobalNumberFields.mixedEmbedding_norm_eq_ideleNorm {K : Type u_1} [Field K] [NumberField K] {z : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hz : (NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) z ∈ IsDedekindDomain.FiniteAdeleRing.integralUnits (NumberField.RingOfIntegers K) K) : NumberField.mixedEmbedding.norm ((NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) (↑z).1) = ↑↑(ideleNorm z)

For an idele whose finite part is an everywhere-integral unit, the idele norm is the mixed norm of its infinite part.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNorm_unitEmbedding {K : Type u_1} [Field K] [NumberField K] (x : Kˣ) : ideleNorm ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x) = 1

The product formula on ideles: the idele norm of a principal idele is 1.

theorem TauCeti.GlobalNumberFields.principalSubgroup_le_ker_ideleNorm {K : Type u_1} [Field K] [NumberField K] : NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K ≤ ideleNorm.ker

The idele norm is trivial on the principal ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_ideleNorm_ofAdicCompletion {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : ↑↑(ideleNorm ((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u)) = ‖↑u‖

On an idele concentrated at one finite place v, the idele norm is the norm of the v-adic coordinate.

theorem TauCeti.GlobalNumberFields.coe_ideleNorm_ofAdicCompletion_of_valued_eq_exp_neg_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hu : Valued.v ↑u = WithZero.exp (-1)) : ↑↑(ideleNorm ((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u)) = (↑(Ideal.absNorm v.asIdeal))⁻¹

An idele concentrated at one finite place v, with a uniformizer of K_v as v-adic coordinate, has idele norm N(v)⁻¹.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_ideleNorm_ofCompletion {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (u : w.Completionˣ) : ↑↑(ideleNorm ((NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K w) u)) = w.completionNormalizedAbsValue ↑u

On an idele concentrated at one infinite place w, the idele norm is the normalized absolute value of the w-coordinate.

The section at one infinite place

noncomputable def TauCeti.GlobalNumberFields.ideleNormSection (K : Type u_1) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) : NNRealˣ →ₜ* NumberField.IdeleGroup (NumberField.RingOfIntegers K) K

The continuous section of the idele norm at the infinite place w: the idele whose w-coordinate is the positive real number t ^ (1 / m_w) and whose other coordinates are 1.

theorem TauCeti.GlobalNumberFields.ideleNormSection_apply {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (t : NNRealˣ) : (ideleNormSection K w) t = (NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K w) (w.completionNormSection t)

The section of the idele norm at w is concentrated at w, with coordinate completionNormSection w t.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNorm_ideleNormSection {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (t : NNRealˣ) : ideleNorm ((ideleNormSection K w) t) = t

The section is right inverse to the idele norm.

Continuity and surjectivity

theorem TauCeti.GlobalNumberFields.continuous_ideleNorm {K : Type u_1} [Field K] [NumberField K] : Continuous ⇑ideleNorm

The idele norm is continuous.

theorem TauCeti.GlobalNumberFields.ideleNorm_surjective {K : Type u_1} [Field K] [NumberField K] : Function.Surjective ⇑ideleNorm

The idele norm is surjective: every positive real number is the idele norm of an idele concentrated at a single infinite place.