Detecting ambient order along affine lines

For a polynomial of finite ambient order at a point over an infinite domain, there is a direction along which its restriction has exactly that order. The coefficient of degree m on a line is the value of the degree-m homogeneous Taylor component at the direction. Thus the good directions are detected by a nonzero polynomial, rather than assumed to exist.

These coefficient formulas supply the algebraic input for choosing uniform directions in families of constant ambient order, and hence for analytic preparation of discriminants.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), Sections 2–3.

theorem MvPolynomial.aeval_C_mul_X_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (v : σ → R) (d : σ →₀ ℕ) (r : R) : (aeval fun (i : σ) => Polynomial.C (v i) * Polynomial.X) ((monomial d) r) = (Polynomial.monomial (Finsupp.degree d)) ((eval v) ((monomial d) r))

Restriction to a line through the origin sends a monomial to a monomial of its total degree, with coefficient given by evaluation at the direction.

@[simp]

theorem MvPolynomial.coeff_aeval_C_mul_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (v : σ → R) (m : ℕ) : ((aeval fun (i : σ) => Polynomial.C (v i) * Polynomial.X) p).coeff m = (eval v) ((homogeneousComponent m) p)

The coefficient of a line restriction is the homogeneous component evaluated at its direction.

theorem MvPolynomial.aeval_C_add_C_mul_X_eq {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (a v : σ → R) : (aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p = (aeval fun (i : σ) => Polynomial.C (v i) * Polynomial.X) ((taylor a) p)

Translating the polynomial first gives the restriction to an affine line.

@[simp]

theorem MvPolynomial.eval_aeval_C_add_C_mul_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (a v : σ → R) (t : R) : Polynomial.eval t ((aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p) = (eval (a + t • v)) p

Evaluation of the affine-line restriction is evaluation at the corresponding point.

@[simp]

theorem MvPolynomial.coeff_aeval_C_add_C_mul_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (a v : σ → R) (m : ℕ) : ((aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p).coeff m = (eval v) ((homogeneousComponent m) ((taylor a) p))

The coefficients of an affine-line restriction are the homogeneous Taylor components evaluated at the direction.

theorem MvPolynomial.coeff_aeval_C_add_C_mul_X_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (a v : σ → R) {m : ℕ} (hm : ↑m < p.orderAt a) : ((aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p).coeff m = 0

Terms below the ambient order vanish in every affine-line restriction.

theorem MvPolynomial.exists_natTrailingDegree_aeval_C_add_C_mul_X_eq {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [Infinite R] (p : MvPolynomial σ R) (a : σ → R) {m : ℕ} (hm : p.orderAt a = ↑m) : ∃ (v : σ → R), (aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p ≠ 0 ∧ ((aeval fun (i : σ) => Polynomial.C (a i) + Polynomial.C (v i) * Polynomial.X) p).natTrailingDegree = m

A polynomial of ambient order m admits a line restriction that is nonzero and has order exactly m at the line parameter zero.