Factorization of polynomial to monic polynomials

Stream: Is there code for X?

[Daniel Weber]

Do we have this in Mathlib? If not, should I PR this (with a better name, I hope, suggestions are welcome)?

open Polynomial

variable (R : Type*) [Field R]

theorem Polynomial.factorize (a : R[X]) :
    ∃ (f : Multiset R[X]) (v : R), (∀ b ∈ f, Irreducible b ∧ b.Monic) ∧ C v * f.prod = a := by
  by_cases ha : a = 0
  · exists ∅, 0
    simp [ha]
  have ⟨f, hf, ha2⟩ := WfDvdMonoid.exists_factors a ha
  let f' := f.map (fun x ↦ C (1 / x.leadingCoeff) * x)
  have : Associated f'.prod f.prod := by
    unfold_let f'
    clear ha ha2 a
    induction f using Multiset.induction_on
    · simp
    rename_i b f hi
    simp only [Multiset.map_cons, Multiset.prod_cons]
    apply Associated.mul_mul
    · apply associated_unit_mul_left
      apply Polynomial.isUnit_C.mpr
      simp only [one_div, isUnit_iff_ne_zero, ne_eq, inv_eq_zero, leadingCoeff_eq_zero]
      apply Irreducible.ne_zero
      apply hf
      simp
    · apply hi
      intro b hb
      apply hf
      simp [hb]
  have ⟨v, hv⟩ := this.trans ha2
  let v' : R[X] := v
  have : IsUnit v' := Units.isUnit v
  rw [Polynomial.isUnit_iff] at this
  obtain ⟨v'', hv'⟩ := this
  exists f', v''
  constructor
  · intro b hb
    unfold_let f' at hb
    simp only [one_div, Multiset.mem_map] at hb
    obtain ⟨a, ha1, ha2⟩ := hb
    rw [← ha2]
    constructor
    · rw [irreducible_isUnit_mul]
      exact hf a ha1
      rw [Polynomial.isUnit_C]
      simp
      apply Irreducible.ne_zero
      exact hf a ha1
    · rw [mul_comm]
      apply Polynomial.monic_mul_leadingCoeff_inv
      apply Irreducible.ne_zero
      exact hf a ha1
  · rw [hv'.2, ← hv, mul_comm]

[Edward van de Meent]

is it just me or does the statement completely not rely on the first hypothesis?

[Daniel Weber]

What do you mean?

[Edward van de Meent]

oh oops i need to learn how to scroll right :upside_down:

[Junyan Xu]

You can use UniqueFactorizationMonoid.normalizedFactors_prod because we have Polynomial.monic_normalize

[Daniel Weber]

Junyan Xu said:

You can use UniqueFactorizationMonoid.normalizedFactors_prod because we have Polynomial.monic_normalize

Ah, so it can just be this, thanks. Is this too simple to add to Mathlib?

theorem Polynomial.factorize (a : R[X]) :
    ∃ (f : Multiset R[X]) (v : R), (∀ b ∈ f, Irreducible b ∧ b.Monic) ∧ C v * f.prod = a := by
  have : DecidableEq R := Classical.decEq _
  by_cases ha : a = 0
  · exists ∅, 0
    simp [ha]
  exists UniqueFactorizationMonoid.normalizedFactors a
  obtain ⟨v, hv⟩ := UniqueFactorizationMonoid.normalizedFactors_prod ha
  let v' : R[X] := v
  have : IsUnit v' := Units.isUnit v
  rw [Polynomial.isUnit_iff] at this
  obtain ⟨v'', hv'⟩ := this
  exists v''
  constructor
  · intro b hb
    constructor
    exact UniqueFactorizationMonoid.irreducible_of_normalized_factor b hb
    have := UniqueFactorizationMonoid.normalize_normalized_factor b hb
    rw [← this]
    apply Polynomial.monic_normalize
    apply Irreducible.ne_zero
    exact UniqueFactorizationMonoid.irreducible_of_normalized_factor b hb
  · rw [hv'.2, mul_comm, hv]

[Yakov Pechersky]

A little cleanup:

import Mathlib.RingTheory.UniqueFactorizationDomain
import Mathlib.Algebra.Polynomial.FieldDivision

open Polynomial

open UniqueFactorizationMonoid in
theorem Polynomial.factorize {R : Type*} [Field R] (a : R[X]) :
    ∃ (f : Multiset R[X]) (v : R), (∀ b ∈ f, Irreducible b ∧ b.Monic) ∧ C v * f.prod = a := by
  classical
  by_cases ha : a = 0
  · use ∅, 0
    simp [ha]
  use normalizedFactors a
  obtain ⟨v, hv⟩ := normalizedFactors_prod ha
  obtain ⟨v', -, hv'⟩ := Polynomial.isUnit_iff.mp v.isUnit
  use v'
  refine ⟨fun _ hb => ⟨?_, ?_⟩, by simpa [hv', mul_comm] using hv⟩
  · exact irreducible_of_normalized_factor _ hb
  rw [← normalize_normalized_factor _ hb]
  apply Polynomial.monic_normalize
  apply Irreducible.ne_zero
  exact irreducible_of_normalized_factor _ hb