Theory Poly_Ideal

section ‹Ideals of the Polynomial Ring; Kronecker's Construction›

theory Poly_Ideal
  imports Poly_Ring Ideal_Theory "HOL-Library.Multiset"
begin

text ‹This theory joins the carrier-set polynomial ring ‹Poly_Ring› to the
  ideal theory of ‹Ideal_Theory›.  The payoff is Kronecker's lemma: over a
  field, the ideal generated by an irreducible polynomial is maximal, so the quotient
  @{text "F[X]/(p)"} is a field.  This is the engine that builds field extensions (and,
  ultimately, finite fields) by adjoining roots of irreducible polynomials.›

context Field
begin

text ‹Inside a field the polynomial ring is a commutative ring, so its principal ideals are
  available through @{const commutative_ring.principal_ideal}.  We abbreviate the principal
  ideal @{text "(p)"} of @{text "F[X]"}.›

text ‹The principal ideal generated by @{term p} in @{text "F[X]"}, written out concretely.›
definition poly_pideal :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) set"
  where "poly_pideal p = {r ⊗⇩P p | r. r ∈ poly_carrier}"

lemma poly_pideal_memI: "r ∈ poly_carrier ⟹ r ⊗⇩P p ∈ poly_pideal p"
  unfolding poly_pideal_def by blast

lemma poly_pideal_contains:
  assumes "p ∈ poly_carrier" shows "p ∈ poly_pideal p"
  by (metis assms poly_mult_one_left poly_one_closed poly_pideal_memI)

text ‹@{const poly_pideal} agrees with the generic @{const commutative_ring.principal_ideal} of
  the polynomial ring, and is therefore an ideal of @{text "F[X]"}.›
lemma poly_pideal_is_ideal:
  assumes p: "p ∈ poly_carrier"
  shows "Ideal (poly_pideal p) poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
proof -
  interpret comm: commutative_ring poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
    by (rule poly_commutative_ring)
  show ?thesis
    using comm.principal_ideal_is_ideal p
    unfolding comm.principal_ideal_def poly_pideal_def by presburger
qed

text ‹∗‹Kronecker's lemma.›  For an irreducible @{term p}, the principal ideal @{text "(p)"} is
  maximal in @{text "F[X]"}.  Properness holds because @{term "𝟭⇩P"} would force @{term p} to be a
  unit; maximality uses that @{text "F[X]"} is a PID (@{thm [source] poly_PID}): any ideal
  @{term J} between @{text "(p)"} and @{text "F[X]"} is principal, @{term "J = poly_pideal b"},
  and @{term "p = c ⊗⇩P b"} forces (by irreducibility) either @{term b} a unit, so
  @{term "J = poly_carrier"}, or @{term c} a unit, so @{term "J ⊆ poly_pideal p"}.›
theorem poly_irreducible_maximal:
  assumes irr: "poly_irreducible p"
  shows "Ideal.maximal_ideal (poly_pideal p) poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
