Homogenize a univariate polynomial

In this file we define a function Polynomial.homogenize p n that takes a polynomial p and a natural number n and returns a homogeneous bivariate polynomial of degree n.

If n is at least the degree of p, then (homogenize p n).eval ![x, 1] = p.eval x.

We use MvPolynomial (Fin 2) R to represent bivariate polynomials instead of R[X][Y] (i.e., Polynomial (Polynomial R)), because Mathlib has a theory about homogeneous multivariate polynomials, but not about homogeneous bivariate polynomials encoded as R[X][Y].

noncomputable def Polynomial.homogenize {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n : ℕ) : MvPolynomial (Fin 2) R

Given a polynomial p and a number n ≥ natDegree p, returns a homogeneous bivariate polynomial q of degree n such that q(x, 1) = p(x).

It is defined as ∑ k + l = n, a_k X_0^k X_1^l, where a_k is the kth coefficient of p.

@[simp]

theorem Polynomial.homogenize_zero {R : Type u_1} [CommSemiring R] (n : ℕ) : homogenize 0 n = 0

@[simp]

theorem Polynomial.homogenize_add {R : Type u_1} [CommSemiring R] (p q : Polynomial R) (n : ℕ) : (p + q).homogenize n = p.homogenize n + q.homogenize n

@[simp]

theorem Polynomial.homogenize_smul {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Module S R] (c : S) (p : Polynomial R) (n : ℕ) : (c • p).homogenize n = c • p.homogenize n

noncomputable def Polynomial.homogenizeLM {R : Type u_1} [CommSemiring R] (n : ℕ) : Polynomial R →ₗ[R] MvPolynomial (Fin 2) R

homogenize as a bundled linear map.

@[simp]

theorem Polynomial.homogenizeLM_apply {R : Type u_1} [CommSemiring R] (n : ℕ) (p : Polynomial R) : (homogenizeLM n) p = p.homogenize n

@[simp]

