Theory Square_Free_Int_To_Square_Free_GFp
section ‹Reconstructing Factors of Integer Polynomials›
subsection ‹Square-Free Polynomials over Finite Fields and Integers›
theory Square_Free_Int_To_Square_Free_GFp
imports
Subresultants.Subresultant_Gcd
Polynomial_Factorization.Rational_Factorization
Finite_Field
Polynomial_Factorization.Square_Free_Factorization
begin
lemma square_free_int_rat: assumes sf: "square_free f"
shows "square_free (map_poly rat_of_int f)"
proof -
let ?r = "map_poly rat_of_int"
from sf[unfolded square_free_def] have f0: "f ≠ 0" "⋀ q. degree q ≠ 0 ⟹ ¬ q * q dvd f" by auto
show ?thesis
proof (rule square_freeI)
show "?r f ≠ 0" using f0 by auto
fix q
assume dq: "degree q > 0" and dvd: "q * q dvd ?r f"
hence q0: "q ≠ 0" by auto
obtain q' c where norm: "rat_to_normalized_int_poly q = (c,q')" by force
from rat_to_normalized_int_poly[OF norm] have c0: "c ≠ 0" by auto
note q = rat_to_normalized_int_poly(1)[OF norm]
from dvd obtain k where rf: "?r f = q * (q * k)" unfolding dvd_def by (auto simp: ac_simps)
from rat_to_int_factor_explicit[OF this norm] obtain s where
f: "f = q' * smult (content f) s" by auto
let ?s = "smult (content f) s"
from arg_cong[OF f, of ?r] c0
have "?r f = q * (smult (inverse c) (?r ?s))"
by (simp add: field_simps q hom_distribs)
from arg_cong[OF this[unfolded rf], of "λ f. f div q"] q0
have "q * k = smult (inverse c) (?r ?s)"
by (metis nonzero_mult_div_cancel_left)
from arg_cong[OF this, of "smult c"] have "?r ?s = q * smult c k" using c0
by (auto simp: field_simps)
from rat_to_int_factor_explicit[OF this norm] obtain t where "?s = q' * t" by blast
from f[unfolded this] sf[unfolded square_free_def] f0 have "degree q' = 0" by auto
with rat_to_normalized_int_poly(4)[OF norm] dq show False by auto
qed
qed
lemma content_free_unit:
assumes "content (p::'a::{idom,semiring_gcd} poly) = 1"
shows "p dvd 1 ⟷ degree p = 0"
by (insert assms, auto dest!:degree0_coeffs simp: normalize_1_iff poly_dvd_1)
lemma square_free_imp_resultant_non_zero: assumes sf: "square_free (f :: int poly)"
shows "resultant f (pderiv f) ≠ 0"
proof (cases "degree f = 0")
case True
from degree0_coeffs[OF this] obtain c where f: "f = [:c:]" by auto
with sf have c: "c ≠ 0" unfolding square_free_def by auto
show ?thesis unfolding f by simp
next
case False note deg = this
define pp where "pp = primitive_part f"
define c where "c = content f"
from sf have f0: "f ≠ 0" unfolding square_free_def by auto
hence c0: "c ≠ 0" unfolding c_def by auto
have f: "f = smult c pp" unfolding c_def pp_def unfolding content_times_primitive_part[of f] ..
from sf[unfolded f] c0 have sf': "square_free pp" by (metis dvd_smult smult_0_right square_free_def)
from deg[unfolded f] c0 have deg': "⋀ x. degree pp > 0 ∨ x" by auto
from content_primitive_part[OF f0] have cp: "content pp = 1" unfolding pp_def .
let ?p' = "pderiv pp"
{
assume "resultant pp ?p' = 0"
from this[unfolded resultant_0_gcd] have "¬ coprime pp ?p'" by auto
then obtain r where r: "r dvd pp" "r dvd ?p'" "¬ r dvd 1"
by (blast elim: not_coprimeE)
from r(1) obtain k where "pp = r * k" ..
from pos_zmult_eq_1_iff_lemma[OF arg_cong[OF this,
of content, unfolded content_mult cp, symmetric]] content_ge_0_int[of r]
have cr: "content r = 1" by auto
with r(3) content_free_unit have dr: "degree r ≠ 0" by auto
let ?r = "map_poly rat_of_int"
from r(1) have dvd: "?r r dvd ?r pp" unfolding dvd_def by (auto simp: hom_distribs)
from r(2) have "?r r dvd ?r ?p'" apply (intro of_int_poly_hom.hom_dvd) by auto
also have "?r ?p' = pderiv (?r pp)" unfolding of_int_hom.map_poly_pderiv ..
finally have dvd': "?r r dvd pderiv (?r pp)" by auto
from dr have dr': "degree (?r r) ≠ 0" by simp
from square_free_imp_separable[OF square_free_int_rat[OF sf']]
have "separable (?r pp)" .
hence cop: "coprime (?r pp) (pderiv (?r pp))" unfolding separable_def .
from f0 f have pp0: "pp ≠ 0" by auto
from dvd dvd' have "?r r dvd gcd (?r pp) (pderiv (?r pp))" by auto
from divides_degree[OF this] pp0 have "degree (?r r) ≤ degree (gcd (?r pp) (pderiv (?r pp)))"
by auto
with dr' have "degree (gcd (?r pp) (pderiv (?r pp))) ≠ 0" by auto
hence "¬ coprime (?r pp) (pderiv (?r pp))" by auto
with cop have False by auto
}
hence "resultant pp ?p' ≠ 0" by auto
with resultant_smult_left[OF c0, of pp ?p', folded f] c0
have "resultant f ?p' ≠ 0" by auto
with resultant_smult_right[OF c0, of f ?p', folded pderiv_smult f] c0
show "resultant f (pderiv f) ≠ 0" by auto
qed
lemma large_mod_0: assumes "(n :: int) > 1" "¦k¦ < n" "k mod n = 0" shows "k = 0"
proof -
from ‹k mod n = 0› have "n dvd k"
by auto
then obtain m where "k = n * m" ..
with ‹n > 1› ‹¦k¦ < n› show ?thesis
by (auto simp add: abs_mult)
qed
definition separable_bound :: "int poly ⇒ int" where
"separable_bound f = max (abs (resultant f (pderiv f)))
(max (abs (lead_coeff f)) (abs (lead_coeff (pderiv f))))"
lemma square_free_int_imp_resultant_non_zero_mod_ring: assumes sf: "square_free f"
and large: "int CARD('a) > separable_bound f"
shows "resultant (map_poly of_int f :: 'a :: prime_card mod_ring poly) (pderiv (map_poly of_int f)) ≠ 0
∧ map_poly of_int f ≠ (0 :: 'a mod_ring poly)"
proof (intro conjI, rule notI)
let ?i = "of_int :: int ⇒ 'a mod_ring"
let ?m = "of_int_poly :: _ ⇒ 'a mod_ring poly"
let ?f = "?m f"
from sf[unfolded square_free_def] have f0: "f ≠ 0" by auto
hence lf: "lead_coeff f ≠ 0" by auto
{
fix k :: int
have C1: "int CARD('a) > 1" using prime_card[where 'a = 'a] by (auto simp: prime_nat_iff)
assume "abs k < CARD('a)" and "?i k = 0"
hence "k = 0" unfolding of_int_of_int_mod_ring
by (transfer) (rule large_mod_0[OF C1])
} note of_int_0 = this
from square_free_imp_resultant_non_zero[OF sf]
have non0: "resultant f (pderiv f) ≠ 0" .
{
fix g :: "int poly"
assume abs: "abs (lead_coeff g) < CARD('a)"
have "degree (?m g) = degree g" by (rule degree_map_poly, insert of_int_0[OF abs], auto)
} note deg = this
note large = large[unfolded separable_bound_def]
from of_int_0[of "lead_coeff f"] large lf have "?i (lead_coeff f) ≠ 0" by auto
thus f0: "?f ≠ 0" unfolding poly_eq_iff by auto
assume 0: "resultant ?f (pderiv ?f) = 0"
have "resultant ?f (pderiv ?f) = ?i (resultant f (pderiv f))"
unfolding of_int_hom.map_poly_pderiv[symmetric]
by (subst of_int_hom.resultant_map_poly(1)[OF deg deg], insert large, auto simp: hom_distribs)
from of_int_0[OF _ this[symmetric, unfolded 0]] non0
show False using large by auto
qed
lemma square_free_int_imp_separable_mod_ring: assumes sf: "square_free f"
and large: "int CARD('a) > separable_bound f"
shows "separable (map_poly of_int f :: 'a :: prime_card mod_ring poly)"
proof -
define g where "g = map_poly (of_int :: int ⇒ 'a mod_ring) f"
from square_free_int_imp_resultant_non_zero_mod_ring[OF sf large]
have res: "resultant g (pderiv g) ≠ 0" and g: "g ≠ 0" unfolding g_def by auto
from res[unfolded resultant_0_gcd] have "degree (gcd g (pderiv g)) = 0" by auto
from degree0_coeffs[OF this]
have "separable g" unfolding separable_def
by (metis degree_pCons_0 g gcd_eq_0_iff is_unit_gcd is_unit_iff_degree)
thus ?thesis unfolding g_def .
qed
lemma square_free_int_imp_square_free_mod_ring: assumes sf: "square_free f"
and large: "int CARD('a) > separable_bound f"
shows "square_free (map_poly of_int f :: 'a :: prime_card mod_ring poly)"
using separable_imp_square_free[OF square_free_int_imp_separable_mod_ring[OF assms]] .
end