proof -
  have p: "p ∈ poly_carrier" using irr by (rule poly_irreducibleD_carrier)
  have pnu: "¬ poly_unit p" using irr by (rule poly_irreducibleD_nonunit)
  interpret I: Ideal "poly_pideal p" poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
    by (rule poly_pideal_is_ideal[OF p])
  ― ‹Properness: the ideal omits @{term "𝟭⇩P"}, else @{term p} would be a unit.›
  have proper: "poly_pideal p ≠ poly_carrier"
  proof
    assume "poly_pideal p = poly_carrier"
    then obtain r where r: "r ∈ poly_carrier" and rp: "𝟭⇩P = r ⊗⇩P p"
      unfolding poly_pideal_def by blast
    then have pr1: "p ⊗⇩P r = 𝟭⇩P" 
      by (simp add: p poly_mult_comm)
    with pnu show False
      using p poly_unitI r rp by force
  qed
  ― ‹Maximality: any larger ideal is principal and collapses to @{text "(p)"} or all of @{text "F[X]"}.›
  have "∀J. Ideal J poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P ⟶ poly_pideal p ⊆ J
            ⟶ J = poly_pideal p ∨ J = poly_carrier"
  proof (intro allI impI)
    fix J assume J: "Ideal J poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P" and sub: "poly_pideal p ⊆ J"
    interpret J: Ideal J poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P" by (rule J)
    obtain b where b: "b ∈ poly_carrier" and Jeq: "J = {r ⊗⇩P b | r. r ∈ poly_carrier}"
      using poly_PID[OF J] by blast
    have JeqP: "J = poly_pideal b" unfolding poly_pideal_def by (rule Jeq)
    ― ‹@{term p} lies in @{term J}, so @{term p} is a multiple of @{term b}.›
    have "p ∈ J" using sub poly_pideal_contains[OF p] by blast
    then obtain c where c: "c ∈ poly_carrier" and pcb: "p = c ⊗⇩P b"
      using JeqP unfolding poly_pideal_def by blast
    from poly_irreducibleD_factor[OF irr c b pcb] show "J = poly_pideal p ∨ J = poly_carrier"
    proof
      ― ‹If @{term b} is a unit then @{term J} is all of @{text "F[X]"}.›
      assume "poly_unit b"
      then obtain b' where b': "b' ∈ poly_carrier" and "b' ⊗⇩P b = 𝟭⇩P"
        unfolding poly_unit_def by blast
      ― ‹@{term "𝟭⇩P = b' ⊗⇩P b"} is a multiple of @{term b}, hence in @{term "J = poly_pideal b"}.›
      have "b' ⊗⇩P b ∈ poly_pideal b" using b' by (rule poly_pideal_memI)
      then have "𝟭⇩P ∈ J" using ‹b' ⊗⇩P b = 𝟭⇩P› JeqP by simp
      then have "poly_carrier ⊆ J"
        using J.Ideal(1) ‹𝟭⇩P ∈ J› poly_mult_one_right by fastforce
      then have "J = poly_carrier" using J.additive.subset by blast
      then show ?thesis ..
    next
      ― ‹If @{term c} is a unit then @{term b} is a multiple of @{term p}, so ‹J ⊆ (p)›.›
      assume "poly_unit c"
      then obtain c' where c': "c' ∈ poly_carrier" and "c ⊗⇩P c' = 𝟭⇩P" and c'c: "c' ⊗⇩P c = 𝟭⇩P"
        unfolding poly_unit_def by blast
      ― ‹From @{term "p = c ⊗⇩P b"}: @{term "b = c' ⊗⇩P p"}.›
      have "c' ⊗⇩P p = c' ⊗⇩P (c ⊗⇩P b)" using pcb by simp
      also have "… = b" using b
        by (metis c c' c'c poly_mult_assoc poly_mult_one_left)
      finally have beq: "b = c' ⊗⇩P p" ..
      ― ‹Hence every multiple of @{term b} is a multiple of @{term p}: ‹J ⊆ (p)›.›
      have "J ⊆ poly_pideal p"
      proof
        fix x assume "x ∈ J"
        then obtain r where "r ∈ poly_carrier" "x = r ⊗⇩P b"
          using JeqP unfolding poly_pideal_def by blast
        then show "x ∈ poly_pideal p" using poly_pideal_memI
          using I.Ideal(1) beq c' by presburger
      qed
      then have "J = poly_pideal p" using sub by blast
      then show ?thesis ..
    qed
  qed
  then show ?thesis using proper unfolding I.maximal_ideal_def by blast
qed

text ‹The principal ideal @{text "(p)"} is an ideal of the ∗‹commutative› polynomial ring, so
  the quotient theory of @{locale ideal_in_comm_ring} applies to it.›
lemma poly_pideal_in_comm_ring:
  assumes p: "p ∈ poly_carrier"
  shows "ideal_in_comm_ring (poly_pideal p) poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
  by (simp add: ideal_in_comm_ring.intro p poly_commutative_ring poly_pideal_is_ideal)