theorem Polynomial.homogenize_finsetSum {R : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (p : ι → Polynomial R) (n : ℕ) : (∑ i ∈ s, p i).homogenize n = ∑ i ∈ s, (p i).homogenize n

theorem Polynomial.homogenize_map {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ) : (map f p).homogenize n = (MvPolynomial.map f) (p.homogenize n)

@[simp]

theorem Polynomial.homogenize_C_mul {R : Type u_1} [CommSemiring R] (c : R) (p : Polynomial R) (n : ℕ) : (C c * p).homogenize n = MvPolynomial.C c * p.homogenize n

@[simp]

theorem Polynomial.homogenize_monomial {R : Type u_1} [CommSemiring R] {m n : ℕ} (h : m ≤ n) (r : R) : ((monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

theorem Polynomial.homogenize_monomial_of_lt {R : Type u_1} [CommSemiring R] {m n : ℕ} (h : n < m) (r : R) : ((monomial m) r).homogenize n = 0

@[simp]

theorem Polynomial.homogenize_X_pow {R : Type u_1} [CommSemiring R] {m n : ℕ} (h : m ≤ n) : (X ^ m).homogenize n = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

@[simp]

theorem Polynomial.homogenize_X {R : Type u_1} [CommSemiring R] {n : ℕ} (hn : n ≠ 0) : X.homogenize n = MvPolynomial.X 0 * MvPolynomial.X 1 ^ (n - 1)

@[simp]

theorem Polynomial.homogenize_C {R : Type u_1} [CommSemiring R] (c : R) (n : ℕ) : (C c).homogenize n = MvPolynomial.C c * MvPolynomial.X 1 ^ n

@[simp]

theorem Polynomial.homogenize_one {R : Type u_1} [CommSemiring R] (n : ℕ) : homogenize 1 n = MvPolynomial.X 1 ^ n

theorem Polynomial.coeff_homogenize {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n : ℕ) (m : Fin 2 →₀ ℕ) : MvPolynomial.coeff m (p.homogenize n) = if m 0 + m 1 = n then p.coeff (m 0) else 0

theorem Polynomial.eq_zero_of_homogenize_eq_zero {R : Type u_1} [CommSemiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (h : p.homogenize n = 0) : p = 0

theorem Polynomial.homogenize_eq_zero_iff {R : Type u_1} [CommSemiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : p.homogenize n = 0 ↔ p = 0

theorem Polynomial.eval₂_homogenize_of_eq_one {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (f : R →+* S) (g : Fin 2 → S) (hg : g 1 = 1) : MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p

theorem Polynomial.aeval_homogenize_of_eq_one {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (g : Fin 2 → A) (hg : g 1 = 1) : (MvPolynomial.aeval g) (p.homogenize n) = (aeval (g 0)) p

@[simp]

theorem Polynomial.aeval_homogenize_X_one {R : Type u_1} [CommSemiring R] (p : Polynomial R) {n : ℕ} (hn : p.natDegree ≤ n) : (MvPolynomial.aeval ![X, 1]) (p.homogenize n) = p

If deg p ≤ n, then homogenize p n (x, 1) = p x.

@[simp]

theorem Polynomial.isHomogeneous_homogenize {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (p.homogenize n).IsHomogeneous n

theorem Polynomial.homogenize_eq_of_isHomogeneous {R : Type u_1} [CommSemiring R] {p : Polynomial R} {n : ℕ} {q : MvPolynomial (Fin 2) R} (hq : q.IsHomogeneous n) (hpq : (MvPolynomial.aeval ![X, 1]) q = p) : p.homogenize n = q

theorem Polynomial.homogenize_mul {R : Type u_1} [CommSemiring R] (p q : Polynomial R) {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) : (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n

theorem Polynomial.homogenize_finsetProd {R : Type u_1} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {p : ι → Polynomial R} {n : ι → ℕ} (h : ∀ i ∈ s, (p i).natDegree ≤ n i) : (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)

theorem Polynomial.homogenize_dvd {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {p q : Polynomial R} (h : p ∣ q) : p.homogenize p.natDegree ∣ q.homogenize q.natDegree

@[simp]

theorem Polynomial.homogenize_neg {R : Type u_1} [CommRing R] (p : Polynomial R) (n : ℕ) : (-p).homogenize n = -p.homogenize n

@[simp]

theorem Polynomial.homogenize_sub {R : Type u_1} [CommRing R] (p q : Polynomial R) (n : ℕ) : (p - q).homogenize n = p.homogenize n - q.homogenize n

theorem Polynomial.eval_homogenize {K : Type u_1} [Semifield K] {p : Polynomial K} {n : ℕ} (hn : p.natDegree ≤ n) (x : Fin 2 → K) (hx : x 1 ≠ 0) : (MvPolynomial.eval x) (p.homogenize n) = eval (x 0 / x 1) p * x 1 ^ n

noncomputable def Polynomial.toTupleMvPolynomial {R : Type u_1} [CommSemiring R] (p : Polynomial R) : Fin 2 → MvPolynomial (Fin 2) R

Given a polynomial p : R[X], this is the vector ![p₀, p₁] of homogeneous bivariate polynomials of degree p.natDegree such that p(x) = p₀(x,1)/p₁(x,1) and p₁ is a monomial.

theorem Polynomial.toTupleMvPolynomial_zero_eq {R : Type u_1} [CommSemiring R] (p : Polynomial R) : p.toTupleMvPolynomial 0 = p.homogenize p.natDegree

theorem Polynomial.toTupleMvPolynomial_one_eq {R : Type u_1} [CommSemiring R] (p : Polynomial R) : p.toTupleMvPolynomial 1 = MvPolynomial.X 1 ^ p.natDegree

theorem Polynomial.isHomogenous_toTupleMvPolynomial {R : Type u_1} [CommSemiring R] (p : Polynomial R) (i : Fin 2) : (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree

theorem Polynomial.eval_X_toTupleMvPolynomial_zero_eq {R : Type u_1} [CommSemiring R] (p : Polynomial R) : (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 0) = p * (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 1)

theorem Polynomial.eval_eq_div_eval_toTupleMvPolynomial {R : Type u_2} [Field R] (p : Polynomial R) (x : R) : eval x p = (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 0) / (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 1)

theorem Polynomial.sum_eq_natDegree_of_mem_support_homogenize {R : Type u_1} [CommSemiring R] (p : Polynomial R) {s : Fin 2 →₀ ℕ} (hs : s ∈ (p.homogenize p.natDegree).support) : s 0 + s 1 = p.natDegree

theorem Polynomial.finsuppSum_homogenize_eq {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] (p : Polynomial R) {f : R → M} : (Finsupp.sum (p.homogenize p.natDegree) fun (x : Fin 2 →₀ ℕ) (c : R) => f c) = p.sum fun (x : ℕ) (c : R) => f c

Summing a function over the coefficients of the homogenization of a polynomial p (of degree p.natDegree) gives the same result as summing over the coefficients of p.