Documentation

TauCeti.Geometry.RealAlgebraic.Projection.Lazard.Basic

The Lazard projection set #

Let F be a finite family of polynomials in one distinguished variable over a commutative ring R with a normalized gcd, and let B be a basis of F, in Lazard's setting an irreducible basis (Finset.IsIrreducibleBasis): a finite set of pairwise nonassociated irreducible polynomials of positive degree whose products of powers recover the members of F up to their contents. The Lazard projection F.lazardProjection B is the finite subset of R consisting of

The trailing coefficient is Mathlib's Polynomial.trailingCoeff, the coefficient of the lowest power of the distinguished variable occurring in b; it is the constant coefficient b.coeff 0 unless the distinguished variable divides b.

The intended coefficient ring is R = MvPolynomial (Fin n) ℝ. Compared with the McCallum projection Finset.mcCallumProjection, only the leading and trailing coefficients of each basis member are kept, rather than all of its coefficients (Finset.lazardProjection_subset_mcCallumProjection). In exchange, the lifting theorem of McCallum, Parusiński and Paunescu asks for invariance of Lazard valuations instead of orders of vanishing, and allows nullification of basis members.

For an irreducible basis over a domain of characteristic zero, no element of the Lazard projection vanishes unless the family itself contains the zero polynomial (Finset.IsIrreducibleBasis.zero_mem_lazardProjection_iff). In particular the discriminant, leading coefficient and trailing coefficient of every member of the basis are nonzero formal polynomials in the base coordinates, as the lifting theorem requires, even though they may vanish at points of a base cell. As for McCallum's projection, the Lazard projection depends on the choice of irreducible basis only up to associates (Finset.IsIrreducibleBasis.exists_associated_mem_lazardProjection).

Main definitions and results #

References #

source
noncomputable def Finset.lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (F B : Finset (Polynomial R)) :
Finset R

The Lazard projection of the family F with respect to the basis B: the contents of the members of F, together with the leading coefficients, trailing coefficients and discriminants of the members of B and the resultants of pairs of distinct members of B. Resultants and discriminants are taken at the actual degrees.

Instances For
    source
    theorem Finset.mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {a : R} :
    a ∈ F.lazardProjection B ↔ (∃ f ∈ F, f.content = a) ∨ (∃ b ∈ B, b.leadingCoeff = a) ∨ (∃ b ∈ B, b.trailingCoeff = a) ∨ (∃ b ∈ B, b.discr = a) ∨ ∃ b ∈ B, ∃ b' ∈ B, b ≠ b' ∧ b.resultant b' = a

    The elements of the Lazard projection: contents of members of the family, and leading coefficients, trailing coefficients, discriminants and pairwise resultants of members of the basis.

    source
    theorem Finset.content_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {f : Polynomial R} (hf : f ∈ F) :
    f.content ∈ F.lazardProjection B

    The content of every member of the family lies in the Lazard projection.

    source
    theorem Finset.leadingCoeff_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} (hb : b ∈ B) :
    b.leadingCoeff ∈ F.lazardProjection B

    The leading coefficient of every member of the basis lies in the Lazard projection.

    source
    theorem Finset.trailingCoeff_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} (hb : b ∈ B) :
    b.trailingCoeff ∈ F.lazardProjection B

    The trailing coefficient of every member of the basis lies in the Lazard projection.

    source
    theorem Finset.discr_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b : Polynomial R} (hb : b ∈ B) :
    b.discr ∈ F.lazardProjection B

    The discriminant of every member of the basis lies in the Lazard projection.

    source
    theorem Finset.resultant_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} {b b' : Polynomial R} (hb : b ∈ B) (hb' : b' ∈ B) (hne : b ≠ b') :
    b.resultant b' ∈ F.lazardProjection B

    The resultant of two distinct members of the basis lies in the Lazard projection.

    source
    @[simp]
    theorem Finset.lazardProjection_empty_right {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F : Finset (Polynomial R)} [DecidableEq R] :
    F.lazardProjection ∅ = image Polynomial.content F

    With the empty basis, the Lazard projection consists of the contents of the family.

    source
    theorem Finset.lazardProjection_mono {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F F' B B' : Finset (Polynomial R)} (hF : F ⊆ F') (hB : B ⊆ B') :
    F.lazardProjection B ⊆ F'.lazardProjection B'

    Enlarging the family or the basis enlarges the Lazard projection.

    source
    theorem Finset.lazardProjection_subset_mcCallumProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} :
    F.lazardProjection B ⊆ F.mcCallumProjection B

    The Lazard projection is contained in the McCallum projection: leading and trailing coefficients are coefficients up to the degree.

    Independence of the basis #

    source
    theorem Finset.IsIrreducibleBasis.exists_associated_mem_lazardProjection {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B B' : Finset (Polynomial R)} [IsDomain R] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') {a : R} (ha : a ∈ F.lazardProjection B') :
    ∃ a' ∈ F.lazardProjection B, Associated a a'

    Independence of the basis. For two irreducible bases B and B' of the same family, every element of the Lazard projection with respect to B' is associated to an element of the Lazard projection with respect to B.

    Nonvanishing #

    source
    @[simp]
    theorem Finset.IsIrreducibleBasis.zero_mem_lazardProjection_iff {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {F B : Finset (Polynomial R)} [IsDomain R] [CharZero R] (hB : F.IsIrreducibleBasis B) :
    0 ∈ F.lazardProjection B ↔ 0 ∈ F

    Nonvanishing of the Lazard projection. In characteristic zero, the Lazard projection of an irreducible basis contains 0 exactly when the family contains the zero polynomial. Thus for a family of nonzero polynomials, the contents of its members and the leading coefficients, trailing coefficients, discriminants and pairwise resultants of the basis are all nonzero.