Places of a number field and their normalized absolute values

Mathlib indexes the two kinds of place of a number field K by two unrelated types: the finite places by IsDedekindDomain.HeightOneSpectrum (𝓞 K) and the infinite places by NumberField.InfinitePlace K. Both carry an absolute value, but with different normalizations, and the product formula NumberField.prod_abs_eq_one is stated as a product over the finite places times a product over the infinite places.

This file introduces the single indexing type TauCeti.GlobalNumberFields.Place K for all places of K, together with the normalized absolute value ‖·‖_v attached to a place v, and states the product formula as one finprod over that type.

The normalization is the one that makes the product formula hold with all exponents equal to one:

• at a finite place v, ‖x‖_v is the v-adic absolute value NumberField.HeightOneSpectrum. adicAbv, that is (N v) ^ (-v x);
• at a real place w, ‖x‖_w = |x| computed through the real embedding;
• at a complex place w, ‖x‖_w = |x| ^ 2 computed through either complex embedding.

Because of the square at the complex places, ‖·‖_v is not an AbsoluteValue — it does not satisfy the triangle inequality there — so it is bundled as a MonoidWithZeroHom. This is the standard normalization: ‖·‖_v is the module of the local field at v, which is what the idele norm and the product formula require.

Main definitions

• TauCeti.GlobalNumberFields.Place: the places of K, finite and infinite together.
• TauCeti.GlobalNumberFields.normalizedAbsValue: the normalized absolute value at a place.

Main results

• TauCeti.GlobalNumberFields.forall_normalizedAbsValue_inl_le_one_iff: an element of K is an algebraic integer exactly when its normalized absolute value is at most 1 at every finite place.
• TauCeti.GlobalNumberFields.hasFiniteMulSupport_normalizedAbsValue: a nonzero element of K has normalized absolute value 1 at all but finitely many places.
• TauCeti.GlobalNumberFields.finprod_normalizedAbsValue_eq_one: the product formula, as a single product over all places of K.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II.
• J. Neukirch, Algebraic Number Theory, Chapter III.

@[reducible, inline]

abbrev TauCeti.GlobalNumberFields.Place (K : Type u_1) [Field K] : Type u_1

A place of a number field K: either a finite place, indexed by a height one prime of 𝓞 K, or an infinite place. This is an abbreviation for the disjoint union of Mathlib's two indexing types; it is the uniform vocabulary in which statements ranging over all places of K (the product formula, the restricted product defining the adeles, the idele norm) are phrased.

Equations

• TauCeti.GlobalNumberFields.Place K = (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) ⊕ NumberField.InfinitePlace K)

noncomputable def TauCeti.GlobalNumberFields.normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] : Place K → K →*₀ ℝ

The normalized absolute value at a place of a number field: the v-adic absolute value at a finite place v, and w x ^ w.mult at an infinite place w, so that a real place contributes |x| and a complex place contributes |x| ^ 2.

At a complex place this is not subadditive, so it is bundled as a MonoidWithZeroHom rather than as an AbsoluteValue.

Equations

• TauCeti.GlobalNumberFields.normalizedAbsValue (Sum.inl v) = (NumberField.HeightOneSpectrum.adicAbv K v).toMonoidWithZeroHom
• TauCeti.GlobalNumberFields.normalizedAbsValue (Sum.inr w) = { toFun := fun (x : K) => w x ^ w.mult, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) : (normalizedAbsValue (Sum.inl v)) x = (NumberField.HeightOneSpectrum.adicAbv K v) x

@[simp]

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (x : K) : (normalizedAbsValue (Sum.inr w)) x = w x ^ w.mult

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_of_isReal {K : Type u_1} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : K) : (normalizedAbsValue (Sum.inr w)) x = w x

At a real place the normalized absolute value is the absolute value itself.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_of_isComplex {K : Type u_1} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (x : K) : (normalizedAbsValue (Sum.inr w)) x = w x ^ 2

At a complex place the normalized absolute value is the square of the absolute value.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_eq_norm_embedding {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (x : K) : (normalizedAbsValue (Sum.inr w)) x = ‖w.embedding x‖ ^ w.mult

The normalized absolute value at an infinite place, computed through a complex embedding defining the place.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_nonneg {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : 0 ≤ (normalizedAbsValue v) x

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_eq_zero {K : Type u_1} [Field K] [NumberField K] (v : Place K) {x : K} : (normalizedAbsValue v) x = 0 ↔ x = 0

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_pos {K : Type u_1} [Field K] [NumberField K] (v : Place K) {x : K} (hx : x ≠ 0) : 0 < (normalizedAbsValue v) x

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) : (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) ≤ 1

An algebraic integer has normalized absolute value at most 1 at every finite place.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) : (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) = 1 ↔ x ∉ v.asIdeal

An algebraic integer has normalized absolute value exactly 1 at a finite place precisely when it avoids the corresponding prime.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_le_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (y : K) : (normalizedAbsValue (Sum.inl v)) y ≤ 1 ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K v) y ≤ 1

At a finite place, having normalized absolute value at most 1 is having v-adic valuation at most 1.

theorem TauCeti.GlobalNumberFields.forall_normalizedAbsValue_inl_le_one_iff {K : Type u_1} [Field K] [NumberField K] (y : K) : (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (normalizedAbsValue (Sum.inl v)) y ≤ 1) ↔ y ∈ (algebraMap (NumberField.RingOfIntegers K) K).range

An element of a number field is an algebraic integer exactly when its normalized absolute value is at most 1 at every finite place.

theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_eq_absNorm_zpow {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) (hx : x ≠ 0) : (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) = ↑(Ideal.absNorm v.asIdeal) ^ (-↑(multiplicity v.asIdeal (Ideal.span {x})))

The normalized absolute value of a nonzero algebraic integer at a finite place, explicitly: the ideal norm of the prime, raised to minus the multiplicity of that prime in the principal ideal generated by the integer.

theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_adicAbv {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (NumberField.HeightOneSpectrum.adicAbv K v) x

A nonzero element of a number field lies outside all but finitely many height one primes, so its v-adic absolute values are almost all 1.

theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : Function.HasFiniteMulSupport fun (v : Place K) => (normalizedAbsValue v) x

A nonzero element of a number field has normalized absolute value 1 at all but finitely many places.

theorem TauCeti.GlobalNumberFields.finprod_normalizedAbsValue_inl {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (normalizedAbsValue (Sum.inl v)) x = ↑|(Algebra.norm ℚ) x|⁻¹

The finite part of the product formula, indexed by the height one primes of 𝓞 K.

theorem TauCeti.GlobalNumberFields.finprod_normalizedAbsValue_eq_one {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : ∏ᶠ (v : Place K), (normalizedAbsValue v) x = 1

The product formula for a number field, as a single product over all of its places, finite and infinite, of the normalized absolute values.