section ‹Getting Small Representative Polynomials via Factorization› text ‹In this theory we import a factorization algorithm for integer polynomials to turn a representing polynomial of some algebraic number into a list of irreducible polynomials where exactly one list element represents the same number. Moreover, we prove that the certain polynomial operations preserve irreducibility, so that no factorization is required.› theory Factors_of_Int_Poly imports Berlekamp_Zassenhaus.Factorize_Int_Poly Algebraic_Numbers_Prelim begin lemma degree_of_gcd: "degree (gcd q r) ≠ 0 ⟷ degree (gcd (of_int_poly q :: 'a :: {field_char_0, field_gcd} poly) (of_int_poly r)) ≠ 0" proof - let ?r = "of_rat :: rat ⇒ 'a" interpret rpoly: field_hom' ?r by (unfold_locales, auto simp: of_rat_add of_rat_mult) { fix p have "of_int_poly p = map_poly (?r o of_int) p" unfolding o_def by auto also have "… = map_poly ?r (map_poly of_int p)" by (subst map_poly_map_poly, auto) finally have "of_int_poly p = map_poly ?r (map_poly of_int p)" . } note id = this show ?thesis unfolding id by (fold hom_distribs, simp add: gcd_rat_to_gcd_int) qed definition factors_of_int_poly :: "int poly ⇒ int poly list" where "factors_of_int_poly p = map (abs_int_poly o fst) (snd (factorize_int_poly p))" lemma factors_of_int_poly_const: assumes "degree p = 0" shows "factors_of_int_poly p = []" proof - from degree0_coeffs[OF assms] obtain a where p: "p = [: a :]" by auto show ?thesis unfolding p factors_of_int_poly_def factorize_int_poly_generic_def x_split_def by (cases "a = 0", auto simp add: Let_def factorize_int_last_nz_poly_def) qed lemma factors_of_int_poly: defines "rp ≡ ipoly :: int poly ⇒ 'a :: {field_gcd,field_char_0} ⇒ 'a" assumes "factors_of_int_poly p = qs" shows "⋀ q. q ∈ set qs ⟹ irreducible q ∧ lead_coeff q > 0 ∧ degree q ≤ degree p ∧ degree q ≠ 0" "p ≠ 0 ⟹ rp p x = 0 ⟷ (∃ q ∈ set qs. rp q x = 0)" "p ≠ 0 ⟹ rp p x = 0 ⟹ ∃! q ∈ set qs. rp q x = 0" "distinct qs" proof - obtain c qis where factt: "factorize_int_poly p = (c,qis)" by force from assms[unfolded factors_of_int_poly_def factt] have qs: "qs = map (abs_int_poly ∘ fst) (snd (c, qis))" by auto note fact = factorize_int_poly(1)[OF factt] note fact_mem = factorize_int_poly(2,3)[OF factt] have sqf: "square_free_factorization p (c, qis)" by (rule fact(1)) note sff = square_free_factorizationD[OF sqf] have sff': "p = Polynomial.smult c (∏(a, i)← qis. a ^ Suc i)" unfolding sff(1) prod.distinct_set_conv_list[OF sff(5)] .. { fix q assume q: "q ∈ set qs" then obtain r i where qi: "(r,i) ∈ set qis" and qr: "q = abs_int_poly r" unfolding qs by auto from split_list[OF qi] obtain qis1 qis2 where qis: "qis = qis1 @ (r,i) # qis2" by auto have dvd: "r dvd p" unfolding sff' qis dvd_def by (intro exI[of _ "smult c (r ^ i * (∏(a, i)←qis1 @ qis2. a ^ Suc i))"], auto) from fact_mem[OF qi] have r0: "r ≠ 0" by auto from qi factt have p: "p ≠ 0" by (cases p, auto) with dvd have deg: "degree r ≤ degree p" by (metis dvd_imp_degree_le) with fact_mem[OF qi] r0 show "irreducible q ∧ lead_coeff q > 0 ∧ degree q ≤ degree p ∧ degree q ≠ 0" unfolding qr lead_coeff_abs_int_poly by auto } note * = this show "distinct qs" unfolding distinct_conv_nth proof (intro allI impI) fix i j assume "i < length qs" "j < length qs" and diff: "i ≠ j" hence ij: "i < length qis" "j < length qis" and id: "qs ! i = abs_int_poly (fst (qis ! i))" "qs ! j = abs_int_poly (fst (qis ! j))" unfolding qs by auto obtain qi I where qi: "qis ! i = (qi, I)" by force obtain qj J where qj: "qis ! j = (qj, J)" by force from sff(5)[unfolded distinct_conv_nth, rule_format, OF ij diff] qi qj have diff: "(qi, I) ≠ (qj, J)" by auto from ij qi qj have "(qi, I) ∈ set qis" "(qj, J) ∈ set qis" unfolding set_conv_nth by force+ from sff(3)[OF this diff] sff(2) this have cop: "coprime qi qj" "degree qi ≠ 0" "degree qj ≠ 0" by auto note i = cf_pos_poly_main[of qi, unfolded smult_prod monom_0] note j = cf_pos_poly_main[of qj, unfolded smult_prod monom_0] from cop(2) i have deg: "degree (qs ! i) ≠ 0" by (auto simp: id qi) have cop: "coprime (qs ! i) (qs ! j)" unfolding id qi qj fst_conv apply (rule coprime_prod[of "[:sgn (lead_coeff qi):]" "[:sgn (lead_coeff qj):]"]) using cop unfolding i j by (auto simp: sgn_eq_0_iff) show "qs ! i ≠ qs ! j" proof assume id: "qs ! i = qs ! j" have "degree (gcd (qs ! i) (qs ! j)) = degree (qs ! i)" unfolding id by simp also have "… ≠ 0" using deg by simp finally show False using cop by simp qed qed assume p: "p ≠ 0" from fact(1) p have c: "c ≠ 0" using sff(1) by auto let ?r = "of_int :: int ⇒ 'a" let ?rp = "map_poly ?r" have rp: "⋀ x p. rp p x = 0 ⟷ poly (?rp p) x = 0" unfolding rp_def .. have "rp p x = 0 ⟷ rp (∏(x, y)←qis. x ^ Suc y) x = 0" unfolding sff'(1) unfolding rp hom_distribs using c by simp also have "… = (∃ (q,i) ∈set qis. poly (?rp (q ^ Suc i)) x = 0)" unfolding qs rp of_int_poly_hom.hom_prod_list poly_prod_list_zero_iff set_map by fastforce also have "… = (∃ (q,i) ∈set qis. poly (?rp q) x = 0)" unfolding of_int_poly_hom.hom_power poly_power_zero_iff by auto also have "… = (∃ q ∈ fst ` set qis. poly (?rp q) x = 0)" by force also have "… = (∃ q ∈ set qs. rp q x = 0)" unfolding rp qs snd_conv o_def bex_simps set_map by simp finally show iff: "rp p x = 0 ⟷ (∃ q ∈ set qs. rp q x = 0)" by auto assume "rp p x = 0" with iff obtain q where q: "q ∈ set qs" and rtq: "rp q x = 0" by auto then obtain i q' where qi: "(q',i) ∈ set qis" and qq': "q = abs_int_poly q'" unfolding qs by auto show "∃! q ∈ set qs. rp q x = 0" proof (intro ex1I, intro conjI, rule q, rule rtq, clarify) fix r assume "r ∈ set qs" and rtr: "rp r x = 0" then obtain j r' where rj: "(r',j) ∈ set qis" and rr': "r = abs_int_poly r'" unfolding qs by auto from rtr rtq have rtr: "rp r' x = 0" and rtq: "rp q' x = 0" unfolding rp rr' qq' by auto from rtr rtq have "[:-x,1:] dvd ?rp q'" "[:-x,1:] dvd ?rp r'" unfolding rp by (auto simp: poly_eq_0_iff_dvd) hence "[:-x,1:] dvd gcd (?rp q') (?rp r')" by simp hence "gcd (?rp q') (?rp r') = 0 ∨ degree (gcd (?rp q') (?rp r')) ≠ 0" by (metis is_unit_gcd_iff is_unit_iff_degree is_unit_pCons_iff one_poly_eq_simps(1)) hence "gcd q' r' = 0 ∨ degree (gcd q' r') ≠ 0" unfolding gcd_eq_0_iff degree_of_gcd[of q' r',symmetric] by auto hence "¬ coprime q' r'" by auto with sff(3)[OF qi rj] have "q' = r'" by auto thus "r = q" unfolding rr' qq' by simp qed qed lemma factors_int_poly_represents: fixes x :: "'a :: {field_char_0,field_gcd}" assumes p: "p represents x" shows "∃ q ∈ set (factors_of_int_poly p). q represents x ∧ irreducible q ∧ lead_coeff q > 0 ∧ degree q ≤ degree p" proof - from representsD[OF p] have p: "p ≠ 0" and rt: "ipoly p x = 0" by auto note fact = factors_of_int_poly[OF refl] from fact(2)[OF p, of x] rt obtain q where q: "q ∈ set (factors_of_int_poly p)" and rt: "ipoly q x = 0" by auto from fact(1)[OF q] rt show ?thesis by (intro bexI[OF _ q], auto simp: represents_def irreducible_def) qed corollary irreducible_represents_imp_degree: fixes x :: "'a :: {field_char_0,field_gcd}" assumes "irreducible f" and "f represents x" and "g represents x" shows "degree f ≤ degree g" proof - from factors_of_int_poly(1)[OF refl, of _ g] factors_of_int_poly(3)[OF refl, of g x] assms(3) obtain h where *: "h represents x" "degree h ≤ degree g" "irreducible h" by blast let ?af = "abs_int_poly f" let ?ah = "abs_int_poly h" from assms have af: "irreducible ?af" "?af represents x" "lead_coeff ?af > 0" by fastforce+ from * have ah: "irreducible ?ah" "?ah represents x" "lead_coeff ?ah > 0" by fastforce+ from algebraic_imp_represents_unique[of x] af ah have id: "?af = ?ah" unfolding algebraic_iff_represents by blast show ?thesis using arg_cong[OF id, of degree] ‹degree h ≤ degree g› by simp qed lemma irreducible_preservation: fixes x :: "'a :: {field_char_0,field_gcd}" assumes irr: "irreducible p" and x: "p represents x" and y: "q represents y" and deg: "degree p ≥ degree q" and f: "⋀ q. q represents y ⟹ (f q) represents x ∧ degree (f q) ≤ degree q" and pr: "primitive q" shows "irreducible q" proof (rule ccontr) define pp where "pp = abs_int_poly p" have dp: "degree p ≠ 0" using x by (rule represents_degree) have dq: "degree q ≠ 0" using y by (rule represents_degree) from dp have p0: "p ≠ 0" by auto from x deg irr p0 have irr: "irreducible pp" and x: "pp represents x" and deg: "degree pp ≥ degree q" and cf_pos: "lead_coeff pp > 0" unfolding pp_def lead_coeff_abs_int_poly by (auto intro!: representsI) from x have ax: "algebraic x" unfolding algebraic_altdef_ipoly represents_def by blast assume "¬ ?thesis" from this irreducible_connect_int[of q] pr have "¬ irreducible⇩_{d}q" by auto from this dq obtain r where r: "degree r ≠ 0" "degree r < degree q" and "r dvd q" by auto then obtain rr where q: "q = r * rr" unfolding dvd_def by auto have "degree q = degree r + degree rr" using dq unfolding q by (subst degree_mult_eq, auto) with r have rr: "degree rr ≠ 0" "degree rr < degree q" by auto from representsD(2)[OF y, unfolded q hom_distribs] have "ipoly r y = 0 ∨ ipoly rr y = 0" by auto with r rr have "r represents y ∨ rr represents y" unfolding represents_def by auto with r rr obtain r where r: "r represents y" "degree r < degree q" by blast from f[OF r(1)] deg r(2) obtain r where r: "r represents x" "degree r < degree pp" by auto from factors_int_poly_represents[OF r(1)] r(2) obtain r where r: "r represents x" "irreducible r" "lead_coeff r > 0" and deg: "degree r < degree pp" by force from algebraic_imp_represents_unique[OF ax] r irr cf_pos x have "r = pp" by auto with deg show False by auto qed declare irreducible_const_poly_iff [simp] lemma poly_uminus_irreducible: assumes p: "irreducible (p :: int poly)" and deg: "degree p ≠ 0" shows "irreducible (poly_uminus p)" proof- from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto from represents_uminus[OF x] have y: "poly_uminus p represents (- x)" . show ?thesis proof (rule irreducible_preservation[OF p x y], force) from deg irreducible_imp_primitive[OF p] have "primitive p" by auto then show "primitive (poly_uminus p)" by simp fix q assume "q represents (- x)" from represents_uminus[OF this] have "(poly_uminus q) represents x" by simp thus "(poly_uminus q) represents x ∧ degree (poly_uminus q) ≤ degree q" by auto qed qed lemma reflect_poly_irreducible: fixes x :: "'a :: {field_char_0,field_gcd}" assumes p: "irreducible p" and x: "p represents x" and x0: "x ≠ 0" shows "irreducible (reflect_poly p)" proof - from represents_inverse[OF x0 x] have y: "(reflect_poly p) represents (inverse x)" by simp from x0 have ix0: "inverse x ≠ 0" by auto show ?thesis proof (rule irreducible_preservation[OF p x y]) from x irreducible_imp_primitive[OF p] show "primitive (reflect_poly p)" by (auto simp: content_reflect_poly) fix q assume "q represents (inverse x)" from represents_inverse[OF ix0 this] have "(reflect_poly q) represents x" by simp with degree_reflect_poly_le show "(reflect_poly q) represents x ∧ degree (reflect_poly q) ≤ degree q" by auto qed (insert p, auto simp: degree_reflect_poly_le) qed lemma poly_add_rat_irreducible: assumes p: "irreducible p" and deg: "degree p ≠ 0" shows "irreducible (cf_pos_poly (poly_add_rat r p))" proof - from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto from represents_add_rat[OF x] have y: "cf_pos_poly (poly_add_rat r p) represents (of_rat r + x)" by simp show ?thesis proof (rule irreducible_preservation[OF p x y], force) fix q assume "q represents (of_rat r + x)" from represents_add_rat[OF this, of "- r"] have "(poly_add_rat (- r) q) represents x" by (simp add: of_rat_minus) thus "(poly_add_rat (- r) q) represents x ∧ degree (poly_add_rat (- r) q) ≤ degree q" by auto qed (insert p, auto) qed lemma poly_mult_rat_irreducible: assumes p: "irreducible p" and deg: "degree p ≠ 0" and r: "r ≠ 0" shows "irreducible (cf_pos_poly (poly_mult_rat r p))" proof - from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto from represents_mult_rat[OF r x] have y: "cf_pos_poly (poly_mult_rat r p) represents (of_rat r * x)" by simp show ?thesis proof (rule irreducible_preservation[OF p x y], force simp: r) fix q from r have r': "inverse r ≠ 0" by simp assume "q represents (of_rat r * x)" from represents_mult_rat[OF r' this] have "(poly_mult_rat (inverse r) q) represents x" using r by (simp add: of_rat_divide field_simps) thus "(poly_mult_rat (inverse r) q) represents x ∧ degree (poly_mult_rat (inverse r) q) ≤ degree q" using r by auto qed (insert p r, auto) qed interpretation coeff_lift_hom: factor_preserving_hom "coeff_lift :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} ⇒ _" by (unfold_locales, auto) end