Documentation

TauCeti.RingTheory.Polynomial.IrreducibleBasis.Basic

Irreducible bases of finite families of polynomials #

Let D be a GCD domain and F a finite family of polynomials in one distinguished variable over D. An irreducible basis of F is a finite set B of pairwise nonassociated irreducible polynomials of positive degree such that every member of F is a constant times a product of powers of members of B, and every member of B divides some nonzero member of F. The constant is the content of the member up to a unit; the product of powers is primitive. Zero members are reconstructed with the constant 0 and contribute nothing to the basis.

The intended coefficient ring is D = MvPolynomial (Fin n) R over a field R, which is a unique factorization domain by Mathlib's MvPolynomial.uniqueFactorizationMonoid. Projection operators for cylindrical algebraic decomposition (McCallum's and Lazard's) are applied to an irreducible basis of the input family together with the contents, and the signs and roots of the original family are recovered from those of the basis and the contents. By Gauss's lemma the basis stays irreducible over the fraction field of D. An irreducible basis is in particular a squarefree basis (Finset.IsSquarefreeBasis), so its members are pairwise coprime and its product is squarefree over the fraction field; hence resultants of distinct members are nonzero, and in characteristic zero (as for R = ℝ) so are discriminants of members. In positive characteristic an irreducible member can be inseparable, with zero discriminant.

Main definitions and results #

References #

source
structure Finset.IsIrreducibleBasis {D : Type u_1} [CommRing D] (F B : Finset (Polynomial D)) :
Prop

B is an irreducible basis of the finite family F of polynomials over D: its members are pairwise nonassociated irreducible polynomials of positive degree, every member of F is a constant times a product of powers of members of B, and every member of B divides a nonzero member of F.

  • irreducible (b : Polynomial D) : b ∈ B → Irreducible b

    Every member of the basis is irreducible.

  • natDegree_pos (b : Polynomial D) : b ∈ B → 0 < b.natDegree

    Every member of the basis has positive degree.

  • eq_of_associated (b : Polynomial D) : b ∈ B → ∀ b' ∈ B, Associated b b' → b = b'

    Distinct members of the basis are not associated.

  • exists_eq_C_mul_prod (f : Polynomial D) : f ∈ F → ∃ (c : D) (e : Polynomial D → ℕ), f = Polynomial.C c * ∏ b ∈ B, b ^ e b

    Every member of the family is a constant times a product of powers of the basis.

  • exists_dvd (b : Polynomial D) : b ∈ B → ∃ f ∈ F, f ≠ 0 ∧ b ∣ f

    Every member of the basis divides a nonzero member of the family.

Instances For
    source
    theorem Finset.IsIrreducibleBasis.isPrimitive {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] (hB : F.IsIrreducibleBasis B) (hb : b ∈ B) :
    b.IsPrimitive

    The members of an irreducible basis are primitive.

    source
    theorem Finset.IsIrreducibleBasis.isSquarefreeBasis {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsDomain D] (hB : F.IsIrreducibleBasis B) :
    F.IsSquarefreeBasis B

    An irreducible basis is a squarefree basis.

    source
    theorem Finset.IsIrreducibleBasis.exists_associated_iff {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) {q : Polynomial D} (hq : Irreducible q) (hdeg : 0 < q.natDegree) :
    (∃ b ∈ B, Associated q b) ↔ ∃ f ∈ F, f ≠ 0 ∧ q ∣ f

    An irreducible polynomial of positive degree is associated to a member of an irreducible basis of F exactly when it divides a nonzero member of F.

    source
    theorem Finset.IsIrreducibleBasis.exists_associated {D : Type u_1} [CommRing D] {F B B' : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') (hb : b ∈ B) :
    ∃ b' ∈ B', Associated b b'

    Irreducible bases of the same family agree up to associates.

    source
    theorem Finset.IsIrreducibleBasis.exists_eq_C_mul {D : Type u_1} [CommRing D] {F B B' : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') (hb : b ∈ B) :
    ∃ b' ∈ B', ∃ (r : D), IsUnit r ∧ b = Polynomial.C r * b'

    Each member of an irreducible basis is a unit multiple of a member of any other irreducible basis of the same family.

    source
    theorem Finset.IsIrreducibleBasis.card_eq {D : Type u_1} [CommRing D] {F B B' : Finset (Polynomial D)} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') :
    B.card = B'.card

    Irreducible bases of the same family have the same number of members.

    source
    theorem Finset.IsIrreducibleBasis.exists_associated_discr {D : Type u_1} [CommRing D] {F B B' : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') (hb : b ∈ B) :
    ∃ c ∈ B', Associated b.discr c.discr

    The discriminant of a member of an irreducible basis is associated to the discriminant of a member of any other irreducible basis of the same family.

    source
    theorem Finset.IsIrreducibleBasis.exists_associated_resultant {D : Type u_1} [CommRing D] {F B B' : Finset (Polynomial D)} {b b' : Polynomial D} [IsDomain D] [IsGCDMonoid D] (hB : F.IsIrreducibleBasis B) (hB' : F.IsIrreducibleBasis B') (hb : b ∈ B) (hb' : b' ∈ B) (hne : b ≠ b') :
    ∃ c ∈ B', ∃ c' ∈ B', c ≠ c' ∧ Associated (b.resultant b') (c.resultant c')

    The resultant of two distinct members of an irreducible basis is associated to the resultant of two distinct members of any other irreducible basis of the same family.

    source
    theorem Finset.IsIrreducibleBasis.irreducible_map {D : Type u_1} [CommRing D] {F B : Finset (Polynomial D)} {b : Polynomial D} [IsDomain D] [IsGCDMonoid D] (K : Type u_2) [Field K] [Algebra D K] [IsFractionRing D K] (hB : F.IsIrreducibleBasis B) (hb : b ∈ B) :
    Irreducible (Polynomial.map (algebraMap D K) b)

    By Gauss's lemma, the members of an irreducible basis stay irreducible over the fraction field.

    source
    theorem Polynomial.exists_eq_C_mul_prod_irreducible {D : Type u_1} [CommRing D] [IsDomain D] [IsGCDMonoid D] (f : Polynomial D) :
    ∃ (c : D) (s : Multiset (Polynomial D)), (∀ q ∈ s, Irreducible q ∧ 0 < q.natDegree) ∧ f = C c * s.prod

    Over a GCD domain, every polynomial is a constant times a product of irreducible polynomials of positive degree. The zero polynomial is included by taking the constant zero.

    source
    theorem Finset.exists_isIrreducibleBasis {D : Type u_1} [CommRing D] [IsDomain D] [IsGCDMonoid D] (F : Finset (Polynomial D)) :
    ∃ (B : Finset (Polynomial D)), F.IsIrreducibleBasis B

    Every finite family of polynomials over a GCD domain has an irreducible basis.