Lazard projection conditions for products

Constant Lazard valuations on a projection set give constant valuations of the leading coefficient, trailing coefficient and discriminant of the product of any subfamily of an irreducible basis. Together with Finset.IsSquarefreeBasis.discr_prod_ne_zero, these are the formal-polynomial conditions needed to apply a single-polynomial Lazard lifting theorem to the product, without requiring nonvanishing of its ordinary fibers.

The coefficient of degree zero also has constant valuation. It agrees with the trailing coefficient when it is a nonzero formal polynomial; otherwise its valuation is everywhere infinite. A lifting theorem requiring a nonzero constant coefficient must therefore separate factors divisible by the distinguished variable before using this constancy result. Over the reals, TauCeti.lazardDelineationCMulLastCoordinate in TauCeti.Geometry.RealAlgebraic.Stack.Lazard.Coordinate supplies the separate Lazard delineation of that coordinate factor.

References

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

theorem Finset.lazardValuation_leadingCoeff_prod_eq_of_lazardProjection {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [IsDomain R] [NormalizedGCDMonoid (MvPolynomial σ R)] {F B A : Finset (Polynomial (MvPolynomial σ R))} (hA : A ⊆ B) (a b : σ → R) (h : ∀ p ∈ F.lazardProjection B, p.lazardValuation a = p.lazardValuation b) : (∏ p ∈ A, p).leadingCoeff.lazardValuation a = (∏ p ∈ A, p).leadingCoeff.lazardValuation b

The Lazard projection determines the valuation of the leading coefficient of the product of any subfamily of the basis. This does not require irreducibility.

theorem Finset.lazardValuation_trailingCoeff_prod_eq_of_lazardProjection {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [IsDomain R] [NormalizedGCDMonoid (MvPolynomial σ R)] {F B A : Finset (Polynomial (MvPolynomial σ R))} (hA : A ⊆ B) (a b : σ → R) (h : ∀ p ∈ F.lazardProjection B, p.lazardValuation a = p.lazardValuation b) : (∏ p ∈ A, p).trailingCoeff.lazardValuation a = (∏ p ∈ A, p).trailingCoeff.lazardValuation b

The Lazard projection determines the valuation of the trailing coefficient of the product of any subfamily of the basis. This does not require irreducibility.

theorem Finset.lazardValuation_coeff_zero_prod_eq_of_lazardProjection {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [IsDomain R] [NormalizedGCDMonoid (MvPolynomial σ R)] {F B A : Finset (Polynomial (MvPolynomial σ R))} (hA : A ⊆ B) (a b : σ → R) (h : ∀ p ∈ F.lazardProjection B, p.lazardValuation a = p.lazardValuation b) : ((∏ p ∈ A, p).coeff 0).lazardValuation a = ((∏ p ∈ A, p).coeff 0).lazardValuation b

The Lazard projection determines the valuation of the constant coefficient of the product of any subfamily of the basis. If that formal coefficient is zero, both valuations are infinite; otherwise it is the trailing coefficient.

theorem Finset.IsIrreducibleBasis.lazardValuation_discr_prod_eq_of_lazardProjection {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [IsDomain R] [NormalizedGCDMonoid (MvPolynomial σ R)] {F B A : Finset (Polynomial (MvPolynomial σ R))} (hB : F.IsIrreducibleBasis B) (hA : A ⊆ B) (a b : σ → R) (h : ∀ p ∈ F.lazardProjection B, p.lazardValuation a = p.lazardValuation b) : (∏ p ∈ A, p).discr.lazardValuation a = (∏ p ∈ A, p).discr.lazardValuation b

The Lazard projection determines the valuation of the discriminant of the product of any subfamily of an irreducible basis. The formal discriminant can vanish at both base points; no nonvanishing of its values or of specialized leading coefficients is assumed.