Squarefree monic polynomials are products of distinct monic irreducibles

Over a domain R with a normalization monoid, such as ℤ, whose polynomial ring has unique factorization, a squarefree monic polynomial is the product of a finite set of monic irreducible polynomials. The set is that of its normalized irreducible factors: a normalized divisor of a monic polynomial is monic, because its leading coefficient is a normalized unit.

A nonzero discriminant gives squarefreeness (Polynomial.Monic.squarefree_of_discr_ne_zero). For monic f : ℤ[X] with disc f ≠ 0 this is the first step in reducing statements about a reducible f to its irreducible factors. The factors are irreducible in ℤ[X], and so, being monic, also over ℚ by Gauss's lemma.

Main results

• Polynomial.Monic.monic_of_mem_normalizedFactors: a normalized irreducible factor of a monic polynomial is monic.
• Polynomial.Monic.prod_toFinset_normalizedFactors_of_squarefree: a squarefree monic polynomial is the product of its distinct normalized irreducible factors.
• Polynomial.Monic.exists_finset_prod_eq_of_squarefree: a squarefree monic polynomial is the product of a finite set of monic irreducible polynomials.
• Polynomial.Monic.exists_finset_prod_eq_of_discr_ne_zero: the same conclusion for a monic polynomial with nonzero discriminant.

theorem Polynomial.Monic.monic_of_mem_normalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid (Polynomial R)] {f : Polynomial R} (hf : f.Monic) {g : Polynomial R} (hg : g ∈ UniqueFactorizationMonoid.normalizedFactors f) : g.Monic

A normalized irreducible factor of a monic polynomial is monic: its leading coefficient is a normalized unit.

theorem Polynomial.Monic.prod_toFinset_normalizedFactors_of_squarefree {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid (Polynomial R)] {f : Polynomial R} [DecidableEq (Polynomial R)] (hf : f.Monic) (hsq : Squarefree f) : ∏ g ∈ (UniqueFactorizationMonoid.normalizedFactors f).toFinset, g = f

A squarefree monic polynomial is the product of its distinct normalized irreducible factors.

theorem Polynomial.Monic.exists_finset_prod_eq_of_squarefree {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid (Polynomial R)] {f : Polynomial R} (hf : f.Monic) (hsq : Squarefree f) : ∃ (s : Finset (Polynomial R)), (∀ g ∈ s, g.Monic ∧ Irreducible g) ∧ ∏ g ∈ s, g = f

A squarefree monic polynomial is the product of a finite set of monic irreducible polynomials, namely its normalized irreducible factors.

theorem Polynomial.Monic.exists_finset_prod_eq_of_discr_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid (Polynomial R)] {f : Polynomial R} (hf : f.Monic) (hd : f.discr ≠ 0) : ∃ (s : Finset (Polynomial R)), (∀ g ∈ s, g.Monic ∧ Irreducible g) ∧ ∏ g ∈ s, g = f

A monic polynomial with nonzero discriminant is the product of a finite set of monic irreducible polynomials. Over ℤ this is the factorization of a monic f with disc f ≠ 0 into distinct monic irreducible factors.