Gauss norms of primitive and split polynomials

At a nonarchimedean absolute value v, the Gauss norm Polynomial.gaussNorm v c is multiplicative (Polynomial.gaussNorm_mul). This file evaluates it on the polynomials that occur when a primitive integer polynomial is factored into linear factors.

Let φ : A →+* R satisfy v (φ a) ≤ 1 for every a : A. A polynomial over A whose coefficients generate the unit ideal has Gauss norm of radius one equal to 1 after mapping along φ: Bézout writes 1 as a combination of the coefficients, and the ultrametric inequality bounds v 1 = 1 by the largest coefficient. Every nonarchimedean absolute value is at most 1 on the integers, so this applies to every primitive P ∈ ℤ[X] and every nonarchimedean absolute value, in any characteristic. The finite places of a number field are the main instance; over ℤ itself the Dedekind-domain form is Mathlib's Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one.

The Gauss norm of radius c ≥ 0 of a linear factor X - C b is max c (v b). Combining these with multiplicativity: if a primitive P ∈ ℤ[X] splits as a ∏_{b ∈ s} (X - b), with roots counted with multiplicity, then v a * ∏_{b ∈ s} max 1 (v b) = 1. For the primitive minimal polynomial of an algebraic number this is the finite-place factor in the identity between the Mahler measure and the absolute Weil height; the leading coefficient must be kept, because the monic rational minimal polynomial does not satisfy the identity.

Main results

• Polynomial.gaussNorm_eq_iSup: the Gauss norm is the supremum over all weighted coefficients.
• Polynomial.gaussNorm_map_eq_one_of_contentIdeal_eq_top: a polynomial whose content ideal is the unit ideal has Gauss norm of radius one equal to 1 after mapping along φ : A →+* R, at a nonarchimedean absolute value v with v (φ a) ≤ 1 for every a : A.
• Polynomial.IsPrimitive.gaussNorm_map_eq_one: a primitive integer polynomial has Gauss norm 1 at every nonarchimedean absolute value.
• Polynomial.gaussNorm_X_sub_C: the Gauss norm of X - C b is max c (v b).
• Polynomial.gaussNorm_multiset_prod: the Gauss norm is multiplicative over finite products.
• Polynomial.IsPrimitive.mul_multiset_prod_max_one_eq_one: if a primitive integer polynomial factors as C a * ∏_{b ∈ s} (X - C b), then v a * ∏_{b ∈ s} max 1 (v b) = 1.
• Polynomial.IsPrimitive.leadingCoeff_mul_prod_roots_max_one_eq_one: the same identity over a domain in which the mapped polynomial splits, stated with its leading coefficient and roots.

References

• C. J. Smyth, The Mahler measure of algebraic numbers: a survey, §1.
• J. Wu, Heights of algebraic numbers, §3, Lemma 3.1.

theorem Polynomial.gaussNorm_eq_iSup {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (p : Polynomial R) (v : F) {c : ℝ} (hc : 0 ≤ c) : gaussNorm v c p = ⨆ (i : ℕ), v (p.coeff i) * c ^ i

A polynomial Gauss norm is the supremum over all weighted coefficients, including the zero coefficients outside its support.

@[simp]

theorem Polynomial.gaussNorm_X {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] [ZeroHomClass F R ℝ] (v : F) (c : ℝ) : gaussNorm v c X = v 1 * c

The Gauss norm of X is the value of the radius, scaled by v 1.

theorem Polynomial.gaussNorm_map_eq_one_of_contentIdeal_eq_top {R : Type u_1} [Semiring R] [Nontrivial R] {v : AbsoluteValue R ℝ} {A : Type u_2} [Semiring A] (hna : IsNonarchimedean ⇑v) (φ : A →+* R) (hφ : ∀ (a : A), v (φ a) ≤ 1) {p : Polynomial A} (hp : p.contentIdeal = ⊤) : gaussNorm v 1 (map φ p) = 1

Let φ : A →+* R and let v be a nonarchimedean absolute value on R with v (φ a) ≤ 1 for all a. If the coefficients of p ∈ A[X] generate the unit ideal, then the Gauss norm of radius one of the image of p is 1.

@[simp]

theorem Polynomial.gaussNorm_X_sub_C {R : Type u_1} [Ring R] [Nontrivial R] {v : AbsoluteValue R ℝ} {c : ℝ} (hc : 0 ≤ c) (b : R) : gaussNorm v c (X - C b) = max c (v b)

At any absolute value, the Gauss norm of radius c ≥ 0 of the linear polynomial X - C b is max c (v b).

theorem Polynomial.IsPrimitive.gaussNorm_map_eq_one {R : Type u_1} [Ring R] [Nontrivial R] {v : AbsoluteValue R ℝ} (hna : IsNonarchimedean ⇑v) {p : Polynomial ℤ} (hp : p.IsPrimitive) : gaussNorm v 1 (map (Int.castRingHom R) p) = 1

Gauss's lemma at a nonarchimedean absolute value. A primitive polynomial with integer coefficients has Gauss norm of radius one equal to 1 at every nonarchimedean absolute value, in any characteristic.

theorem Polynomial.gaussNorm_multiset_prod {R : Type u_1} [CommRing R] {v : AbsoluteValue R ℝ} {c : ℝ} [Nontrivial R] (hna : IsNonarchimedean ⇑v) (hc : 0 ≤ c) (s : Multiset (Polynomial R)) : gaussNorm v c s.prod = (Multiset.map (gaussNorm v c) s).prod

At a nonarchimedean absolute value, the Gauss norm of nonnegative radius of a finite product is the product of the Gauss norms.

theorem Polynomial.IsPrimitive.mul_multiset_prod_max_one_eq_one {R : Type u_1} [CommRing R] {v : AbsoluteValue R ℝ} [Nontrivial R] (hna : IsNonarchimedean ⇑v) {p : Polynomial ℤ} (hp : p.IsPrimitive) {a : R} {s : Multiset R} (h : map (Int.castRingHom R) p = C a * (Multiset.map (fun (b : R) => X - C b) s).prod) : v a * (Multiset.map (fun (b : R) => max 1 (v b)) s).prod = 1

If a primitive integer polynomial factors as C a * ∏_{b ∈ s} (X - C b) over R, roots counted with multiplicity, then v a * ∏_{b ∈ s} max 1 (v b) = 1 at every nonarchimedean absolute value v on R.

theorem Polynomial.IsPrimitive.leadingCoeff_mul_prod_roots_max_one_eq_one {R : Type u_1} [CommRing R] {v : AbsoluteValue R ℝ} [IsDomain R] (hna : IsNonarchimedean ⇑v) {p : Polynomial ℤ} (hp : p.IsPrimitive) (hs : (map (Int.castRingHom R) p).Splits) : v (map (Int.castRingHom R) p).leadingCoeff * (Multiset.map (fun (b : R) => max 1 (v b)) (map (Int.castRingHom R) p).roots).prod = 1

Let P be a primitive integer polynomial whose image in R[X] splits, with leading coefficient a and roots b in the domain R, counted with multiplicity. Then v a * ∏_b max 1 (v b) = 1 at every nonarchimedean absolute value v on R.