Squarefree homogenizations and the reflection

Candidates for Mathlib.Algebra.Polynomial.Homogenize: when the homogenization of a polynomial is squarefree, and the homogenization of its reflection.

Main statements

• Polynomial.homogenize_eq_homogenize_natDegree_mul: the homogenizations of p of degree n ≥ p.natDegree are that of degree p.natDegree times powers of the second variable.
• Polynomial.squarefree_of_squarefree_homogenize: over a commutative semiring without zero divisors, a polynomial with a squarefree homogenization is squarefree.
• Polynomial.squarefree_homogenize_iff: for a polynomial p over a domain and n ≥ p.natDegree, the homogenization of degree n is squarefree if and only if p is squarefree and n ≤ p.natDegree + 1.
• Polynomial.homogenize_reflect: the homogenization of degree n of the reflection of p in degree n is that of p with the two variables exchanged, for every p and n.
• Polynomial.squarefree_homogenize_reflect_iff: so the reflection does not change whether the homogenization is squarefree.
• Polynomial.squarefree_homogenize_iff_squarefree_reflect: for n ≥ p.natDegree, the homogenization of degree n of a polynomial over a domain is squarefree exactly when the reflection of p in degree n is, if n exceeds the degree of the reflection by at most one.

Proof

For n ≥ p.natDegree + 2, X 1 ^ 2 divides the homogenization (Polynomial.homogenize_eq_homogenize_natDegree_mul), and if a * a divides p, the square of the homogenization of a divides it (Polynomial.squarefree_of_squarefree_homogenize). Conversely, let A * A divide the homogenization for n ≤ p.natDegree + 1: then A is homogeneous (MvPolynomial.IsHomogeneous.of_mul_left), X 1 does not divide it, since X 1 ^ (n - p.natDegree) is the largest power of X 1 that divides the homogenization (Polynomial.not_X_one_dvd_homogenize_natDegree), and the square of its value at (X, 1) divides p, so that this value is a unit; hence A is a unit. The reflection compares the coefficients of the two homogenizations, and the exchange of the variables is a ring automorphism, which preserves squarefreeness (MulEquiv.squarefree_iff). Mathlib's file does not import squarefreeness.

theorem Polynomial.homogenize_eq_homogenize_natDegree_mul {R : Type u_1} [CommSemiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : p.homogenize n = p.homogenize p.natDegree * MvPolynomial.X 1 ^ (n - p.natDegree)

For n ≥ p.natDegree, the homogenization of degree n of p is that of degree p.natDegree times the power n - p.natDegree of the second variable.

theorem Polynomial.not_X_one_dvd_homogenize_natDegree {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p ≠ 0) : ¬MvPolynomial.X 1 ∣ p.homogenize p.natDegree

The second variable does not divide the homogenization of degree p.natDegree of a polynomial p ≠ 0: the coefficient of X 0 ^ p.natDegree there is the leading coefficient of p, while every multiple of X 1 has the coefficient 0 there.

theorem Polynomial.squarefree_of_squarefree_homogenize {R : Type u_1} [CommSemiring R] {p : Polynomial R} {n : ℕ} [NoZeroDivisors R] (hn : p.natDegree ≤ n) (h : Squarefree (p.homogenize n)) : Squarefree p

A polynomial over a commutative semiring without zero divisors is squarefree if some homogenization of it is, of degree n ≥ p.natDegree.

theorem Polynomial.homogenize_reflect {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n : ℕ) : (reflect n p).homogenize n = (MvPolynomial.rename ⇑(Equiv.swap 0 1)) (p.homogenize n)

The homogenization of degree n of the reflection of p in degree n is that of p with the two variables exchanged, for every p and n: both see only the coefficients of p up to n.

theorem Polynomial.squarefree_homogenize_reflect_iff {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n : ℕ) : Squarefree ((reflect n p).homogenize n) ↔ Squarefree (p.homogenize n)

theorem Polynomial.squarefree_homogenize_iff {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : Squarefree (p.homogenize n) ↔ Squarefree p ∧ n ≤ p.natDegree + 1

The homogenization of degree n ≥ p.natDegree of a polynomial p over a domain is squarefree if and only if p is squarefree and n exceeds the degree of p by at most one; for larger n, X 1 ^ 2 divides it.

theorem Polynomial.squarefree_homogenize_iff_squarefree_reflect {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (h : n ≤ (reflect n p).natDegree + 1) : Squarefree (p.homogenize n) ↔ Squarefree (reflect n p)

For n ≥ p.natDegree, the homogenization of degree n of a polynomial p over a domain is squarefree exactly when the reflection of p in degree n is, if n exceeds the degree of the reflection by at most one: the homogenization of degree n of the reflection is that of p with the variables exchanged (Polynomial.homogenize_reflect).