Predicates on polynomials and ideals

Named forms of hypotheses that recur throughout the library: homogeneity of an ideal of a polynomial ring, absolute irreducibility of a polynomial (irreducibility over the algebraic closure of ℚ), and absolute irreducibility of its top-degree homogeneous part (the hypothesis of CCDN Theorem 4). All are abbreviations, so proofs may use them as their unfolded statements.

@[reducible, inline]

abbrev CCDN.IsHomogeneousIdeal {σ : Type u_1} {K : Type u_2} [CommSemiring K] (I : Ideal (MvPolynomial σ K)) : Prop

An ideal of a polynomial ring is homogeneous when it contains every homogeneous component of each of its elements.

Equations

• CCDN.IsHomogeneousIdeal I = ∀ f ∈ I, ∀ (N : ℕ), (MvPolynomial.homogeneousComponent N) f ∈ I

@[reducible, inline]

abbrev CCDN.AbsolutelyIrreducible {σ : Type u_1} (f : MvPolynomial σ ℤ) : Prop

An integer polynomial is absolutely irreducible when it is irreducible over the algebraic closure of ℚ.

Equations

• CCDN.AbsolutelyIrreducible f = Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure ℚ))) f)

@[reducible, inline]

abbrev CCDN.AbsolutelyIrreducibleRat {σ : Type u_1} (f : MvPolynomial σ ℚ) : Prop

A rational polynomial is absolutely irreducible when it is irreducible over the algebraic closure of ℚ.

Equations

• CCDN.AbsolutelyIrreducibleRat f = Irreducible ((MvPolynomial.map (algebraMap ℚ (AlgebraicClosure ℚ))) f)

theorem CCDN.absolutelyIrreducibleRat_map_iff {σ : Type u_1} (f : MvPolynomial σ ℤ) : AbsolutelyIrreducibleRat ((MvPolynomial.map (Int.castRingHom ℚ)) f) ↔ AbsolutelyIrreducible f

An integer polynomial is absolutely irreducible exactly when its image over ℚ is.

@[reducible, inline]

abbrev CCDN.HasAbsIrreducibleTopForm {σ : Type u_1} (f : MvPolynomial σ ℤ) : Prop

The top-degree homogeneous part of an integer polynomial is irreducible over the algebraic closure of ℚ.

Equations

• CCDN.HasAbsIrreducibleTopForm f = CCDN.AbsolutelyIrreducible ((MvPolynomial.homogeneousComponent f.totalDegree) f)

@[reducible, inline]

abbrev CCDN.HasAbsIrreducibleTopFormRat {σ : Type u_1} (f : MvPolynomial σ ℚ) : Prop

The top-degree homogeneous part of a rational polynomial is irreducible over the algebraic closure of ℚ.

Equations

• CCDN.HasAbsIrreducibleTopFormRat f = CCDN.AbsolutelyIrreducibleRat ((MvPolynomial.homogeneousComponent f.totalDegree) f)