The Product Formula for number fields

In this file we prove the Product Formula for number fields: for any non-zero element x of a number field K, we have ∏ |x|ᵥ=1 where the product runs over the equivalence classes of absolute values of K. The |⬝|ᵥ are normalized as follows:

• for the infinite places, |⬝|ᵥ is the absolute value on K induced by the corresponding field embedding in ℂ and the usual absolute value on ℂ;
• for the finite places and a non-zero x, |x|ᵥ is equal to the norm of the corresponding maximal ideal of 𝓞 K raised to the power of the v-adic valuation of x.

Main Results

• NumberField.FinitePlace.prod_eq_inv_abs_norm: for any non-zero element x of a number field K, the product ∏ |x|ᵥ of the absolute values of x associated to the finite places of K is equal to the inverse of the norm of x.
• NumberField.prod_abs_eq_one: for any non-zero element x of a number field K, we have ∏ |x|ᵥ=1, where the product runs over the equivalence classes of absolute values of K.

Tags

number field, embeddings, places, infinite places, finite places, product formula

theorem NumberField.FinitePlace.prod_eq_inv_abs_norm_int {K : Type u_1} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} (h_x_nezero : x ≠ 0) : ∏ᶠ (w : NumberField.FinitePlace K), w ↑x = |↑((Algebra.norm ℤ) x)|⁻¹

For any non-zero x in 𝓞 K, the prduct of w x, where w runs over FinitePlace K, is equal to the inverse of the absolute value of Algebra.norm ℤ x.

theorem NumberField.FinitePlace.prod_eq_inv_abs_norm {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) : ∏ᶠ (w : NumberField.FinitePlace K), w x = ↑|(Algebra.norm ℚ) x|⁻¹

For any non-zero x in K, the prduct of w x, where w runs over FinitePlace K, is equal to the inverse of the absolute value of Algebra.norm ℚ x.

theorem NumberField.prod_abs_eq_one {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) : (∏ w : NumberField.InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : NumberField.FinitePlace K), w x = 1

The Product Formula for the Number Field K.