Lazard valuations in a specified coordinate order

The Lazard valuation depends on the linear order of the polynomial variables. An equivalence from the variables of a polynomial to a linearly ordered type therefore specifies an elimination order: rename the polynomial along the equivalence and reindex the point by its inverse before taking the ordinary Lazard valuation.

MvPolynomial.lazardValuationReindex packages this simultaneous reindexing. It preserves evaluation at the original point, so its zero and top cases have the same intrinsic characterizations as the ordinary valuation. Reindexings compose, renaming by the inverse equivalence cancels the reindexing, and the basic product law continues to hold. Reindexing along an order isomorphism only relabels the exponent, so the elimination order matters only through the order it induces on the variables. The finite rotation formula identifies the coordinate order used when a cylindrical stack moves its distinguished coordinate from the front to the end.

This interface makes the coordinate order explicit in projection-and-lifting arguments, where successive stages use different presentations of the same ambient variables.

References

S. McCallum, A. Parusiński, and L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Sections 2 and 5.

noncomputable def MvPolynomial.lazardValuationReindex {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : WithTop (Lex (τ →₀ ℕ))

The Lazard valuation after ordering the variables of p through an equivalence e. The point is reindexed simultaneously, so polynomial evaluation is unchanged.

theorem MvPolynomial.lazardValuationReindex_def {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : p.lazardValuationReindex e a = ((rename ⇑e) p).lazardValuation (a ∘ ⇑e.symm)

Lazard valuation in a reindexed coordinate order, unfolded.

@[simp]

theorem MvPolynomial.lazardValuationReindex_refl {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedGT σ] (p : MvPolynomial σ R) (a : σ → R) : p.lazardValuationReindex (Equiv.refl σ) a = p.lazardValuation a

Reindexing by the identity equivalence gives the ordinary Lazard valuation.

theorem MvPolynomial.lazardValuationReindex_trans {R : Type u_1} {σ : Type u_2} {τ : Type u_3} {υ : Type u_4} [CommSemiring R] [LinearOrder υ] [WellFoundedGT υ] (p : MvPolynomial σ R) (e : σ ≃ τ) (f : τ ≃ υ) (a : σ → R) : p.lazardValuationReindex (e.trans f) a = ((rename ⇑e) p).lazardValuationReindex f (a ∘ ⇑e.symm)

Successive changes of coordinate order combine by composition of their equivalences.

@[simp]

theorem MvPolynomial.lazardValuationReindex_rename_symm {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial τ R) (e : σ ≃ τ) (a : σ → R) : ((rename ⇑e.symm) p).lazardValuationReindex e a = p.lazardValuation (a ∘ ⇑e.symm)

Reindexing a polynomial renamed by the inverse equivalence gives the ordinary Lazard valuation at the reindexed point.

@[simp]

theorem MvPolynomial.lazardValuationReindex_eq_zero_iff {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : p.lazardValuationReindex e a = 0 ↔ (eval a) p ≠ 0

A reindexed Lazard valuation is zero exactly when the original polynomial does not vanish at the original point.

@[simp]

theorem MvPolynomial.lazardValuationReindex_zero {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (e : σ ≃ τ) (a : σ → R) : lazardValuationReindex 0 e a = ⊤

The reindexed Lazard valuation of the zero polynomial is top.

@[simp]

theorem MvPolynomial.lazardValuationReindex_eq_top_iff {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : p.lazardValuationReindex e a = ⊤ ↔ p = 0

A reindexed Lazard valuation is top exactly for the zero polynomial.

@[simp]

theorem MvPolynomial.lazardValuationReindex_one {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [Nontrivial R] [LinearOrder τ] [WellFoundedGT τ] (e : σ ≃ τ) (a : σ → R) : lazardValuationReindex 1 e a = 0

The reindexed Lazard valuation of one is zero.

theorem MvPolynomial.lazardValuationReindex_mul {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [NoZeroDivisors R] [LinearOrder τ] [WellFoundedGT τ] (p q : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : (p * q).lazardValuationReindex e a = p.lazardValuationReindex e a + q.lazardValuationReindex e a

Reindexed Lazard valuation is additive on products over a domain.

theorem MvPolynomial.lazardValuationReindex_pow {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) (n : ℕ) : (p ^ n).lazardValuationReindex e a = n • p.lazardValuationReindex e a

Reindexed Lazard valuation scales by the exponent under powers.

@[simp]

theorem MvPolynomial.lazardValuationReindex_neg {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) (a : σ → R) : (-p).lazardValuationReindex e a = p.lazardValuationReindex e a

Negation does not change a reindexed Lazard valuation.

theorem MvPolynomial.lazardValuationReindex_toEquiv {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder σ] [WellFoundedGT σ] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃o τ) (a : σ → R) : p.lazardValuationReindex e.toEquiv a = WithTop.map (fun (v : Lex (σ →₀ ℕ)) => toLex (Finsupp.mapDomain (⇑e) (ofLex v))) (p.lazardValuation a)

Reindexing along an order isomorphism only relabels the Lazard valuation: an elimination order that agrees with the given order of the variables gives the same valuation, with its exponent transported along the isomorphism.

theorem MvPolynomial.finite_range_lazardValuationReindex {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] [LinearOrder τ] [WellFoundedGT τ] (p : MvPolynomial σ R) (e : σ ≃ τ) : (Set.range (p.lazardValuationReindex e)).Finite

A polynomial has only finitely many Lazard valuations in any fixed reindexed coordinate order.

theorem MvPolynomial.lazardValuationReindex_finRotate_symm {R : Type u_1} {n : ℕ} [CommSemiring R] (p : MvPolynomial (Fin (n + 1)) R) (a : Fin (n + 1) → R) : p.lazardValuationReindex (Equiv.symm (finRotate (n + 1))) a = ((rename ⇑(Equiv.symm (finRotate (n + 1)))) p).lazardValuation (Fin.snoc (Fin.tail a) (a 0))

Moving coordinate zero to the end is reindexing by the inverse finite rotation.