text ‹∗‹Kronecker's theorem.›  For an irreducible @{term p}, the principal ideal @{text "(p)"} is
  a maximal ideal of the ∗‹commutative› polynomial ring @{text "F[X]"}.  By the maximal-ideal
  characterisation @{thm [source] ideal_in_comm_ring.maximal_ideal_iff_quotient_field}, this is
  exactly the statement that the quotient @{text "F[X]/(p)"} is a field: it is nontrivial and
  every nonzero coset is invertible.›
theorem poly_quotient_field:
  assumes irr: "poly_irreducible p"
  shows "ideal_in_comm_ring (poly_pideal p) poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P
         ∧ Ideal.maximal_ideal (poly_pideal p) poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
  by (simp add: irr poly_irreducibleD_carrier poly_irreducible_maximal
      poly_pideal_in_comm_ring)


subsection ‹The size of the quotient ring›

text ‹Membership in the principal ideal @{text "(p)"} is detected by the remainder: @{term x} is a
  multiple of @{term p} iff @{term "pmod x p = 𝟬⇩P"}.›
lemma poly_pideal_iff_pmod:
  assumes p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P" and x: "x ∈ poly_carrier"
  shows "x ∈ poly_pideal p ⟷ pmod x p = 𝟬⇩P"
proof
  assume "x ∈ poly_pideal p"
  then obtain r where r: "r ∈ poly_carrier" and xr: "x = r ⊗⇩P p"
    unfolding poly_pideal_def by blast
  ― ‹‹x = (p ⊗ r) ⊕ 𝟬›, so its remainder is @{term "𝟬⇩P"}.›
  have "x = (p ⊗⇩P r) ⊕⇩P 𝟬⇩P"
    by (metis p poly_add_comm poly_add_zero poly_mult_comm poly_zero_closed r x xr) 
  then show "pmod x p = 𝟬⇩P"
    using pmod_unique[OF x p pnz r poly_zero_closed] by simp
next
  assume z: "pmod x p = 𝟬⇩P"
  obtain q where q: "q ∈ poly_carrier" and xeq: "x = (p ⊗⇩P q) ⊕⇩P pmod x p"
    using pmod_spec[OF x p pnz] by blast
  have "x = (p ⊗⇩P q) ⊕⇩P 𝟬⇩P" 
    using xeq z by simp
  also have "… = q ⊗⇩P p"
    using p q by (simp add: poly_add_comm poly_add_zero poly_mult_comm poly_zero_closed poly_mult_closed)
  finally have "x = q ⊗⇩P p" .
  then show "x ∈ poly_pideal p" using q by (auto simp: poly_pideal_def)
qed

text ‹The coset map ‹r ↦ coset r› restricted to @{term "low_poly (degree p)"}
  is a bijection onto the set of cosets: every coset has a unique representative of degree below
  @{term p}.  Injectivity is uniqueness of @{const pmod} (equal cosets have equal remainders, and a
  low-degree polynomial is its own remainder).›
theorem bij_betw_low_poly_cosets:
  assumes p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P"
  shows "bij_betw (Ideal.coset (poly_pideal p) poly_carrier (⊕⇩P) 𝟬⇩P)
                  (low_poly (degree p))
                  (Ideal.quotient_set (poly_pideal p) poly_carrier (⊕⇩P) 𝟬⇩P)"
