The monic irreducible factors of a polynomial over a field

For a polynomial f over a field K, Polynomial.Factors f is the type of its distinct monic irreducible factors: the subtype of K[X] cut out by Irreducible p ∧ p.Monic ∧ p ∣ f. Working with this subtype rather than with normalizedFactors f keeps DecidableEq K out of the statements; the two are compared by Mathlib's Polynomial.mem_normalizedFactors_iff, whose conjunct order the predicate above follows.

The factors are pairwise coprime, and when f is nonzero and squarefree their product is associated to f, so the ideal (f) is the intersection of the ideals (p). That is the input for the Chinese Remainder decomposition of K[X] ⧸ (f) into the fields K[X] ⧸ (p).

Main definitions

• Polynomial.Factors: the distinct monic irreducible factors of f, as a type.
• Polynomial.Factors.linearEquivRoots: the linear factors correspond to the roots of f, with linearEquivRoots_apply and linearEquivRoots_symm_apply computing both directions.

Main results

• Polynomial.Factors.finite: a nonzero polynomial has finitely many factors.
• Polynomial.Factors.normalizedFactors_eq_map_univ_val: for a nonzero squarefree polynomial, its normalized factors are precisely the distinct monic irreducible factors.
• Polynomial.Factors.isCoprime: distinct factors are coprime.
• Polynomial.Factors.span_eq_iInf_span: for f nonzero and squarefree, (f) = ⨅ p, (p).
• Polynomial.sum_natDegree_normalizedFactors: the degrees of the normalized irreducible factors, counted with multiplicity, sum to the degree.
• Polynomial.map_natDegree_normalizedFactors_eq_singleton_iff: those degrees form a singleton exactly when the polynomial is irreducible.

Provenance

Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, commit 66889eada51a), EllipticCurves/Mathlib/Basic.lean, section EtaleDecomposition. The source is written against Lean v4.32.0; this is a forward port.

@[reducible, inline]

abbrev Polynomial.Factors {K : Type u_1} [Field K] (f : Polynomial K) : Type u_1

The distinct monic irreducible factors of f, as an index type.

This is not defined via normalizedFactors (which would require DecidableEq K); the predicate is spelled in the order of Polynomial.mem_normalizedFactors_iff, which is therefore the characterization of membership in normalizedFactors f.

Equations

