Theory Card_Irreducible_Polynomials_Aux
section ‹Counting Irreducible Polynomials \label{sec:card_irred}›
subsection ‹The polynomial $X^n - X$›
theory Card_Irreducible_Polynomials_Aux
imports
"HOL-Algebra.Multiplicative_Group"
Formal_Polynomial_Derivatives
Monic_Polynomial_Factorization
begin
lemma (in domain)
assumes "subfield K R"
assumes "f ∈ carrier (K[X])" "degree f > 0"
shows embed_inj: "inj_on (rupture_surj K f ∘ poly_of_const) K"
and rupture_order: "order (Rupt K f) = card K^degree f"
and rupture_char: "char (Rupt K f) = char R"
proof -
interpret p: principal_domain "K[X]"
using univ_poly_is_principal[OF assms(1)] by simp
interpret I: ideal "PIdl⇘K[X]⇙ f" "K[X]"
using p.cgenideal_ideal[OF assms(2)] by simp
interpret d: ring "Rupt K f"
unfolding rupture_def using I.quotient_is_ring by simp
have e: "subring K R"
using assms(1) subfieldE(1) by auto
interpret h:
ring_hom_ring "R ⦇ carrier := K ⦈"
"Rupt K f" "rupture_surj K f ∘ poly_of_const"
using rupture_surj_norm_is_hom[OF e assms(2)]
using ring_hom_ringI2 subring_is_ring d.ring_axioms e
by blast
have "field (R ⦇carrier := K⦈)"
using assms(1) subfield_iff(2) by simp
hence "subfield K (R⦇carrier := K⦈)"
using ring.subfield_iff[OF subring_is_ring[OF e]] by simp
hence b: "subfield (rupture_surj K f ` poly_of_const ` K) (Rupt K f)"
unfolding image_image comp_def[symmetric]
by (intro h.img_is_subfield rupture_one_not_zero assms, simp)
have "inj_on poly_of_const K"
using poly_of_const_inj inj_on_subset by auto
moreover have
"poly_of_const ` K ⊆ ((λq. q pmod f) ` carrier (K [X]))"
proof (rule image_subsetI)
fix x assume "x ∈ K"
hence f:
"poly_of_const x ∈ carrier (K[X])"
"degree (poly_of_const x) = 0"
using poly_of_const_over_subfield[OF assms(1)] by auto
moreover
have "degree (poly_of_const x) < degree f"
using f(2) assms by simp
hence "poly_of_const x pmod f = poly_of_const x"
by (intro pmod_const(2)[OF assms(1)] f assms(2), simp)
ultimately show
"poly_of_const x ∈ ((λq. q pmod f) ` carrier (K [X]))"
by force
qed
hence "inj_on (rupture_surj K f) (poly_of_const ` K)"
using rupture_surj_inj_on[OF assms(1,2)] inj_on_subset by blast
ultimately show d: "inj_on (rupture_surj K f ∘ poly_of_const) K"
using comp_inj_on by auto
have a: "d.dimension (degree f) (rupture_surj K f ` poly_of_const ` K)
(carrier (Rupt K f))"
using rupture_dimension[OF assms(1-3)] by auto
then obtain base where base_def:
"set base ⊆ carrier (Rupt K f)"
"d.independent (rupture_surj K f ` poly_of_const ` K) base"
"length base = degree f"
"d.Span (rupture_surj K f ` poly_of_const ` K) base =
carrier (Rupt K f)"
using d.exists_base[OF b a] by auto
have "order (Rupt K f) =
card (d.Span (rupture_surj K f ` poly_of_const ` K) base)"
unfolding order_def base_def(4) by simp
also have "... =
card (rupture_surj K f ` poly_of_const ` K) ^ length base"
using d.card_span[OF b base_def(2,1)] by simp
also have "...
= card ((rupture_surj K f ∘ poly_of_const) ` K) ^ degree f"
using base_def(3) image_image unfolding comp_def by metis
also have "... = card K^degree f"
by (subst card_image[OF d], simp)
finally show "order (Rupt K f) = card K^degree f" by simp
have "char (Rupt K f) = char (R ⦇ carrier := K ⦈)"
using h.char_consistent d by simp
also have "... = char R"
using char_consistent[OF subfieldE(1)[OF assms(1)]] by simp
finally show "char (Rupt K f) = char R" by simp
qed
definition gauss_poly where
"gauss_poly K n = X⇘K⇙ [^]⇘poly_ring K⇙ (n::nat) ⊖⇘poly_ring K⇙ X⇘K⇙"
context field
begin
interpretation polynomial_ring "R" "carrier R"
unfolding polynomial_ring_def polynomial_ring_axioms_def
using field_axioms carrier_is_subfield by simp
text ‹The following lemma can be found in Ireland and Rosen~\<^cite>‹‹\textsection 7.1, Lemma 2› in "ireland1982"›.›
lemma gauss_poly_div_gauss_poly_iff_1:
fixes l m :: nat
assumes "l > 0"
shows "(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) pdivides (X [^]⇘P⇙ m ⊖⇘P⇙ 𝟭⇘P⇙) ⟷ l dvd m"
(is "?lhs ⟷ ?rhs")
proof -
define q where "q = m div l"
define r where "r = m mod l"
have m_def: "m = q * l + r" and r_range: "r < l"
using assms by (auto simp add:q_def r_def)
have pow_sum_carr:"(⨁⇘P⇙i∈{..<q}. (X [^]⇘P⇙ l)[^]⇘P⇙ i) ∈ carrier P"
using var_pow_closed
by (intro p.finsum_closed, simp)
have "(X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙) = ((X [^]⇘P⇙ l)[^]⇘P⇙ q) ⊖⇘P⇙ 𝟭⇘P⇙"
using var_closed
by (subst p.nat_pow_pow, simp_all add:algebra_simps)
also have "... =
(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) ⊗⇘P⇙ (⨁⇘P⇙i∈{..<q}. (X [^]⇘P⇙ l) [^]⇘P⇙ i)"
using var_pow_closed
by (subst p.geom[symmetric], simp_all)
finally have pow_sum_fact: "(X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙) =
(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) ⊗⇘P⇙ (⨁⇘P⇙i∈{..<q}. (X⇘R⇙ [^]⇘P⇙ l) [^]⇘P⇙ i)"
by simp
have "(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) divides⇘P⇙ (X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙)"
by (rule dividesI[OF pow_sum_carr pow_sum_fact])
hence c:"(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) divides⇘P⇙ X [^]⇘P⇙ r ⊗⇘P⇙ (X [^]⇘P⇙ (q * l) ⊖⇘P⇙ 𝟭⇘P⇙)"
using var_pow_closed
by (intro p.divides_prod_l, auto)
have "(X [^]⇘P⇙ m ⊖⇘P⇙ 𝟭⇘P⇙) = X [^]⇘P⇙ (r + q * l) ⊖⇘P⇙ 𝟭⇘P⇙"
unfolding m_def using add.commute by metis
also have "... = (X [^]⇘P⇙ r) ⊗⇘P⇙ (X [^]⇘P⇙ (q*l)) ⊕⇘P⇙ (⊖⇘P⇙ 𝟭⇘P⇙)"
using var_closed
by (subst p.nat_pow_mult, auto simp add:a_minus_def)
also have "... = ((X [^]⇘P⇙ r) ⊗⇘P⇙ (X [^]⇘P⇙ (q*l) ⊕⇘P⇙ (⊖⇘P⇙ 𝟭⇘P⇙))
⊕⇘P⇙ (X [^]⇘P⇙ r)) ⊖⇘P⇙ 𝟭⇘P⇙"
using var_pow_closed
by algebra
also have "... = (X [^]⇘P⇙ r) ⊗⇘P⇙ (X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙)
⊕⇘P⇙ (X [^]⇘P⇙ r) ⊖⇘P⇙ 𝟭⇘P⇙"
by algebra
also have "... = (X [^]⇘P⇙ r) ⊗⇘P⇙ (X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙)
⊕⇘P⇙ ((X [^]⇘P⇙ r) ⊖⇘P⇙ 𝟭⇘P⇙)"
unfolding a_minus_def using var_pow_closed
by (subst p.a_assoc, auto)
finally have a:"(X [^]⇘P⇙ m ⊖⇘P⇙ 𝟭⇘P⇙) =
(X [^]⇘P⇙ r) ⊗⇘P⇙ (X [^]⇘P⇙ (q*l) ⊖⇘P⇙ 𝟭⇘P⇙) ⊕⇘P⇙ (X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙)"
(is "_ = ?x")
by simp
have xn_m_1_deg': "degree (X [^]⇘P⇙ n ⊖⇘P⇙ 𝟭⇘P⇙) = n"
if "n > 0" for n :: nat
proof -
have "degree (X [^]⇘P⇙ n ⊖⇘P⇙ 𝟭⇘P⇙) = degree (X [^]⇘P⇙ n ⊕⇘P⇙ ⊖⇘P⇙ 𝟭⇘P⇙)"
by (simp add:a_minus_def)
also have "... = max (degree (X [^]⇘P⇙ n)) (degree (⊖⇘P⇙ 𝟭⇘P⇙))"
using var_pow_closed var_pow_carr var_pow_degree
using univ_poly_a_inv_degree degree_one that
by (subst degree_add_distinct, auto)
also have "... = n"
using var_pow_degree degree_one univ_poly_a_inv_degree
by simp
finally show ?thesis by simp
qed
have xn_m_1_deg: "degree (X [^]⇘P⇙ n ⊖⇘P⇙ 𝟭⇘P⇙) = n" for n :: nat
proof (cases "n > 0")
case True
then show ?thesis using xn_m_1_deg' by auto
next
case False
hence "n = 0" by simp
hence "degree (X [^]⇘P⇙ n ⊖⇘P⇙ 𝟭⇘P⇙) = degree (𝟬⇘P⇙)"
by (intro arg_cong[where f="degree"], simp)
then show ?thesis using False by (simp add:univ_poly_zero)
qed
have b: "degree (X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) > degree (X⇘R⇙ [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙)"
using r_range unfolding xn_m_1_deg by simp
have xn_m_1_carr: "X [^]⇘P⇙ n ⊖⇘P⇙ 𝟭⇘P⇙ ∈ carrier P" for n :: nat
unfolding a_minus_def
by (intro p.a_closed var_pow_closed, simp)
have "?lhs ⟷ (X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) pdivides ?x"
by (subst a, simp)
also have "... ⟷ (X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) pdivides (X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙)"
unfolding pdivides_def
by (intro p.div_sum_iff c var_pow_closed
xn_m_1_carr p.a_closed p.m_closed)
also have "... ⟷ r = 0"
proof (cases "r = 0")
case True
have "(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) pdivides 𝟬⇘P⇙"
unfolding univ_poly_zero
by (intro pdivides_zero xn_m_1_carr)
also have "... = (X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙)"
by (simp add:a_minus_def True) algebra
finally show ?thesis using True by simp
next
case False
hence "degree (X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙) > 0" using xn_m_1_deg by simp
hence "X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙ ≠ []" by auto
hence "¬(X [^]⇘P⇙ l ⊖⇘P⇙ 𝟭⇘P⇙) pdivides (X [^]⇘P⇙ r ⊖⇘P⇙ 𝟭⇘P⇙)"
using pdivides_imp_degree_le b xn_m_1_carr
by (metis le_antisym less_or_eq_imp_le nat_neq_iff)
thus ?thesis using False by simp
qed
also have "... ⟷ l dvd m"
unfolding m_def using r_range assms by auto
finally show ?thesis
by simp
qed
lemma gauss_poly_factor:
assumes "n > 0"
shows "gauss_poly R n = (X [^]⇘P⇙ (n-1) ⊖⇘P⇙ 𝟭⇘P⇙) ⊗⇘P⇙ X" (is "_ = ?rhs")
proof -
have a:"1 + (n - 1) = n"
using assms by simp
have "gauss_poly R n = X [^]⇘P⇙ (1+(n-1)) ⊖⇘P⇙ X"
unfolding gauss_poly_def by (subst a, simp)
also have "... = (X [^]⇘P⇙ (n-1)) ⊗⇘P⇙ X ⊖⇘P⇙ 𝟭⇘P⇙ ⊗⇘P⇙ X"
using var_closed by simp
also have "... = ?rhs"
unfolding a_minus_def using var_closed l_one
by (subst p.l_distr, auto, algebra)
finally show ?thesis by simp
qed
lemma var_neq_zero: "X ≠ 𝟬⇘P⇙"
by (simp add:var_def univ_poly_zero)
lemma var_pow_eq_one_iff: "X [^]⇘P⇙ k = 𝟭⇘P⇙ ⟷ k = (0::nat)"
proof (cases "k=0")
case True
then show ?thesis using var_closed(1) by simp
next
case False
have "degree (X⇘R⇙ [^]⇘P⇙ k) = k "
using var_pow_degree by simp
also have "... ≠ degree (𝟭⇘P⇙)" using False degree_one by simp
finally have "degree (X⇘R⇙ [^]⇘P⇙ k) ≠ degree 𝟭⇘P⇙" by simp
then show ?thesis by auto
qed
lemma gauss_poly_carr: "gauss_poly R n ∈ carrier P"
using var_closed(1)
unfolding gauss_poly_def by simp
lemma gauss_poly_degree:
assumes "n > 1"
shows "degree (gauss_poly R n) = n"
proof -
have "degree (gauss_poly R n) = max n 1"
unfolding gauss_poly_def a_minus_def
using var_pow_carr var_carr degree_var
using var_pow_degree univ_poly_a_inv_degree
using assms by (subst degree_add_distinct, auto)
also have "... = n" using assms by simp
finally show ?thesis by simp
qed
lemma gauss_poly_not_zero:
assumes "n > 1"
shows "gauss_poly R n ≠ 𝟬⇘P⇙"
proof -
have "degree (gauss_poly R n) ≠ degree ( 𝟬⇘P⇙)"
using assms by (subst gauss_poly_degree, simp_all add:univ_poly_zero)
thus ?thesis by auto
qed
lemma gauss_poly_monic:
assumes "n > 1"
shows "monic_poly R (gauss_poly R n)"
proof -
have "monic_poly R (X [^]⇘P⇙ n)"
by (intro monic_poly_pow monic_poly_var)
moreover have "⊖⇘P⇙ X ∈ carrier P"
using var_closed by simp
moreover have "degree (⊖⇘P⇙ X) < degree (X [^]⇘P⇙ n)"
using assms univ_poly_a_inv_degree var_closed
using degree_var
unfolding var_pow_degree by (simp)
ultimately show ?thesis
unfolding gauss_poly_def a_minus_def
by (intro monic_poly_add_distinct, auto)
qed
lemma geom_nat:
fixes q :: nat
fixes x :: "_ :: {comm_ring,monoid_mult}"
shows "(x-1) * (∑i ∈ {..<q}. x^i) = x^q-1"
by (induction q, auto simp:algebra_simps)
text ‹The following lemma can be found in Ireland and Rosen~\<^cite>‹‹\textsection 7.1, Lemma 3› in "ireland1982"›.›
lemma gauss_poly_div_gauss_poly_iff_2:
fixes a :: int
fixes l m :: nat
assumes "l > 0" "a > 1"
shows "(a ^ l - 1) dvd (a ^ m - 1) ⟷ l dvd m"
(is "?lhs ⟷ ?rhs")
proof -
define q where "q = m div l"
define r where "r = m mod l"
have m_def: "m = q * l + r" and r_range: "r < l" "r ≥ 0"
using assms by (auto simp add:q_def r_def)
have "a ^ (l * q) - 1 = (a ^ l) ^ q - 1"
by (simp add: power_mult)
also have "... = (a^l - 1) * (∑i ∈ {..<q}. (a^l)^i)"
by (subst geom_nat[symmetric], simp)
finally have "a ^ (l * q) - 1 = (a^l - 1) * (∑i ∈ {..<q}. (a^l)^i)"
by simp
hence c:"a ^ l - 1 dvd a^ r * (a ^ (q * l) - 1)" by (simp add:mult.commute)
have "a ^ m - 1 = a ^ (r + q * l) - 1"
unfolding m_def using add.commute by metis
also have "... = (a ^ r) * (a ^ (q*l)) -1"
by (simp add: power_add)
also have "... = ((a ^ r) * (a ^ (q*l) -1)) + (a ^ r) - 1"
by (simp add: right_diff_distrib)
also have "... = (a ^ r) * (a ^ (q*l) - 1) + ((a ^ r) - 1)"
by simp
finally have a:
"a ^ m - 1 = (a ^ r) * (a ^ (q*l) - 1) + ((a ^ r) - 1)"
(is "_ = ?x")
by simp
have "?lhs ⟷ (a^l -1) dvd ?x"
by (subst a, simp)
also have "... ⟷ (a^l -1) dvd (a^r -1)"
using c dvd_add_right_iff by auto
also have "... ⟷ r = 0"
proof
assume "a ^ l - 1 dvd a ^ r - 1"
hence "a ^ l - 1 ≤ a ^ r -1 ∨ r = 0 "
using assms r_range zdvd_not_zless by force
moreover have "a ^ r < a^l" using assms r_range by simp
ultimately show "r= 0"by simp
next
assume "r = 0"
thus "a ^ l - 1 dvd a ^ r - 1" by simp
qed
also have "... ⟷ l dvd m"
using r_def by auto
finally show ?thesis by simp
qed
lemma gauss_poly_div_gauss_poly_iff:
assumes "m > 0" "n > 0" "a > 1"
shows "gauss_poly R (a^n) pdivides⇘R⇙ gauss_poly R (a^m)
⟷ n dvd m" (is "?lhs=?rhs")
proof -
have a:"a^m > 1" using assms one_less_power by blast
hence a1: "a^m > 0" by linarith
have b:"a^n > 1" using assms one_less_power by blast
hence b1:"a^n > 0" by linarith
have "?lhs ⟷
(X [^]⇘P⇙ (a^n-1) ⊖⇘P⇙ 𝟭⇘P⇙) ⊗⇘P⇙ X pdivides
(X [^]⇘P⇙ (a^m-1) ⊖⇘P⇙ 𝟭⇘P⇙) ⊗⇘P⇙ X"
using gauss_poly_factor a1 b1 by simp
also have "... ⟷
(X [^]⇘P⇙ (a^n-1) ⊖⇘P⇙ 𝟭⇘P⇙) pdivides
(X [^]⇘P⇙ (a^m-1) ⊖⇘P⇙ 𝟭⇘P⇙)"
using var_closed a b var_neq_zero
by (subst pdivides_mult_r, simp_all add:var_pow_eq_one_iff)
also have "... ⟷ a^n-1 dvd a^m-1"
using b
by (subst gauss_poly_div_gauss_poly_iff_1) simp_all
also have "... ⟷ int (a^n-1) dvd int (a^m-1)"
by (subst of_nat_dvd_iff, simp)
also have "... ⟷ int a^n-1 dvd int a^m-1"
using a b by (simp add:of_nat_diff)
also have "... ⟷ n dvd m"
using assms
by (subst gauss_poly_div_gauss_poly_iff_2) simp_all
finally show ?thesis by simp
qed
end
context finite_field
begin
interpretation polynomial_ring "R" "carrier R"
unfolding polynomial_ring_def polynomial_ring_axioms_def
using field_axioms carrier_is_subfield by simp
lemma div_gauss_poly_iff:
assumes "n > 0"
assumes "monic_irreducible_poly R f"
shows "f pdivides⇘R⇙ gauss_poly R (order R^n) ⟷ degree f dvd n"
proof -
have f_carr: "f ∈ carrier P"
using assms(2) unfolding monic_irreducible_poly_def
unfolding monic_poly_def by simp
have f_deg: "degree f > 0"
using assms(2) monic_poly_min_degree by fastforce
define K where "K = Rupt⇘R⇙ (carrier R) f"
have field_K: "field K"
using assms(2) unfolding K_def monic_irreducible_poly_def
unfolding monic_poly_def
by (subst rupture_is_field_iff_pirreducible) auto
have a: "order K = order R^degree f"
using rupture_order[OF carrier_is_subfield] f_carr f_deg
unfolding K_def order_def by simp
have char_K: "char K = char R"
using rupture_char[OF carrier_is_subfield] f_carr f_deg
unfolding K_def by simp
have "card (carrier K) > 0"
using a f_deg finite_field_min_order unfolding order_def by simp
hence d: "finite (carrier K)" using card_ge_0_finite by auto
interpret f: finite_field "K"
using field_K d by (intro finite_fieldI, simp_all)
interpret fp: polynomial_ring "K" "(carrier K)"
unfolding polynomial_ring_def polynomial_ring_axioms_def
using f.field_axioms f.carrier_is_subfield by simp
define φ where "φ = rupture_surj (carrier R) f"
interpret h:ring_hom_ring "P" "K" "φ"
unfolding K_def φ_def using f_carr rupture_surj_hom by simp
have embed_inj: "inj_on (φ ∘ poly_of_const) (carrier R)"
unfolding φ_def
using embed_inj[OF carrier_is_subfield f_carr f_deg] by simp
interpret r:ring_hom_ring "R" "P" "poly_of_const"
using canonical_embedding_ring_hom by simp
obtain rn where "order R = char K^rn" "rn > 0"
unfolding char_K using finite_field_order by auto
hence ord_rn: "order R ^n = char K^(rn * n)" using assms(1)
by (simp add: power_mult)
interpret q:ring_hom_cring "K" "K" "λx. x [^]⇘K⇙ order R^n"
using ord_rn
by (intro f.frobenius_hom f.finite_carr_imp_char_ge_0 d, simp)
have o1: "order R^degree f > 1"
using f_deg finite_field_min_order one_less_power
by blast
hence o11: "order R^degree f > 0" by linarith
have o2: "order R^n > 1"
using assms(1) finite_field_min_order one_less_power
by blast
hence o21: "order R^n > 0" by linarith
let ?g1 = "gauss_poly K (order R^degree f)"
let ?g2 = "gauss_poly K (order R^n)"
have g1_monic: "monic_poly K ?g1"
using f.gauss_poly_monic[OF o1] by simp
have c:"x [^]⇘K⇙ (order R^degree f) = x" if b:"x ∈ carrier K" for x
using b d order_pow_eq_self
unfolding a[symmetric]
by (intro f.order_pow_eq_self, auto)
have k_cycle:
"φ (poly_of_const x) [^]⇘K⇙ (order R^n) = φ(poly_of_const x)"
if k_cycle_1: "x ∈ carrier R" for x
proof -
have "φ (poly_of_const x) [^]⇘K⇙ (order R^n) =
φ (poly_of_const (x [^]⇘R⇙ (order R^n)))"
using k_cycle_1 by (simp add: h.hom_nat_pow r.hom_nat_pow)
also have "... = φ (poly_of_const x)"
using order_pow_eq_self' k_cycle_1 by simp
finally show ?thesis by simp
qed
have roots_g1: "pmult⇘K⇙ d ?g1 ≥ 1"
if roots_g1_assms: "degree d = 1" "monic_irreducible_poly K d" for d
proof -
obtain x where x_def: "x ∈ carrier K" "d = [𝟭⇘K⇙, ⊖⇘K⇙ x]"
using f.degree_one_monic_poly roots_g1_assms by auto
interpret x:ring_hom_cring "poly_ring K" "K" "(λp. f.eval p x)"
by (intro fp.eval_cring_hom x_def)
have "ring.eval K ?g1 x = 𝟬⇘K⇙"
unfolding gauss_poly_def a_minus_def
using fp.var_closed f.eval_var x_def c
by (simp, algebra)
hence "f.is_root ?g1 x"
using x_def f.gauss_poly_not_zero[OF o1]
unfolding f.is_root_def univ_poly_zero by simp
hence "[𝟭⇘K⇙, ⊖⇘K⇙ x] pdivides⇘K⇙ ?g1"
using f.is_root_imp_pdivides f.gauss_poly_carr by simp
hence "d pdivides⇘K⇙ ?g1" by (simp add:x_def)
thus "pmult⇘K⇙ d ?g1 ≥ 1"
using that f.gauss_poly_not_zero f.gauss_poly_carr o1
by (subst f.multiplicity_ge_1_iff_pdivides, simp_all)
qed
show ?thesis
proof
assume f:"f pdivides⇘R⇙ gauss_poly R (order R^n)"
have "(φ X) [^]⇘K⇙ (order R^n) ⊖⇘K⇙ (φ X⇘R⇙) =
φ (gauss_poly R (order R^n))"
unfolding gauss_poly_def a_minus_def using var_closed
by (simp add: h.hom_nat_pow)
also have "... = 𝟬⇘K⇙"
unfolding K_def φ_def using f_carr gauss_poly_carr f
by (subst rupture_eq_0_iff, simp_all)
finally have "(φ X⇘R⇙) [^]⇘K⇙ (order R^n) ⊖⇘K⇙ (φ X⇘R⇙) = 𝟬⇘K⇙"
by simp
hence g:"(φ X) [^]⇘K⇙ (order R^n) = (φ X)"
using var_closed by simp
have roots_g2: "pmult⇘K⇙ d ?g2 ≥ 1"
if roots_g2_assms: "degree d = 1" "monic_irreducible_poly K d" for d
proof -
obtain y where y_def: "y ∈ carrier K" "d = [𝟭⇘K⇙, ⊖⇘K⇙ y]"
using f.degree_one_monic_poly roots_g2_assms by auto
interpret x:ring_hom_cring "poly_ring K" "K" "(λp. f.eval p y)"
by (intro fp.eval_cring_hom y_def)
obtain x where x_def: "x ∈ carrier P" "y = φ x"
using y_def unfolding φ_def K_def rupture_def
unfolding FactRing_def A_RCOSETS_def'
by auto
let ?τ = "λi. poly_of_const (coeff x i)"
have test: "?τ i ∈ carrier P" for i
by (intro r.hom_closed coeff_range x_def)
have test_2: "coeff x i ∈ carrier R" for i
by (intro coeff_range x_def)
have x_coeff_carr: "i ∈ set x ⟹ i ∈ carrier R" for i
using x_def(1)
by (auto simp add:univ_poly_carrier[symmetric] polynomial_def)
have a:"map (φ ∘ poly_of_const) x ∈ carrier (poly_ring K)"
using rupture_surj_norm_is_hom[OF f_carr]
using domain_axioms f.domain_axioms embed_inj
by (intro carrier_hom'[OF x_def(1)])
(simp_all add:φ_def K_def)
have "(φ x) [^]⇘K⇙ (order R^n) =
f.eval (map (φ ∘ poly_of_const) x) (φ X) [^]⇘K⇙ (order R^n)"
unfolding φ_def K_def
by (subst rupture_surj_as_eval[OF f_carr x_def(1)], simp)
also have "... =
f.eval (map (λx. φ (poly_of_const x) [^]⇘K⇙ order R ^ n) x) (φ X)"
using a h.hom_closed var_closed(1)
by (subst q.ring.eval_hom[OF f.carrier_is_subring])
(simp_all add:comp_def g)
also have "... = f.eval (map (λx. φ (poly_of_const x)) x) (φ X)"
using k_cycle x_coeff_carr
by (intro arg_cong2[where f="f.eval"] map_cong, simp_all)
also have "... = (φ x)"
unfolding φ_def K_def
by (subst rupture_surj_as_eval[OF f_carr x_def(1)], simp add:comp_def)
finally have "φ x [^]⇘K⇙ order R ^ n = φ x" by simp
hence "y [^]⇘K⇙ (order R^n) = y" using x_def by simp
hence "ring.eval K ?g2 y = 𝟬⇘K⇙"
unfolding gauss_poly_def a_minus_def
using fp.var_closed f.eval_var y_def
by (simp, algebra)
hence "f.is_root ?g2 y"
using y_def f.gauss_poly_not_zero[OF o2]
unfolding f.is_root_def univ_poly_zero by simp
hence "d pdivides⇘K⇙ ?g2"
unfolding y_def
by (intro f.is_root_imp_pdivides f.gauss_poly_carr, simp)
thus "pmult⇘K⇙ d ?g2 ≥ 1"
using that f.gauss_poly_carr f.gauss_poly_not_zero o2
by (subst f.multiplicity_ge_1_iff_pdivides, auto)
qed
have inv_k_inj: "inj_on (λx. ⊖⇘K⇙ x) (carrier K)"
by (intro inj_onI, metis f.minus_minus)
let ?mip = "monic_irreducible_poly K"
have "sum' (λd. pmult⇘K⇙ d ?g1 * degree d) {d. ?mip d} = degree ?g1"
using f.gauss_poly_monic o1
by (subst f.degree_monic_poly', simp_all)
also have "... = order K"
using f.gauss_poly_degree o1 a by simp
also have "... = card ((λk. [𝟭⇘K⇙, ⊖⇘K⇙ k]) ` carrier K)"
unfolding order_def using inj_onD[OF inv_k_inj]
by (intro card_image[symmetric] inj_onI) (simp_all)
also have "... = card {d. ?mip d ∧ degree d = 1}"
using f.degree_one_monic_poly
by (intro arg_cong[where f="card"], simp add:set_eq_iff image_iff)
also have "... = sum (λd. 1) {d. ?mip d ∧ degree d = 1}"
by simp
also have "... = sum' (λd. 1) {d. ?mip d ∧ degree d = 1}"
by (intro sum.eq_sum[symmetric]
finite_subset[OF _ fp.finite_poly(1)[OF d]])
(auto simp:monic_irreducible_poly_def monic_poly_def)
also have "... = sum' (λd. of_bool (degree d = 1)) {d. ?mip d}"
by (intro sum.mono_neutral_cong_left' subsetI, simp_all)
also have "... ≤ sum' (λd. of_bool (degree d = 1)) {d. ?mip d}"
by simp
finally have "sum' (λd. pmult⇘K⇙ d ?g1 * degree d) {d. ?mip d}
≤ sum' (λd. of_bool (degree d = 1)) {d. ?mip d}"
by simp
moreover have
"pmult⇘K⇙ d ?g1 * degree d ≥ of_bool (degree d = 1)"
if v:"monic_irreducible_poly K d" for d
proof (cases "degree d = 1")
case True
then obtain x where "x ∈ carrier K" "d = [𝟭⇘K⇙, ⊖⇘K⇙ x]"
using f.degree_one_monic_poly v by auto
hence "pmult⇘K⇙ d ?g1 ≥ 1"
using roots_g1 v by simp
then show ?thesis using True by simp
next
case False
then show ?thesis by simp
qed
moreover have
"finite {d. ?mip d ∧ pmult⇘K⇙ d ?g1 * degree d > 0}"
by (intro finite_subset[OF _ f.factor_monic_poly_fin[OF g1_monic]]
subsetI) simp
ultimately have v2:
"∀d ∈ {d. ?mip d}. pmult⇘K⇙ d ?g1 * degree d =
of_bool (degree d = 1)"
by (intro sum'_eq_iff, simp_all add:not_le)
have "pmult⇘K⇙ d ?g1 ≤ pmult⇘K⇙ d ?g2" if "?mip d" for d
proof (cases "degree d = 1")
case True
hence "pmult⇘K⇙ d ?g1 = 1" using v2 that by auto
also have "... ≤ pmult⇘K⇙ d ?g2"
by (intro roots_g2 True that)
finally show ?thesis by simp
next
case False
hence "degree d > 1"
using f.monic_poly_min_degree[OF that] by simp
hence "pmult⇘K⇙ d ?g1 = 0" using v2 that by force
then show ?thesis by simp
qed
hence "?g1 pdivides⇘K⇙ ?g2"
using o1 o2 f.divides_monic_poly f.gauss_poly_monic by simp
thus "degree f dvd n"
by (subst (asm) f.gauss_poly_div_gauss_poly_iff
[OF assms(1) f_deg finite_field_min_order], simp)
next
have d:"φ X⇘R⇙ ∈ carrier K"
by (intro h.hom_closed var_closed)
have "φ (gauss_poly R (order R^degree f)) =
(φ X⇘R⇙) [^]⇘K⇙ (order R^degree f) ⊖⇘K⇙ (φ X⇘R⇙)"
unfolding gauss_poly_def a_minus_def using var_closed
by (simp add: h.hom_nat_pow)
also have "... = 𝟬⇘K⇙"
using c d by simp
finally have "φ (gauss_poly R (order R^degree f)) = 𝟬⇘K⇙" by simp
hence "f pdivides⇘R⇙ gauss_poly R (order R^degree f)"
unfolding K_def φ_def using f_carr gauss_poly_carr
by (subst (asm) rupture_eq_0_iff, simp_all)
moreover assume "degree f dvd n"
hence "gauss_poly R (order R^degree f) pdivides
(gauss_poly R (order R^n))"
using gauss_poly_div_gauss_poly_iff
[OF assms(1) f_deg finite_field_min_order]
by simp
ultimately show "f pdivides⇘R⇙ gauss_poly R (order R^n)"
using f_carr a p.divides_trans unfolding pdivides_def by blast
qed
qed
lemma gauss_poly_splitted:
"splitted (gauss_poly R (order R))"
proof -
have "degree q ≤ 1" if
"q ∈ carrier P"
"pirreducible (carrier R) q"
"q pdivides gauss_poly R (order R)" for q
proof -
have q_carr: "q ∈ carrier (mult_of P)"
using that unfolding ring_irreducible_def by simp
moreover have "irreducible (mult_of P) q"
using that unfolding ring_irreducible_def
by (intro p.irreducible_imp_irreducible_mult that, simp_all)
ultimately obtain p where p_def:
"monic_irreducible_poly R p" "q ∼⇘mult_of P⇙ p"
using monic_poly_span by auto
have p_carr: "p ∈ carrier P" "p ≠ []"
using p_def(1)
unfolding monic_irreducible_poly_def monic_poly_def
by auto
moreover have "p divides⇘mult_of P⇙ q"
using associatedE[OF p_def(2)] by auto
hence "p pdivides q"
unfolding pdivides_def using divides_mult_imp_divides by simp
moreover have "q pdivides gauss_poly R (order R^1)"
using that by simp
ultimately have "p pdivides gauss_poly R (order R^1)"
unfolding pdivides_def using p.divides_trans by blast
hence "degree p dvd 1"
using div_gauss_poly_iff[where n="1"] p_def(1) by simp
hence "degree p = 1" by simp
moreover have "q divides⇘mult_of P⇙ p"
using associatedE[OF p_def(2)] by auto
hence "q pdivides p"
unfolding pdivides_def using divides_mult_imp_divides by simp
hence "degree q ≤ degree p"
using that p_carr
by (intro pdivides_imp_degree_le) auto
ultimately show ?thesis by simp
qed
thus ?thesis
using gauss_poly_carr
by (intro trivial_factors_imp_splitted, auto)
qed
text ‹The following lemma, for the case when @{term "R"} is a simple prime field, can be found in
Ireland and Rosen~\<^cite>‹‹\textsection 7.1, Theorem 2› in "ireland1982"›. Here the result is verified even
for arbitrary finite fields.›
lemma multiplicity_of_factor_of_gauss_poly:
assumes "n > 0"
assumes "monic_irreducible_poly R f"
shows
"pmult⇘R⇙ f (gauss_poly R (order R^n)) = of_bool (degree f dvd n)"
proof (cases "degree f dvd n")
case True
let ?g = "gauss_poly R (order R^n)"
have f_carr: "f ∈ carrier P" "f ≠ []"
using assms(2)
unfolding monic_irreducible_poly_def monic_poly_def
by auto
have o2: "order R^n > 1"
using finite_field_min_order assms(1) one_less_power by blast
hence o21: "order R^n > 0" by linarith
obtain d :: nat where order_dim: "order R = char R ^ d" "d > 0"
using finite_field_order by blast
have "d * n > 0" using order_dim assms by simp
hence char_dvd_order: "int (char R) dvd int (order R ^ n)"
unfolding order_dim
using finite_carr_imp_char_ge_0[OF finite_carrier]
by (simp add:power_mult[symmetric])
interpret h: ring_hom_ring "R" "P" "poly_of_const"
using canonical_embedding_ring_hom by simp
have "f pdivides⇘R⇙ ?g"
using True div_gauss_poly_iff[OF assms] by simp
hence "pmult⇘R⇙ f ?g ≥ 1"
using multiplicity_ge_1_iff_pdivides[OF assms(2)]
using gauss_poly_carr gauss_poly_not_zero[OF o2]
by auto
moreover have "pmult⇘R⇙ f ?g < 2"
proof (rule ccontr)
assume "¬ pmult⇘R⇙ f ?g < 2"
hence "pmult⇘R⇙ f ?g ≥ 2" by simp
hence "(f [^]⇘P⇙ (2::nat)) pdivides⇘R⇙ ?g"
using gauss_poly_carr gauss_poly_not_zero[OF o2]
by (subst (asm) multiplicity_ge_iff[OF assms(2)]) simp_all
hence "(f [^]⇘P⇙ (2::nat)) divides⇘mult_of P⇙ ?g"
unfolding pdivides_def
using f_carr gauss_poly_not_zero o2 gauss_poly_carr
by (intro p.divides_imp_divides_mult) simp_all
then obtain h where h_def:
"h ∈ carrier (mult_of P)"
"?g = f [^]⇘P⇙ (2::nat) ⊗⇘P⇙ h"
using dividesD by auto
have "⊖⇘P⇙ 𝟭⇘P⇙ = int_embed P (order R ^ n)
⊗⇘P⇙ (X⇘R⇙ [^]⇘P⇙ (order R ^ n-1)) ⊖⇘P⇙ 𝟭⇘P⇙"
using var_closed
apply (subst int_embed_consistent_with_poly_of_const)
apply (subst iffD2[OF embed_char_eq_0_iff char_dvd_order])
by (simp add:a_minus_def)
also have "... = pderiv⇘R⇙ (X⇘R⇙ [^]⇘P⇙ order R ^ n) ⊖⇘P⇙ pderiv⇘R⇙ X⇘R⇙"
using pderiv_var
by (subst pderiv_var_pow[OF o21], simp)
also have "... = pderiv⇘R⇙ ?g"
unfolding gauss_poly_def a_minus_def using var_closed
by (subst pderiv_add, simp_all add:pderiv_inv)
also have "... = pderiv⇘R⇙ (f [^]⇘P⇙ (2::nat) ⊗⇘P⇙ h)"
using h_def(2) by simp
also have "... = pderiv⇘R⇙ (f [^]⇘P⇙ (2::nat)) ⊗⇘P⇙ h
⊕⇘P⇙ (f [^]⇘P⇙ (2::nat)) ⊗⇘P⇙ pderiv⇘R⇙ h"
using f_carr h_def
by (intro pderiv_mult, simp_all)
also have "... = int_embed P 2 ⊗⇘P⇙ f ⊗⇘P⇙ pderiv⇘R⇙ f ⊗⇘P⇙ h
⊕⇘P⇙ f ⊗⇘P⇙ f ⊗⇘P⇙ pderiv⇘R⇙ h"
using f_carr
by (subst pderiv_pow, simp_all add:numeral_eq_Suc)
also have "... = f ⊗⇘P⇙ (int_embed P 2 ⊗⇘P⇙ pderiv⇘R⇙ f ⊗⇘P⇙ h)
⊕⇘P⇙ f ⊗⇘P⇙ (f ⊗⇘P⇙ pderiv⇘R⇙ h)"
using f_carr pderiv_carr h_def p.int_embed_closed
apply (intro arg_cong2[where f="(⊕⇘P⇙)"])
by (subst p.m_comm, simp_all add:p.m_assoc)
also have "... = f ⊗⇘P⇙
(int_embed P 2 ⊗⇘P⇙ pderiv⇘R⇙ f ⊗⇘P⇙ h ⊕⇘P⇙ f ⊗⇘P⇙ pderiv⇘R⇙ h)"
using f_carr pderiv_carr h_def p.int_embed_closed
by (subst p.r_distr, simp_all)
finally have "⊖⇘P⇙ 𝟭⇘P⇙ = f ⊗⇘P⇙
(int_embed P 2 ⊗⇘P⇙ pderiv⇘R⇙ f ⊗⇘P⇙ h ⊕⇘P⇙ f ⊗⇘P⇙ pderiv⇘R⇙ h)"
(is "_ = f ⊗⇘P⇙ ?q")
by simp
hence "f pdivides⇘R⇙ ⊖⇘P⇙ 𝟭⇘P⇙"
unfolding factor_def pdivides_def
using f_carr pderiv_carr h_def p.int_embed_closed
by auto
moreover have "⊖⇘P⇙ 𝟭⇘P⇙ ≠ 𝟬⇘P⇙" by simp
ultimately have "degree f ≤ degree (⊖⇘P⇙ 𝟭⇘P⇙)"
using f_carr
by (intro pdivides_imp_degree_le, simp_all add:univ_poly_zero)
also have "... = 0"
by (subst univ_poly_a_inv_degree, simp)
(simp add:univ_poly_one)
finally have "degree f = 0" by simp
then show "False"
using pirreducible_degree assms(2)
unfolding monic_irreducible_poly_def monic_poly_def
by fastforce
qed
ultimately have "pmult⇘R⇙ f ?g = 1" by simp
then show ?thesis using True by simp
next
case False
have o2: "order R^n > 1"
using finite_field_min_order assms(1) one_less_power by blast
have "¬(f pdivides⇘R⇙ gauss_poly R (order R^n))"
using div_gauss_poly_iff[OF assms] False by simp
hence "pmult⇘R⇙ f (gauss_poly R (order R^n)) = 0"
using multiplicity_ge_1_iff_pdivides[OF assms(2)]
using gauss_poly_carr gauss_poly_not_zero[OF o2] leI less_one
by blast
then show ?thesis using False by simp
qed
text ‹The following lemma, for the case when @{term "R"} is a simple prime field, can be found in Ireland
and Rosen~\<^cite>‹‹\textsection 7.1, Corollary 1› in "ireland1982"›. Here the result is verified even for
arbitrary finite fields.›
lemma card_irred_aux:
assumes "n > 0"
shows "order R^n = (∑d | d dvd n. d *
card {f. monic_irreducible_poly R f ∧ degree f = d})"
(is "?lhs = ?rhs")
proof -
let ?G = "{f. monic_irreducible_poly R f ∧ degree f dvd n}"
let ?D = "{f. monic_irreducible_poly R f}"
have a: "finite {d. d dvd n}" using finite_divisors_nat assms by simp
have b: "finite {f. monic_irreducible_poly R f ∧ degree f = k}" for k
proof -
have "{f. monic_irreducible_poly R f ∧ degree f = k} ⊆
{f. f ∈ carrier P ∧ degree f ≤ k}"
unfolding monic_irreducible_poly_def monic_poly_def by auto
moreover have "finite {f. f ∈ carrier P ∧ degree f ≤ k}"
using finite_poly[OF finite_carrier] by simp
ultimately show ?thesis using finite_subset by simp
qed
have G_split: "?G =
⋃ {{f. monic_irreducible_poly R f ∧ degree f = d} | d. d dvd n}"
by auto
have c: "finite ?G"
using a b by (subst G_split, auto)
have d: "order R^n > 1"
using assms finite_field_min_order one_less_power by blast
have "?lhs = degree (gauss_poly R (order R^n))"
using d
by (subst gauss_poly_degree, simp_all)
also have "... =
sum' (λd. pmult⇘R⇙ d (gauss_poly R (order R^n)) * degree d) ?D"
using d
by (intro degree_monic_poly'[symmetric] gauss_poly_monic)
also have "... = sum' (λd. of_bool (degree d dvd n) * degree d) ?D"
using multiplicity_of_factor_of_gauss_poly[OF assms]
by (intro sum.cong', auto)
also have "... = sum' (λd. degree d) ?G"
by (intro sum.mono_neutral_cong_right' subsetI, auto)
also have "... = (∑ d ∈ ?G. degree d)"
using c by (intro sum.eq_sum, simp)
also have "... =
(∑ f ∈ (⋃ d ∈ {d. d dvd n}.
{f. monic_irreducible_poly R f ∧ degree f = d}). degree f)"
by (intro sum.cong, auto simp add:set_eq_iff)
also have "... = (∑d | d dvd n. sum degree
{f. monic_irreducible_poly R f ∧ degree f = d})"
using a b by (subst sum.UNION_disjoint, auto simp add:set_eq_iff)
also have "... = (∑d | d dvd n. sum (λ_. d)
{f. monic_irreducible_poly R f ∧ degree f = d})"
by (intro sum.cong, simp_all)
also have "... = ?rhs"
by (simp add:mult.commute)
finally show ?thesis
by simp
qed
end
end