proof -
  interpret I: ideal_in_comm_ring "poly_pideal p" poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
    by (rule poly_pideal_in_comm_ring[OF p])
  ― ‹Two carrier polynomials are in the same coset iff their difference is a multiple of @{term p}.›
  ― ‹The additive-group inverse in @{text "F[X]"} is the polynomial negation @{term "⊖⇩P y"}.›
  have inv_eq: "I.additive.inverse y = ⊖⇩P y" if y: "y ∈ poly_carrier" for y
    by (simp add: poly_diff_zero_eq poly_neg_closed poly_neg_neg y)
  have same_coset: "I.coset x = I.coset y ⟷ x ⊕⇩P (⊖⇩P y) ∈ poly_pideal p"
    if x: "x ∈ poly_carrier" and y: "y ∈ poly_carrier" for x y
    using I.coset_eq_iff[OF x y] by (simp add: inv_eq[OF y])
  ― ‹A polynomial of degree below @{term p} that is a multiple of @{term p} must be zero.›
  have low_mult_zero: "d = 𝟬⇩P"
    if dc: "d ∈ poly_carrier" "d = 𝟬⇩P ∨ degree d < degree p" "d ∈ poly_pideal p" for d
    by (metis that p pmod_small pnz poly_pideal_iff_pmod)
  show ?thesis
  proof (rule bij_betw_imageI)
    ― ‹Injective: equal cosets give equal remainders, and low-degree polys are their own remainders.›
    show "inj_on (I.coset) (low_poly (degree p))"
    proof (rule inj_onI)
      fix r1 r2 assume r1: "r1 ∈ low_poly (degree p)" and r2: "r2 ∈ low_poly (degree p)"
        and eq: "I.coset r1 = I.coset r2"
      have r1c: "r1 ∈ poly_carrier" using r1 by (rule low_poly_closed)
      have r2c: "r2 ∈ poly_carrier" using r2 by (rule low_poly_closed)
      have d1: "r1 = 𝟬⇩P ∨ degree r1 < degree p" using r1 r1c by (simp add: low_poly_iff_degree)
      have d2: "r2 = 𝟬⇩P ∨ degree r2 < degree p" using r2 r2c by (simp add: low_poly_iff_degree)
      ― ‹The difference is a low-degree multiple of @{term p}, hence zero.›
      have diffc: "r1 ⊕⇩P (⊖⇩P r2) ∈ poly_carrier"
        using r1c r2c poly_neg_closed by (simp add: poly_add_closed)
      have "r1 ⊕⇩P (⊖⇩P r2) ∈ poly_pideal p" using same_coset[OF r1c r2c] eq by simp
      moreover have "r1 ⊕⇩P (⊖⇩P r2) = 𝟬⇩P ∨ degree (r1 ⊕⇩P (⊖⇩P r2)) < degree p"
      proof (cases "r1 ⊕⇩P (⊖⇩P r2) = 𝟬⇩P")
        case False
        ― ‹The difference is nonzero, so @{term "degree p > 0"} (else @{term r1}, @{term r2} both zero).›
        have dp: "degree p > 0"
          using d1 d2 poly_add_neg_right False by force
        have "degree (r1 ⊕⇩P (⊖⇩P r2)) ≤ max (degree r1) (degree r2)"
          by (metis degree_add_le degree_neg poly_neg_closed r1c r2c)
        then show ?thesis using d1 d2 dp by auto
      qed simp
      ultimately have "r1 ⊕⇩P (⊖⇩P r2) = 𝟬⇩P" using low_mult_zero[OF diffc] by blast
      then show "r1 = r2" using poly_diff_zero_eq[OF r1c r2c] by simp
    qed
    ― ‹Image is exactly the set of cosets.›
    show "(I.coset) ` low_poly (degree p) = I.quotient_set"
    proof
      show "(I.coset) ` low_poly (degree p) ⊆ I.quotient_set"
        by (meson I.coset_in_quotient_set image_subsetI low_poly_closed)
      show "I.quotient_set ⊆ (I.coset) ` low_poly (degree p)"
      proof
        fix C assume "C ∈ I.quotient_set"
        then obtain a where a: "a ∈ poly_carrier" and Ca: "C = I.coset a"
          using I.quotient_set_repr by blast
        ― ‹The remainder of @{term a} is a low-degree representative of the same coset.›
        have mc: "pmod a p ∈ poly_carrier" using pmod_closed[OF a p pnz] .
        have pmc: "pmod a p ∈ low_poly (degree p)"
          using mc pmod_degree[OF a p pnz] by (simp add: low_poly_iff_degree)
        ― ‹‹a ⊕ ⊖(pmod a p) = p ⊗ q ∈ (p)›, so @{term a} and @{term "pmod a p"} share a coset.›
        obtain q where q: "q ∈ poly_carrier" and aeq: "a = (p ⊗⇩P q) ⊕⇩P pmod a p"
          using pmod_spec[OF a p pnz] by blast
        have pqc: "p ⊗⇩P q ∈ poly_carrier" using p q by (rule poly_mult_closed)
        ― ‹Cancel @{term "pmod a p"}: ‹a ⊕ ⊖(pmod a p) = p ⊗ q›.›
        have "a ⊕⇩P (⊖⇩P pmod a p) = p ⊗⇩P q"
          by (metis I.additive.commute_iff_inverse aeq inv_eq mc poly_add_comm pqc) 
        then have "a ⊕⇩P (⊖⇩P pmod a p) = q ⊗⇩P p"
          using poly_mult_comm[OF p q] by simp
        then have mem: "a ⊕⇩P (⊖⇩P pmod a p) ∈ poly_pideal p"
          using q by (simp add: poly_pideal_memI)
        have "I.coset a = I.coset (pmod a p)"
          by (rule iffD2[OF same_coset[OF a mc] mem])
        then show "C ∈ (I.coset) ` low_poly (degree p)"
          by (simp add: Ca pmc)
      qed
    qed
  qed
