Delineating sets over a point

Let f be a polynomial in the variables X 0, …, X n, with X 0 the distinguished variable, and let α be a point of the base R ^ n. The ordinary fibre of f over α is the univariate polynomial t ↦ f(t, α), obtained by mapping MvPolynomial.finSuccEquiv R n f along evaluation at α. When the fibre is zero, f is nullified over α. Its roots then say nothing about the order of vanishing of f along the line {α} × R, which can still vary. For X 1 * X 0 + X 2 ^ 2 over the origin of ℝ ^ 2, the fibre is zero, but the order is 2 at the origin of ℝ ^ 3 and 1 at every other point of the line (TauCeti.exists_forall_eval_eq_zero_orderAt_ne).

The delineating set f.delineatingSet α repairs this. It consists of the nonzero fibres over α of all iterated partial derivatives of f, in all variables, of order at most the total degree of f. By the derivative characterization of the order (MvPolynomial.le_orderAt_iff_eval_foldl_pderiv), the order of f at (t, α) depends only on which members of the delineating set vanish at t. Hence it is the same at all points t that are roots of no member, and refining the line at the finitely many roots of the delineating set cuts it into a point for each root and open intervals, on each of which f has constant order. When the fibre itself is nonzero, it belongs to the delineating set, so the refinement also separates its roots.

This is the treatment of nullification over zero-dimensional cells in McCallum's projection theory: there the lifting over such a cell refines the fibre at the roots of the delineating set, so that the order of the nullified polynomial is constant on each cell above it.

Main definitions

• MvPolynomial.delineatingSet: the nonzero fibres over a point of the iterated partial derivatives of f up to its total degree.

Main results

• MvPolynomial.orderAt_cons_eq_of_eval_eq_zero_iff: the order of f at (t, α) is determined by which members of the delineating set vanish at t.
• MvPolynomial.orderAt_eq_of_mem_stackCells: over the point α, f has constant order on each cell of any stack whose sections include every root of the delineating set.
• MvPolynomial.exists_strictMono_orderAt_eq_of_mem_stackCells: the roots of the delineating set define such a finite stack.
• TauCeti.exists_forall_eval_eq_zero_orderAt_ne: the ordinary fibre alone does not determine the order.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), pp. 242–268.
• C. W. Brown, The McCallum projection, lifting, and order-invariance, technical report USNA-CS-TR-2005-02, U.S. Naval Academy (2005).

noncomputable def MvPolynomial.delineatingSet {R : Type u_1} [CommRing R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (α : Fin n → R) : Finset (Polynomial R)

The delineating set of f over the point α of the base: the nonzero fibres over α of the iterated partial derivatives of f, in all variables, of order at most the total degree of f. The fibre of g over α is the univariate polynomial t ↦ g(t, α), that is, (finSuccEquiv R n g).map (eval α).

theorem MvPolynomial.mem_delineatingSet {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} {q : Polynomial R} : q ∈ f.delineatingSet α ↔ q ≠ 0 ∧ ∃ (l : List (Fin (n + 1))), l.length ≤ f.totalDegree ∧ Polynomial.map (eval α) ((finSuccEquiv R n) (List.foldl (fun (q : MvPolynomial (Fin (n + 1)) R) (i : Fin (n + 1)) => (pderiv i) q) f l)) = q

The members of the delineating set of f over α are the nonzero fibres over α of the iterated partial derivatives of f along lists of at most f.totalDegree variables.

theorem MvPolynomial.map_finSuccEquiv_mem_delineatingSet {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} (h : Polynomial.map (eval α) ((finSuccEquiv R n) f) ≠ 0) : Polynomial.map (eval α) ((finSuccEquiv R n) f) ∈ f.delineatingSet α

A nonzero fibre of f itself belongs to the delineating set.

theorem MvPolynomial.orderAt_cons_eq_of_eval_eq_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} [IsAddTorsionFree R] {t t' : R} (h : ∀ q ∈ f.delineatingSet α, Polynomial.eval t q = 0 ↔ Polynomial.eval t' q = 0) : f.orderAt (Fin.cons t α) = f.orderAt (Fin.cons t' α)

The order of f at the point (t, α) depends only on which members of the delineating set of f over α vanish at t.

theorem MvPolynomial.orderAt_cons_eq_of_not_isRoot {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} [IsAddTorsionFree R] {t t' : R} (ht : ∀ q ∈ f.delineatingSet α, ¬q.IsRoot t) (ht' : ∀ q ∈ f.delineatingSet α, ¬q.IsRoot t') : f.orderAt (Fin.cons t α) = f.orderAt (Fin.cons t' α)

Away from the roots of the delineating set of f over α, the order of f along the line over α is constant.

theorem MvPolynomial.orderAt_eq_of_mem_stackCells {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} [IsAddTorsionFree R] [LinearOrder R] {k : ℕ} {c : Fin k → R} (hc : ∀ q ∈ f.delineatingSet α, ∀ (t : R), q.IsRoot t → t ∈ Set.range c) {E : Set (Fin (n + 1) → R)} (hE : E ∈ TauCeti.stackCells {α} fun (i : Fin k) (x : ↑{α}) => c i) {y y' : Fin (n + 1) → R} (hy : y ∈ E) (hy' : y' ∈ E) : f.orderAt y = f.orderAt y'

Over the point α, f has constant order on each cell of the stack cut out by points c i of the line, provided every root of every member of the delineating set of f over α is one of the c i. The points c i may include further roots, for instance those of other polynomials of a family.

theorem MvPolynomial.exists_strictMono_orderAt_eq_of_mem_stackCells {R : Type u_1} [CommRing R] {n : ℕ} [IsAddTorsionFree R] [LinearOrder R] [IsDomain R] (f : MvPolynomial (Fin (n + 1)) R) (α : Fin n → R) : ∃ (k : ℕ) (c : Fin k → R), StrictMono c ∧ (∀ (i : Fin k), ∃ q ∈ f.delineatingSet α, q.IsRoot (c i)) ∧ ∀ E ∈ TauCeti.stackCells {α} fun (i : Fin k) (x : ↑{α}) => c i, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'

Refinement of a nullified fibre. Over a domain, the roots of the members of the delineating set of f over α are finitely many points c₀ < … < cₖ₋₁ of the line, and f has constant order on each cell of the stack over α that they cut out: each point cᵢ, and each open interval between consecutive points.

theorem TauCeti.exists_forall_eval_eq_zero_orderAt_ne : ∃ (f : MvPolynomial (Fin 3) ℝ), (∀ (t : ℝ), (MvPolynomial.eval ![t, 0, 0]) f = 0) ∧ f.orderAt ![0, 0, 0] = 2 ∧ ∀ (t : ℝ), t ≠ 0 → f.orderAt ![t, 0, 0] = 1

The fibre of a polynomial does not determine its order of vanishing. The polynomial X 1 * X 0 + X 2 ^ 2 vanishes on the whole line {(t, 0, 0)} over the origin of ℝ ^ 2, but its order is 2 at the origin of ℝ ^ 3 and 1 at every other point (t, 0, 0) of the line.