• f.Factors = { p : Polynomial K // Irreducible p ∧ p.Monic ∧ p ∣ f }

theorem Polynomial.Factors.irreducible {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : Irreducible ↑p

theorem Polynomial.Factors.monic {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : (↑p).Monic

theorem Polynomial.Factors.dvd {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : ↑p ∣ f

theorem Polynomial.Factors.ne_zero {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : ↑p ≠ 0

theorem Polynomial.Factors.prime {K : Type u_1} [Field K] {f : Polynomial K} (p : f.Factors) : Prime ↑p

theorem Polynomial.Factors.separable {K : Type u_1} [Field K] {f : Polynomial K} (hf : f.Separable) (p : f.Factors) : (↑p).Separable

theorem Polynomial.Factors.finite {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) : Finite f.Factors

theorem Polynomial.Factors.normalizedFactors_eq_map_univ_val {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] [DecidableEq K] (hf : f ≠ 0) (hsq : Squarefree f) : UniqueFactorizationMonoid.normalizedFactors f = Multiset.map Subtype.val Finset.univ.val

For a nonzero squarefree polynomial, its normalized factors list its distinct monic irreducible factors exactly once.

theorem Polynomial.Factors.nonempty {K : Type u_1} [Field K] {f : Polynomial K} (hu : ¬IsUnit f) : Nonempty f.Factors

noncomputable def Polynomial.Factors.linearEquivRoots {K : Type u_1} [Field K] {f : Polynomial K} : { p : f.Factors // (↑p).natDegree = 1 } ≃ { x : K // eval x f = 0 }

The monic linear factors of f correspond to the roots of f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.Factors.linearEquivRoots_apply {K : Type u_1} [Field K] {f : Polynomial K} (p : { p : f.Factors // (↑p).natDegree = 1 }) : ↑(linearEquivRoots p) = -(↑↑p).coeff 0

linearEquivRoots sends a monic linear factor to the root it records, the negated constant coefficient.

@[simp]

theorem Polynomial.Factors.linearEquivRoots_symm_apply {K : Type u_1} [Field K] {f : Polynomial K} (x : { x : K // eval x f = 0 }) : ↑↑(linearEquivRoots.symm x) = X - C ↑x

linearEquivRoots.symm sends a root x to the monic linear factor X - C x.

theorem Polynomial.Factors.isCoprime {K : Type u_1} [Field K] {f : Polynomial K} {p q : f.Factors} (hne : p ≠ q) : IsCoprime ↑p ↑q

Distinct monic irreducible factors of f are coprime: each spans a maximal ideal, and the two ideals differ because a monic polynomial is determined by the ideal it spans.

theorem Polynomial.Factors.isCoprime_span {K : Type u_1} [Field K] {f : Polynomial K} {p q : f.Factors} (hne : p ≠ q) : IsCoprime (Ideal.span {↑p}) (Ideal.span {↑q})

theorem Polynomial.Factors.associated_prod {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] (hf : f ≠ 0) (hsq : Squarefree f) : Associated (∏ p : f.Factors, ↑p) f

A nonzero squarefree polynomial is associated to the product of its distinct monic irreducible factors.

theorem Polynomial.Factors.sum_natDegree_le {K : Type u_1} [Field K] {f : Polynomial K} [Fintype f.Factors] (hf : f ≠ 0) : ∑ p : f.Factors, (↑p).natDegree ≤ f.natDegree

The degrees of the distinct monic irreducible factors of f ≠ 0 sum to at most the degree of f.

theorem Polynomial.Factors.span_eq_iInf_span {K : Type u_1} [Field K] {f : Polynomial K} (hf : f ≠ 0) (hsq : Squarefree f) : Ideal.span {f} = ⨅ (p : f.Factors), Ideal.span {↑p}

For f nonzero and squarefree, the ideal (f) is the intersection of the ideals (p) over the monic irreducible factors p of f. This is the input for the Chinese Remainder decomposition of K[X] ⧸ (f).

theorem Polynomial.Factors.exists_dvd_map {K : Type u_1} [Field K] {f : Polynomial K} {L : Type u_2} [CommSemiring L] (σ : K →+* L) (hf : f ≠ 0) {q : Polynomial L} (hq : Prime q) (hdvd : q ∣ map σ f) : ∃ (p : f.Factors), q ∣ map σ ↑p

A prime factor of the image of f under a ring homomorphism to a commutative semiring divides the image of one of the monic irreducible factors of f.

This lets computations after changing coefficients be indexed by the factors over the base field, including when the target is a nonfield ring such as a product of fields.

Degrees of the normalized irreducible factors

Polynomial.Factors keeps DecidableEq K out of its statements by working with a subtype, at the cost of forgetting multiplicities. The lemmas below are the counterparts for normalizedFactors, which does record them.

theorem Polynomial.sum_natDegree_normalizedFactors {K : Type u_1} [Field K] [DecidableEq K] (g : Polynomial K) : (Multiset.map natDegree (UniqueFactorizationMonoid.normalizedFactors g)).sum = g.natDegree

The degrees of the normalized irreducible factors of a polynomial over a field, counted with multiplicity, sum to its degree.

theorem Polynomial.irreducible_of_card_normalizedFactors_eq_one {K : Type u_1} [Field K] [DecidableEq K] {g : Polynomial K} (h : (UniqueFactorizationMonoid.normalizedFactors g).card = 1) : Irreducible g

A polynomial over a field with exactly one normalized irreducible factor, counted with multiplicity, is irreducible.

@[simp]

theorem Polynomial.map_natDegree_normalizedFactors_eq_singleton_iff {K : Type u_1} [Field K] [DecidableEq K] {g : Polynomial K} : Multiset.map natDegree (UniqueFactorizationMonoid.normalizedFactors g) = {g.natDegree} ↔ Irreducible g

The degrees of the normalized irreducible factors of a polynomial over a field form the singleton {g.natDegree} exactly when the polynomial is irreducible.