qed

text ‹∗‹The quotient ‹F[X]/(p)› has ‹¦F¦⇧d⇧e⇧g⇧p› elements› when the field @{term F} is finite:
  the cosets are in bijection with the @{term "card R ^ degree p"} polynomials of degree below
  @{term p}.›
theorem card_poly_quotient:
  assumes "finite R" "p ∈ poly_carrier" "p ≠ 𝟬⇩P"
  shows "card (Ideal.quotient_set (poly_pideal p) poly_carrier (⊕⇩P) 𝟬⇩P) = card R ^ degree p"
  by (metis bij_betw_low_poly_cosets bij_betw_same_card card_low_poly assms)


subsection ‹Divisibility and Euclid's lemma›

text ‹Divisibility in @{text "F[X]"}: @{term d} divides @{term x} when @{term x} is a multiple of
  @{term d}.  This is exactly membership of @{term x} in the principal ideal @{term "poly_pideal d"}.›
definition poly_dvd :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ bool"
  where "poly_dvd d x ⟷ (∃q. q ∈ poly_carrier ∧ x = q ⊗⇩P d)"

lemma poly_dvd_iff_mem_pideal: "poly_dvd d x ⟷ x ∈ poly_pideal d"
  unfolding poly_dvd_def poly_pideal_def by blast

text ‹A concrete divisibility witness with a polynomial divisor necessarily has a polynomial
  dividend.  This recovers the carrier condition after working with the ambient function type.›
lemma poly_dvd_closed:
  assumes dvd: "poly_dvd d x" and d: "d ∈ poly_carrier"
  shows "x ∈ poly_carrier"
proof -
  obtain q where q: "q ∈ poly_carrier" and xeq: "x = q ⊗⇩P d"
    using dvd unfolding poly_dvd_def by blast
  then show ?thesis using d by (simp add: poly_mult_closed)
qed

text ‹For a nonzero divisor, concrete polynomial divisibility is equivalent to having zero
  remainder under the polynomial division algorithm.›
lemma poly_dvd_iff_pmod_zero:
  assumes d: "d ∈ poly_carrier" and dnz: "d ≠ 𝟬⇩P"
    and x: "x ∈ poly_carrier"
  shows "poly_dvd d x ⟷ pmod x d = 𝟬⇩P"
  using poly_dvd_iff_mem_pideal poly_pideal_iff_pmod[OF d dnz x] by blast

text ‹∗‹Euclid's lemma / irreducibles are prime.›  For an irreducible @{term p}, if @{term p}
  divides a product @{term "a ⊗⇩P b"} then it divides one of the factors.  This is primality of the
  maximal ideal @{term "poly_pideal p"} (@{thm [source] ideal_in_comm_ring.maximal_imp_prime_ideal}
  applied to @{thm [source] poly_irreducible_maximal}).›
theorem poly_irreducible_prime:
  assumes irr: "poly_irreducible p"
    and a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
    and dvd: "poly_dvd p (a ⊗⇩P b)"
  shows "poly_dvd p a ∨ poly_dvd p b"
