Mathlib.RingTheory.Polynomial.UniqueFactorization

Module docstring

{"# Unique factorization for univariate and multivariate polynomials

Main results

Polynomial.wfDvdMonoid: If an integral domain is a WFDvdMonoid, then so is its polynomial ring.
Polynomial.uniqueFactorizationMonoid, MvPolynomial.uniqueFactorizationMonoid: If an integral domain is a UniqueFactorizationMonoid, then so is its polynomial ring (of any number of variables). "}

Polynomial.wfDvdMonoid instance

: WfDvdMonoid R[X]

Full source

instance (priority := 100) wfDvdMonoid : WfDvdMonoid R[X] where
  wf := by
    classical
      refine
        RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnitDvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      dsimp
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [cne0, ane0, Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

Polynomial Rings over Well-Founded Divisibility Monoids are Well-Founded Divisibility Monoids

Informal description

For any integral domain $R$ that is a well-founded divisibility monoid, the polynomial ring $R[X]$ is also a well-founded divisibility monoid.

Polynomial.exists_irreducible_of_degree_pos theorem

(hf : 0 < f.degree) : ∃ g, Irreducible g ∧ g ∣ f

Full source

theorem exists_irreducible_of_degree_pos (hf : 0 < f.degree) : ∃ g, Irreducible g ∧ g ∣ f :=
  WfDvdMonoid.exists_irreducible_factor (fun huf => ne_of_gt hf <| degree_eq_zero_of_isUnit huf)
    fun hf0 => not_lt_of_lt hf <| hf0.symm ▸ (@degree_zero R _).symm ▸ WithBot.bot_lt_coe _

Existence of Irreducible Factor for Polynomials with Positive Degree

Informal description

For any polynomial $f$ with positive degree, there exists an irreducible polynomial $g$ that divides $f$.

Polynomial.exists_irreducible_of_natDegree_pos theorem

(hf : 0 < f.natDegree) : ∃ g, Irreducible g ∧ g ∣ f

Full source

theorem exists_irreducible_of_natDegree_pos (hf : 0 < f.natDegree) : ∃ g, Irreducible g ∧ g ∣ f :=
  exists_irreducible_of_degree_pos <| by
    contrapose! hf
    exact natDegree_le_of_degree_le hf

Existence of Irreducible Factor for Polynomials with Positive Natural Degree

Informal description

For any polynomial $f$ with positive natural degree, there exists an irreducible polynomial $g$ that divides $f$.

Polynomial.exists_irreducible_of_natDegree_ne_zero theorem

(hf : f.natDegree ≠ 0) : ∃ g, Irreducible g ∧ g ∣ f

Full source

theorem exists_irreducible_of_natDegree_ne_zero (hf : f.natDegree ≠ 0) :
    ∃ g, Irreducible g ∧ g ∣ f :=
  exists_irreducible_of_natDegree_pos <| Nat.pos_of_ne_zero hf

Existence of Irreducible Factor for Non-Constant Polynomials

Informal description

For any polynomial $f$ with non-zero natural degree, there exists an irreducible polynomial $g$ that divides $f$.

Polynomial.uniqueFactorizationMonoid instance

: UniqueFactorizationMonoid D[X]

Full source

instance (priority := 100) uniqueFactorizationMonoid : UniqueFactorizationMonoid D[X] := by
  letI := Classical.arbitrary (NormalizedGCDMonoid D)
  exact ufm_of_decomposition_of_wfDvdMonoid

Polynomial Rings over UFDs are UFDs

Informal description

For any unique factorization domain $D$, the polynomial ring $D[X]$ is also a unique factorization domain.

Polynomial.fintypeSubtypeMonicDvd definition

(f : D[X]) (hf : f ≠ 0) : Fintype { g : D[X] // g.Monic ∧ g ∣ f }

Full source

/-- If `D` is a unique factorization domain, `f` is a non-zero polynomial in `D[X]`, then `f` has
only finitely many monic factors.
(Note that its factors up to unit may be more than monic factors.)
See also `UniqueFactorizationMonoid.fintypeSubtypeDvd`. -/
noncomputable def fintypeSubtypeMonicDvd (f : D[X]) (hf : f ≠ 0) :
    Fintype { g : D[X] // g.Monic ∧ g ∣ f } := by
  set G := { g : D[X] // g.Monic ∧ g ∣ f }
  let y : Associates D[X] := Associates.mk f
  have hy : y ≠ 0 := Associates.mk_ne_zero.mpr hf
  let H := { x : Associates D[X] // x ∣ y }
  let hfin : Fintype H := UniqueFactorizationMonoid.fintypeSubtypeDvd y hy
  let i : G → H := fun x ↦ ⟨Associates.mk x.1, Associates.mk_dvd_mk.2 x.2.2⟩
  refine Fintype.ofInjective i fun x y heq ↦ ?_
  rw [Subtype.mk.injEq] at heq ⊢
  exact eq_of_monic_of_associated x.2.1 y.2.1 (Associates.mk_eq_mk_iff_associated.mp heq)

Finiteness of monic divisors of a non-zero polynomial over a UFD

Informal description

For any non-zero polynomial $ f $ over a unique factorization domain $ D $, the set of monic divisors of $ f $ is finite.

MvPolynomial.uniqueFactorizationMonoid instance

: UniqueFactorizationMonoid (MvPolynomial σ D)

Full source

instance (priority := 100) uniqueFactorizationMonoid :
    UniqueFactorizationMonoid (MvPolynomial σ D) := by
  rw [iff_exists_prime_factors]
  intro a ha; obtain ⟨s, a', rfl⟩ := exists_finset_rename a
  obtain ⟨w, h, u, hw⟩ :=
    iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h =>
      ha <| by simp [h]
  exact
    ⟨w.map (rename (↑)), fun b hb =>
      let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
      he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
      Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
      rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]⟩

Multivariate Polynomial Ring over a UFD is a UFD

Informal description

For any unique factorization domain $D$ and any type $\sigma$, the ring of multivariate polynomials over $D$ with variables indexed by $\sigma$ is also a unique factorization domain.

Polynomial.exists_monic_irreducible_factor theorem

{F : Type*} [Field F] (f : F[X]) (hu : ¬IsUnit f) : ∃ g : F[X], g.Monic ∧ Irreducible g ∧ g ∣ f

Full source

/-- A polynomial over a field which is not a unit must have a monic irreducible factor.
See also `WfDvdMonoid.exists_irreducible_factor`. -/
theorem Polynomial.exists_monic_irreducible_factor {F : Type*} [Field F] (f : F[X])
    (hu : ¬IsUnit f) : ∃ g : F[X], g.Monic ∧ Irreducible g ∧ g ∣ f := by
  by_cases hf : f = 0
  · exact ⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩
  obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf
  have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
    isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv
  exact ⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩

Existence of Monic Irreducible Factor for Non-Unit Polynomials over a Field

Informal description

For any field $F$ and any non-unit polynomial $f \in F[X]$, there exists a monic irreducible polynomial $g \in F[X]$ that divides $f$.