Products of polynomials in disjoint sets of variables

If P and Q involve disjoint sets of variables, no two products of a monomial of P and a monomial of Q coincide: an exponent a + b, with a supported on the variables of P and b on those of Q, determines a as its restriction to the variables of P. Hence the coefficients of P * Q are exactly the products of a coefficient of P and a coefficient of Q, with no cancellation or addition between them. This is what makes the height of such a product the product of the heights, as used in the inductive step of Roth's lemma, where a generalized Wronskian in some variables is multiplied by a Wronskian in another variable.

Main results

• MvPolynomial.injOn_add_of_disjoint_vars: the addition of exponents is injective on pairs of exponents supported on the variables of P and of Q.
• MvPolynomial.coeff_add_mul_of_disjoint_vars: (P * Q).coeff (a + b) = P.coeff a * Q.coeff b for such exponents.
• MvPolynomial.vars_rename_subset_Ioi: if f sends every variable of a above i, then every variable of rename f a lies above i.
• Polynomial.vars_toMvPolynomial_subset: a one-variable polynomial placed in the coordinate i involves at most the variable i.

theorem MvPolynomial.injOn_add_of_disjoint_vars {R : Type u_1} {σ : Type u_2} [CommSemiring R] {P Q : MvPolynomial σ R} (h : Disjoint P.vars Q.vars) : Set.InjOn (fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) => p.1 + p.2) {p : (σ →₀ ℕ) × (σ →₀ ℕ) | p.1.support ⊆ P.vars ∧ p.2.support ⊆ Q.vars}

If P and Q involve disjoint sets of variables, the sum a + b of an exponent a supported on the variables of P and an exponent b supported on the variables of Q determines a and b.

theorem MvPolynomial.coeff_add_mul_of_disjoint_vars {R : Type u_1} {σ : Type u_2} [CommSemiring R] {P Q : MvPolynomial σ R} (h : Disjoint P.vars Q.vars) {a b : σ →₀ ℕ} (ha : a.support ⊆ P.vars) (hb : b.support ⊆ Q.vars) : (P * Q).coeff (a + b) = P.coeff a * Q.coeff b

Coefficients of a product in disjoint variables. If P and Q involve disjoint sets of variables, and the exponents a and b are supported on the variables of P and of Q respectively, then the coefficient of P * Q at a + b is P.coeff a * Q.coeff b.

theorem MvPolynomial.vars_rename_subset_Ioi {R : Type u_1} {σ : Type u_2} [CommSemiring R] {τ : Type u_3} [Preorder τ] [LocallyFiniteOrderTop τ] (f : σ → τ) {a : MvPolynomial σ R} {i : τ} (h : ∀ j ∈ a.vars, i < f j) : ((rename f) a).vars ⊆ Finset.Ioi i

If f sends every variable of a above i, then every variable of rename f a lies above i.

theorem Polynomial.vars_toMvPolynomial_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : Polynomial R) (i : σ) : ((toMvPolynomial i) p).vars ⊆ {i}

A one-variable polynomial placed in the coordinate i involves at most the variable i.