proof -
  have p: "p ∈ poly_carrier" using irr by (rule poly_irreducibleD_carrier)
  interpret I: ideal_in_comm_ring "poly_pideal p" poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
    by (rule poly_pideal_in_comm_ring[OF p])
  have "I.prime_ideal" using poly_irreducible_maximal[OF irr] by (rule I.maximal_imp_prime_ideal)
  ― ‹Primality: ‹a ⊗ b ∈ (p)› gives ‹a ∈ (p)› or ‹b ∈ (p)›.›
  have "a ∈ poly_pideal p ∨ b ∈ poly_pideal p"
    using I.prime_ideal_def ‹I.prime_ideal› a b dvd poly_dvd_iff_mem_pideal by blast
  then show ?thesis by (simp add: poly_dvd_iff_mem_pideal)
qed

text ‹An irreducible polynomial does not divide @{term "𝟭⇩P"} (else it would be a unit).›
lemma poly_irreducible_not_dvd_one:
  assumes irr: "poly_irreducible p" shows "¬ poly_dvd p 𝟭⇩P"
proof
  assume "poly_dvd p 𝟭⇩P"
  then obtain q where q: "q ∈ poly_carrier" and "𝟭⇩P = q ⊗⇩P p"
    unfolding poly_dvd_def by blast
  then have "poly_unit p" 
    using poly_unitI irr poly_irreducibleD_carrier poly_mult_comm by presburger
  with poly_irreducibleD_nonunit[OF irr] show False ..
qed

text ‹∗‹Euclid's lemma for products.›  If an irreducible @{term p} divides a product of a list of
  polynomials, it divides one of them.  (Base case: it cannot divide the empty product @{term "𝟭⇩P"};
  step: split off the head with @{thm [source] poly_irreducible_prime}.)›
lemma poly_irreducible_prime_list:
  assumes irr: "poly_irreducible p"
  shows "⟦ ∀f∈set fs. f ∈ poly_carrier; poly_dvd p (poly_prod fs) ⟧
           ⟹ ∃f∈set fs. poly_dvd p f"
proof (induct fs)
  case Nil
  then have "poly_dvd p 𝟭⇩P" by simp
  with poly_irreducible_not_dvd_one[OF irr] show ?case ..
next
  case (Cons g gs)
  have gc: "g ∈ poly_carrier" using Cons.prems(1) by simp
  have gsc: "∀f∈set gs. f ∈ poly_carrier" using Cons.prems(1) by simp
  have gsprod: "poly_prod gs ∈ poly_carrier"
    by (rule poly_prod_closed) (use gsc in blast)
  have "poly_dvd p (g ⊗⇩P poly_prod gs)" using Cons.prems(2) by simp
  then have "poly_dvd p g ∨ poly_dvd p (poly_prod gs)"
    using poly_irreducible_prime[OF irr gc gsprod] by simp
  then show ?case
    using Cons.hyps gsc by force
qed


subsection ‹Uniqueness of the irreducible factorisation›

text ‹A nonzero divisor has degree at most that of its multiple.›
lemma poly_dvd_degree_le:
  assumes dvd: "poly_dvd d x" and dc: "d ∈ poly_carrier" and xnz: "x ≠ 𝟬⇩P"
  shows "degree d ≤ degree x"
proof -
  obtain q where q: "q ∈ poly_carrier" and xeq: "x = q ⊗⇩P d"
    using dvd unfolding poly_dvd_def by blast
  have "degree x = degree q + degree d" using xeq degree_mult[OF q dc]
    using dc poly_mult_comm poly_mult_zero_right q xnz by force
  then show ?thesis by simp
qed

text ‹Two monic irreducibles that divide one another are equal: @{term p} dividing the irreducible
  @{term q} makes @{term p} a unit or an associate of @{term q}; being a non-unit monic, it equals
  the monic @{term q}.›
lemma monic_irreducible_dvd_eq:
  assumes ip: "poly_irreducible p" and iq: "poly_irreducible q"
    and mp: "poly_monic p" and mq: "poly_monic q" and dvd: "poly_dvd p q"
  shows "p = q"
