Constant ambient order passes to polynomial factors

Taylor coefficients vary continuously with their center, so the ambient order of a fixed polynomial cannot increase near a point. Over a domain, orders add on products. If a nonzero product has constant order along a continuous parametrization, neither factor can lose order locally, because the other factor cannot gain it. Each factor therefore has locally constant order, and constant order on a preconnected parameter set.

The nonzero-product hypothesis is essential: a zero product has infinite order everywhere and gives no information about the orders of its factors. Zero polynomials are nevertheless included in the local upper bound.

These results complement additivity of ambient order: on a preconnected set, a nonzero product is order-invariant exactly when its factors are. In particular, constant product order gives constant factor orders, which imply sign-invariance of the factors over a linearly ordered topological ring. A continuous root section is another possible parametrization. The order is computed in all polynomial variables, rather than in a specialized univariate fiber.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), pp. 242–268, the product order-invariance lemma. IsPreconnected.orderAt_eq_of_prod generalizes its product-to-factors implication to continuous parametrizations over topological domains.

theorem MvPolynomial.continuous_coeff_taylor {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : MvPolynomial σ R) (d : σ →₀ ℕ) : Continuous fun (a : σ → R) => ((taylor a) p).coeff d

Each Taylor coefficient of a fixed polynomial depends continuously on the center.

theorem MvPolynomial.eventually_orderAt_le {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] (p : MvPolynomial σ R) (a : σ → R) : ∀ᶠ (b : σ → R) in nhds a, p.orderAt b ≤ p.orderAt a

Near any center, the ambient order of a polynomial is at most its order at that center. This includes the zero polynomial, whose order is infinite.

theorem MvPolynomial.eventually_orderAt_eq_of_dvd {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [NoZeroDivisors R] [T1Space R] {Y : Type u_3} {l : Filter Y} {f : Y → σ → R} {a : σ → R} (p : MvPolynomial σ R) {q : MvPolynomial σ R} (hq : q ≠ 0) (hpq : p ∣ q) (hf : Filter.Tendsto f l (nhds a)) (horder : ∀ᶠ (y : Y) in l, q.orderAt (f y) = q.orderAt a) : ∀ᶠ (y : Y) in l, p.orderAt (f y) = p.orderAt a

Along a parametrization tending to a, a divisor of a nonzero polynomial has eventually constant ambient order whenever the ambient order of the polynomial is eventually constant.

theorem MvPolynomial.orderAt_eq_of_dvd {σ : Type u_1} {R : Type u_2} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [NoZeroDivisors R] [T1Space R] {Y : Type u_3} {f : Y → σ → R} (p : MvPolynomial σ R) {q : MvPolynomial σ R} (hq : q ≠ 0) (hpq : p ∣ q) [TopologicalSpace Y] {S : Set Y} (hS : IsPreconnected S) (hf : ContinuousOn f S) (horder : ∀ x ∈ S, ∀ y ∈ S, q.orderAt (f x) = q.orderAt (f y)) {x y : Y} (hx : x ∈ S) (hy : y ∈ S) : p.orderAt (f x) = p.orderAt (f y)

On a preconnected parameter set, a divisor of a nonzero polynomial has constant ambient order if the polynomial has constant ambient order. The centers may be any continuous parametrization, including a moving root section.

theorem IsPreconnected.orderAt_eq_of_prod {σ : Type u_1} {R : Type u_2} {Y : Type u_3} {ι : Type u_4} [CommSemiring R] [NoZeroDivisors R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] [TopologicalSpace Y] {S : Set Y} (hS : IsPreconnected S) (p : ι → MvPolynomial σ R) (s : Finset ι) {f : Y → σ → R} (hprod : ∏ i ∈ s, p i ≠ 0) (hf : ContinuousOn f S) (horder : ∀ x ∈ S, ∀ y ∈ S, (∏ i ∈ s, p i).orderAt (f x) = (∏ i ∈ s, p i).orderAt (f y)) {i : ι} (hi : i ∈ s) {x y : Y} (hx : x ∈ S) (hy : y ∈ S) : (p i).orderAt (f x) = (p i).orderAt (f y)

Constant finite ambient order of a polynomial product on a preconnected parameter set implies constant ambient order of every factor. Repeated factors and the empty product are allowed, but the product must be nonzero.