Ambient order in reciprocal polynomial coordinates

For a polynomial family p in one distinguished variable, reflection at a fixed degree bound represents z ^ N * p(x, z⁻¹). Away from z = 0, reciprocal coordinates preserve ambient polynomial order. This compares the order in all variables, rather than only the multiplicity of a root in a fiber. It allows section-order conclusions in reciprocal coordinates to be transported back to the original polynomial family.

The bound is chosen before specialization: no preservation of the fiber degree is required. Reversal is the specialization to the formal degree of the family.

Integral normalization also preserves ambient order, once the distinguished coordinate is rescaled by the leading coefficient at base points where that coefficient does not vanish. Translating to a center τ, reversing and normalizing turns a family whose leading coefficient may vanish into a monic one: the translated reversal has leading coefficient the value p(τ), and integral normalization then makes it monic. Ambient orders of the monic family at the image of a point (t, x) with t ≠ τ and p(τ)(x) ≠ 0 are the ambient orders of p at (t, x).

Main results

• Polynomial.orderAt_reflect, Polynomial.orderAt_reverse: reciprocal coordinates preserve ambient order.
• Polynomial.orderAt_integralNormalization: integral normalization preserves ambient order after rescaling the distinguished coordinate by the leading coefficient.
• Polynomial.orderAt_integralNormalization_reverse_comp_X_add_C: normalized reciprocal coordinates centered at τ preserve ambient order.

References

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

@[simp]

theorem Polynomial.orderAt_reflect {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n N : ℕ} (p : Polynomial (MvPolynomial (Fin n) 𝕜)) (hN : p.natDegree ≤ N) (a : Fin n → 𝕜) {z : 𝕜} (hz : z ≠ 0) : ((MvPolynomial.finSuccEquiv 𝕜 n).symm (reflect N p)).orderAt (Fin.cons z⁻¹ a) = ((MvPolynomial.finSuccEquiv 𝕜 n).symm p).orderAt (Fin.cons z a)

Reflection at a fixed bound preserves the ambient order at reciprocal nonzero coordinates. The bound concerns the formal polynomial, not its specialized fibers.

@[simp]

theorem Polynomial.orderAt_reverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (p : Polynomial (MvPolynomial (Fin n) 𝕜)) (a : Fin n → 𝕜) {z : 𝕜} (hz : z ≠ 0) : ((MvPolynomial.finSuccEquiv 𝕜 n).symm p.reverse).orderAt (Fin.cons z⁻¹ a) = ((MvPolynomial.finSuccEquiv 𝕜 n).symm p).orderAt (Fin.cons z a)

Reversing a polynomial family preserves ambient order under inversion of its nonzero distinguished coordinate, even when the fiber degree drops.

@[simp]

theorem Polynomial.orderAt_integralNormalization {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (p : Polynomial (MvPolynomial (Fin n) 𝕜)) {a : Fin n → 𝕜} (ha : (MvPolynomial.eval a) p.leadingCoeff ≠ 0) (z : 𝕜) : ((MvPolynomial.finSuccEquiv 𝕜 n).symm p.integralNormalization).orderAt (Fin.cons ((MvPolynomial.eval a) p.leadingCoeff * z) a) = ((MvPolynomial.finSuccEquiv 𝕜 n).symm p).orderAt (Fin.cons z a)

Integral normalization preserves ambient order when its distinguished coordinate is rescaled by the leading coefficient: at a base point a where the leading coefficient of p does not vanish, the order of p.integralNormalization at (p.leadingCoeff(a) * z, a) is the order of p at (z, a).

@[simp]

theorem Polynomial.orderAt_integralNormalization_reverse_comp_X_add_C {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (p : Polynomial (MvPolynomial (Fin n) 𝕜)) {τ : 𝕜} {a : Fin n → 𝕜} (ha : (MvPolynomial.eval a) (eval (MvPolynomial.C τ) p) ≠ 0) {t : 𝕜} (ht : t ≠ τ) : ((MvPolynomial.finSuccEquiv 𝕜 n).symm (p.comp (X + C (MvPolynomial.C τ))).reverse.integralNormalization).orderAt (Fin.cons ((MvPolynomial.eval a) (eval (MvPolynomial.C τ) p) * (t - τ)⁻¹) a) = ((MvPolynomial.finSuccEquiv 𝕜 n).symm p).orderAt (Fin.cons t a)

Normalized reciprocal coordinates centered at τ preserve ambient order. If the value c = p(τ) of the family does not vanish at the base point a, then the normalized reversal (p.comp (X + C τ)).reverse.integralNormalization has order at (c(a) / (t - τ), a) equal to the order of p at (t, a), for every t ≠ τ.