proof -
  have p: "p ∈ poly_carrier" using ip by (rule poly_irreducibleD_carrier)
  have qc: "q ∈ poly_carrier" using iq by (rule poly_irreducibleD_carrier)
  obtain c where c: "c ∈ poly_carrier" and qcp: "q = c ⊗⇩P p" and uc: "poly_unit c"
    using dvd unfolding poly_dvd_def
    by (metis ip iq poly_irreducible_def)
  ― ‹@{term q} irreducible and @{term "q = c ⊗⇩P p"}: one of @{term c}, @{term p} is a unit.›
  ― ‹A unit has degree @{text 0}, so @{term c} is a nonzero constant and @{term p}, @{term q}
      have equal degree; being monic, they have equal leading terms too.›
  have cconst: "c = poly_const (c 0) ∧ c 0 ≠ 𝟬" and dc0: "degree c = 0"
    using poly_unit_imp_const[OF uc] by auto
  have c0R: "c 0 ∈ R" using c by (rule poly_carrier_coeff_closed)
  have pnz: "p ≠ 𝟬⇩P" using ip by (rule poly_irreducibleD_nonzero)
  ― ‹Leading coefficient of @{term "q = poly_const (c 0) ⊗⇩P p"} is @{term "c 0 ⋅ lead_coeff p"}.›
  have "lead_coeff q = c 0 ⋅ lead_coeff p"
    using qcp cconst lead_coeff_poly_const_mult[OF c0R _ p pnz] by simp
  moreover have "lead_coeff q = 𝟭"  "lead_coeff p = 𝟭" 
    using mp mq by (simp_all add: poly_monic_def)
  ultimately have "c 0 = 𝟭" using c0R by simp
  ― ‹Hence @{term "c = 𝟭⇩P"} and @{term "q = p"}.›
  then show ?thesis using qcp p
    using cconst poly_mult_one_left by auto
qed

text ‹Pulling a factor out of a product: if @{term g} occurs in @{term gs}, the product factors as
  @{term g} times the product of the rest.›
lemma poly_prod_remove1:
  assumes "g ∈ set gs" and "∀f∈set gs. f ∈ poly_carrier"
  shows "poly_prod gs = g ⊗⇩P poly_prod (remove1 g gs)"
  using assms
proof (induct gs)
  case Nil then show ?case by simp
next
  case (Cons h hs)
  show ?case
  proof (cases "g = h")
    case True then show ?thesis by simp
  next
    case False
    then have gs: "g ∈ set hs" and hc: "h ∈ poly_carrier" and hsc: "∀f∈set hs. f ∈ poly_carrier" 
      using Cons.prems by auto
    have gc: "g ∈ poly_carrier" using gs hsc by blast
    have hsprod: "poly_prod (remove1 g hs) ∈ poly_carrier"
      by (meson hsc notin_set_remove1 poly_prod_closed)
    have "poly_prod (h # hs) = h ⊗⇩P poly_prod hs" by simp
    also have "… = g ⊗⇩P (h ⊗⇩P poly_prod (remove1 g hs))"
      using hc gc hsprod Cons
      by (metis gs hsc poly_mult_assoc poly_mult_comm)
    finally show ?thesis
      using False by simp
  qed
qed


text ‹∗‹Uniqueness of the monic irreducible factorisation.›  Two lists of monic irreducibles with
  equal products are permutations of one another.  By induction on the first
  list: the head @{term f} divides the other product, hence equals some monic 
  irreducible @{term g} in it; cancel @{term f} and recurse on the remaining factors.›
theorem factorization_unique:
  "⟦ ∀f∈set fs. poly_irreducible f ∧ poly_monic f;
     ∀g∈set gs. poly_irreducible g ∧ poly_monic g;
     poly_prod fs = poly_prod gs ⟧ ⟹ mset fs = mset gs"
