Separating one variable of a multivariate polynomial

Over a field K, every polynomial P ∈ K[X_σ] can be written, for a chosen variable Xᵢ, as

P = ∑_{k < m} fₖ · gₖ(Xᵢ)

where the fₖ do not involve Xᵢ, the gₖ are one-variable polynomials, both families are linearly independent over K, and m ≤ deg_{Xᵢ} P + 1. Moreover the fₖ have partial degrees at most those of P and the gₖ have degree at most deg_{Xᵢ} P.

This is the separation of variables in the proof of Roth's lemma: for rows D k that do not differentiate in Xᵢ, the determinant of the Hasse derivatives ∂^(D k + l eᵢ) P factors as the generalized Wronskian of the fₖ times the one-variable Wronskian of the gₖ (MvPolynomial.det_hasseDeriv_sum_mul_toMvPolynomial). Over a field of characteristic zero, the linear independence of the fₖ gives admissible rows D with W_D(f) ≠ 0, and the linear independence of the gₖ makes their Hasse Wronskian nonzero.

Main results

• MvPolynomial.exists_eq_sum_mul_X_pow: the expansion P = ∑_{j ≤ deg_{Xᵢ} P} Qⱼ · Xᵢ ^ j with coefficients Qⱼ free of Xᵢ, over any commutative semiring.
• MvPolynomial.exists_sum_mul_linearIndependent: the separated expression of P in the variable Xᵢ, with both families linearly independent.

Implementation notes

Write P = ∑_{j ≤ N} Qⱼ Xᵢ ^ j with Qⱼ free of Xᵢ, where N = deg_{Xᵢ} P. The fₖ are a basis of the span of the Qⱼ, and gₖ = ∑ⱼ cⱼₖ X ^ j (built with Polynomial.ofFn) where cⱼₖ is the k-th coordinate of Qⱼ. A linear relation among the gₖ gives a linear form on the span vanishing on every Qⱼ, hence identically, which forces the relation to be trivial.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (version of 17 January 2022), §3.3, Lemma 3.3.8.

theorem TauCeti.sum_mul_X_pow_eq_sum_mul_toMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] {r N : ℕ} (i : σ) (Q : Fin N → MvPolynomial σ R) (b : Fin r → MvPolynomial σ R) (c : Fin N → Fin r → R) (hQb : ∀ (j : Fin N), Q j = ∑ k : Fin r, c j k • b k) : ∑ j : Fin N, Q j * MvPolynomial.X i ^ ↑j = ∑ k : Fin r, b k * (Polynomial.toMvPolynomial i) ((Polynomial.ofFn N) fun (j : Fin N) => c j k)

Rewriting ∑ⱼ Qⱼ Xᵢʲ along the expansions Qⱼ = ∑ₖ cⱼₖ bₖ of the coefficients in a family b, as ∑ₖ bₖ · gₖ(Xᵢ) with gₖ = ∑ⱼ cⱼₖ Tʲ.

theorem MvPolynomial.exists_eq_sum_mul_X_pow {R : Type u_1} {σ : Type u_3} [CommSemiring R] (P : MvPolynomial σ R) (i : σ) : ∃ (Q : ℕ → MvPolynomial σ R), (∀ (j : ℕ), i ∉ (Q j).vars ∧ ∀ (k : σ), degreeOf k (Q j) ≤ degreeOf k P) ∧ P = ∑ j ∈ Finset.range (degreeOf i P + 1), Q j * X i ^ j

Expansion of P in powers of the variable Xᵢ: P = ∑_{j ≤ deg_{Xᵢ} P} Qⱼ · Xᵢ ^ j, where the coefficients Qⱼ do not involve Xᵢ and have partial degrees at most those of P.

theorem MvPolynomial.exists_sum_mul_linearIndependent {K : Type u_2} {σ : Type u_3} [Field K] (P : MvPolynomial σ K) (i : σ) : ∃ m ≤ degreeOf i P + 1, ∃ (f : Fin m → MvPolynomial σ K) (g : Fin m → Polynomial K), LinearIndependent K f ∧ LinearIndependent K g ∧ (∀ (k : Fin m), i ∉ (f k).vars) ∧ (∀ (k : Fin m) (j : σ), degreeOf j (f k) ≤ degreeOf j P) ∧ (∀ (k : Fin m), (g k).natDegree ≤ degreeOf i P) ∧ P = ∑ k : Fin m, f k * (Polynomial.toMvPolynomial i) (g k)

Separation of one variable (Pottmeyer, Lemma 3.3.8). Over a field, a polynomial P is a sum ∑_{k < m} fₖ · gₖ(Xᵢ) of m ≤ deg_{Xᵢ} P + 1 products, where the fₖ are linearly independent and do not involve Xᵢ, and the gₖ are linearly independent one-variable polynomials. The fₖ have partial degrees at most those of P, and the gₖ have degree at most deg_{Xᵢ} P.