Transverse plane slices preserving ambient order

Keep coordinate zero as a free root coordinate and restrict the remaining coordinates to an affine line. One base direction can be chosen so that these plane restrictions preserve ambient order for finitely many polynomial–point pairs. The points and polynomials need not be distinct, and zero polynomials are included.

This permits ambient order along polynomial root sections to be calculated using two-variable slices, while retaining the distinguished root coordinate. In particular, one direction can test a discriminant at a base point and the original polynomial at each of its finitely many roots above that point. Preservation at those points is a conclusion; preservation at other points is not asserted.

The plane coordinates are (line parameter, root coordinate), so that the slice is centered at ![0, a 0] and evaluates to p(z, Fin.tail a + y • v) at ![y, z]. Fixing the line parameter y recovers the fiber of p over Fin.tail a + y • v as a univariate polynomial in the root coordinate. Shifting the root coordinate by a 0 moves the center of the slice to the origin.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (ambient order and delineability).

theorem MvPolynomial.eval_aeval_finCons_C_add_C_mul_X {R : Type u_1} {n : ℕ} [CommSemiring R] (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin n → R) (y z : R) : (eval ![y, z]) ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p) = (eval (Fin.cons z (a + y • v))) p

Evaluation of a transverse plane restriction keeps the root coordinate free and moves the base along an affine line.

theorem MvPolynomial.aeval_C_X_aeval_finCons_C_add_C_mul_X {R : Type u_1} {n : ℕ} [CommSemiring R] (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin n → R) (s : R) : (aeval ![Polynomial.C s, Polynomial.X]) ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p) = Polynomial.map (eval (a + s • v)) ((finSuccEquiv R n) p)

Restricting a transverse plane slice to the root-coordinate line at line parameter s gives the fiber of the polynomial over the base point a + s • v.

theorem MvPolynomial.map_aeval_finCons_C_add_C_mul_X {R : Type u_1} {n : ℕ} [CommSemiring R] {S : Type u_2} [CommSemiring S] (φ : R →+* S) (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin n → R) : (map φ) ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p) = (aeval (Fin.cons (X 1) fun (j : Fin n) => C (φ (a j)) + C (φ (v j)) * X 0)) ((map φ) p)

Transverse plane slices commute with coefficient maps, with the base point and direction mapped along the same homomorphism.

theorem MvPolynomial.orderAt_map_aeval_finCons_C_add_C_mul_X {R : Type u_1} {n : ℕ} [CommSemiring R] {S : Type u_2} [CommSemiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin n → R) (t : R) : ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (φ (a j)) + C (φ (v j)) * X 0)) ((map φ) p)).orderAt ![0, φ t] = ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p).orderAt ![0, t]

Mapping the coefficients along an injective ring homomorphism commutes with taking the order of a transverse plane slice at a point of the root-coordinate line.

theorem MvPolynomial.orderAt_aeval_finCons_C_add_X {R : Type u_1} {n : ℕ} [CommSemiring R] (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin n → R) (t : R) : ((aeval (Fin.cons (C t + X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p).orderAt 0 = ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j) + C (v j) * X 0)) p).orderAt ![0, t]

Centering a transverse plane slice at the root coordinate t turns its order at ![0, t] into the order at the origin of the slice with X 1 shifted by t.

theorem MvPolynomial.orderAt_aeval_finCons_C_add_C_mul_X_eq {R : Type u_1} {n : ℕ} [CommRing R] (p : MvPolynomial (Fin (n + 1)) R) (a v : Fin (n + 1) → R) (hv : ((aeval fun (j : Fin (n + 1)) => Polynomial.C (a j) + Polynomial.C (v j) * Polynomial.X) p).trailingDegree = p.orderAt a) : ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a j.succ) + C (v j.succ) * X 0)) p).orderAt ![0, a 0] = p.orderAt a

If an affine line detects ambient order, the plane containing that line and the distinguished coordinate also detects it. This statement allows infinite order.

theorem MvPolynomial.exists_forall_orderAt_aeval_finCons_C_add_C_mul_X_eq {R : Type u_1} {n : ℕ} [CommRing R] [IsDomain R] [Infinite R] {ι : Type u_2} (s : Finset ι) (p : ι → MvPolynomial (Fin (n + 1)) R) (a : ι → Fin (n + 1) → R) : ∃ (v : Fin n → R), ∀ i ∈ s, ((aeval (Fin.cons (X 1) fun (j : Fin n) => C (a i j.succ) + C (v j) * X 0)) (p i)).orderAt ![0, a i 0] = (p i).orderAt (a i)

A single base direction gives transverse plane restrictions preserving ambient order for finitely many polynomial–point pairs over an infinite domain. Coordinate zero remains free. Zero polynomials retain infinite order, and an empty family is allowed.