proof (induct fs arbitrary: gs)
  case Nil 
  ― ‹Empty product is @{term "𝟭⇩P"}; a nonempty @{term gs} would have an irreducible dividing
      @{term "𝟭⇩P"}.›
  have "gs = []"
  proof (rule ccontr)
    assume "gs ≠ []"
    then obtain g gs' where gs: "gs = g # gs'" by (cases gs) auto
    have ig: "poly_irreducible g" using Nil.prems(2) gs by simp
    have gsc: "∀f∈set gs. f ∈ poly_carrier"
      using Nil.prems(2) by (auto simp: poly_irreducibleD_carrier)
    have "poly_prod gs = 𝟭⇩P" using Nil.prems(3) by simp
    then have "g ⊗⇩P poly_prod gs' = 𝟭⇩P" using gs by simp
    ― ‹So @{term g} divides @{term "𝟭⇩P"} --- impossible for an irreducible.›
    moreover have "poly_prod gs' ∈ poly_carrier"
      using gsc gs by (auto intro!: poly_prod_closed)
    ultimately have "poly_dvd g 𝟭⇩P"
      unfolding poly_dvd_def
      using poly_irreducibleD_carrier[OF ig] by (metis poly_mult_comm)
    with poly_irreducible_not_dvd_one[OF ig] show False ..
  qed
  then show ?case using Nil.prems(3) by simp
next
  case (Cons f fs')
  have iff: "poly_irreducible f" and mf: "poly_monic f" using Cons.prems(1) by auto
  have fc: "f ∈ poly_carrier" using iff by (rule poly_irreducibleD_carrier)
  have fs'c: "∀h∈set fs'. poly_irreducible h ∧ poly_monic h" using Cons.prems(1) by simp
  have gsc: "∀g∈set gs. poly_irreducible g ∧ poly_monic g" using Cons.prems(2) .
  have gscarr: "∀g∈set gs. g ∈ poly_carrier"
    using gsc by (auto simp: poly_irreducibleD_carrier)
  have fs'carr: "∀h∈set fs'. h ∈ poly_carrier"
    using fs'c by (auto simp: poly_irreducibleD_carrier)
  have fs'prod: "poly_prod fs' ∈ poly_carrier"
    by (rule poly_prod_closed) (use fs'carr in blast)
  ― ‹@{term f} divides @{term "poly_prod gs = poly_prod (f # fs')"}, so divides some @{term g} in
      @{term gs}; both monic irreducibles, hence @{term "f = g"}.›
  have "poly_dvd f (poly_prod gs)"
    unfolding poly_dvd_def using Cons.prems(3) fs'prod by (metis poly_prod_Cons poly_mult_comm fc)
  then obtain g where g: "g ∈ set gs" and "poly_dvd f g"
    using poly_irreducible_prime_list[OF iff gscarr] by blast
  have ig: "poly_irreducible g" and mg: "poly_monic g" using gsc g by auto
  have feq: "f = g" using monic_irreducible_dvd_eq[OF iff ig mf mg ‹poly_dvd f g›] .
  ― ‹Cancel @{term f}: @{term "poly_prod fs' = poly_prod (remove1 g gs)"}.›
  have gc: "g ∈ poly_carrier" using ig by (rule poly_irreducibleD_carrier)
  have rprod: "poly_prod (remove1 g gs) ∈ poly_carrier"
    by (meson gscarr notin_set_remove1 poly_prod_closed)
  have gnz: "g ≠ 𝟬⇩P" using ig by (rule poly_irreducibleD_nonzero)
  have "g ⊗⇩P poly_prod fs' = g ⊗⇩P poly_prod (remove1 g gs)"
    using Cons.prems(3) feq g gscarr poly_prod_remove1 by auto
  then have "poly_prod fs' = poly_prod (remove1 g gs)"
    using poly_mult_left_cancel[OF gc gnz fs'prod rprod] by simp
  ― ‹Recurse on the remaining factors.›
  moreover have "∀g'∈set (remove1 g gs). poly_irreducible g' ∧ poly_monic g'"
    using gsc by (meson notin_set_remove1)
  ultimately show ?case
    using Cons.hyps[OF fs'c]
    by (simp add: feq g)
qed

end

end