Reconstructing ambient orders from a squarefree basis

A squarefree basis, in particular an irreducible basis, reconstructs each input polynomial as its content, a unit, and a product of powers of basis members. Over a polynomial coefficient ring over a domain, the unit has order zero, so the ambient Taylor order of the input is the order of its content plus the weighted sum of the orders of its basis factors. Thus constant ambient orders for the content and basis transfer to the input family.

The distinguished variable is coordinate zero, through MvPolynomial.finSuccEquiv. The content is evaluated at the remaining coordinates. The statements include zero inputs, vanishing contents, and empty bases. Orders are ambient Taylor orders, including infinity for the zero polynomial; no restriction to a cell is taken before computing them.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268, Sections 2–3 (basis preprocessing and order-invariance).

theorem Finset.IsSquarefreeBasis.exists_orderAt_eq_content_add_sum {R : Type u_1} [CommRing R] {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [IsDomain R] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) : ∃ (e : Polynomial (MvPolynomial (Fin n) R) → ℕ), ∀ (a : Fin (n + 1) → R), ((MvPolynomial.finSuccEquiv R n).symm f).orderAt a = f.content.orderAt (Fin.tail a) + ∑ b ∈ B, e b • ((MvPolynomial.finSuccEquiv R n).symm b).orderAt a

The ambient order of an input is the order of its content plus the sum of the orders of the basis factors, weighted by their exponents in its factorization. The same exponents work at every point, including where the content vanishes.

theorem Finset.IsSquarefreeBasis.orderAt_eq {R : Type u_1} [CommRing R] {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [IsDomain R] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) {a a' : Fin (n + 1) → R} (hc : f.content.orderAt (Fin.tail a) = f.content.orderAt (Fin.tail a')) (hb : ∀ b ∈ B, ((MvPolynomial.finSuccEquiv R n).symm b).orderAt a = ((MvPolynomial.finSuccEquiv R n).symm b).orderAt a') : ((MvPolynomial.finSuccEquiv R n).symm f).orderAt a = ((MvPolynomial.finSuccEquiv R n).symm f).orderAt a'

Constant ambient orders for the content and basis factors imply constant ambient order for each input polynomial. No connectedness assumption is needed.