Reconstructing signs 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 an ordered domain, that unit is a nonzero scalar. Thus the signs of the content and the basis, together with the scalar sign, determine the sign of the input.

The distinguished variable is coordinate zero, through MvPolynomial.finSuccEquiv. The content is evaluated at the remaining coordinates. Constant signs for the basis and contents transfer to the original family. The statements include zero inputs, vanishing contents, and empty bases. The corresponding ambient-order reconstruction and transfer are in TauCeti.RingTheory.MvPolynomial.SquarefreeBasis.Basic.

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_sign_eval_eq_content_mul_unit_mul_prod {R : Type u_1} [CommRing R] {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [LinearOrder R] [IsStrictOrderedRing R] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) : ∃ (ε : SignType), ε ≠ 0 ∧ ∃ (e : Polynomial (MvPolynomial (Fin n) R) → ℕ), ∀ (a : Fin (n + 1) → R), SignType.sign ((MvPolynomial.eval a) ((MvPolynomial.finSuccEquiv R n).symm f)) = SignType.sign ((MvPolynomial.eval (Fin.tail a)) f.content) * ε * ∏ b ∈ B, SignType.sign ((MvPolynomial.eval a) ((MvPolynomial.finSuccEquiv R n).symm b)) ^ e b

The signs of the content and the basis factors reconstruct the sign of each input, with one fixed nonzero scalar sign and fixed exponents. The identity holds also on zero fibers, so nullified inputs need no separate sign convention.

theorem Finset.IsSquarefreeBasis.signInvariant_eval {R : Type u_1} [CommRing R] {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [LinearOrder R] [IsStrictOrderedRing R] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) {S : Set (Fin (n + 1) → R)} (hc : TauCeti.SignInvariant (fun (a : Fin (n + 1) → R) => (MvPolynomial.eval (Fin.tail a)) f.content) S) (hb : ∀ b ∈ B, TauCeti.SignInvariant (fun (a : Fin (n + 1) → R) => (MvPolynomial.eval a) ((MvPolynomial.finSuccEquiv R n).symm b)) S) : TauCeti.SignInvariant (fun (a : Fin (n + 1) → R) => (MvPolynomial.eval a) ((MvPolynomial.finSuccEquiv R n).symm f)) S

Sign-invariance of the content and the basis on a set implies sign-invariance of every input on that set. The set may be disconnected, and may contain points at which some basis members or the content vanish.