diff --git a/thys/Finite_Fields/Card_Irreducible_Polynomials.thy b/thys/Finite_Fields/Card_Irreducible_Polynomials.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Card_Irreducible_Polynomials.thy @@ -0,0 +1,231 @@ +subsection \Gauss Formula\label{sec:card_irred}\ + +theory Card_Irreducible_Polynomials + imports + Dirichlet_Series.Moebius_Mu + Card_Irreducible_Polynomials_Aux +begin + +hide_const "Polynomial.order" + +text \The following theorem is a slightly generalized form of the formula discovered by +Gauss for the number of monic irreducible polynomials over a finite field. He originally verified +the result for the case when @{term "R"} is a simple prime field. +The version of the formula here for the case where @{term "R"} may be an arbitrary finite field can +be found in Chebolu and Min{\'a}{\v{c}}~\cite{chebolu2010}.\ + +theorem (in finite_field) card_irred: + assumes "n > 0" + shows "n * card {f. monic_irreducible_poly R f \ degree f = n} = + (\d | d dvd n. moebius_mu d * (order R^(n div d)))" + (is "?lhs = ?rhs") +proof - + have "?lhs = dirichlet_prod moebius_mu (\x. int (order R) ^ x) n" + using card_irred_aux + by (intro moebius_inversion assms) (simp flip:of_nat_power) + also have "... = ?rhs" + by (simp add:dirichlet_prod_def) + finally show ?thesis by simp +qed + +text \In the following an explicit analytic lower bound for the cardinality of monic irreducible +polynomials is shown, with which existence follows. This part deviates from the classic approach, +where existence is verified using a divisibility argument. The reason for the deviation is that an +analytic bound can also be used to estimate the runtime of a randomized algorithm selecting an +irreducible polynomial, by randomly sampling monic polynomials.\ + +lemma (in finite_field) card_irred_1: + "card {f. monic_irreducible_poly R f \ degree f = 1} = order R" +proof - + have "int (1 * card {f. monic_irreducible_poly R f \ degree f = 1}) + = int (order R)" + by (subst card_irred, auto) + thus ?thesis by simp +qed + +lemma (in finite_field) card_irred_2: + "real (card {f. monic_irreducible_poly R f \ degree f = 2}) = + (real (order R)^2 - order R) / 2" +proof - + have "x dvd 2 \ x = 1 \ x = 2" for x :: nat + using nat_dvd_not_less[where m="2"] + by (metis One_nat_def even_zero gcd_nat.strict_trans2 + less_2_cases nat_neq_iff pos2) + hence a: "{d. d dvd 2} = {1,2::nat}" + by (auto simp add:set_eq_iff) + + have "2*real (card {f. monic_irreducible_poly R f \ degree f = 2}) + = of_int (2* card {f. monic_irreducible_poly R f \ degree f = 2})" + by simp + also have "... = + of_int (\d | d dvd 2. moebius_mu d * int (order R) ^ (2 div d))" + by (subst card_irred, auto) + also have "... = order R^2 - int (order R)" + by (subst a, simp) + also have "... = real (order R)^2 - order R" + by simp + finally have + "2 * real (card {f. monic_irreducible_poly R f \ degree f = 2}) = + real (order R)^2 - order R" + by simp + thus ?thesis by simp +qed + +lemma (in finite_field) card_irred_gt_2: + assumes "n > 2" + shows "real (order R)^n / (2*real n) \ + card {f. monic_irreducible_poly R f \ degree f = n}" + (is "?lhs \ ?rhs") +proof - + let ?m = "real (order R)" + have a:"?m \ 2" + using finite_field_min_order by simp + + have b:"moebius_mu n \ -(1::real)" for n :: nat + using abs_moebius_mu_le[where n="n"] + unfolding abs_le_iff by auto + + have c: "n > 0" using assms by simp + have d: "x < n - 1" if d_assms: "x dvd n" "x \ n" for x :: nat + proof - + have "x < n" + using d_assms dvd_nat_bounds c by auto + moreover have "\(n-1 dvd n)" using assms + by (metis One_nat_def Suc_diff_Suc c diff_zero + dvd_add_triv_right_iff nat_dvd_1_iff_1 + nat_neq_iff numeral_2_eq_2 plus_1_eq_Suc) + hence "x \ n-1" using d_assms by auto + ultimately show "x < n-1" by simp + qed + + have "?m^n / 2 = ?m^n - ?m^n/2" by simp + also have "... \ ?m^n - ?m^n/?m^1" + using a by (intro diff_mono divide_left_mono, simp_all) + also have "... \ ?m^n - ?m^(n-1)" + using a c by (subst power_diff, simp_all) + also have "... \ ?m^n - (?m^(n-1) - 1)/1" by simp + also have "... \ ?m^n - (?m^(n-1)-1)/(?m-1)" + using a by (intro diff_left_mono divide_left_mono, simp_all) + also have "... = ?m^n - (\i \ {.. ?m^n - (\i \ {k. k dvd n \ k \ n}. ?m^i)" + using d + by (intro diff_mono sum_mono2 subsetI, auto simp add:not_less) + also have "... = ?m^n + (\i \ {k. k dvd n \ k \ n}. (-1) * ?m^i)" + by (subst sum_distrib_left[symmetric], simp) + also have "... \ moebius_mu 1 * ?m^n + + (\i \ {k. k dvd n \ k \ n}. moebius_mu (n div i) * ?m^i)" + using b + by (intro add_mono sum_mono mult_right_mono) + (simp_all add:not_less) + also have "... = (\i \ insert n {k. k dvd n \ k \ n}. + moebius_mu (n div i) * ?m^i)" + using c by (subst sum.insert, auto) + also have "... = (\i \ {k. k dvd n}. moebius_mu (n div i) * ?m^i)" + by (intro sum.cong, auto simp add:set_eq_iff) + also have "... = dirichlet_prod (\i. ?m^i) moebius_mu n" + unfolding dirichlet_prod_def by (intro sum.cong, auto) + also have "... = dirichlet_prod moebius_mu (\i. ?m^i) n" + using dirichlet_prod_moebius_commute by metis + also have "... = + of_int (\d | d dvd n. moebius_mu d * order R^(n div d))" + unfolding dirichlet_prod_def by simp + also have "... = of_int (n * + card {f. monic_irreducible_poly R f \ length f - 1 = n})" + using card_irred[OF c] by simp + also have "... = n * ?rhs" by simp + finally have "?m^n / 2 \ n * ?rhs" by simp + hence "?m ^ n \ 2 * n * ?rhs" by simp + hence "?m^n/(2*real n) \ ?rhs" + using c by (subst pos_divide_le_eq, simp_all add:algebra_simps) + thus ?thesis by simp +qed + +lemma (in finite_field) exist_irred: + assumes "n > 0" + obtains f where "monic_irreducible_poly R f" "degree f = n" +proof - + consider (i) "n = 1" | (ii) "n = 2" | (iii) "n>2" + using assms by linarith + then have + "card {f. monic_irreducible_poly R f \ degree f = n} > 0" + (is "card ?A > 0") + proof (cases) + case i + hence "card ?A = order R" + using card_irred_1 by simp + also have "... > 0" + using finite_field_min_order by simp + finally show ?thesis by simp + next + case ii + have "0 < (real (order R) * (real (order R) - 1)) / 2" + using finite_field_min_order by simp + also have "... = (real (order R)^2 - order R) / 2" + by (simp add:power2_eq_square algebra_simps) + also have "... = real (card ?A)" + using ii by (subst card_irred_2[symmetric], simp) + finally have " 0 < real (card ?A)" by simp + then show ?thesis by simp + next + case iii + have "0 < real (order R)^n / (2*real n)" + using finite_field_min_order assms by simp + also have "... \ real (card ?A)" + using iii card_irred_gt_2 by simp + finally have "0 < real (card ?A)" by simp + then show ?thesis by simp + qed + hence "?A \ {}" + by (metis card.empty nless_le) + then obtain f where "monic_irreducible_poly R f" "degree f = n" + by auto + thus ?thesis using that by simp +qed + +theorem existence: + assumes "n > 0" + assumes "Factorial_Ring.prime p" + shows "\(F:: int set list set ring). finite_field F \ order F = p^n" +proof - + interpret zf: finite_field "ZFact (int p)" + using zfact_prime_is_finite_field assms by simp + + interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)" + unfolding polynomial_ring_def polynomial_ring_axioms_def + using zf.field_axioms zf.carrier_is_subfield by simp + + have p_gt_0: "p > 0" using prime_gt_0_nat assms(2) by simp + + obtain f where f_def: + "monic_irreducible_poly (ZFact (int p)) f" + "degree f = n" + using zf.exist_irred assms by auto + + let ?F = "Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" + have "f \ carrier (poly_ring (ZFact (int p)))" + using f_def(1) zf.monic_poly_carr + unfolding monic_irreducible_poly_def + by simp + moreover have "degree f > 0" + using assms(1) f_def by simp + ultimately have "order ?F = card (carrier (ZFact p))^degree f" + by (intro zf.rupture_order[OF zf.carrier_is_subfield]) auto + hence a:"order ?F = p^n" + unfolding f_def(2) card_zfact_carr[OF p_gt_0] by simp + + have "field ?F" + using f_def(1) zf.monic_poly_carr monic_irreducible_poly_def + by (subst zfp.rupture_is_field_iff_pirreducible) auto + moreover have "order ?F > 0" + unfolding a using assms(1,2) p_gt_0 by simp + ultimately have b:"finite_field ?F" + using card_ge_0_finite + by (intro finite_fieldI, auto simp add:Coset.order_def) + + show ?thesis + using a b + by (intro exI[where x="?F"], simp) +qed + +end diff --git a/thys/Finite_Fields/Card_Irreducible_Polynomials_Aux.thy b/thys/Finite_Fields/Card_Irreducible_Polynomials_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Card_Irreducible_Polynomials_Aux.thy @@ -0,0 +1,916 @@ +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\<^bsub>K[X]\<^esub> 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.is_ring 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\<^bsub>K\<^esub> [^]\<^bsub>poly_ring K\<^esub> (n::nat) \\<^bsub>poly_ring K\<^esub> X\<^bsub>K\<^esub>" + +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]{ireland1982}.\ + +lemma gauss_poly_div_gauss_poly_iff_1: + fixes l m :: nat + assumes "l > 0" + shows "(X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides (X [^]\<^bsub>P\<^esub> m \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \ 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:"(\\<^bsub>P\<^esub>i\{..P\<^esub> l)[^]\<^bsub>P\<^esub> i) \ carrier P" + using var_pow_closed + by (intro p.finsum_closed, simp) + + have "(X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = ((X [^]\<^bsub>P\<^esub> l)[^]\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + using var_closed + by (subst p.nat_pow_pow, simp_all add:algebra_simps) + also have "... = + (X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> (\\<^bsub>P\<^esub>i\{..P\<^esub> l) [^]\<^bsub>P\<^esub> i)" + using var_pow_closed + by (subst p.geom[symmetric], simp_all) + finally have pow_sum_fact: "(X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = + (X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> (\\<^bsub>P\<^esub>i\{..R\<^esub> [^]\<^bsub>P\<^esub> l) [^]\<^bsub>P\<^esub> i)" + by simp + + have "(X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) divides\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + by (rule dividesI[OF pow_sum_carr pow_sum_fact]) + + hence c:"(X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) divides\<^bsub>P\<^esub> X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q * l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + using var_pow_closed + by (intro p.divides_prod_l, auto) + + have "(X [^]\<^bsub>P\<^esub> m \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = X [^]\<^bsub>P\<^esub> (r + q * l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + unfolding m_def using add.commute by metis + also have "... = (X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l)) \\<^bsub>P\<^esub> (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + using var_closed + by (subst p.nat_pow_mult, auto simp add:a_minus_def) + also have "... = ((X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)) + \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> r)) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + using var_pow_closed + by algebra + also have "... = (X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) + \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + by algebra + also have "... = (X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) + \\<^bsub>P\<^esub> ((X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + unfolding a_minus_def using var_pow_closed + by (subst p.a_assoc, auto) + finally have a:"(X [^]\<^bsub>P\<^esub> m \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = + (X [^]\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> (q*l) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> (X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + (is "_ = ?x") + by simp + + have xn_m_1_deg': "degree (X [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = n" + if "n > 0" for n :: nat + proof - + have "degree (X [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = degree (X [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + by (simp add:a_minus_def) + also have "... = max (degree (X [^]\<^bsub>P\<^esub> n)) (degree (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub>))" + 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 [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = 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 [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) = degree (\\<^bsub>P\<^esub>)" + by (intro arg_cong[where f="degree"], simp) + then show ?thesis using False by (simp add:univ_poly_zero) + qed + + have b: "degree (X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) > degree (X\<^bsub>R\<^esub> [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + using r_range unfolding xn_m_1_deg by simp + + have xn_m_1_carr: "X [^]\<^bsub>P\<^esub> n \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> \ carrier P" for n :: nat + unfolding a_minus_def + by (intro p.a_closed var_pow_closed, simp) + + have "?lhs \ (X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides ?x" + by (subst a, simp) + also have "... \ (X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides (X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + 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 [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides \\<^bsub>P\<^esub>" + unfolding univ_poly_zero + by (intro pdivides_zero xn_m_1_carr) + also have "... = (X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + by (simp add:a_minus_def True) algebra + finally show ?thesis using True by simp + next + case False + hence "degree (X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) > 0" using xn_m_1_deg by simp + hence "X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> \ []" by auto + hence "\(X [^]\<^bsub>P\<^esub> l \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides (X [^]\<^bsub>P\<^esub> r \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + 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 [^]\<^bsub>P\<^esub> (n-1) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> X" (is "_ = ?rhs") +proof - + have a:"1 + (n - 1) = n" + using assms by simp + have "gauss_poly R n = X [^]\<^bsub>P\<^esub> (1+(n-1)) \\<^bsub>P\<^esub> X" + unfolding gauss_poly_def by (subst a, simp) + also have "... = (X [^]\<^bsub>P\<^esub> (n-1)) \\<^bsub>P\<^esub> X \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> 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 \ \\<^bsub>P\<^esub>" + by (simp add:var_def univ_poly_zero) + +lemma var_pow_eq_one_iff: "X [^]\<^bsub>P\<^esub> k = \\<^bsub>P\<^esub> \ k = (0::nat)" +proof (cases "k=0") + case True + then show ?thesis using var_closed(1) by simp +next + case False + have "degree (X\<^bsub>R\<^esub> [^]\<^bsub>P\<^esub> k) = k " + using var_pow_degree by simp + also have "... \ degree (\\<^bsub>P\<^esub>)" using False degree_one by simp + finally have "degree (X\<^bsub>R\<^esub> [^]\<^bsub>P\<^esub> k) \ degree \\<^bsub>P\<^esub>" 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 \ \\<^bsub>P\<^esub>" +proof - + have "degree (gauss_poly R n) \ degree ( \\<^bsub>P\<^esub>)" + 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 [^]\<^bsub>P\<^esub> n)" + by (intro monic_poly_pow monic_poly_var) + moreover have "\\<^bsub>P\<^esub> X \ carrier P" + using var_closed by simp + moreover have "degree (\\<^bsub>P\<^esub> X) < degree (X [^]\<^bsub>P\<^esub> 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 \ {..The following lemma can be found in Ireland and Rosen~\cite[\textsection 7.1, Lemma 3]{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 \ {..i \ {.. (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\<^bsub>R\<^esub> 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 [^]\<^bsub>P\<^esub> (a^n-1) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> X pdivides + (X [^]\<^bsub>P\<^esub> (a^m-1) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) \\<^bsub>P\<^esub> X" + using gauss_poly_factor a1 b1 by simp + also have "... \ + (X [^]\<^bsub>P\<^esub> (a^n-1) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) pdivides + (X [^]\<^bsub>P\<^esub> (a^m-1) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + 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\<^bsub>R\<^esub> 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\<^bsub>R\<^esub> (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 [^]\<^bsub>K\<^esub> 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 [^]\<^bsub>K\<^esub> (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) [^]\<^bsub>K\<^esub> (order R^n) = \(poly_of_const x)" + if k_cycle_1: "x \ carrier R" for x + proof - + have "\ (poly_of_const x) [^]\<^bsub>K\<^esub> (order R^n) = + \ (poly_of_const (x [^]\<^bsub>R\<^esub> (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\<^bsub>K\<^esub> 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 = [\\<^bsub>K\<^esub>, \\<^bsub>K\<^esub> 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 = \\<^bsub>K\<^esub>" + 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 "[\\<^bsub>K\<^esub>, \\<^bsub>K\<^esub> x] pdivides\<^bsub>K\<^esub> ?g1" + using f.is_root_imp_pdivides f.gauss_poly_carr by simp + hence "d pdivides\<^bsub>K\<^esub> ?g1" by (simp add:x_def) + thus "pmult\<^bsub>K\<^esub> 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\<^bsub>R\<^esub> gauss_poly R (order R^n)" + have "(\ X) [^]\<^bsub>K\<^esub> (order R^n) \\<^bsub>K\<^esub> (\ X\<^bsub>R\<^esub>) = + \ (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 "... = \\<^bsub>K\<^esub>" + unfolding K_def \_def using f_carr gauss_poly_carr f + by (subst rupture_eq_0_iff, simp_all) + finally have "(\ X\<^bsub>R\<^esub>) [^]\<^bsub>K\<^esub> (order R^n) \\<^bsub>K\<^esub> (\ X\<^bsub>R\<^esub>) = \\<^bsub>K\<^esub>" + by simp + hence g:"(\ X) [^]\<^bsub>K\<^esub> (order R^n) = (\ X)" + using var_closed by simp + + have roots_g2: "pmult\<^bsub>K\<^esub> 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 = [\\<^bsub>K\<^esub>, \\<^bsub>K\<^esub> 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) [^]\<^bsub>K\<^esub> (order R^n) = + f.eval (map (\ \ poly_of_const) x) (\ X) [^]\<^bsub>K\<^esub> (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) [^]\<^bsub>K\<^esub> 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 [^]\<^bsub>K\<^esub> order R ^ n = \ x" by simp + + hence "y [^]\<^bsub>K\<^esub> (order R^n) = y" using x_def by simp + hence "ring.eval K ?g2 y = \\<^bsub>K\<^esub>" + 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\<^bsub>K\<^esub> ?g2" + unfolding y_def + by (intro f.is_root_imp_pdivides f.gauss_poly_carr, simp) + thus "pmult\<^bsub>K\<^esub> 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. \\<^bsub>K\<^esub> x) (carrier K)" + by (intro inj_onI, metis f.minus_minus) + let ?mip = "monic_irreducible_poly K" + + have "sum' (\d. pmult\<^bsub>K\<^esub> 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. [\\<^bsub>K\<^esub>, \\<^bsub>K\<^esub> 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\<^bsub>K\<^esub> d ?g1 * degree d) {d. ?mip d} + \ sum' (\d. of_bool (degree d = 1)) {d. ?mip d}" + by simp + moreover have + "pmult\<^bsub>K\<^esub> 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 = [\\<^bsub>K\<^esub>, \\<^bsub>K\<^esub> x]" + using f.degree_one_monic_poly v by auto + hence "pmult\<^bsub>K\<^esub> 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\<^bsub>K\<^esub> 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\<^bsub>K\<^esub> d ?g1 * degree d = + of_bool (degree d = 1)" + by (intro sum'_eq_iff, simp_all add:not_le) + have "pmult\<^bsub>K\<^esub> d ?g1 \ pmult\<^bsub>K\<^esub> d ?g2" if "?mip d" for d + proof (cases "degree d = 1") + case True + hence "pmult\<^bsub>K\<^esub> d ?g1 = 1" using v2 that by simp + also have "... \ pmult\<^bsub>K\<^esub> 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\<^bsub>K\<^esub> d ?g1 = 0" using v2 that by auto + then show ?thesis by simp + qed + hence "?g1 pdivides\<^bsub>K\<^esub> ?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\<^bsub>R\<^esub> \ carrier K" + by (intro h.hom_closed var_closed) + + have "\ (gauss_poly R (order R^degree f)) = + (\ X\<^bsub>R\<^esub>) [^]\<^bsub>K\<^esub> (order R^degree f) \\<^bsub>K\<^esub> (\ X\<^bsub>R\<^esub>)" + unfolding gauss_poly_def a_minus_def using var_closed + by (simp add: h.hom_nat_pow) + also have "... = \\<^bsub>K\<^esub>" + using c d by simp + finally have "\ (gauss_poly R (order R^degree f)) = \\<^bsub>K\<^esub>" by simp + hence "f pdivides\<^bsub>R\<^esub> 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\<^bsub>R\<^esub> 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 \\<^bsub>mult_of P\<^esub> 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\<^bsub>mult_of P\<^esub> 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\<^bsub>mult_of P\<^esub> 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]{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\<^bsub>R\<^esub> 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\<^bsub>R\<^esub> ?g" + using True div_gauss_poly_iff[OF assms] by simp + hence "pmult\<^bsub>R\<^esub> 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\<^bsub>R\<^esub> f ?g < 2" + proof (rule ccontr) + assume "\ pmult\<^bsub>R\<^esub> f ?g < 2" + hence "pmult\<^bsub>R\<^esub> f ?g \ 2" by simp + hence "(f [^]\<^bsub>P\<^esub> (2::nat)) pdivides\<^bsub>R\<^esub> ?g" + using gauss_poly_carr gauss_poly_not_zero[OF o2] + by (subst (asm) multiplicity_ge_iff[OF assms(2)]) simp_all + hence "(f [^]\<^bsub>P\<^esub> (2::nat)) divides\<^bsub>mult_of P\<^esub> ?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 [^]\<^bsub>P\<^esub> (2::nat) \\<^bsub>P\<^esub> h" + using dividesD by auto + have "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> = int_embed P (order R ^ n) + \\<^bsub>P\<^esub> (X\<^bsub>R\<^esub> [^]\<^bsub>P\<^esub> (order R ^ n-1)) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + 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\<^bsub>R\<^esub> (X\<^bsub>R\<^esub> [^]\<^bsub>P\<^esub> order R ^ n) \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> X\<^bsub>R\<^esub>" + using pderiv_var + by (subst pderiv_var_pow[OF o21], simp) + also have "... = pderiv\<^bsub>R\<^esub> ?g" + unfolding gauss_poly_def a_minus_def using var_closed + by (subst pderiv_add, simp_all add:pderiv_inv) + also have "... = pderiv\<^bsub>R\<^esub> (f [^]\<^bsub>P\<^esub> (2::nat) \\<^bsub>P\<^esub> h)" + using h_def(2) by simp + also have "... = pderiv\<^bsub>R\<^esub> (f [^]\<^bsub>P\<^esub> (2::nat)) \\<^bsub>P\<^esub> h + \\<^bsub>P\<^esub> (f [^]\<^bsub>P\<^esub> (2::nat)) \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> h" + using f_carr h_def + by (intro pderiv_mult, simp_all) + also have "... = int_embed P 2 \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> f \\<^bsub>P\<^esub> h + \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> h" + using f_carr + by (subst pderiv_pow, simp_all add:numeral_eq_Suc) + also have "... = f \\<^bsub>P\<^esub> (int_embed P 2 \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> f \\<^bsub>P\<^esub> h) + \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> (f \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> h)" + using f_carr pderiv_carr h_def p.int_embed_closed + apply (intro arg_cong2[where f="(\\<^bsub>P\<^esub>)"]) + by (subst p.m_comm, simp_all add:p.m_assoc) + also have "... = f \\<^bsub>P\<^esub> + (int_embed P 2 \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> f \\<^bsub>P\<^esub> h \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> h)" + using f_carr pderiv_carr h_def p.int_embed_closed + by (subst p.r_distr, simp_all) + finally have "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> = f \\<^bsub>P\<^esub> + (int_embed P 2 \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> f \\<^bsub>P\<^esub> h \\<^bsub>P\<^esub> f \\<^bsub>P\<^esub> pderiv\<^bsub>R\<^esub> h)" + (is "_ = f \\<^bsub>P\<^esub> ?q") + by simp + + hence "f pdivides\<^bsub>R\<^esub> \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>" + unfolding factor_def pdivides_def + using f_carr pderiv_carr h_def p.int_embed_closed + by auto + moreover have "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> \ \\<^bsub>P\<^esub>" by simp + ultimately have "degree f \ degree (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub>)" + 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\<^bsub>R\<^esub> 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\<^bsub>R\<^esub> gauss_poly R (order R^n))" + using div_gauss_poly_iff[OF assms] False by simp + hence "pmult\<^bsub>R\<^esub> 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]{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\<^bsub>R\<^esub> 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 diff --git a/thys/Finite_Fields/Finite_Fields_Factorization_Ext.thy b/thys/Finite_Fields/Finite_Fields_Factorization_Ext.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Finite_Fields_Factorization_Ext.thy @@ -0,0 +1,516 @@ +subsection "Factorization" + +theory Finite_Fields_Factorization_Ext + imports Finite_Fields_Preliminary_Results +begin + +text \This section contains additional results building on top of the development in +@{theory "HOL-Algebra.Divisibility"} about factorization in a @{locale "factorial_monoid"}.\ + +definition factor_mset where "factor_mset G x = + (THE f. (\ as. f = fmset G as \ wfactors G as x \ set as \ carrier G))" + +text \In @{theory "HOL-Algebra.Divisibility"} it is already verified that the multiset representing +the factorization of an element of a factorial monoid into irreducible factors is well-defined. +With these results it is then possible to define @{term "factor_mset"} and show its properties, +without referring to a factorization in list form first.\ + +definition multiplicity where + "multiplicity G d g = Max {(n::nat). (d [^]\<^bsub>G\<^esub> n) divides\<^bsub>G\<^esub> g}" + +definition canonical_irreducibles where + "canonical_irreducibles G A = ( + A \ {a. a \ carrier G \ irreducible G a} \ + (\x y. x \ A \ y \ A \ x \\<^bsub>G\<^esub> y \ x = y) \ + (\x \ carrier G. irreducible G x \ (\y \ A. x \\<^bsub>G\<^esub> y)))" + +text \A set of irreducible elements that contains exactly one element from each equivalence class +of an irreducible element formed by association, is called a set of +@{term "canonical_irreducibles"}. An example is the set of monic irreducible polynomials as +representatives of all irreducible polynomials.\ + +context factorial_monoid +begin + +lemma assoc_as_fmset_eq: + assumes "wfactors G as a" + and "wfactors G bs b" + and "a \ carrier G" + and "b \ carrier G" + and "set as \ carrier G" + and "set bs \ carrier G" + shows "a \ b \ (fmset G as = fmset G bs)" +proof - + have "a \ b \ (a divides b \ b divides a)" + by (simp add:associated_def) + also have "... \ + (fmset G as \# fmset G bs \ fmset G bs \# fmset G as)" + using divides_as_fmsubset assms by blast + also have "... \ (fmset G as = fmset G bs)" by auto + finally show ?thesis by simp +qed + +lemma factor_mset_aux_1: + assumes "a \ carrier G" "set as \ carrier G" "wfactors G as a" + shows "factor_mset G a = fmset G as" +proof - + define H where "H = {as. wfactors G as a \ set as \ carrier G}" + have b:"as \ H" + using H_def assms by simp + + have c: "x \ H \ y \ H \ fmset G x = fmset G y" for x y + unfolding H_def using assoc_as_fmset_eq + using associated_refl assms by blast + + have "factor_mset G a = (THE f. \as \ H. f= fmset G as)" + by (simp add:factor_mset_def H_def, metis) + + also have "... = fmset G as" + using b c + by (intro the1_equality) blast+ + finally have "factor_mset G a = fmset G as" by simp + + thus ?thesis + using b unfolding H_def by auto +qed + +lemma factor_mset_aux: + assumes "a \ carrier G" + shows "\as. factor_mset G a = fmset G as \ wfactors G as a \ + set as \ carrier G" +proof - + obtain as where as_def: "wfactors G as a" "set as \ carrier G" + using wfactors_exist assms by blast + thus ?thesis using factor_mset_aux_1 assms by blast +qed + +lemma factor_mset_set: + assumes "a \ carrier G" + assumes "x \# factor_mset G a" + obtains y where + "y \ carrier G" + "irreducible G y" + "assocs G y = x" +proof - + obtain as where as_def: + "factor_mset G a = fmset G as" + "wfactors G as a" "set as \ carrier G" + using factor_mset_aux assms by blast + hence "x \# fmset G as" + using assms by simp + hence "x \ assocs G ` set as" + using assms as_def by (simp add:fmset_def) + hence "\y. y \ set as \ x = assocs G y" + by auto + moreover have "y \ carrier G \ irreducible G y" + if "y \ set as" for y + using as_def that wfactors_def + by (simp add: wfactors_def) auto + ultimately show ?thesis + using that by blast +qed + +lemma factor_mset_mult: + assumes "a \ carrier G" "b \ carrier G" + shows "factor_mset G (a \ b) = factor_mset G a + factor_mset G b" +proof - + obtain as where as_def: + "factor_mset G a = fmset G as" + "wfactors G as a" "set as \ carrier G" + using factor_mset_aux assms by blast + obtain bs where bs_def: + "factor_mset G b = fmset G bs" + "wfactors G bs b" "set bs \ carrier G" + using factor_mset_aux assms(2) by blast + have "a \ b \ carrier G" using assms by auto + then obtain cs where cs_def: + "factor_mset G (a \ b) = fmset G cs" + "wfactors G cs (a \ b)" + "set cs \ carrier G" + using factor_mset_aux assms by blast + have "fmset G cs = fmset G as + fmset G bs" + using as_def bs_def cs_def assms + by (intro mult_wfactors_fmset[where a="a" and b="b"]) auto + thus ?thesis + using as_def bs_def cs_def by auto +qed + +lemma factor_mset_unit: "factor_mset G \ = {#}" +proof - + have "factor_mset G \ = factor_mset G (\ \ \)" + by simp + also have "... = factor_mset G \ + factor_mset G \" + by (intro factor_mset_mult, auto) + finally show "factor_mset G \ = {#}" + by simp +qed + +lemma factor_mset_irred: + assumes "x \ carrier G" "irreducible G x" + shows "factor_mset G x = image_mset (assocs G) {#x#}" +proof - + have "wfactors G [x] x" + using assms by (simp add:wfactors_def) + hence "factor_mset G x = fmset G [x]" + using factor_mset_aux_1 assms by simp + also have "... = image_mset (assocs G) {#x#}" + by (simp add:fmset_def) + finally show ?thesis by simp +qed + +lemma factor_mset_divides: + assumes "a \ carrier G" "b \ carrier G" + shows "a divides b \ factor_mset G a \# factor_mset G b" +proof - + obtain as where as_def: + "factor_mset G a = fmset G as" + "wfactors G as a" "set as \ carrier G" + using factor_mset_aux assms by blast + obtain bs where bs_def: + "factor_mset G b = fmset G bs" + "wfactors G bs b" "set bs \ carrier G" + using factor_mset_aux assms(2) by blast + hence "a divides b \ fmset G as \# fmset G bs" + using as_def bs_def assms + by (intro divides_as_fmsubset) auto + also have "... \ factor_mset G a \# factor_mset G b" + using as_def bs_def by simp + finally show ?thesis by simp +qed + +lemma factor_mset_sim: + assumes "a \ carrier G" "b \ carrier G" + shows "a \ b \ factor_mset G a = factor_mset G b" + using factor_mset_divides assms + by (simp add:associated_def) auto + +lemma factor_mset_prod: + assumes "finite A" + assumes "f ` A \ carrier G" + shows "factor_mset G (\a \ A. f a) = + (\a \ A. factor_mset G (f a))" + using assms +proof (induction A rule:finite_induct) + case empty + then show ?case by (simp add:factor_mset_unit) +next + case (insert x F) + have "factor_mset G (finprod G f (insert x F)) = + factor_mset G (f x \ finprod G f F)" + using insert by (subst finprod_insert) auto + also have "... = factor_mset G (f x) + factor_mset G (finprod G f F)" + using insert by (intro factor_mset_mult finprod_closed) auto + also have + "... = factor_mset G (f x) + (\a \ F. factor_mset G (f a))" + using insert by simp + also have "... = (\a\insert x F. factor_mset G (f a))" + using insert by simp + finally show ?case by simp +qed + +lemma factor_mset_pow: + assumes "a \ carrier G" + shows "factor_mset G (a [^] n) = repeat_mset n (factor_mset G a)" +proof (induction n) + case 0 + then show ?case by (simp add:factor_mset_unit) +next + case (Suc n) + have "factor_mset G (a [^] Suc n) = factor_mset G (a [^] n \ a)" + by simp + also have "... = factor_mset G (a [^] n) + factor_mset G a" + using assms by (intro factor_mset_mult) auto + also have "... = repeat_mset n (factor_mset G a) + factor_mset G a" + using Suc by simp + also have "... = repeat_mset (Suc n) (factor_mset G a)" + by simp + finally show ?case by simp +qed + +lemma image_mset_sum: + assumes "finite F" + shows + "image_mset h (\x \ F. f x) = (\x \ F. image_mset h (f x))" + using assms + by (induction F rule:finite_induct, simp, simp) + +lemma decomp_mset: + "(\x\set_mset R. replicate_mset (count R x) x) = R" + by (rule multiset_eqI, simp add:count_sum count_eq_zero_iff) + +lemma factor_mset_count: + assumes "a \ carrier G" "d \ carrier G" "irreducible G d" + shows "count (factor_mset G a) (assocs G d) = multiplicity G d a" +proof - + have a: + "count (factor_mset G a) (assocs G d) \ m \ d [^] m divides a" + (is "?lhs \ ?rhs") for m + proof - + have "?lhs \ replicate_mset m (assocs G d) \# factor_mset G a" + by (simp add:count_le_replicate_mset_subset_eq) + also have "... \ factor_mset G (d [^] m) \# factor_mset G a" + using assms(2,3) by (simp add:factor_mset_pow factor_mset_irred) + also have "... \ ?rhs" + using assms(1,2) by (subst factor_mset_divides) auto + finally show ?thesis by simp + qed + + define M where "M = {(m::nat). d [^] m divides a}" + + have M_alt: "M = {m. m \ count (factor_mset G a) (assocs G d)}" + using a by (simp add:M_def) + + hence "Max M = count (factor_mset G a) (assocs G d)" + by (intro Max_eqI, auto) + thus ?thesis + unfolding multiplicity_def M_def by auto +qed + +lemma multiplicity_ge_iff: + assumes "d \ carrier G" "irreducible G d" "a \ carrier G" + shows "multiplicity G d a \ k \ d [^] k divides a" + (is "?lhs \ ?rhs") +proof - + have "?lhs \ count (factor_mset G a) (assocs G d) \ k" + using factor_mset_count[OF assms(3,1,2)] by simp + also have "... \ replicate_mset k (assocs G d) \# factor_mset G a" + by (subst count_le_replicate_mset_subset_eq, simp) + also have "... \ + repeat_mset k (factor_mset G d) \# factor_mset G a" + by (subst factor_mset_irred[OF assms(1,2)], simp) + also have "... \ factor_mset G (d [^]\<^bsub>G\<^esub> k) \# factor_mset G a" + by (subst factor_mset_pow[OF assms(1)], simp) + also have "... \ (d [^] k) divides\<^bsub>G\<^esub> a" + using assms(1) factor_mset_divides[OF _ assms(3)] by simp + finally show ?thesis by simp +qed + +lemma multiplicity_gt_0_iff: + assumes "d \ carrier G" "irreducible G d" "a \ carrier G" + shows "multiplicity G d a > 0 \ d divides a" + using multiplicity_ge_iff[OF assms(1,2,3), where k="1"] assms + by auto + +lemma factor_mset_count_2: + assumes "a \ carrier G" + assumes "\z. z \ carrier G \ irreducible G z \ y \ assocs G z" + shows "count (factor_mset G a) y = 0" + using factor_mset_set [OF assms(1)] assms(2) by (metis count_inI) + +lemma factor_mset_choose: + assumes "a \ carrier G" "set_mset R \ carrier G" + assumes "image_mset (assocs G) R = factor_mset G a" + shows "a \ (\x\set_mset R. x [^] count R x)" (is "a \ ?rhs") +proof - + have b:"irreducible G x" if a:"x \# R" for x + proof - + have x_carr: "x \ carrier G" + using a assms(2) by auto + have "assocs G x \ assocs G ` set_mset R" + using a by simp + hence "assocs G x \# factor_mset G a" + using assms(3) a in_image_mset by metis + then obtain z where z_def: + "z \ carrier G" "irreducible G z" "assocs G x = assocs G z" + using factor_mset_set assms(1) by metis + have "z \ x" using z_def(1,3) assocs_eqD x_carr by simp + thus ?thesis using z_def(1,2) x_carr irreducible_cong by simp + qed + + have "factor_mset G ?rhs = + (\x\set_mset R. factor_mset G (x [^] count R x))" + using assms(2) by (subst factor_mset_prod, auto) + also have "... = + (\x\set_mset R. repeat_mset (count R x) (factor_mset G x))" + using assms(2) by (intro sum.cong, auto simp add:factor_mset_pow) + also have "... = (\x\set_mset R. + repeat_mset (count R x) (image_mset (assocs G) {#x#}))" + using assms(2) b by (intro sum.cong, auto simp add:factor_mset_irred) + also have "... = (\x\set_mset R. + image_mset (assocs G) (replicate_mset (count R x) x))" + by simp + also have "... = image_mset (assocs G) + (\x\set_mset R. (replicate_mset (count R x) x))" + by (simp add: image_mset_sum) + also have "... = image_mset (assocs G) R" + by (simp add:decomp_mset) + also have "... = factor_mset G a" + using assms by simp + finally have "factor_mset G ?rhs = factor_mset G a" by simp + moreover have "(\x\set_mset R. x [^] count R x) \ carrier G" + using assms(2) by (intro finprod_closed, auto) + ultimately show ?thesis + using assms(1) by (subst factor_mset_sim) auto +qed + +lemma divides_iff_mult_mono: + assumes "a \ carrier G" "b \ carrier G" + assumes "canonical_irreducibles G R" + assumes "\d. d \ R \ multiplicity G d a \ multiplicity G d b" + shows "a divides b" +proof - + have "count (factor_mset G a) d \ count (factor_mset G b) d" for d + proof (cases "\y \ carrier G. irreducible G y \ d = assocs G y") + case True + then obtain y where y_def: + "irreducible G y" "y \ carrier G" "d = assocs G y" + by blast + then obtain z where z_def: "z \ R" "y \ z" + using assms(3) unfolding canonical_irreducibles_def by metis + have z_more: "irreducible G z" "z \ carrier G" + using z_def(1) assms(3) + unfolding canonical_irreducibles_def by auto + have "y \ assocs G z" using z_def(2) z_more(2) y_def(2) + by (simp add: closure_ofI2) + hence d_def: "d = assocs G z" + using y_def(2,3) z_more(2) assocs_repr_independence + by blast + have "count (factor_mset G a) d = multiplicity G z a" + unfolding d_def + by (intro factor_mset_count[OF assms(1) z_more(2,1)]) + also have "... \ multiplicity G z b" + using assms(4) z_def(1) by simp + also have "... = count (factor_mset G b) d" + unfolding d_def + by (intro factor_mset_count[symmetric, OF assms(2) z_more(2,1)]) + finally show ?thesis by simp + next + case False + have "count (factor_mset G a) d = 0" using False + by (intro factor_mset_count_2[OF assms(1)], simp) + moreover have "count (factor_mset G b) d = 0" using False + by (intro factor_mset_count_2[OF assms(2)], simp) + ultimately show ?thesis by simp + qed + + hence "factor_mset G a \# factor_mset G b" + unfolding subseteq_mset_def by simp + thus ?thesis using factor_mset_divides assms(1,2) by simp +qed + +lemma count_image_mset_inj: + assumes "inj_on f R" "x \ R" "set_mset A \ R" + shows "count (image_mset f A) (f x) = count A x" +proof (cases "x \# A") + case True + hence "(f y = f x \ y \# A) = (y = x)" for y + by (meson assms(1) assms(3) inj_onD subsetD) + hence "(f -` {f x} \ set_mset A) = {x}" + by (simp add:set_eq_iff) + thus ?thesis + by (subst count_image_mset, simp) +next + case False + hence "x \ set_mset A" by simp + hence "f x \ f ` set_mset A" using assms + by (simp add: inj_on_image_mem_iff) + hence "count (image_mset f A) (f x) = 0" + by (simp add:count_eq_zero_iff) + thus ?thesis by (metis count_inI False) +qed + +text \Factorization of an element from a @{locale "factorial_monoid"} using a selection of representatives +from each equivalence class formed by @{term "(\)"}.\ + +lemma split_factors: + assumes "canonical_irreducibles G R" + assumes "a \ carrier G" + shows + "finite {d. d \ R \ multiplicity G d a > 0}" + "a \ (\d\{d. d \ R \ multiplicity G d a > 0}. + d [^] multiplicity G d a)" (is "a \ ?rhs") +proof - + have r_1: "R \ {x. x \ carrier G \ irreducible G x}" + using assms(1) unfolding canonical_irreducibles_def by simp + have r_2: "\x y. x \ R \ y \ R \ x \ y \ x = y" + using assms(1) unfolding canonical_irreducibles_def by simp + + have assocs_inj: "inj_on (assocs G) R" + using r_1 r_2 assocs_eqD by (intro inj_onI, blast) + + define R' where + "R' = (\d\ {d. d \ R \ multiplicity G d a > 0}. + replicate_mset (multiplicity G d a) d)" + + have "count (factor_mset G a) (assocs G x) > 0" + if "x \ R" "0 < multiplicity G x a" for x + using assms r_1 r_2 that + by (subst factor_mset_count[OF assms(2)]) auto + hence "assocs G ` {d \ R. 0 < multiplicity G d a} + \ set_mset (factor_mset G a)" + by (intro image_subsetI, simp) + hence a:"finite (assocs G ` {d \ R. 0 < multiplicity G d a})" + using finite_subset by auto + + show "finite {d \ R. 0 < multiplicity G d a}" + using assocs_inj inj_on_subset[OF assocs_inj] + by (intro finite_imageD[OF a], simp) + + hence count_R': + "count R' d = (if d \ R then multiplicity G d a else 0)" + for d + by (auto simp add:R'_def count_sum) + + have set_R': "set_mset R' = {d \ R. 0 < multiplicity G d a}" + unfolding set_mset_def using count_R' by auto + + have "count (image_mset (assocs G) R') x = + count (factor_mset G a) x" for x + proof (cases "\x'. x' \ R \ x = assocs G x'") + case True + then obtain x' where x'_def: "x' \ R" "x = assocs G x'" + by blast + have "count (image_mset (assocs G) R') x = count R' x'" + using assocs_inj inj_on_subset[OF assocs_inj] x'_def + by (subst x'_def(2), subst count_image_mset_inj[OF assocs_inj]) + (auto simp:set_R') + also have "... = multiplicity G x' a" + using count_R' x'_def by simp + also have "... = count (factor_mset G a) (assocs G x')" + using x'_def(1) r_1 + by (subst factor_mset_count[OF assms(2)]) auto + also have "... = count (factor_mset G a) x" + using x'_def(2) by simp + finally show ?thesis by simp + next + case False + have a:"x \ assocs G z" + if a1: "z \ carrier G" and a2: "irreducible G z" for z + proof - + obtain v where v_def: "v \ R" "z \ v" + using a1 a2 assms(1) + unfolding canonical_irreducibles_def by auto + hence "z \ assocs G v" + using a1 r_1 v_def(1) by (simp add: closure_ofI2) + hence "assocs G z = assocs G v" + using a1 r_1 v_def(1) assocs_repr_independence + by auto + moreover have "x \ assocs G v" + using False v_def(1) by simp + ultimately show ?thesis by simp + qed + + have "count (image_mset (assocs G) R') x = 0" + using False count_R' by (simp add: count_image_mset) auto + also have "... = count (factor_mset G a) x" + using a + by (intro factor_mset_count_2[OF assms(2), symmetric]) auto + finally show ?thesis by simp + qed + + hence "image_mset (assocs G) R' = factor_mset G a" + by (rule multiset_eqI) + + moreover have "set_mset R' \ carrier G" + using r_1 by (auto simp add:set_R') + ultimately have "a \ (\x\set_mset R'. x [^] count R' x)" + using assms(2) by (intro factor_mset_choose, auto) + also have "... = ?rhs" + using set_R' assms r_1 r_2 + by (intro finprod_cong', auto simp add:count_R') + finally show "a \ ?rhs" by simp +qed + +end + +end \ No newline at end of file diff --git a/thys/Finite_Fields/Finite_Fields_Isomorphic.thy b/thys/Finite_Fields/Finite_Fields_Isomorphic.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Finite_Fields_Isomorphic.thy @@ -0,0 +1,367 @@ +section \Isomorphism between Finite Fields\label{sec:uniqueness}\ + +theory Finite_Fields_Isomorphic + imports + Card_Irreducible_Polynomials +begin + +lemma (in finite_field) eval_on_root_is_iso: + defines "p \ char R" + assumes "f \ carrier (poly_ring (ZFact p))" + assumes "pirreducible\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" + assumes "order R = p^degree f" + assumes "x \ carrier R" + assumes "eval (map (char_iso R) f) x = \" + shows "ring_hom_ring (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) R + (\g. the_elem ((\g'. eval (map (char_iso R) g') x) ` g))" +proof - + let ?P = "poly_ring (ZFact p)" + + have char_pos: "char R > 0" + using finite_carr_imp_char_ge_0[OF finite_carrier] by simp + + have p_prime: "Factorial_Ring.prime p" + unfolding p_def + using characteristic_is_prime[OF char_pos] by simp + + interpret zf: finite_field "ZFact p" + using zfact_prime_is_finite_field p_prime by simp + interpret pzf: principal_domain "poly_ring (ZFact p)" + using zf.univ_poly_is_principal[OF zf.carrier_is_subfield] by simp + + interpret i: ideal "(PIdl\<^bsub>?P\<^esub> f)" "?P" + by (intro pzf.cgenideal_ideal assms(2)) + have rupt_carr: "y \ carrier (poly_ring (ZFact p))" + if "y \ carrier (Rupt\<^bsub>ZFact p\<^esub> (carrier (ZFact p)) f)" for y + using that pzf.quot_carr i.ideal_axioms by (simp add:rupture_def) + + have rupt_is_ring: "ring (Rupt\<^bsub>ZFact p\<^esub> (carrier (ZFact p)) f)" + unfolding rupture_def by (intro i.quotient_is_ring) + + have "map (char_iso R) \ + ring_iso ?P (poly_ring (R\carrier := char_subring R\))" + using lift_iso_to_poly_ring[OF char_iso] zf.domain_axioms + using char_ring_is_subdomain subdomain_is_domain + by (simp add:p_def) + moreover have "(char_subring R)[X] = + poly_ring (R \carrier := char_subring R\)" + using univ_poly_consistent[OF char_ring_is_subring] by simp + ultimately have + "map (char_iso R) \ ring_hom ?P ((char_subring R)[X])" + by (simp add:ring_iso_def) + moreover have "(\p. eval p x) \ ring_hom ((char_subring R)[X]) R" + using eval_is_hom char_ring_is_subring assms(5) by simp + ultimately have + "(\p. eval p x) \ map (char_iso R) \ ring_hom ?P R" + using ring_hom_trans by blast + hence a:"(\p. eval (map (char_iso R) p) x) \ ring_hom ?P R" + by (simp add:comp_def) + interpret h:ring_hom_ring "?P" "R" "(\p. eval (map (char_iso R) p) x)" + by (intro ring_hom_ringI2 pzf.is_ring a ring_axioms) + + let ?h = "(\p. eval (map (char_iso R) p) x)" + let ?J = "a_kernel (poly_ring (ZFact (int p))) R ?h" + + have "?h ` a_kernel (poly_ring (ZFact (int p))) R ?h \ {\}" + by auto + moreover have + "\\<^bsub>?P\<^esub> \ a_kernel (poly_ring (ZFact (int p))) R ?h" + "?h \\<^bsub>?P\<^esub> = \" + unfolding a_kernel_def' by simp_all + hence "{\} \ ?h ` a_kernel (poly_ring (ZFact (int p))) R ?h" + by simp + ultimately have c: + "?h ` a_kernel (poly_ring (ZFact (int p))) R ?h = {\}" + by auto + + have d: "PIdl\<^bsub>?P\<^esub> f \ a_kernel ?P R ?h" + proof (rule subsetI) + fix y assume "y \ PIdl\<^bsub>?P\<^esub> f" + then obtain y' where y'_def: "y' \ carrier ?P" "y = y' \\<^bsub>?P\<^esub> f" + unfolding cgenideal_def by auto + have "?h y = ?h (y' \\<^bsub>?P\<^esub> f)" by (simp add:y'_def) + also have "... = ?h y' \ ?h f" + using y'_def assms(2) by simp + also have "... = ?h y' \ \" + using assms(6) by simp + also have "... = \" + using y'_def by simp + finally have "?h y = \" by simp + moreover have "y \ carrier ?P" using y'_def assms(2) by simp + ultimately show "y \ a_kernel ?P R ?h" + unfolding a_kernel_def kernel_def by simp + qed + + have "(\y. the_elem ((\p. eval (map (char_iso R) p) x) ` y)) + \ ring_hom (?P Quot ?J) R" + using h.the_elem_hom by simp + moreover have "(\y. ?J <+>\<^bsub>?P\<^esub> y) + \ ring_hom (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) (?P Quot ?J)" + unfolding rupture_def using h.kernel_is_ideal d assms(2) + by (intro pzf.quot_quot_hom pzf.cgenideal_ideal) auto + ultimately have "(\y. the_elem (?h ` y)) \ (\y. ?J <+>\<^bsub>?P\<^esub> y) + \ ring_hom (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) R" + using ring_hom_trans by blast + hence b: "(\y. the_elem (?h ` (?J <+>\<^bsub>?P\<^esub> y))) \ + ring_hom (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) R" + by (simp add:comp_def) + have "?h ` y = ?h ` (?J <+>\<^bsub>?P\<^esub> y)" + if "y \ carrier (Rupt\<^bsub>ZFact p\<^esub> (carrier (ZFact p)) f)" + for y + proof - + have y_range: "y \ carrier ?P" + using rupt_carr that by simp + have "?h ` y = {\} <+>\<^bsub>R\<^esub> ?h ` y" + using y_range h.hom_closed by (subst set_add_zero, auto) + also have "... = ?h ` ?J <+>\<^bsub>R\<^esub> ?h ` y" + by (subst c, simp) + also have "... = ?h ` (?J <+>\<^bsub>?P\<^esub> y)" + by (subst set_add_hom[OF a _ y_range], subst a_kernel_def') auto + finally show ?thesis by simp + qed + hence "(\y. the_elem (?h ` y)) \ + ring_hom (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) R" + by (intro ring_hom_cong[OF _ rupt_is_ring b]) simp + thus ?thesis + by (intro ring_hom_ringI2 rupt_is_ring ring_axioms, simp) +qed + +lemma (in domain) pdivides_consistent: + assumes "subfield K R" "f \ carrier (K[X])" "g \ carrier (K[X])" + shows "f pdivides g \ f pdivides\<^bsub>R \ carrier := K \\<^esub> g" +proof - + have a:"subring K R" + using assms(1) subfieldE(1) by auto + let ?S = "R \ carrier := K \" + have "f pdivides g \ f divides\<^bsub>K[X]\<^esub> g" + using pdivides_iff_shell[OF assms] by simp + also have "... \ (\x \ carrier (K[X]). f \\<^bsub>K[X]\<^esub> x = g)" + unfolding pdivides_def factor_def by auto + also have "... \ + (\x \ carrier (poly_ring ?S). f \\<^bsub>poly_ring ?S\<^esub> x = g)" + using univ_poly_consistent[OF a] by simp + also have "... \ f divides\<^bsub>poly_ring ?S\<^esub> g" + unfolding pdivides_def factor_def by auto + also have "... \ f pdivides\<^bsub>?S\<^esub> g" + unfolding pdivides_def by simp + finally show ?thesis by simp +qed + +lemma (in finite_field) find_root: + assumes "subfield K R" + assumes "monic_irreducible_poly (R \ carrier := K \) f" + assumes "order R = card K^degree f" + obtains x where "eval f x = \" "x \ carrier R" +proof - + define \ :: "'a list \ 'a list" where "\ = id" + let ?K = "R \ carrier := K \" + have "finite K" + using assms(1) by (intro finite_subset[OF _ finite_carrier], simp) + hence fin_K: "finite (carrier (?K))" + by simp + interpret f: finite_field "?K" + using assms(1) subfield_iff fin_K finite_fieldI by blast + have b:"subring K R" + using assms(1) subfieldE(1) by blast + interpret e: ring_hom_ring "(K[X])" "(poly_ring R)" "\" + using embed_hom[OF b] by (simp add:\_def) + + have a: "card K^degree f > 1" + using assms(3) finite_field_min_order by simp + have "f \ carrier (poly_ring ?K)" + using f.monic_poly_carr assms(2) + unfolding monic_irreducible_poly_def by simp + hence f_carr_2: "f \ carrier (K[X])" + using univ_poly_consistent[OF b] by simp + have f_carr: "f \ carrier (poly_ring R)" + using e.hom_closed[OF f_carr_2] unfolding \_def by simp + + have gp_carr: "gauss_poly ?K (order ?K^degree f) \ carrier (K[X])" + using f.gauss_poly_carr univ_poly_consistent[OF b] by simp + + have "gauss_poly ?K (order ?K^degree f) = + gauss_poly ?K (card K^degree f)" + by (simp add:Coset.order_def) + also have "... = + X\<^bsub>?K\<^esub> [^]\<^bsub>poly_ring ?K\<^esub> card K ^ degree f \\<^bsub>poly_ring ?K\<^esub> X\<^bsub>?K\<^esub>" + unfolding gauss_poly_def by simp + also have "... = X\<^bsub>R\<^esub> [^]\<^bsub>K[X]\<^esub> card K ^ degree f \\<^bsub>K[X]\<^esub> X\<^bsub>R\<^esub>" + unfolding var_def using univ_poly_consistent[OF b] by simp + also have "... = \ (X\<^bsub>R\<^esub> [^]\<^bsub>K[X]\<^esub> card K ^ degree f \\<^bsub>K[X]\<^esub> X\<^bsub>R\<^esub>)" + unfolding \_def by simp + also have "... = gauss_poly R (card K^degree f)" + unfolding gauss_poly_def a_minus_def using var_closed[OF b] + by (simp add:e.hom_nat_pow, simp add:\_def) + finally have gp_consistent: "gauss_poly ?K (order ?K^degree f) = + gauss_poly R (card K^degree f)" + by simp + + have deg_f: "degree f > 0" + using f.monic_poly_min_degree[OF assms(2)] by simp + + have "splitted f" + proof (cases "degree f > 1") + case True + + have "f pdivides\<^bsub>?K\<^esub> gauss_poly ?K (order ?K^degree f)" + using f.div_gauss_poly_iff[OF deg_f assms(2)] by simp + hence "f pdivides gauss_poly ?K (order ?K^degree f)" + using pdivides_consistent[OF assms(1)] f_carr_2 gp_carr by simp + hence "f pdivides gauss_poly R (card K^degree f)" + using gp_consistent by simp + moreover have "splitted (gauss_poly R (card K^degree f))" + unfolding assms(3)[symmetric] using gauss_poly_splitted by simp + moreover have "gauss_poly R (card K^degree f) \ []" + using gauss_poly_not_zero a by (simp add: univ_poly_zero) + ultimately show "splitted f" + using pdivides_imp_splitted f_carr gauss_poly_carr by auto + next + case False + hence "degree f = 1" using deg_f by simp + thus ?thesis using f_carr degree_one_imp_splitted by auto + qed + hence "size (roots f) > 0" + using deg_f unfolding splitted_def by simp + then obtain x where x_def: "x \ carrier R" "is_root f x" + using roots_mem_iff_is_root[OF f_carr] + by (metis f_carr nonempty_has_size not_empty_rootsE) + have "eval f x = \" + using x_def is_root_def by blast + thus ?thesis using x_def using that by simp +qed + +lemma (in finite_field) find_iso_from_zfact: + defines "p \ int (char R)" + assumes "monic_irreducible_poly (ZFact p) f" + assumes "order R = char R^degree f" + shows "\\. \ \ ring_iso (Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f) R" +proof - + have char_pos: "char R > 0" + using finite_carr_imp_char_ge_0[OF finite_carrier] by simp + + interpret zf: finite_field "ZFact p" + unfolding p_def using zfact_prime_is_finite_field + using characteristic_is_prime[OF char_pos] by simp + + interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)" + unfolding polynomial_ring_def polynomial_ring_axioms_def + using zf.field_axioms zf.carrier_is_subfield by simp + + let ?f' = "map (char_iso R) f" + let ?F = "Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" + + have "domain (R\carrier := char_subring R\)" + using char_ring_is_subdomain subdomain_is_domain by simp + + hence "monic_irreducible_poly (R \ carrier := char_subring R \) ?f'" + using char_iso p_def zf.domain_axioms + by (intro monic_irreducible_poly_hom[OF assms(2)]) auto + moreover have "order R = card (char_subring R)^degree ?f'" + using assms(3) unfolding char_def by simp + ultimately obtain x where x_def: "eval ?f' x = \" "x \ carrier R" + using find_root[OF char_ring_is_subfield[OF char_pos]] by blast + let ?\ = "(\g. the_elem ((\g'. eval (map (char_iso R) g') x) ` g))" + interpret r: ring_hom_ring "?F" "R" "?\" + using assms(2,3) + unfolding monic_irreducible_poly_def monic_poly_def p_def + by (intro eval_on_root_is_iso x_def, auto) + have a:"?\ \ ring_hom ?F R" + using r.homh by auto + + have "field (Rupt\<^bsub>ZFact p\<^esub> (carrier (ZFact p)) f)" + using assms(2) + unfolding monic_irreducible_poly_def monic_poly_def + by (subst zfp.rupture_is_field_iff_pirreducible, simp_all) + hence b:"inj_on ?\ (carrier ?F)" + using non_trivial_field_hom_is_inj[OF a _ field_axioms] by simp + + have "card (?\ ` carrier ?F) = order ?F" + using card_image[OF b] unfolding Coset.order_def by simp + also have "... = card (carrier (ZFact p))^degree f" + using assms(2) zf.monic_poly_min_degree[OF assms(2)] + unfolding monic_irreducible_poly_def monic_poly_def + by (intro zf.rupture_order[OF zf.carrier_is_subfield]) auto + also have "... = char R ^degree f" + unfolding p_def by (subst card_zfact_carr[OF char_pos], simp) + also have "... = card (carrier R)" + using assms(3) unfolding Coset.order_def by simp + finally have "card (?\ ` carrier ?F) = card (carrier R)" by simp + moreover have "?\ ` carrier ?F \ carrier R" + by (intro image_subsetI, simp) + ultimately have "?\ ` carrier ?F = carrier R" + by (intro card_seteq finite_carrier, auto) + hence "bij_betw ?\ (carrier ?F) (carrier R)" + using b bij_betw_imageI by auto + + thus ?thesis + unfolding ring_iso_def using a b by auto +qed + +theorem uniqueness: + assumes "finite_field F\<^sub>1" + assumes "finite_field F\<^sub>2" + assumes "order F\<^sub>1 = order F\<^sub>2" + shows "F\<^sub>1 \ F\<^sub>2" +proof - + obtain n where o1: "order F\<^sub>1 = char F\<^sub>1^n" "n > 0" + using finite_field.finite_field_order[OF assms(1)] by auto + obtain m where o2: "order F\<^sub>2 = char F\<^sub>2^m" "m > 0" + using finite_field.finite_field_order[OF assms(2)] by auto + + interpret f1: "finite_field" F\<^sub>1 using assms(1) by simp + interpret f2: "finite_field" F\<^sub>2 using assms(2) by simp + + have char_pos: "char F\<^sub>1 > 0" "char F\<^sub>2 > 0" + using f1.finite_carrier f1.finite_carr_imp_char_ge_0 + using f2.finite_carrier f2.finite_carr_imp_char_ge_0 by auto + hence char_prime: + "Factorial_Ring.prime (char F\<^sub>1)" + "Factorial_Ring.prime (char F\<^sub>2)" + using f1.characteristic_is_prime f2.characteristic_is_prime + by auto + + have "char F\<^sub>1^n = char F\<^sub>2^m" + using o1 o2 assms(3) by simp + hence eq: "n = m" "char F\<^sub>1 = char F\<^sub>2" + using char_prime char_pos o1(2) o2(2) prime_power_inj' by auto + + obtain p where p_def: "p = char F\<^sub>1" "p = char F\<^sub>2" + using eq by simp + + have p_prime: "Factorial_Ring.prime p" + unfolding p_def(1) + using f1.characteristic_is_prime char_pos by simp + + interpret zf: finite_field "ZFact (int p)" + using zfact_prime_is_finite_field p_prime o1(2) + using prime_nat_int_transfer by blast + + interpret zfp: polynomial_ring "ZFact p" "carrier (ZFact p)" + unfolding polynomial_ring_def polynomial_ring_axioms_def + using zf.field_axioms zf.carrier_is_subfield by simp + + obtain f where f_def: + "monic_irreducible_poly (ZFact (int p)) f" "degree f = n" + using zf.exist_irred o1(2) by auto + + let ?F\<^sub>0 = "Rupt\<^bsub>(ZFact p)\<^esub> (carrier (ZFact p)) f" + + obtain \\<^sub>1 where \\<^sub>1_def: "\\<^sub>1 \ ring_iso ?F\<^sub>0 F\<^sub>1" + using f1.find_iso_from_zfact f_def o1 + unfolding p_def by auto + + obtain \\<^sub>2 where \\<^sub>2_def: "\\<^sub>2 \ ring_iso ?F\<^sub>0 F\<^sub>2" + using f2.find_iso_from_zfact f_def o2 + unfolding p_def(2) eq(1) by auto + + have "?F\<^sub>0 \ F\<^sub>1" using \\<^sub>1_def is_ring_iso_def by auto + moreover have "?F\<^sub>0 \ F\<^sub>2" using \\<^sub>2_def is_ring_iso_def by auto + moreover have "field ?F\<^sub>0" + using f_def(1) zf.monic_poly_carr monic_irreducible_poly_def + by (subst zfp.rupture_is_field_iff_pirreducible) auto + hence "ring ?F\<^sub>0" using field.is_ring by auto + ultimately show ?thesis + using ring_iso_trans ring_iso_sym by blast +qed + +end diff --git a/thys/Finite_Fields/Finite_Fields_Preliminary_Results.thy b/thys/Finite_Fields/Finite_Fields_Preliminary_Results.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Finite_Fields_Preliminary_Results.thy @@ -0,0 +1,1010 @@ +section \Introduction\ + +text \The following section starts with preliminary results. Section~\ref{sec:ring_char} introduces +the characteristic of rings with the Frobenius endomorphism. Whenever it makes sense, +the definitions and facts do not assume the finiteness of the fields or rings. For example the +characteristic is defined over arbitrary rings (and also fields). + +While formal derivatives do exist for type-class based structures in +\verb|HOL-Computational_Algebra|, as far as I can tell, they do not exist for the structure based +polynomials in \verb|HOL-Algebra|. These are introduced in Section~\ref{sec:pderiv}. + +A cornerstone of the proof is the derivation of Gauss' formula for the number of monic irreducible +polynomials over a finite field $R$ in Section~\ref{sec:card_irred}. The proof follows the +derivation by Ireland and Rosen~\cite[\textsection 7]{ireland1982} closely, with the caveat that it +does not assume that $R$ is a simple prime field, but that it is just a finite field. +This works by adjusting a proof step with the information that the order of a finite field must be +of the form $p^n$, where $p$ is the characteristic of the field, derived in Section~\ref{sec:ring_char}. +The final step relies on the M\"obius inversion theorem formalized by +Eberl~\cite{Dirichlet_Series-AFP}.\footnote{Thanks to Katharina Kreuzer for discovering that +formalization.} + +With Gauss' formula it is possible to show the existence of the finite fields of order $p^n$ +where $p$ is a prime and $n > 0$. During the proof the fact that the polynomial $X^n - X$ splits +in a field of order $n$ is also derived, which is necessary for the uniqueness result as well. + +The uniqueness proof is inspired by the derivation of the same result in +Lidl and Niederreiter~\cite{lidl1986}, but because of the already derived existence proof for +irreducible polynomials, it was possible to reduce its complexity. + +The classification consists of three theorems: +\begin{itemize} +\item \emph{Existence}: For each prime power $p^n$ there exists a finite field of that size. + This is shown at the conclusion of Section~\ref{sec:card_irred}. +\item \emph{Uniqueness}: Any two finite fields of the same size are isomorphic. + This is shown at the conclusion of Section~\ref{sec:uniqueness}. +\item \emph{Completeness}: Any finite fields' size must be a prime power. + This is shown at the conclusion of Section~\ref{sec:ring_char}. +\end{itemize} +\ + +section \Preliminary Results\ + +theory Finite_Fields_Preliminary_Results + imports "HOL-Algebra.Polynomial_Divisibility" +begin + +subsection \Summation in the discrete topology\ + +text \The following lemmas transfer the corresponding result from the summation over finite sets +to summation over functions which vanish outside of a finite set.\ + +lemma sum'_subtractf_nat: + fixes f :: "'a \ nat" + assumes "finite {i \ A. f i \ 0}" + assumes "\i. i \ A \ g i \ f i" + shows "sum' (\i. f i - g i) A = sum' f A - sum' g A" + (is "?lhs = ?rhs") +proof - + have c:"finite {i \ A. g i \ 0}" + using assms(2) + by (intro finite_subset[OF _ assms(1)] subsetI, force) + let ?B = "{i \ A. f i \ 0 \ g i \ 0}" + + have b:"?B = {i \ A. f i \ 0} \ {i \ A. g i \ 0}" + by (auto simp add:set_eq_iff) + have a:"finite ?B" + using assms(1) c by (subst b, simp) + have "?lhs = sum' (\i. f i - g i) ?B" + by (intro sum.mono_neutral_cong_right', simp_all) + also have "... = sum (\i. f i - g i) ?B" + by (intro sum.eq_sum a) + also have "... = sum f ?B - sum g ?B" + using assms(2) by (subst sum_subtractf_nat, auto) + also have "... = sum' f ?B - sum' g ?B" + by (intro arg_cong2[where f="(-)"] sum.eq_sum[symmetric] a) + also have "... = ?rhs" + by (intro arg_cong2[where f="(-)"] sum.mono_neutral_cong_left') + simp_all + finally show ?thesis + by simp +qed + +lemma sum'_nat_eq_0_iff: + fixes f :: "'a \ nat" + assumes "finite {i \ A. f i \ 0}" + assumes "sum' f A = 0" + shows "\i. i \ A \ f i = 0" +proof - + let ?B = "{i \ A. f i \ 0}" + + have "sum f ?B = sum' f ?B" + by (intro sum.eq_sum[symmetric] assms(1)) + also have "... = sum' f A" + by (intro sum.non_neutral') + also have "... = 0" using assms(2) by simp + finally have a:"sum f ?B = 0" by simp + have "\i. i \ ?B \ f i = 0" + using sum_nonneg_0[OF assms(1) _ a] by blast + thus "\i. i \ A \ f i = 0" + by blast +qed + +lemma sum'_eq_iff: + fixes f :: "'a \ nat" + assumes "finite {i \ A. f i \ 0}" + assumes "\i. i \ A \ f i \ g i" + assumes "sum' f A \ sum' g A" + shows "\i \ A. f i = g i" +proof - + have "{i \ A. g i \ 0} \ {i \ A. f i \ 0}" + using assms(2) order_less_le_trans + by (intro subsetI, auto) + hence a:"finite {i \ A. g i \ 0}" + by (rule finite_subset, intro assms(1)) + have " {i \ A. f i - g i \ 0} \ {i \ A. f i \ 0}" + by (intro subsetI, simp_all) + hence b: "finite {i \ A. f i - g i \ 0}" + by (rule finite_subset, intro assms(1)) + have "sum' (\i. f i - g i) A = sum' f A - sum' g A" + using assms(1,2) a by (subst sum'_subtractf_nat, auto) + also have "... = 0" + using assms(3) by simp + finally have "sum' (\i. f i - g i) A = 0" by simp + hence "\i. i \ A \ f i - g i = 0" + using sum'_nat_eq_0_iff[OF b] by simp + thus ?thesis + using assms(2) diff_is_0_eq' diffs0_imp_equal by blast +qed + +subsection \Polynomials\ + +text \The embedding of the constant polynomials into the polynomials is injective:\ + +lemma (in ring) poly_of_const_inj: + "inj poly_of_const" +proof - + have "coeff (poly_of_const x) 0 = x" for x + unfolding poly_of_const_def normalize_coeff[symmetric] + by simp + thus ?thesis by (metis injI) +qed + +lemma (in domain) embed_hom: + assumes "subring K R" + shows "ring_hom_ring (K[X]) (poly_ring R) id" +proof (rule ring_hom_ringI) + show "ring (K[X])" + using univ_poly_is_ring[OF assms(1)] by simp + show "ring (poly_ring R)" + using univ_poly_is_ring[OF carrier_is_subring] by simp + have "K \ carrier R" + using subringE(1)[OF assms(1)] by simp + thus "\x. x \ carrier (K [X]) \ id x \ carrier (poly_ring R)" + unfolding univ_poly_carrier[symmetric] polynomial_def by auto + show "id (x \\<^bsub>K [X]\<^esub> y) = id x \\<^bsub>poly_ring R\<^esub> id y" + if "x \ carrier (K [X])" "y \ carrier (K [X])" for x y + unfolding univ_poly_mult by simp + show "id (x \\<^bsub>K [X]\<^esub> y) = id x \\<^bsub>poly_ring R\<^esub> id y" + if "x \ carrier (K [X])" "y \ carrier (K [X])" for x y + unfolding univ_poly_add by simp + show "id \\<^bsub>K [X]\<^esub> = \\<^bsub>poly_ring R\<^esub>" + unfolding univ_poly_one by simp +qed + +text \The following are versions of the properties of the degrees of polynomials, that abstract +over the definition of the polynomial ring structure. In the theories +@{theory "HOL-Algebra.Polynomials"} and also @{theory "HOL-Algebra.Polynomial_Divisibility"} +these abstract version are usually indicated with the suffix ``shell'', consider for example: +@{thm [source] "domain.pdivides_iff_shell"}.\ + +lemma (in ring) degree_add_distinct: + assumes "subring K R" + assumes "f \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + assumes "g \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + assumes "degree f \ degree g" + shows "degree (f \\<^bsub>K[X]\<^esub> g) = max (degree f) (degree g)" + unfolding univ_poly_add using assms(2,3,4) + by (subst poly_add_degree_eq[OF assms(1)]) + (auto simp:univ_poly_carrier univ_poly_zero) + +lemma (in domain) degree_mult: + assumes "subring K R" + assumes "f \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + assumes "g \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + shows "degree (f \\<^bsub>K[X]\<^esub> g) = degree f + degree g" + unfolding univ_poly_mult using assms(2,3) + by (subst poly_mult_degree_eq[OF assms(1)]) + (auto simp:univ_poly_carrier univ_poly_zero) + +lemma (in ring) degree_one: + "degree (\\<^bsub>K[X]\<^esub>) = 0" + unfolding univ_poly_one by simp + +lemma (in domain) pow_non_zero: + "x \ carrier R \ x \ \ \ x [^] (n :: nat) \ \" + using integral by (induction n, auto) + +lemma (in domain) degree_pow: + assumes "subring K R" + assumes "f \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + shows "degree (f [^]\<^bsub>K[X]\<^esub> n) = degree f * n" +proof - + interpret p:domain "K[X]" + using univ_poly_is_domain[OF assms(1)] by simp + + show ?thesis + proof (induction n) + case 0 + then show ?case by (simp add:univ_poly_one) + next + case (Suc n) + have "degree (f [^]\<^bsub>K [X]\<^esub> Suc n) = degree (f [^]\<^bsub>K [X]\<^esub> n \\<^bsub>K[X]\<^esub> f)" + by simp + also have "... = degree (f [^]\<^bsub>K [X]\<^esub> n) + degree f" + using p.pow_non_zero assms(2) + by (subst degree_mult[OF assms(1)], auto) + also have "... = degree f * Suc n" + by (subst Suc, simp) + finally show ?case by simp + qed +qed + +lemma (in ring) degree_var: + "degree (X\<^bsub>R\<^esub>) = 1" + unfolding var_def by simp + +lemma (in domain) var_carr: + fixes n :: nat + assumes "subring K R" + shows "X\<^bsub>R\<^esub> \ carrier (K[X]) - {\\<^bsub>K [X]\<^esub>}" +proof - + have "X\<^bsub>R\<^esub> \ carrier (K[X])" + using var_closed[OF assms(1)] by simp + moreover have "X \ \\<^bsub>K [X]\<^esub>" + unfolding var_def univ_poly_zero by simp + ultimately show ?thesis by simp +qed + +lemma (in domain) var_pow_carr: + fixes n :: nat + assumes "subring K R" + shows "X\<^bsub>R\<^esub> [^]\<^bsub>K [X]\<^esub> n \ carrier (K[X]) - {\\<^bsub>K [X]\<^esub>}" +proof - + interpret p:domain "K[X]" + using univ_poly_is_domain[OF assms(1)] by simp + + have "X\<^bsub>R\<^esub> [^]\<^bsub>K [X]\<^esub> n \ carrier (K[X])" + using var_pow_closed[OF assms(1)] by simp + moreover have "X \ \\<^bsub>K [X]\<^esub>" + unfolding var_def univ_poly_zero by simp + hence "X\<^bsub>R\<^esub> [^]\<^bsub>K [X]\<^esub> n \ \\<^bsub>K [X]\<^esub>" + using var_closed(1)[OF assms(1)] + by (intro p.pow_non_zero, auto) + ultimately show ?thesis by simp +qed + +lemma (in domain) var_pow_degree: + fixes n :: nat + assumes "subring K R" + shows "degree (X\<^bsub>R\<^esub> [^]\<^bsub>K [X]\<^esub> n) = n" + using var_carr[OF assms(1)] degree_var + by (subst degree_pow[OF assms(1)], auto) + +lemma (in domain) finprod_non_zero: + assumes "finite A" + assumes "f \ A \ carrier R - {\}" + shows "(\i \ A. f i) \ carrier R - {\}" + using assms +proof (induction A rule:finite_induct) + case empty + then show ?case by simp +next + case (insert x F) + have "finprod R f (insert x F) = f x \ finprod R f F" + using insert by (subst finprod_insert, simp_all add:Pi_def) + also have "... \ carrier R-{\}" + using integral insert by auto + finally show ?case by simp +qed + +lemma (in domain) degree_prod: + assumes "finite A" + assumes "subring K R" + assumes "f \ A \ carrier (K[X]) - {\\<^bsub>K[X]\<^esub>}" + shows "degree (\\<^bsub>K[X]\<^esub>i \ A. f i) = (\i \ A. degree (f i))" + using assms +proof - + interpret p:domain "K[X]" + using univ_poly_is_domain[OF assms(2)] by simp + + show ?thesis + using assms(1,3) + proof (induction A rule: finite_induct) + case empty + then show ?case by (simp add:univ_poly_one) + next + case (insert x F) + have "degree (finprod (K[X]) f (insert x F)) = + degree (f x \\<^bsub>K[X]\<^esub> finprod (K[X]) f F)" + using insert by (subst p.finprod_insert, auto) + also have "... = degree (f x) + degree (finprod (K[X]) f F)" + using insert p.finprod_non_zero[OF insert(1)] + by (subst degree_mult[OF assms(2)], simp_all) + also have "... = degree (f x) + (\i \ F. degree (f i))" + using insert by (subst insert(3), auto) + also have "... = (\i \ insert x F. degree (f i))" + using insert by simp + finally show ?case by simp + qed +qed + +lemma (in ring) coeff_add: + assumes "subring K R" + assumes "f \ carrier (K[X])" "g \ carrier (K[X])" + shows "coeff (f \\<^bsub>K[X]\<^esub> g) i = coeff f i \\<^bsub>R\<^esub> coeff g i" +proof - + have a:"set f \ carrier R" + using assms(1,2) univ_poly_carrier + using subringE(1)[OF assms(1)] polynomial_incl + by blast + have b:"set g \ carrier R" + using assms(1,3) univ_poly_carrier + using subringE(1)[OF assms(1)] polynomial_incl + by blast + show ?thesis + unfolding univ_poly_add poly_add_coeff[OF a b] by simp +qed + +text \This is a version of geometric sums for commutative rings:\ + +lemma (in cring) geom: + fixes q:: nat + assumes [simp]: "a \ carrier R" + shows "(a \ \) \ (\i\{.. \)" + (is "?lhs = ?rhs") +proof - + have [simp]: "a [^] i \ carrier R" for i :: nat + by (intro nat_pow_closed assms) + have [simp]: "\ \ \ x = \ x" if "x \ carrier R" for x + using l_minus l_one one_closed that by presburger + + let ?cterm = "(\i\{1.. (\i\{.. (\i\{..i\{.. a [^] i) \ (\i\{..i\{.. (\i\{..i\Suc ` {.. (\i\{..i\ insert q {1.. + (\i\ insert 0 {1.. 0") + case True + moreover have "Suc ` {.. ?cterm) \ (\ \ ?cterm)" + by simp + also have "... = a [^] q \ ?cterm \ (\ \ \ \ ?cterm)" + unfolding a_minus_def by (subst minus_add, simp_all) + also have "... = a [^] q \ (?cterm \ (\ \ \ \ ?cterm))" + by (subst a_assoc, simp_all) + also have "... = a [^] q \ (?cterm \ (\ ?cterm \ \ \))" + by (subst a_comm[where x="\ \"], simp_all) + also have "... = a [^] q \ ((?cterm \ (\ ?cterm)) \ \ \)" + by (subst a_assoc, simp_all) + also have "... = a [^] q \ (\ \ \ \)" + by (subst r_neg, simp_all) + also have "... = a [^] q \ \" + unfolding a_minus_def by simp + finally show ?thesis by simp +qed + +lemma (in domain) rupture_eq_0_iff: + assumes "subfield K R" "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "rupture_surj K p q = \\<^bsub>Rupt K p\<^esub> \ p pdivides q" + (is "?lhs \ ?rhs") +proof - + interpret h:ring_hom_ring "K[X]" "(Rupt K p)" "(rupture_surj K p)" + using assms subfieldE by (intro rupture_surj_hom) auto + + have a: "q pmod p \ (\q. q pmod p) ` carrier (K [X])" + using assms(3) by simp + have "\\<^bsub>K[X]\<^esub> = \\<^bsub>K[X]\<^esub> pmod p" + using assms(1,2) long_division_zero(2) + by (simp add:univ_poly_zero) + hence b: "\\<^bsub>K[X]\<^esub> \ (\q. q pmod p) ` carrier (K[X])" + by (simp add:image_iff) auto + + have "?lhs \ rupture_surj K p (q pmod p) = + rupture_surj K p (\\<^bsub>K[X]\<^esub>)" + by (subst rupture_surj_composed_with_pmod[OF assms]) simp + also have "... \ q pmod p = \\<^bsub>K[X]\<^esub>" + using assms(3) + by (intro inj_on_eq_iff[OF rupture_surj_inj_on[OF assms(1,2)]] a b) + also have "... \ ?rhs" + unfolding univ_poly_zero + by (intro pmod_zero_iff_pdivides[OF assms(1)] assms(2,3)) + finally show "?thesis" by simp +qed + +subsection \Ring Isomorphisms\ + +text \The following lemma shows that an isomorphism between domains also induces an isomorphism +between the corresponding polynomial rings.\ + +lemma lift_iso_to_poly_ring: + assumes "h \ ring_iso R S" "domain R" "domain S" + shows "map h \ ring_iso (poly_ring R) (poly_ring S)" +proof (rule ring_iso_memI) + interpret dr: domain "R" using assms(2) by blast + interpret ds: domain "S" using assms(3) by blast + interpret pdr: domain "poly_ring R" + using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp + interpret pds: domain "poly_ring S" + using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp + interpret h: ring_hom_ring "R" "S" h + using dr.is_ring ds.is_ring assms(1) + by (intro ring_hom_ringI2, simp_all add:ring_iso_def) + let ?R = "poly_ring R" + let ?S = "poly_ring S" + + have h_img: "h ` (carrier R) = carrier S" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + have h_inj: "inj_on h (carrier R)" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + hence h_non_zero_iff: "h x \ \\<^bsub>S\<^esub>" + if "x \ \\<^bsub>R\<^esub>" "x \ carrier R" for x + using h.hom_zero dr.zero_closed inj_onD that by metis + + have norm_elim: "ds.normalize (map h x) = map h x" + if "x \ carrier (poly_ring R)" for x + proof (cases "x") + case Nil then show ?thesis by simp + next + case (Cons xh xt) + have "xh \ carrier R" "xh \ \\<^bsub>R\<^esub>" + using that unfolding Cons univ_poly_carrier[symmetric] + unfolding polynomial_def by auto + hence "h xh \ \\<^bsub>S\<^esub>" using h_non_zero_iff by simp + then show ?thesis unfolding Cons by simp + qed + + show t_1: "map h x \ carrier ?S" + if "x \ carrier ?R" for x + using that hd_in_set h_non_zero_iff hd_map + unfolding univ_poly_carrier[symmetric] polynomial_def + by (cases x, auto) + + show "map h (x \\<^bsub>?R\<^esub> y) = map h x \\<^bsub>?S\<^esub> map h y" + if "x \ carrier ?R" "y \ carrier ?R" for x y + proof - + have "map h (x \\<^bsub>?R\<^esub> y) = ds.normalize (map h (x \\<^bsub>?R\<^esub> y))" + using that by (intro norm_elim[symmetric],simp) + also have "... = map h x \\<^bsub>?S\<^esub> map h y" + using that unfolding univ_poly_mult univ_poly_carrier[symmetric] + unfolding polynomial_def + by (intro h.poly_mult_hom'[of x y] , auto) + finally show ?thesis by simp + qed + + show "map h (x \\<^bsub>?R\<^esub> y) = map h x \\<^bsub>?S\<^esub> map h y" + if "x \ carrier ?R" "y \ carrier ?R" for x y + proof - + have "map h (x \\<^bsub>?R\<^esub> y) = ds.normalize (map h (x \\<^bsub>?R\<^esub> y))" + using that by (intro norm_elim[symmetric],simp) + also have "... = map h x \\<^bsub>?S\<^esub> map h y" + using that + unfolding univ_poly_add univ_poly_carrier[symmetric] + unfolding polynomial_def + by (intro h.poly_add_hom'[of x y], auto) + finally show ?thesis by simp + qed + + show "map h \\<^bsub>?R\<^esub> = \\<^bsub>?S\<^esub>" + unfolding univ_poly_one by simp + + let ?hinv = "map (the_inv_into (carrier R) h)" + + have "map h \ carrier ?R \ carrier ?S" + using t_1 by simp + moreover have "?hinv x \ carrier ?R" + if "x \ carrier ?S" for x + proof (cases "x = []") + case True + then show ?thesis + by (simp add:univ_poly_carrier[symmetric] polynomial_def) + next + case False + have set_x: "set x \ h ` carrier R" + using that h_img unfolding univ_poly_carrier[symmetric] + unfolding polynomial_def by auto + have "lead_coeff x \ \\<^bsub>S\<^esub>" "lead_coeff x \ carrier S" + using that False unfolding univ_poly_carrier[symmetric] + unfolding polynomial_def by auto + hence "the_inv_into (carrier R) h (lead_coeff x) \ + the_inv_into (carrier R) h \\<^bsub>S\<^esub>" + using inj_on_the_inv_into[OF h_inj] inj_onD + using ds.zero_closed h_img by metis + hence "the_inv_into (carrier R) h (lead_coeff x) \ \\<^bsub>R\<^esub>" + unfolding h.hom_zero[symmetric] + unfolding the_inv_into_f_f[OF h_inj dr.zero_closed] by simp + hence "lead_coeff (?hinv x) \ \\<^bsub>R\<^esub>" + using False by (simp add:hd_map) + moreover have "the_inv_into (carrier R) h ` set x \ carrier R" + using the_inv_into_into[OF h_inj] set_x + by (intro image_subsetI) auto + hence "set (?hinv x) \ carrier R" by simp + ultimately show ?thesis + by (simp add:univ_poly_carrier[symmetric] polynomial_def) + qed + moreover have "?hinv (map h x) = x" if "x \ carrier ?R" for x + proof - + have set_x: "set x \ carrier R" + using that unfolding univ_poly_carrier[symmetric] + unfolding polynomial_def by auto + have "?hinv (map h x) = + map (\y. the_inv_into (carrier R) h (h y)) x" + by simp + also have "... = map id x" + using set_x by (intro map_cong) + (auto simp add:the_inv_into_f_f[OF h_inj]) + also have "... = x" by simp + finally show ?thesis by simp + qed + moreover have "map h (?hinv x) = x" + if "x \ carrier ?S" for x + proof - + have set_x: "set x \ h ` carrier R" + using that h_img unfolding univ_poly_carrier[symmetric] + unfolding polynomial_def by auto + have "map h (?hinv x) = + map (\y. h (the_inv_into (carrier R) h y)) x" + by simp + also have "... = map id x" + using set_x by (intro map_cong) + (auto simp add:f_the_inv_into_f[OF h_inj]) + also have "... = x" by simp + finally show ?thesis by simp + qed + ultimately show "bij_betw (map h) (carrier ?R) (carrier ?S)" + by (intro bij_betwI[where g="?hinv"], auto) +qed + +lemma carrier_hom: + assumes "f \ carrier (poly_ring R)" + assumes "h \ ring_iso R S" "domain R" "domain S" + shows "map h f \ carrier (poly_ring S)" +proof - + note poly_iso = lift_iso_to_poly_ring[OF assms(2,3,4)] + show ?thesis + using ring_iso_memE(1)[OF poly_iso assms(1)] by simp +qed + +lemma carrier_hom': + assumes "f \ carrier (poly_ring R)" + assumes "h \ ring_hom R S" + assumes "domain R" "domain S" + assumes "inj_on h (carrier R)" + shows "map h f \ carrier (poly_ring S)" +proof - + let ?S = "S \ carrier := h ` carrier R \" + + interpret dr: domain "R" using assms(3) by blast + interpret ds: domain "S" using assms(4) by blast + interpret h1: ring_hom_ring R S h + using assms(2) ring_hom_ringI2 dr.ring_axioms + using ds.ring_axioms by blast + have subr: "subring (h ` carrier R) S" + using h1.img_is_subring[OF dr.carrier_is_subring] by blast + interpret h: ring_hom_ring "((h ` carrier R)[X]\<^bsub>S\<^esub>)" "poly_ring S" "id" + using ds.embed_hom[OF subr] by simp + + let ?S = "S \ carrier := h ` carrier R \" + have "h \ ring_hom R ?S" + using assms(2) unfolding ring_hom_def by simp + moreover have "bij_betw h (carrier R) (carrier ?S)" + using assms(5) bij_betw_def by auto + ultimately have h_iso: "h \ ring_iso R ?S" + unfolding ring_iso_def by simp + + have dom_S: "domain ?S" + using ds.subring_is_domain[OF subr] by simp + + note poly_iso = lift_iso_to_poly_ring[OF h_iso assms(3) dom_S] + have "map h f \ carrier (poly_ring ?S)" + using ring_iso_memE(1)[OF poly_iso assms(1)] by simp + also have "carrier (poly_ring ?S) = + carrier (univ_poly S (h ` carrier R))" + using ds.univ_poly_consistent[OF subr] by simp + also have "... \ carrier (poly_ring S)" + using h.hom_closed by auto + finally show ?thesis by simp +qed + +text \The following lemmas transfer properties like divisibility, irreducibility etc. between +ring isomorphisms.\ + +lemma divides_hom: + assumes "h \ ring_iso R S" + assumes "domain R" "domain S" + assumes "x \ carrier R" "y \ carrier R" + shows "x divides\<^bsub>R\<^esub> y \ (h x) divides\<^bsub>S\<^esub> (h y)" (is "?lhs \ ?rhs") +proof - + interpret dr: domain "R" using assms(2) by blast + interpret ds: domain "S" using assms(3) by blast + interpret pdr: domain "poly_ring R" + using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp + interpret pds: domain "poly_ring S" + using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp + interpret h: ring_hom_ring "R" "S" h + using dr.is_ring ds.is_ring assms(1) + by (intro ring_hom_ringI2, simp_all add:ring_iso_def) + + have h_inj_on: "inj_on h (carrier R)" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + have h_img: "h ` (carrier R) = carrier S" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + + have "?lhs \ (\c \ carrier R. y = x \\<^bsub>R\<^esub> c)" + unfolding factor_def by simp + also have "... \ (\c \ carrier R. h y = h x \\<^bsub>S\<^esub> h c)" + using assms(4,5) inj_onD[OF h_inj_on] + by (intro bex_cong, auto simp flip:h.hom_mult) + also have "... \ (\c \ carrier S. h y = h x \\<^bsub>S\<^esub> c)" + unfolding h_img[symmetric] by simp + also have "... \ ?rhs" + unfolding factor_def by simp + finally show ?thesis by simp +qed + +lemma properfactor_hom: + assumes "h \ ring_iso R S" + assumes "domain R" "domain S" + assumes "x \ carrier R" "b \ carrier R" + shows "properfactor R b x \ properfactor S (h b) (h x)" + using divides_hom[OF assms(1,2,3)] assms(4,5) + unfolding properfactor_def by simp + +lemma Units_hom: + assumes "h \ ring_iso R S" + assumes "domain R" "domain S" + assumes "x \ carrier R" + shows "x \ Units R \ h x \ Units S" +proof - + + interpret dr: domain "R" using assms(2) by blast + interpret ds: domain "S" using assms(3) by blast + interpret pdr: domain "poly_ring R" + using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp + interpret pds: domain "poly_ring S" + using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp + interpret h: ring_hom_ring "R" "S" h + using dr.is_ring ds.is_ring assms(1) + by (intro ring_hom_ringI2, simp_all add:ring_iso_def) + + have h_img: "h ` (carrier R) = carrier S" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + + have h_inj_on: "inj_on h (carrier R)" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + + hence h_one_iff: "h x = \\<^bsub>S\<^esub> \ x = \\<^bsub>R\<^esub>" if "x \ carrier R" for x + using h.hom_one that by (metis dr.one_closed inj_onD) + + have "x \ Units R \ + (\y\carrier R. x \\<^bsub>R\<^esub> y = \\<^bsub>R\<^esub> \ y \\<^bsub>R\<^esub> x = \\<^bsub>R\<^esub>)" + using assms unfolding Units_def by auto + also have "... \ + (\y\carrier R. h x \\<^bsub>S\<^esub> h y = h \\<^bsub>R\<^esub> \ h y \\<^bsub>S\<^esub> h x = h \\<^bsub>R\<^esub>)" + using h_one_iff assms by (intro bex_cong, simp_all flip:h.hom_mult) + also have "... \ + (\y\carrier S. h x \\<^bsub>S\<^esub> y = h \\<^bsub>R\<^esub> \ y \\<^bsub>S\<^esub> h x = \\<^bsub>S\<^esub>)" + unfolding h_img[symmetric] by simp + also have "... \ h x \ Units S" + using assms h.hom_closed unfolding Units_def by auto + finally show ?thesis by simp +qed + +lemma irreducible_hom: + assumes "h \ ring_iso R S" + assumes "domain R" "domain S" + assumes "x \ carrier R" + shows "irreducible R x = irreducible S (h x)" +proof - + have h_img: "h ` (carrier R) = carrier S" + using assms(1) unfolding ring_iso_def bij_betw_def by auto + + have "irreducible R x \ (x \ Units R \ + (\b\carrier R. properfactor R b x \ b \ Units R))" + unfolding Divisibility.irreducible_def by simp + also have "... \ (x \ Units R \ + (\b\carrier R. properfactor S (h b) (h x) \ b \ Units R))" + using properfactor_hom[OF assms(1,2,3)] assms(4) by simp + also have "... \ (h x \ Units S \ + (\b\carrier R. properfactor S (h b) (h x) \ h b \ Units S))" + using assms(4) Units_hom[OF assms(1,2,3)] by simp + also have "...\ (h x \ Units S \ + (\b\h ` carrier R. properfactor S b (h x) \ b \ Units S))" + by simp + also have "... \ irreducible S (h x)" + unfolding h_img Divisibility.irreducible_def by simp + finally show ?thesis by simp +qed + +lemma pirreducible_hom: + assumes "h \ ring_iso R S" + assumes "domain R" "domain S" + assumes "f \ carrier (poly_ring R)" + shows "pirreducible\<^bsub>R\<^esub> (carrier R) f = + pirreducible\<^bsub>S\<^esub> (carrier S) (map h f)" + (is "?lhs = ?rhs") +proof - + note lift_iso = lift_iso_to_poly_ring[OF assms(1,2,3)] + interpret dr: domain "R" using assms(2) by blast + interpret ds: domain "S" using assms(3) by blast + interpret pdr: domain "poly_ring R" + using dr.univ_poly_is_domain[OF dr.carrier_is_subring] by simp + interpret pds: domain "poly_ring S" + using ds.univ_poly_is_domain[OF ds.carrier_is_subring] by simp + + have mh_inj_on: "inj_on (map h) (carrier (poly_ring R))" + using lift_iso unfolding ring_iso_def bij_betw_def by auto + moreover have "map h \\<^bsub>poly_ring R\<^esub> = \\<^bsub>poly_ring S\<^esub>" + by (simp add:univ_poly_zero) + ultimately have mh_zero_iff: + "map h f = \\<^bsub>poly_ring S\<^esub> \ f = \\<^bsub>poly_ring R\<^esub>" + using assms(4) by (metis pdr.zero_closed inj_onD) + + have "?lhs \ (f \ \\<^bsub>poly_ring R\<^esub> \ irreducible (poly_ring R) f)" + unfolding ring_irreducible_def by simp + also have "... \ + (f \ \\<^bsub>poly_ring R\<^esub> \ irreducible (poly_ring S) (map h f))" + using irreducible_hom[OF lift_iso] pdr.domain_axioms + using assms(4) pds.domain_axioms by simp + also have "... \ + (map h f \ \\<^bsub>poly_ring S\<^esub> \ irreducible (poly_ring S) (map h f))" + using mh_zero_iff by simp + also have "... \ ?rhs" + unfolding ring_irreducible_def by simp + finally show ?thesis by simp +qed + + +lemma ring_hom_cong: + assumes "\x. x \ carrier R \ f' x = f x" + assumes "ring R" + assumes "f \ ring_hom R S" + shows "f' \ ring_hom R S" +proof - + interpret ring "R" using assms(2) by simp + show ?thesis + using assms(1) ring_hom_memE[OF assms(3)] + by (intro ring_hom_memI, auto) +qed + +text \The natural homomorphism between factor rings, where one ideal is a subset of the other.\ + +lemma (in ring) quot_quot_hom: + assumes "ideal I R" + assumes "ideal J R" + assumes "I \ J" + shows "(\x. (J <+>\<^bsub>R\<^esub> x)) \ ring_hom (R Quot I) (R Quot J)" +proof (rule ring_hom_memI) + interpret ji: ideal J R + using assms(2) by simp + interpret ii: ideal I R + using assms(1) by simp + + have a:"J <+>\<^bsub>R\<^esub> I = J" + using assms(3) unfolding set_add_def set_mult_def by auto + + show "J <+>\<^bsub>R\<^esub> x \ carrier (R Quot J)" + if "x \ carrier (R Quot I)" for x + proof - + have " \y\carrier R. x = I +> y" + using that unfolding FactRing_def A_RCOSETS_def' by simp + then obtain y where y_def: "y \ carrier R" "x = I +> y" + by auto + have "J <+>\<^bsub>R\<^esub> (I +> y) = (J <+>\<^bsub>R\<^esub> I) +> y" + using y_def(1) by (subst a_setmult_rcos_assoc) auto + also have "... = J +> y" using a by simp + finally have "J <+>\<^bsub>R\<^esub> (I +> y) = J +> y" by simp + thus ?thesis + using y_def unfolding FactRing_def A_RCOSETS_def' by auto + qed + + show "J <+>\<^bsub>R\<^esub> x \\<^bsub>R Quot I\<^esub> y = + (J <+>\<^bsub>R\<^esub> x) \\<^bsub>R Quot J\<^esub> (J <+>\<^bsub>R\<^esub> y)" + if "x \ carrier (R Quot I)" "y \ carrier (R Quot I)" + for x y + proof - + have "\x1\carrier R. x = I +> x1" "\y1\carrier R. y = I +> y1" + using that unfolding FactRing_def A_RCOSETS_def' by auto + then obtain x1 y1 + where x1_def: "x1 \ carrier R" "x = I +> x1" + and y1_def: "y1 \ carrier R" "y = I +> y1" + by auto + have "J <+>\<^bsub>R\<^esub> x \\<^bsub>R Quot I\<^esub> y = J <+>\<^bsub>R\<^esub> (I +> x1 \ y1)" + using x1_def y1_def + by (simp add: FactRing_def ii.rcoset_mult_add) + also have "... = (J <+>\<^bsub>R\<^esub> I) +> x1 \ y1" + using x1_def(1) y1_def(1) + by (subst a_setmult_rcos_assoc) auto + also have "... = J +> x1 \ y1" + using a by simp + also have "... = [mod J:] (J +> x1) \ (J +> y1)" + using x1_def(1) y1_def(1) by (subst ji.rcoset_mult_add, auto) + also have "... = + [mod J:] ((J <+>\<^bsub>R\<^esub> I) +> x1) \ ((J <+>\<^bsub>R\<^esub> I) +> y1)" + using a by simp + also have "... = + [mod J:] (J <+>\<^bsub>R\<^esub> (I +> x1)) \ (J <+>\<^bsub>R\<^esub> (I +> y1))" + using x1_def(1) y1_def(1) + by (subst (1 2) a_setmult_rcos_assoc) auto + also have "... = (J <+>\<^bsub>R\<^esub> x) \\<^bsub>R Quot J\<^esub> (J <+>\<^bsub>R\<^esub> y)" + using x1_def y1_def by (simp add: FactRing_def) + finally show ?thesis by simp + qed + + show "J <+>\<^bsub>R\<^esub> x \\<^bsub>R Quot I\<^esub> y = + (J <+>\<^bsub>R\<^esub> x) \\<^bsub>R Quot J\<^esub> (J <+>\<^bsub>R\<^esub> y)" + if "x \ carrier (R Quot I)" "y \ carrier (R Quot I)" + for x y + proof - + have "\x1\carrier R. x = I +> x1" "\y1\carrier R. y = I +> y1" + using that unfolding FactRing_def A_RCOSETS_def' by auto + then obtain x1 y1 + where x1_def: "x1 \ carrier R" "x = I +> x1" + and y1_def: "y1 \ carrier R" "y = I +> y1" + by auto + have "J <+>\<^bsub>R\<^esub> x \\<^bsub>R Quot I\<^esub> y = + J <+>\<^bsub>R\<^esub> ((I +> x1) <+>\<^bsub>R\<^esub> (I +> y1))" + using x1_def y1_def by (simp add:FactRing_def) + also have "... = J <+>\<^bsub>R\<^esub> (I +> (x1 \ y1))" + using x1_def y1_def ii.a_rcos_sum by simp + also have "... = (J <+>\<^bsub>R\<^esub> I) +> (x1 \ y1)" + using x1_def y1_def by (subst a_setmult_rcos_assoc) auto + also have "... = J +> (x1 \ y1)" + using a by simp + also have "... = + ((J <+>\<^bsub>R\<^esub> I) +> x1) <+>\<^bsub>R\<^esub> ((J <+>\<^bsub>R\<^esub> I) +> y1)" + using x1_def y1_def ji.a_rcos_sum a by simp + also have "... = + J <+>\<^bsub>R\<^esub> (I +> x1) <+>\<^bsub>R\<^esub> (J <+>\<^bsub>R\<^esub> (I +> y1))" + using x1_def y1_def by (subst (1 2) a_setmult_rcos_assoc) auto + also have "... = (J <+>\<^bsub>R\<^esub> x) \\<^bsub>R Quot J\<^esub> (J <+>\<^bsub>R\<^esub> y)" + using x1_def y1_def by (simp add:FactRing_def) + finally show ?thesis by simp + qed + + have "J <+>\<^bsub>R\<^esub> \\<^bsub>R Quot I\<^esub> = J <+>\<^bsub>R\<^esub> (I +> \)" + unfolding FactRing_def by simp + also have "... = (J <+>\<^bsub>R\<^esub> I) +> \" + by (subst a_setmult_rcos_assoc) auto + also have "... = J +> \" using a by simp + also have "... = \\<^bsub>R Quot J\<^esub>" + unfolding FactRing_def by simp + finally show "J <+>\<^bsub>R\<^esub> \\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot J\<^esub>" + by simp +qed + +lemma (in ring) quot_carr: + assumes "ideal I R" + assumes "y \ carrier (R Quot I)" + shows "y \ carrier R" +proof - + interpret ideal I R using assms(1) by simp + have "y \ a_rcosets I" + using assms(2) unfolding FactRing_def by simp + then obtain v where y_def: "y = I +> v" "v \ carrier R" + unfolding A_RCOSETS_def' by auto + have "I +> v \ carrier R" + using y_def(2) a_r_coset_subset_G a_subset by presburger + thus "y \ carrier R" unfolding y_def by simp +qed + +lemma (in ring) set_add_zero: + assumes "A \ carrier R" + shows "{\} <+>\<^bsub>R\<^esub> A = A" +proof - + have "{\} <+>\<^bsub>R\<^esub> A = (\x\A. {\ \ x})" + using assms unfolding set_add_def set_mult_def by simp + also have "... = (\x\A. {x})" + using assms by (intro arg_cong[where f="Union"] image_cong, auto) + also have "... = A" by simp + finally show ?thesis by simp +qed + +text \Adapted from the proof of @{thm [source] domain.polynomial_rupture}\ + +lemma (in domain) rupture_surj_as_eval: + assumes "subring K R" + assumes "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "rupture_surj K p q = + ring.eval (Rupt K p) (map ((rupture_surj K p) \ poly_of_const) q) + (rupture_surj K p X)" +proof - + let ?surj = "rupture_surj K p" + + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF assms(1)] . + interpret h: ring_hom_ring "K[X]" "Rupt K p" ?surj + using rupture_surj_hom(2)[OF assms(1,2)] . + + have "(h.S.eval) (map (?surj \ poly_of_const) q) (?surj X) = + ?surj ((UP.eval) (map poly_of_const q) X)" + using h.eval_hom[OF UP.carrier_is_subring var_closed(1)[OF assms(1)] + map_norm_in_poly_ring_carrier[OF assms(1,3)]] by simp + also have " ... = ?surj q" + unfolding sym[OF eval_rewrite[OF assms(1,3)]] .. + finally show ?thesis by simp +qed + +subsection \Divisibility\ + +lemma (in field) f_comm_group_1: + assumes "x \ carrier R" "y \ carrier R" + assumes "x \ \" "y \ \" + assumes "x \ y = \" + shows "False" + using integral assms by auto + +lemma (in field) f_comm_group_2: + assumes "x \ carrier R" + assumes "x \ \" + shows " \y\carrier R - {\}. y \ x = \" +proof - + have x_unit: "x \ Units R" using field_Units assms by simp + thus ?thesis unfolding Units_def by auto +qed + +sublocale field < mult_of: comm_group "mult_of R" + rewrites "mult (mult_of R) = mult R" + and "one (mult_of R) = one R" + using f_comm_group_1 f_comm_group_2 + by (auto intro!:comm_groupI m_assoc m_comm) + +lemma (in domain) div_neg: + assumes "a \ carrier R" "b \ carrier R" + assumes "a divides b" + shows "a divides (\ b)" +proof - + obtain r1 where r1_def: "r1 \ carrier R" "a \ r1 = b" + using assms by (auto simp:factor_def) + + have "a \ (\ r1) = \ (a \ r1)" + using assms(1) r1_def(1) by algebra + also have "... = \ b" + using r1_def(2) by simp + finally have "\b = a \ (\ r1)" by simp + moreover have "\r1 \ carrier R" + using r1_def(1) by simp + ultimately show ?thesis + by (auto simp:factor_def) +qed + +lemma (in domain) div_sum: + assumes "a \ carrier R" "b \ carrier R" "c \ carrier R" + assumes "a divides b" + assumes "a divides c" + shows "a divides (b \ c)" +proof - + obtain r1 where r1_def: "r1 \ carrier R" "a \ r1 = b" + using assms by (auto simp:factor_def) + + obtain r2 where r2_def: "r2 \ carrier R" "a \ r2 = c" + using assms by (auto simp:factor_def) + + have "a \ (r1 \ r2) = (a \ r1) \ (a \ r2)" + using assms(1) r1_def(1) r2_def(1) by algebra + also have "... = b \ c" + using r1_def(2) r2_def(2) by simp + finally have "b \ c = a \ (r1 \ r2)" by simp + moreover have "r1 \ r2 \ carrier R" + using r1_def(1) r2_def(1) by simp + ultimately show ?thesis + by (auto simp:factor_def) +qed + +lemma (in domain) div_sum_iff: + assumes "a \ carrier R" "b \ carrier R" "c \ carrier R" + assumes "a divides b" + shows "a divides (b \ c) \ a divides c" +proof + assume "a divides (b \ c)" + moreover have "a divides (\ b)" + using div_neg assms(1,2,4) by simp + ultimately have "a divides ((b \ c) \ (\ b))" + using div_sum assms by simp + also have "... = c" using assms(1,2,3) by algebra + finally show "a divides c" by simp +next + assume "a divides c" + thus "a divides (b \ c)" + using assms by (intro div_sum) auto +qed + +end diff --git a/thys/Finite_Fields/Formal_Polynomial_Derivatives.thy b/thys/Finite_Fields/Formal_Polynomial_Derivatives.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Formal_Polynomial_Derivatives.thy @@ -0,0 +1,414 @@ +section \Formal Derivatives\label{sec:pderiv}\ + +theory Formal_Polynomial_Derivatives + imports "HOL-Algebra.Polynomial_Divisibility" "Ring_Characteristic" +begin + +definition pderiv ("pderiv\") where + "pderiv\<^bsub>R\<^esub> x = ring.normalize R ( + map (\i. int_embed R i \\<^bsub>R\<^esub> ring.coeff R x i) (rev [1.. carrier (K[X])" + shows "coeff f i \ K" +proof - + have "coeff f i \ set f \ {\}" + using coeff_img(3) by auto + also have "... \ K \ {\}" + using assms(2) univ_poly_carrier polynomial_incl by blast + also have "... \ K" + using subringE[OF assms(1)] by simp + finally show ?thesis by simp +qed + +lemma pderiv_carr: + assumes "subring K R" + assumes "f \ carrier (K[X])" + shows "pderiv f \ carrier (K[X])" +proof - + have "int_embed R i \ coeff f i \ K" for i + using coeff_range[OF assms] int_embed_range[OF assms(1)] + using subringE[OF assms(1)] by simp + hence "polynomial K (pderiv f)" + unfolding pderiv_def by (intro normalize_gives_polynomial, auto) + thus ?thesis + using univ_poly_carrier by auto +qed + +lemma pderiv_coeff: + assumes "subring K R" + assumes "f \ carrier (K[X])" + shows "coeff (pderiv f) k = int_embed R (Suc k) \ coeff f (Suc k)" + (is "?lhs = ?rhs") +proof (cases "k + 1 < length f") + case True + define j where "j = length f - k - 2" + define d where + "d = map (\i. int_embed R i \ coeff f i) (rev [1.. coeff f (length f - j - 1)" + using b e unfolding d_def by simp + also have "... = ?rhs" + using f by simp + finally show ?thesis by simp +next + case False + hence "Suc k \ length f" + by simp + hence a:"coeff f (Suc k) = \" + using coeff_img by blast + have b:"coeff (pderiv f) k = \" + unfolding pderiv_def normalize_coeff[symmetric] using False + by (intro coeff_length, simp) + show ?thesis + using int_embed_range[OF carrier_is_subring] by (simp add:a b) +qed + +lemma pderiv_const: + assumes "degree x = 0" + shows "pderiv x = \\<^bsub>K[X]\<^esub>" +proof (cases "length x = 0") + case True + then show ?thesis by (simp add:univ_poly_zero pderiv_def) +next + case False + hence "length x = 1" using assms by linarith + then obtain y where "x = [y]" by (cases x, auto) + then show ?thesis by (simp add:univ_poly_zero pderiv_def) +qed + +lemma pderiv_var: + shows "pderiv X = \\<^bsub>K[X]\<^esub>" + unfolding var_def pderiv_def + by (simp add:univ_poly_one int_embed_def) + +lemma pderiv_zero: + shows "pderiv \\<^bsub>K[X]\<^esub> = \\<^bsub>K[X]\<^esub>" + unfolding pderiv_def univ_poly_zero by simp + +lemma pderiv_add: + assumes "subring K R" + assumes [simp]: "f \ carrier (K[X])" "g \ carrier (K[X])" + shows "pderiv (f \\<^bsub>K[X]\<^esub> g) = pderiv f \\<^bsub>K[X]\<^esub> pderiv g" + (is "?lhs = ?rhs") +proof - + interpret p: ring "(K[X])" + using univ_poly_is_ring[OF assms(1)] by simp + + let ?n = "(\i. int_embed R i)" + + have a[simp]:"?n k \ carrier R" for k + using int_embed_range[OF carrier_is_subring] by auto + have b[simp]:"coeff f k \ carrier R" if "f \ carrier (K[X])" for k f + using coeff_range[OF assms(1)] that + using subringE(1)[OF assms(1)] by auto + + have "coeff ?lhs i = coeff ?rhs i" for i + proof - + have "coeff ?lhs i = ?n (i+1) \ coeff (f \\<^bsub>K [X]\<^esub> g) (i+1)" + by (simp add: pderiv_coeff[OF assms(1)]) + also have "... = ?n (i+1) \ (coeff f (i+1) \ coeff g (i+1))" + by (subst coeff_add[OF assms], simp) + also have "... = ?n (i+1) \ coeff f (i+1) + \ int_embed R (i+1) \ coeff g (i+1)" + by (subst r_distr, simp_all) + also have "... = coeff (pderiv f) i \ coeff (pderiv g) i" + by (simp add: pderiv_coeff[OF assms(1)]) + also have "... = coeff (pderiv f \\<^bsub>K [X]\<^esub> pderiv g) i" + using pderiv_carr[OF assms(1)] + by (subst coeff_add[OF assms(1)], auto) + finally show ?thesis by simp + qed + hence "coeff ?lhs = coeff ?rhs" by auto + thus "?lhs = ?rhs" + using pderiv_carr[OF assms(1)] + by (subst coeff_iff_polynomial_cond[where K="K"]) + (simp_all add:univ_poly_carrier)+ +qed + +lemma pderiv_inv: + assumes "subring K R" + assumes [simp]: "f \ carrier (K[X])" + shows "pderiv (\\<^bsub>K[X]\<^esub> f) = \\<^bsub>K[X]\<^esub> pderiv f" (is "?lhs = ?rhs") +proof - + interpret p: cring "(K[X])" + using univ_poly_is_cring[OF assms(1)] by simp + + have "pderiv (\\<^bsub>K[X]\<^esub> f) = pderiv (\\<^bsub>K[X]\<^esub> f) \\<^bsub>K[X]\<^esub> \\<^bsub>K[X]\<^esub>" + using pderiv_carr[OF assms(1)] + by (subst p.r_zero, simp_all) + also have "... = pderiv (\\<^bsub>K[X]\<^esub> f) \\<^bsub>K[X]\<^esub> (pderiv f \\<^bsub>K[X]\<^esub> pderiv f)" + using pderiv_carr[OF assms(1)] by simp + also have "... = pderiv (\\<^bsub>K[X]\<^esub> f) \\<^bsub>K[X]\<^esub> pderiv f \\<^bsub>K[X]\<^esub> pderiv f" + using pderiv_carr[OF assms(1)] + unfolding a_minus_def by (simp add:p.a_assoc) + also have "... = pderiv (\\<^bsub>K[X]\<^esub> f \\<^bsub>K[X]\<^esub> f) \\<^bsub>K[X]\<^esub> pderiv f" + by (subst pderiv_add[OF assms(1)], simp_all) + also have "... = pderiv \\<^bsub>K[X]\<^esub> \\<^bsub>K[X]\<^esub> pderiv f" + by (subst p.l_neg, simp_all) + also have "... = \\<^bsub>K[X]\<^esub> \\<^bsub>K[X]\<^esub> pderiv f" + by (subst pderiv_zero, simp) + also have "... = \\<^bsub>K[X]\<^esub> pderiv f" + unfolding a_minus_def using pderiv_carr[OF assms(1)] + by (subst p.l_zero, simp_all) + finally show "pderiv (\\<^bsub>K[X]\<^esub> f) = \\<^bsub>K[X]\<^esub> pderiv f" + by simp +qed + + +lemma coeff_mult: + assumes "subring K R" + assumes "f \ carrier (K[X])" "g \ carrier (K[X])" + shows "coeff (f \\<^bsub>K[X]\<^esub> g) i = + (\ k \ {..i}. (coeff f) k \ (coeff g) (i - k))" +proof - + have a:"set f \ carrier R" + using assms(1,2) univ_poly_carrier + using subringE(1)[OF assms(1)] polynomial_incl by blast + have b:"set g \ carrier R" + using assms(1,3) univ_poly_carrier + using subringE(1)[OF assms(1)] polynomial_incl by blast + show ?thesis + unfolding univ_poly_mult poly_mult_coeff[OF a b] by simp +qed + +lemma pderiv_mult: + assumes "subring K R" + assumes [simp]: "f \ carrier (K[X])" "g \ carrier (K[X])" + shows "pderiv (f \\<^bsub>K[X]\<^esub> g) = + pderiv f \\<^bsub>K[X]\<^esub> g \\<^bsub>K[X]\<^esub> f \\<^bsub>K[X]\<^esub> pderiv g" + (is "?lhs = ?rhs") +proof - + interpret p: cring "(K[X])" + using univ_poly_is_cring[OF assms(1)] by simp + + let ?n = "(\i. int_embed R i)" + + have a[simp]:"?n k \ carrier R" for k + using int_embed_range[OF carrier_is_subring] by auto + have b[simp]:"coeff f k \ carrier R" if "f \ carrier (K[X])" for k f + using coeff_range[OF assms(1)] + using subringE(1)[OF assms(1)] that by auto + + have "coeff ?lhs i = coeff ?rhs i" for i + proof - + have "coeff ?lhs i = ?n (i+1) \ coeff (f \\<^bsub>K [X]\<^esub> g) (i+1)" + using assms(2,3) by (simp add: pderiv_coeff[OF assms(1)]) + also have "... = ?n (i+1) \ + (\k \ {..i+1}. coeff f k \ (coeff g (i + 1 - k)))" + by (subst coeff_mult[OF assms], simp) + also have "... = + (\k \ {..i+1}. ?n (i+1) \ (coeff f k \ coeff g (i + 1 - k)))" + by (intro finsum_rdistr, simp_all add:Pi_def) + also have "... = + (\k \ {..i+1}. ?n k \ (coeff f k \ coeff g (i + 1 - k)) \ + ?n (i+1-k) \ (coeff f k \ coeff g (i + 1 - k)))" + using int_embed_add[symmetric] of_nat_diff + by (intro finsum_cong') + (simp_all add:l_distr[symmetric] of_nat_diff) + also have "... = + (\k \ {..i+1}. ?n k \ coeff f k \ coeff g (i + 1 - k) \ + coeff f k \ (?n (i+1-k) \ coeff g (i + 1 - k)))" + using Pi_def a b m_assoc m_comm + by (intro finsum_cong' arg_cong2[where f="(\)"], simp_all) + also have "... = + (\k \ {..i+1}. ?n k \ coeff f k \ coeff g (i+1-k)) \ + (\k \ {..i+1}. coeff f k \ (?n (i+1-k) \ coeff g (i+1-k)))" + by (subst finsum_addf[symmetric], simp_all add:Pi_def) + also have "... = + (\k\insert 0 {1..i+1}. ?n k \ coeff f k \ coeff g (i+1-k)) \ + (\k\insert (i+1) {..i}. coeff f k \ (?n (i+1-k) \ coeff g (i+1-k)))" + using subringE(1)[OF assms(1)] + by (intro arg_cong2[where f="(\)"] finsum_cong') + (auto simp:set_eq_iff) + also have "... = + (\k \ {1..i+1}. ?n k \ coeff f k \ coeff g (i+1-k)) \ + (\k \ {..i}. coeff f k \ (?n (i+1-k) \ coeff g (i+1-k)))" + by (subst (1 2) finsum_insert, auto simp add:int_embed_zero) + also have "... = + (\k \ Suc ` {..i}. ?n k \ coeff f (k) \ coeff g (i+1-k)) \ + (\k \ {..i}. coeff f k \ (?n (i+1-k) \ coeff g (i+1-k)))" + by (intro arg_cong2[where f="(\)"] finsum_cong') + (simp_all add:Pi_def atMost_atLeast0) + also have "... = + (\k \ {..i}. ?n (k+1) \ coeff f (k+1) \ coeff g (i-k)) \ + (\k \ {..i}. coeff f k \ (?n (i+1-k) \ coeff g (i+1-k)))" + by (subst finsum_reindex, auto) + also have "... = + (\k \ {..i}. coeff (pderiv f) k \ coeff g (i-k)) \ + (\k \ {..i}. coeff f k \ coeff (pderiv g) (i-k))" + using Suc_diff_le + by (subst (1 2) pderiv_coeff[OF assms(1)]) + (auto intro!: finsum_cong') + also have "... = + coeff (pderiv f \\<^bsub>K[X]\<^esub> g) i \ coeff (f \\<^bsub>K[X]\<^esub> pderiv g) i" + using pderiv_carr[OF assms(1)] + by (subst (1 2) coeff_mult[OF assms(1)], auto) + also have "... = coeff ?rhs i" + using pderiv_carr[OF assms(1)] + by (subst coeff_add[OF assms(1)], auto) + finally show ?thesis by simp + qed + + hence "coeff ?lhs = coeff ?rhs" by auto + thus "?lhs = ?rhs" + using pderiv_carr[OF assms(1)] + by (subst coeff_iff_polynomial_cond[where K="K"]) + (simp_all add:univ_poly_carrier) +qed + +lemma pderiv_pow: + assumes "n > (0 :: nat)" + assumes "subring K R" + assumes [simp]: "f \ carrier (K[X])" + shows "pderiv (f [^]\<^bsub>K[X]\<^esub> n) = + int_embed (K[X]) n \\<^bsub>K[X]\<^esub> f [^]\<^bsub>K[X]\<^esub> (n-1) \\<^bsub>K[X]\<^esub> pderiv f" + (is "?lhs = ?rhs") +proof - + interpret p: cring "(K[X])" + using univ_poly_is_cring[OF assms(2)] by simp + + let ?n = "\n. int_embed (K[X]) n" + + have [simp]: "?n i \ carrier (K[X])" for i + using p.int_embed_range[OF p.carrier_is_subring] by simp + + obtain m where n_def: "n = Suc m" using assms(1) lessE by blast + have "pderiv (f [^]\<^bsub>K[X]\<^esub> (m+1)) = + ?n (m+1) \\<^bsub>K[X]\<^esub> f [^]\<^bsub>K[X]\<^esub> m \\<^bsub>K[X]\<^esub> pderiv f" + proof (induction m) + case 0 + then show ?case + using pderiv_carr[OF assms(2)] assms(3) + using p.int_embed_one by simp + next + case (Suc m) + have "pderiv (f [^]\<^bsub>K [X]\<^esub> (Suc m + 1)) = + pderiv (f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K[X]\<^esub> f) " + by simp + also have "... = + pderiv (f [^]\<^bsub>K [X]\<^esub> (m+1)) \\<^bsub>K[X]\<^esub> f \\<^bsub>K[X]\<^esub> + f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K[X]\<^esub> pderiv f" + using assms(3) by (subst pderiv_mult[OF assms(2)], auto) + also have "... = + (?n (m+1) \\<^bsub>K [X]\<^esub> f [^]\<^bsub>K [X]\<^esub> m \\<^bsub>K [X]\<^esub> pderiv f) \\<^bsub>K[X]\<^esub> f + \\<^bsub>K[X]\<^esub> f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K[X]\<^esub> pderiv f" + by (subst Suc(1), simp) + also have + "... = ?n (m+1) \\<^bsub>K[X]\<^esub> (f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K[X]\<^esub> pderiv f) + \\<^bsub>K[X]\<^esub> \\<^bsub>K [X]\<^esub> \\<^bsub>K[X]\<^esub> (f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K[X]\<^esub> pderiv f)" + using assms(3) pderiv_carr[OF assms(2)] + apply (intro arg_cong2[where f="(\\<^bsub>K[X]\<^esub>)"]) + apply (simp add:p.m_assoc) + apply (simp add:p.m_comm) + by simp + also have + "... = (?n (m+1) \\<^bsub>K[X]\<^esub> \\<^bsub>K [X]\<^esub>) \\<^bsub>K [X]\<^esub> + (f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K [X]\<^esub> pderiv f)" + using assms(3) pderiv_carr[OF assms(2)] + by (subst p.l_distr[symmetric], simp_all) + also have "... = + (\\<^bsub>K [X]\<^esub> \\<^bsub>K[X]\<^esub> ?n (m+1)) \\<^bsub>K [X]\<^esub> + (f [^]\<^bsub>K [X]\<^esub> (m+1) \\<^bsub>K [X]\<^esub> pderiv f)" + using assms(3) pderiv_carr[OF assms(2)] + by (subst p.a_comm, simp_all) + also have "... = ?n (1+ Suc m) + \\<^bsub>K [X]\<^esub> f [^]\<^bsub>K [X]\<^esub> (Suc m) \\<^bsub>K [X]\<^esub> pderiv f" + using assms(3) pderiv_carr[OF assms(2)] of_nat_add + apply (subst (2) of_nat_add, subst p.int_embed_add) + by (simp add:p.m_assoc p.int_embed_one) + finally show ?case by simp + qed + thus "?thesis" using n_def by auto +qed + +lemma pderiv_var_pow: + assumes "n > (0::nat)" + assumes "subring K R" + shows "pderiv (X [^]\<^bsub>K[X]\<^esub> n) = + int_embed (K[X]) n \\<^bsub>K[X]\<^esub> X [^]\<^bsub>K[X]\<^esub> (n-1)" +proof - + interpret p: cring "(K[X])" + using univ_poly_is_cring[OF assms(2)] by simp + + have [simp]: "int_embed (K[X]) i \ carrier (K[X])" for i + using p.int_embed_range[OF p.carrier_is_subring] by simp + + show ?thesis + using var_closed[OF assms(2)] + using pderiv_var[where K="K"] pderiv_carr[OF assms(2)] + by (subst pderiv_pow[OF assms(1,2)], simp_all) +qed + +lemma int_embed_consistent_with_poly_of_const: + assumes "subring K R" + shows "int_embed (K[X]) m = poly_of_const (int_embed R m)" +proof - + define K' where "K' = R \ carrier := K \" + interpret p: cring "(K[X])" + using univ_poly_is_cring[OF assms] by simp + interpret d: domain "K'" + unfolding K'_def + using assms(1) subdomainI' subdomain_is_domain by simp + interpret h: ring_hom_ring "K'" "K[X]" "poly_of_const" + unfolding K'_def + using canonical_embedding_ring_hom[OF assms(1)] by simp + + define n where "n=nat (abs m)" + + have a1: "int_embed (K[X]) (int n) = poly_of_const (int_embed K' n)" + proof (induction n) + case 0 + then show ?case by (simp add:d.int_embed_zero p.int_embed_zero) + next + case (Suc n) + then show ?case + using d.int_embed_closed d.int_embed_add d.int_embed_one + by (simp add:p.int_embed_add p.int_embed_one) + qed + also have "... = poly_of_const (int_embed R n)" + unfolding K'_def using int_embed_consistent[OF assms] by simp + finally have a: + "int_embed (K[X]) (int n) = poly_of_const (int_embed R (int n))" + by simp + + have "int_embed (K[X]) (-(int n)) = + poly_of_const (int_embed K' (- (int n)))" + using d.int_embed_closed a1 by (simp add: p.int_embed_inv d.int_embed_inv) + also have "... = poly_of_const (int_embed R (- (int n)))" + unfolding K'_def using int_embed_consistent[OF assms] by simp + finally have b: + "int_embed (K[X]) (-int n) = poly_of_const (int_embed R (-int n))" + by simp + + show ?thesis + using a b n_def by (cases "m \ 0", simp, simp) +qed + +end + +end diff --git a/thys/Finite_Fields/Monic_Polynomial_Factorization.thy b/thys/Finite_Fields/Monic_Polynomial_Factorization.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Monic_Polynomial_Factorization.thy @@ -0,0 +1,658 @@ +section \Factorization into Monic Polynomials\label{sec:monic}\ + +theory Monic_Polynomial_Factorization +imports + Finite_Fields_Factorization_Ext + Formal_Polynomial_Derivatives +begin + +hide_const Factorial_Ring.multiplicity +hide_const Factorial_Ring.irreducible + +lemma (in domain) finprod_mult_of: + assumes "finite A" + assumes "\x. x \ A \ f x \ carrier (mult_of R)" + shows "finprod R f A = finprod (mult_of R) f A" + using assms by (induction A rule:finite_induct, auto) + +lemma (in ring) finite_poly: + assumes "subring K R" + assumes "finite K" + shows + "finite {f. f \ carrier (K[X]) \ degree f = n}" (is "finite ?A") + "finite {f. f \ carrier (K[X]) \ degree f \ n}" (is "finite ?B") +proof - + have "finite {f. set f \ K \ length f \ n + 1}" (is "finite ?C") + using assms(2) finite_lists_length_le by auto + moreover have "?B \ ?C" + by (intro subsetI) + (auto simp:univ_poly_carrier[symmetric] polynomial_def) + ultimately show a: "finite ?B" + using finite_subset by auto + moreover have "?A \ ?B" + by (intro subsetI, simp) + ultimately show "finite ?A" + using finite_subset by auto +qed + +definition pmult :: "_ \ 'a list \ 'a list \ nat" ("pmult\") + where "pmult\<^bsub>R\<^esub> d p = multiplicity (mult_of (poly_ring R)) d p" + +definition monic_poly :: "_ \ 'a list \ bool" + where "monic_poly R f = + (f \ [] \ lead_coeff f = \\<^bsub>R\<^esub> \ f \ carrier (poly_ring R))" + +definition monic_irreducible_poly where + "monic_irreducible_poly R f = + (monic_poly R f \ pirreducible\<^bsub>R\<^esub> (carrier R) f)" + +abbreviation "m_i_p \ monic_irreducible_poly" + +locale polynomial_ring = field + + fixes K + assumes polynomial_ring_assms: "subfield K R" +begin + +lemma K_subring: "subring K R" + using polynomial_ring_assms subfieldE(1) by auto + +abbreviation P where "P \ K[X]" + +text \This locale is used to specialize the following lemmas for a fixed coefficient ring. +It can be introduced in a context as an intepretation to be able to use the following specialized +lemmas. Because it is not (and should not) introduced as a sublocale it has no lasting effect +for the field locale itself.\ + +lemmas + poly_mult_lead_coeff = poly_mult_lead_coeff[OF K_subring] +and degree_add_distinct = degree_add_distinct[OF K_subring] +and coeff_add = coeff_add[OF K_subring] +and var_closed = var_closed[OF K_subring] +and degree_prod = degree_prod[OF _ K_subring] +and degree_pow = degree_pow[OF K_subring] +and pirreducible_degree = pirreducible_degree[OF polynomial_ring_assms] +and degree_one_imp_pirreducible = + degree_one_imp_pirreducible[OF polynomial_ring_assms] +and var_pow_closed = var_pow_closed[OF K_subring] +and var_pow_carr = var_pow_carr[OF K_subring] +and univ_poly_a_inv_degree = univ_poly_a_inv_degree[OF K_subring] +and var_pow_degree = var_pow_degree[OF K_subring] +and pdivides_zero = pdivides_zero[OF K_subring] +and pdivides_imp_degree_le = pdivides_imp_degree_le[OF K_subring] +and var_carr = var_carr[OF K_subring] +and rupture_eq_0_iff = rupture_eq_0_iff[OF polynomial_ring_assms] +and rupture_is_field_iff_pirreducible = + rupture_is_field_iff_pirreducible[OF polynomial_ring_assms] +and rupture_surj_hom = rupture_surj_hom[OF K_subring] +and canonical_embedding_ring_hom = + canonical_embedding_ring_hom[OF K_subring] +and rupture_surj_norm_is_hom = rupture_surj_norm_is_hom[OF K_subring] +and rupture_surj_as_eval = rupture_surj_as_eval[OF K_subring] +and eval_cring_hom = eval_cring_hom[OF K_subring] +and coeff_range = coeff_range[OF K_subring] +and finite_poly = finite_poly[OF K_subring] +and int_embed_consistent_with_poly_of_const = + int_embed_consistent_with_poly_of_const[OF K_subring] +and pderiv_var_pow = pderiv_var_pow[OF _ K_subring] +and pderiv_add = pderiv_add[OF K_subring] +and pderiv_inv = pderiv_inv[OF K_subring] +and pderiv_mult = pderiv_mult[OF K_subring] +and pderiv_pow = pderiv_pow[OF _ K_subring] +and pderiv_carr = pderiv_carr[OF K_subring] + +sublocale p:principal_domain "poly_ring R" + by (simp add: carrier_is_subfield univ_poly_is_principal) + +end + +context field +begin + +interpretation polynomial_ring "R" "carrier R" + using carrier_is_subfield field_axioms + by (simp add:polynomial_ring_def polynomial_ring_axioms_def) + +lemma pdivides_mult_r: + assumes "a \ carrier (mult_of P)" + assumes "b \ carrier (mult_of P)" + assumes "c \ carrier (mult_of P)" + shows "a \\<^bsub>P\<^esub> c pdivides b \\<^bsub>P\<^esub> c \ a pdivides b" + (is "?lhs \ ?rhs") +proof - + have a:"b \\<^bsub>P\<^esub> c \ carrier P - {\\<^bsub>P\<^esub>}" + using assms p.mult_of.m_closed by force + have b:"a \\<^bsub>P\<^esub> c \ carrier P" + using assms by simp + have c:"b \ carrier P - {\\<^bsub>P\<^esub>}" + using assms p.mult_of.m_closed by force + have d:"a \ carrier P" using assms by simp + have "?lhs \ a \\<^bsub>P\<^esub> c divides\<^bsub>mult_of P\<^esub> b \\<^bsub>P\<^esub> c" + unfolding pdivides_def using p.divides_imp_divides_mult a b + by (meson divides_mult_imp_divides) + also have "... \ a divides\<^bsub>mult_of P\<^esub> b" + using p.mult_of.divides_mult_r[OF assms] by simp + also have "... \ ?rhs" + unfolding pdivides_def using p.divides_imp_divides_mult c d + by (meson divides_mult_imp_divides) + finally show ?thesis by simp +qed + +lemma lead_coeff_carr: + assumes "x \ carrier (mult_of P)" + shows "lead_coeff x \ carrier R - {\}" +proof (cases x) + case Nil + then show ?thesis using assms by (simp add:univ_poly_zero) +next + case (Cons a list) + hence a: "polynomial (carrier R) (a # list)" + using assms univ_poly_carrier by auto + have "lead_coeff x = a" + using Cons by simp + also have "a \ carrier R - {\}" + using lead_coeff_not_zero a by simp + finally show ?thesis by simp +qed + +lemma lead_coeff_poly_of_const: + assumes "r \ \" + shows "lead_coeff (poly_of_const r) = r" + using assms + by (simp add:poly_of_const_def) + +lemma lead_coeff_mult: + assumes "f \ carrier (mult_of P)" + assumes "g \ carrier (mult_of P)" + shows "lead_coeff (f \\<^bsub>P\<^esub> g) = lead_coeff f \ lead_coeff g" + unfolding univ_poly_mult using assms + using univ_poly_carrier[where R="R" and K="carrier R"] + by (subst poly_mult_lead_coeff) (simp_all add:univ_poly_zero) + +lemma monic_poly_carr: + assumes "monic_poly R f" + shows "f \ carrier P" + using assms unfolding monic_poly_def by simp + +lemma monic_poly_add_distinct: + assumes "monic_poly R f" + assumes "g \ carrier P" "degree g < degree f" + shows "monic_poly R (f \\<^bsub>P\<^esub> g)" +proof (cases "g \ \\<^bsub>P\<^esub>") + case True + define n where "n = degree f" + have "f \ carrier P - {\\<^bsub>P\<^esub>}" + using assms(1) univ_poly_zero + unfolding monic_poly_def by auto + hence "degree (f \\<^bsub>P\<^esub> g) = max (degree f) (degree g)" + using assms(2,3) True + by (subst degree_add_distinct, simp_all) + also have "... = degree f" + using assms(3) by simp + finally have b: "degree (f \\<^bsub>P\<^esub> g) = n" + unfolding n_def by simp + moreover have "n > 0" + using assms(3) unfolding n_def by simp + ultimately have "degree (f \\<^bsub>P\<^esub> g) \ degree ([])" + by simp + hence a:"f \\<^bsub>P\<^esub> g \ []" by auto + + have "degree [] = 0" by simp + also have "... < degree f" + using assms(3) by simp + finally have "degree f \ degree []" by simp + hence c: "f \ []" by auto + + have d: "length g \ n" + using assms(3) unfolding n_def by simp + + have "lead_coeff (f \\<^bsub>P\<^esub> g) = coeff (f \\<^bsub>P\<^esub> g) n" + using a b by (cases "f \\<^bsub>P\<^esub> g", auto) + also have "... = coeff f n \ coeff g n" + using monic_poly_carr assms + by (subst coeff_add, auto) + also have "... = lead_coeff f \ coeff g n" + using c unfolding n_def by (cases "f", auto) + also have "... = \ \ \" + using assms(1) unfolding monic_poly_def + unfolding subst coeff_length[OF d] by simp + also have "... = \" + by simp + finally have "lead_coeff (f \\<^bsub>P\<^esub> g) = \" by simp + moreover have "f \\<^bsub>P\<^esub> g \ carrier P" + using monic_poly_carr assms by simp + ultimately show ?thesis + using a unfolding monic_poly_def by auto +next + case False + then show ?thesis using assms monic_poly_carr by simp +qed + +lemma monic_poly_one: "monic_poly R \\<^bsub>P\<^esub>" +proof - + have "\\<^bsub>P\<^esub> \ carrier P" + by simp + thus ?thesis + by (simp add:univ_poly_one monic_poly_def) +qed + +lemma monic_poly_var: "monic_poly R X" +proof - + have "X \ carrier P" + using var_closed by simp + thus ?thesis + by (simp add:var_def monic_poly_def) +qed + +lemma monic_poly_carr_2: + assumes "monic_poly R f" + shows "f \ carrier (mult_of P)" + using assms unfolding monic_poly_def + by (simp add:univ_poly_zero) + +lemma monic_poly_mult: + assumes "monic_poly R f" + assumes "monic_poly R g" + shows "monic_poly R (f \\<^bsub>P\<^esub> g)" +proof - + have "lead_coeff (f \\<^bsub>P\<^esub> g) = lead_coeff f \\<^bsub>R\<^esub> lead_coeff g" + using assms monic_poly_carr_2 + by (subst lead_coeff_mult) auto + also have "... = \" + using assms unfolding monic_poly_def by simp + finally have "lead_coeff (f \\<^bsub>P\<^esub> g) = \\<^bsub>R\<^esub>" by simp + moreover have "(f \\<^bsub>P\<^esub> g) \ carrier (mult_of P)" + using monic_poly_carr_2 assms by blast + ultimately show ?thesis + by (simp add:monic_poly_def univ_poly_zero) +qed + +lemma monic_poly_pow: + assumes "monic_poly R f" + shows "monic_poly R (f [^]\<^bsub>P\<^esub> (n::nat))" + using assms monic_poly_one monic_poly_mult + by (induction n, auto) + +lemma monic_poly_prod: + assumes "finite A" + assumes "\x. x \ A \ monic_poly R (f x)" + shows "monic_poly R (finprod P f A)" + using assms +proof (induction A rule:finite_induct) + case empty + then show ?case by (simp add:monic_poly_one) +next + case (insert x F) + have a: "f \ F \ carrier P" + using insert monic_poly_carr by simp + have b: "f x \ carrier P" + using insert monic_poly_carr by simp + have "monic_poly R (f x \\<^bsub>P\<^esub> finprod P f F)" + using insert by (intro monic_poly_mult) auto + thus ?case + using insert a b by (subst p.finprod_insert, auto) +qed + +lemma monic_poly_not_assoc: + assumes "monic_poly R f" + assumes "monic_poly R g" + assumes "f \\<^bsub>(mult_of P)\<^esub> g" + shows "f = g" +proof - + obtain u where u_def: "f = g \\<^bsub>P\<^esub> u" "u \ Units (mult_of P)" + using p.mult_of.associatedD2 assms monic_poly_carr_2 + by blast + + hence "u \ Units P" by simp + then obtain v where v_def: "u = [v]" "v \ \\<^bsub>R\<^esub>" "v \ carrier R" + using univ_poly_carrier_units by auto + + have "\ = lead_coeff f" + using assms(1) by (simp add:monic_poly_def) + also have "... = lead_coeff (g \\<^bsub>P\<^esub> u)" + by (simp add:u_def) + also have "... = lead_coeff g \ lead_coeff u" + using assms(2) monic_poly_carr_2 v_def u_def(2) + by (subst lead_coeff_mult, auto simp add:univ_poly_zero) + also have "... = lead_coeff g \ v" + using v_def by simp + also have "... = v" + using assms(2) v_def(3) by (simp add:monic_poly_def) + finally have "\ = v" by simp + hence "u = \\<^bsub>P\<^esub>" + using v_def by (simp add:univ_poly_one) + thus "f = g" + using u_def assms monic_poly_carr by simp +qed + +lemma monic_poly_span: + assumes "x \ carrier (mult_of P)" "irreducible (mult_of P) x" + shows "\y. monic_irreducible_poly R y \ x \\<^bsub>(mult_of P)\<^esub> y" +proof - + define z where "z = poly_of_const (inv (lead_coeff x))" + define y where "y = x \\<^bsub>P\<^esub> z" + + have x_carr: "x \ carrier (mult_of P)" using assms by simp + + hence lx_ne_0: "lead_coeff x \ \" + and lx_unit: "lead_coeff x \ Units R" + using lead_coeff_carr[OF x_carr] by (auto simp add:field_Units) + have lx_inv_ne_0: "inv (lead_coeff x) \ \" + using lx_unit + by (metis Units_closed Units_r_inv r_null zero_not_one) + have lx_inv_carr: "inv (lead_coeff x) \ carrier R" + using lx_unit by simp + + have "z \ carrier P" + using lx_inv_carr poly_of_const_over_carrier + unfolding z_def by auto + moreover have "z \ \\<^bsub>P\<^esub>" + using lx_inv_ne_0 + by (simp add:z_def poly_of_const_def univ_poly_zero) + ultimately have z_carr: "z \ carrier (mult_of P)" by simp + have z_unit: "z \ Units (mult_of P)" + using lx_inv_ne_0 lx_inv_carr + by (simp add:univ_poly_carrier_units z_def poly_of_const_def) + have y_exp: "y = x \\<^bsub>(mult_of P)\<^esub> z" + by (simp add:y_def) + hence y_carr: "y \ carrier (mult_of P)" + using x_carr z_carr p.mult_of.m_closed by simp + + have "irreducible (mult_of P) y" + unfolding y_def using assms z_unit z_carr + by (intro p.mult_of.irreducible_prod_rI, auto) + moreover have "lead_coeff y = \\<^bsub>R\<^esub>" + unfolding y_def using x_carr z_carr lx_inv_ne_0 lx_unit + by (simp add: lead_coeff_mult z_def lead_coeff_poly_of_const) + hence "monic_poly R y" + using y_carr unfolding monic_poly_def + by (simp add:univ_poly_zero) + ultimately have "monic_irreducible_poly R y" + using p.irreducible_mult_imp_irreducible y_carr + by (simp add:monic_irreducible_poly_def ring_irreducible_def) + moreover have "y \\<^bsub>(mult_of P)\<^esub> x" + by (intro p.mult_of.associatedI2[OF z_unit] y_def x_carr) + hence "x \\<^bsub>(mult_of P)\<^esub> y" + using x_carr y_carr by (simp add:p.mult_of.associated_sym) + ultimately show ?thesis by auto +qed + +lemma monic_polys_are_canonical_irreducibles: + "canonical_irreducibles (mult_of P) {d. monic_irreducible_poly R d}" + (is "canonical_irreducibles (mult_of P) ?S") +proof - + have sp_1: + "?S \ {x \ carrier (mult_of P). irreducible (mult_of P) x}" + unfolding monic_irreducible_poly_def ring_irreducible_def + using monic_poly_carr + by (intro subsetI, simp add: p.irreducible_imp_irreducible_mult) + have sp_2: "x = y" + if "x \ ?S" "y \ ?S" "x \\<^bsub>(mult_of P)\<^esub> y" for x y + using that monic_poly_not_assoc + by (simp add:monic_irreducible_poly_def) + + have sp_3: "\y \ ?S. x \\<^bsub>(mult_of P)\<^esub> y" + if "x \ carrier (mult_of P)" "irreducible (mult_of P) x" for x + using that monic_poly_span by simp + + thus ?thesis using sp_1 sp_2 sp_3 + unfolding canonical_irreducibles_def by simp +qed + +lemma + assumes "monic_poly R a" + shows factor_monic_poly: + "a = (\\<^bsub>P\<^esub>d\{d. monic_irreducible_poly R d \ pmult d a > 0}. + d [^]\<^bsub>P\<^esub> pmult d a)" (is "?lhs = ?rhs") + and factor_monic_poly_fin: + "finite {d. monic_irreducible_poly R d \ pmult d a > 0}" +proof - + let ?S = "{d. monic_irreducible_poly R d}" + let ?T = "{d. monic_irreducible_poly R d \ pmult d a > 0}" + let ?mip = "monic_irreducible_poly R" + + have sp_4: "a \ carrier (mult_of P)" + using assms monic_poly_carr_2 + unfolding monic_irreducible_poly_def by simp + + have b_1: "x \ carrier (mult_of P)" if "?mip x" for x + using that monic_poly_carr_2 + unfolding monic_irreducible_poly_def by simp + have b_2:"irreducible (mult_of P) x" if "?mip x" for x + using that + unfolding monic_irreducible_poly_def ring_irreducible_def + by (simp add: monic_poly_carr p.irreducible_imp_irreducible_mult) + have b_3:"x \ carrier P" if "?mip x" for x + using that monic_poly_carr + unfolding monic_irreducible_poly_def + by simp + + have a_carr: "a \ carrier P - {\\<^bsub>P\<^esub>}" + using sp_4 by simp + + have "?T = {d. ?mip d \ multiplicity (mult_of P) d a > 0}" + by (simp add:pmult_def) + also have "... = {d \ ?S. multiplicity (mult_of P) d a > 0}" + using p.mult_of.multiplicity_gt_0_iff[OF b_1 b_2 sp_4] + by (intro order_antisym subsetI, auto) + finally have t:"?T = {d \ ?S. multiplicity (mult_of P) d a > 0}" + by simp + + show fin_T: "finite ?T" + unfolding t + using p.mult_of.split_factors(1) + [OF monic_polys_are_canonical_irreducibles] + using sp_4 by auto + + have a:"x [^]\<^bsub>P\<^esub> (n::nat) \ carrier (mult_of P)" if "?mip x" for x n + proof - + have "monic_poly R (x [^]\<^bsub>P\<^esub> n)" + using that monic_poly_pow + unfolding monic_irreducible_poly_def by auto + thus ?thesis + using monic_poly_carr_2 by simp + qed + + have "?lhs \\<^bsub>(mult_of P)\<^esub> + finprod (mult_of P) + (\d. d [^]\<^bsub>(mult_of P)\<^esub> (multiplicity (mult_of P) d a)) ?T" + unfolding t + by (intro p.mult_of.split_factors(2) + [OF monic_polys_are_canonical_irreducibles sp_4]) + also have "... = + finprod (mult_of P) (\d. d [^]\<^bsub>P\<^esub> (multiplicity (mult_of P) d a)) ?T" + by (simp add:nat_pow_mult_of) + also have "... = ?rhs" + using fin_T a + by (subst p.finprod_mult_of, simp_all add:pmult_def) + finally have "?lhs \\<^bsub>(mult_of P)\<^esub> ?rhs" by simp + moreover have "monic_poly R ?rhs" + using fin_T + by (intro monic_poly_prod monic_poly_pow) + (auto simp:monic_irreducible_poly_def) + ultimately show "?lhs = ?rhs" + using monic_poly_not_assoc assms monic_irreducible_poly_def + by blast +qed + +lemma degree_monic_poly': + assumes "monic_poly R f" + shows + "sum' (\d. pmult d f * degree d) {d. monic_irreducible_poly R d} = + degree f" +proof - + let ?mip = "monic_irreducible_poly R" + + have b: "d \ carrier P - {\\<^bsub>P\<^esub>}" if "?mip d" for d + using that monic_poly_carr_2 + unfolding monic_irreducible_poly_def by simp + have a: "d [^]\<^bsub>P\<^esub> n \ carrier P - {\\<^bsub>P\<^esub>}" if "?mip d" for d and n :: "nat" + using b that monic_poly_pow + unfolding monic_irreducible_poly_def + by (simp add: p.pow_non_zero) + + have "degree f = + degree (\\<^bsub>P\<^esub>d\{d. ?mip d \ pmult d f > 0}. d [^]\<^bsub>P\<^esub> pmult d f)" + using factor_monic_poly[OF assms(1)] by simp + also have "... = + (\i\{d. ?mip d \ 0 < pmult d f}. degree (i [^]\<^bsub>P\<^esub> pmult i f))" + using a assms(1) + by (subst degree_prod[OF factor_monic_poly_fin]) + (simp_all add:Pi_def) + also have "... = + (\i\{d. ?mip d \ 0 < pmult d f}. degree i * pmult i f)" + using b degree_pow by (intro sum.cong, auto) + also have "... = + (\d\{d. ?mip d \ 0 < pmult d f}. pmult d f * degree d)" + by (simp add:mult.commute) + also have "... = + sum' (\d. pmult d f * degree d) {d. ?mip d \ 0 < pmult d f}" + using sum.eq_sum factor_monic_poly_fin[OF assms(1)] by simp + also have "... = sum' (\d. pmult d f * degree d) {d. ?mip d}" + by (intro sum.mono_neutral_cong_left' subsetI, auto) + finally show ?thesis by simp +qed + +lemma monic_poly_min_degree: + assumes "monic_irreducible_poly R f" + shows "degree f \ 1" + using assms unfolding monic_irreducible_poly_def monic_poly_def + by (intro pirreducible_degree) auto + +lemma degree_one_monic_poly: + "monic_irreducible_poly R f \ degree f = 1 \ + (\x \ carrier R. f = [\, \x])" +proof + assume "monic_irreducible_poly R f \ degree f = 1" + hence a:"monic_poly R f" "length f = 2" + unfolding monic_irreducible_poly_def by auto + then obtain u v where f_def: "f = [u,v]" + by (cases f, simp, cases "tl f", auto) + + have "u = \" using a unfolding monic_poly_def f_def by simp + moreover have "v \ carrier R" + using a unfolding monic_poly_def univ_poly_carrier[symmetric] + unfolding polynomial_def f_def by simp + ultimately have "f = [\, \(\v)]" "(\v) \ carrier R" + using a_inv_closed f_def by auto + thus "(\x \ carrier R. f = [\\<^bsub>R\<^esub>, \\<^bsub>R\<^esub>x])" by auto +next + assume "(\x \ carrier R. f = [\, \x])" + then obtain x where f_def: "f = [\,\x]" "x \ carrier R" by auto + have a:"degree f = 1" using f_def(2) unfolding f_def by simp + have b:"f \ carrier P" + using f_def(2) unfolding univ_poly_carrier[symmetric] + unfolding f_def polynomial_def by simp + have c: "pirreducible (carrier R) f" + by (intro degree_one_imp_pirreducible a b) + have d: "lead_coeff f = \" unfolding f_def by simp + show "monic_irreducible_poly R f \ degree f = 1" + using a b c d + unfolding monic_irreducible_poly_def monic_poly_def + by auto +qed + +lemma multiplicity_ge_iff: + assumes "monic_irreducible_poly R d" + assumes "f \ carrier P - {\\<^bsub>P\<^esub>}" + shows "pmult d f \ k \ d [^]\<^bsub>P\<^esub> k pdivides f" +proof - + have a:"f \ carrier (mult_of P)" + using assms(2) by simp + have b: "d \ carrier (mult_of P)" + using assms(1) monic_poly_carr_2 + unfolding monic_irreducible_poly_def by simp + have c: "irreducible (mult_of P) d" + using assms(1) monic_poly_carr_2 + using p.irreducible_imp_irreducible_mult + unfolding monic_irreducible_poly_def + unfolding ring_irreducible_def monic_poly_def + by simp + have d: "d [^]\<^bsub>P\<^esub> k \ carrier P" using b by simp + + have "pmult d f \ k \ d [^]\<^bsub>(mult_of P)\<^esub> k divides\<^bsub>(mult_of P)\<^esub> f" + unfolding pmult_def + by (intro p.mult_of.multiplicity_ge_iff a b c) + also have "... \ d [^]\<^bsub>P\<^esub> k pdivides\<^bsub>R\<^esub> f" + using p.divides_imp_divides_mult[OF d assms(2)] + using divides_mult_imp_divides + unfolding pdivides_def nat_pow_mult_of + by auto + finally show ?thesis by simp +qed + +lemma multiplicity_ge_1_iff_pdivides: + assumes "monic_irreducible_poly R d" "f \ carrier P - {\\<^bsub>P\<^esub>}" + shows "pmult d f \ 1 \ d pdivides f" +proof - + have "d \ carrier P" + using assms(1) monic_poly_carr + unfolding monic_irreducible_poly_def + by simp + thus ?thesis + using multiplicity_ge_iff[OF assms, where k="1"] + by simp +qed + +lemma divides_monic_poly: + assumes "monic_poly R f" "monic_poly R g" + assumes "\d. monic_irreducible_poly R d + \ pmult d f \ pmult d g" + shows "f pdivides g" +proof - + have a:"f \ carrier (mult_of P)" "g \ carrier (mult_of P)" + using monic_poly_carr_2 assms(1,2) by auto + + have "f divides\<^bsub>(mult_of P)\<^esub> g" + using assms(3) unfolding pmult_def + by (intro p.mult_of.divides_iff_mult_mono + [OF a monic_polys_are_canonical_irreducibles]) simp + thus ?thesis + unfolding pdivides_def using divides_mult_imp_divides by simp +qed + +end + +lemma monic_poly_hom: + assumes "monic_poly R f" + assumes "h \ ring_iso R S" "domain R" "domain S" + shows "monic_poly S (map h f)" +proof - + have c: "h \ ring_hom R S" + using assms(2) ring_iso_def by auto + have e: "f \ carrier (poly_ring R)" + using assms(1) unfolding monic_poly_def by simp + + have a:"f \ []" + using assms(1) unfolding monic_poly_def by simp + hence "map h f \ []" by simp + moreover have "lead_coeff f = \\<^bsub>R\<^esub>" + using assms(1) unfolding monic_poly_def by simp + hence "lead_coeff (map h f) = \\<^bsub>S\<^esub>" + using ring_hom_one[OF c] by (simp add: hd_map[OF a]) + ultimately show ?thesis + using carrier_hom[OF e assms(2-4)] + unfolding monic_poly_def by simp +qed + +lemma monic_irreducible_poly_hom: + assumes "monic_irreducible_poly R f" + assumes "h \ ring_iso R S" "domain R" "domain S" + shows "monic_irreducible_poly S (map h f)" +proof - + have a: + "pirreducible\<^bsub>R\<^esub> (carrier R) f" + "f \ carrier (poly_ring R)" + "monic_poly R f" + using assms(1) + unfolding monic_poly_def monic_irreducible_poly_def + by auto + + have "pirreducible\<^bsub>S\<^esub> (carrier S) (map h f)" + using a pirreducible_hom assms by auto + moreover have "monic_poly S (map h f)" + using a monic_poly_hom[OF _ assms(2,3,4)] by simp + ultimately show ?thesis + unfolding monic_irreducible_poly_def by simp +qed + +end diff --git a/thys/Finite_Fields/ROOT b/thys/Finite_Fields/ROOT new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/ROOT @@ -0,0 +1,18 @@ +chapter AFP + +session Finite_Fields (AFP) = "HOL-Algebra" + + options [timeout = 600] + sessions + Dirichlet_Series + theories + Card_Irreducible_Polynomials + Card_Irreducible_Polynomials_Aux + Finite_Fields_Factorization_Ext + Finite_Fields_Isomorphic + Finite_Fields_Preliminary_Results + Formal_Polynomial_Derivatives + Monic_Polynomial_Factorization + Ring_Characteristic + document_files + "root.tex" + "root.bib" diff --git a/thys/Finite_Fields/Ring_Characteristic.thy b/thys/Finite_Fields/Ring_Characteristic.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Ring_Characteristic.thy @@ -0,0 +1,1017 @@ +section \Characteristic of Rings\label{sec:ring_char}\ + +theory Ring_Characteristic + imports + "Finite_Fields_Factorization_Ext" + "HOL-Algebra.IntRing" + "HOL-Algebra.Embedded_Algebras" +begin + +locale finite_field = field + + assumes finite_carrier: "finite (carrier R)" +begin + +lemma finite_field_min_order: + "order R > 1" +proof (rule ccontr) + assume a:"\(1 < order R)" + have "{\\<^bsub>R\<^esub>,\\<^bsub>R\<^esub>} \ carrier R" by auto + hence "card {\\<^bsub>R\<^esub>,\\<^bsub>R\<^esub>} \ card (carrier R)" + using card_mono finite_carrier by blast + also have "... \ 1" using a by (simp add:order_def) + finally have "card {\\<^bsub>R\<^esub>,\\<^bsub>R\<^esub>} \ 1" by blast + thus "False" by simp +qed + +lemma (in finite_field) order_pow_eq_self: + assumes "x \ carrier R" + shows "x [^] (order R) = x" +proof (cases "x = \") + case True + have "order R > 0" + using assms(1) order_gt_0_iff_finite finite_carrier by simp + then obtain n where n_def:"order R = Suc n" + using lessE by blast + have "x [^] (order R) = \" + unfolding n_def using True by (subst nat_pow_Suc, simp) + thus ?thesis using True by simp +next + case False + have x_carr:"x \ carrier (mult_of R)" + using False assms by simp + + have carr_non_empty: "card (carrier R) > 0" + using order_gt_0_iff_finite finite_carrier + unfolding order_def by simp + have "x [^] (order R) = x [^]\<^bsub>mult_of R\<^esub> (order R)" + by (simp add:nat_pow_mult_of) + also have "... = x [^]\<^bsub>mult_of R\<^esub> (order (mult_of R)+1)" + using carr_non_empty unfolding order_def + by (intro arg_cong[where f="\t. x [^]\<^bsub>mult_of R\<^esub> t"]) (simp) + also have "... = x" + using x_carr + by (simp add:mult_of.pow_order_eq_1) + finally show "x [^] (order R) = x" + by simp +qed + +lemma (in finite_field) order_pow_eq_self': + assumes "x \ carrier R" + shows "x [^] (order R ^ d) = x" +proof (induction d) + case 0 + then show ?case using assms by simp +next + case (Suc d) + have "x [^] order R ^ (Suc d) = x [^] (order R ^ d * order R)" + by (simp add:mult.commute) + also have "... = (x [^] (order R ^ d)) [^] order R" + using assms by (simp add: nat_pow_pow) + also have "... = (x [^] (order R ^ d))" + using order_pow_eq_self assms by simp + also have "... = x" + using Suc by simp + finally show ?case by simp +qed + +end + +lemma finite_fieldI: + assumes "field R" + assumes "finite (carrier R)" + shows "finite_field R" + using assms + unfolding finite_field_def finite_field_axioms_def + by auto + +lemma (in domain) finite_domain_units: + assumes "finite (carrier R)" + shows "Units R = carrier R - {\}" (is "?lhs = ?rhs") +proof + have "Units R \ carrier R" by (simp add:Units_def) + moreover have "\ \ Units R" + by (meson zero_is_prime(1) primeE) + ultimately show "Units R \ carrier R - {\}" by blast +next + have "x \ Units R" if a: "x \ carrier R - {\}" for x + proof - + have x_carr: "x \ carrier R" using a by blast + define f where "f = (\y. y \\<^bsub>R\<^esub> x)" + have "inj_on f (carrier R)" unfolding f_def + by (rule inj_onI, metis DiffD1 DiffD2 a m_rcancel insertI1) + hence "card (carrier R) = card (f ` carrier R)" + by (metis card_image) + moreover have "f ` carrier R \ carrier R" unfolding f_def + by (rule image_subsetI, simp add: ring.ring_simprules x_carr) + ultimately have "f ` carrier R = carrier R" + using card_subset_eq assms by metis + moreover have "\\<^bsub>R\<^esub> \ carrier R" by simp + ultimately have "\y \ carrier R. f y = \\<^bsub>R\<^esub>" + by (metis image_iff) + then obtain y + where y_carrier: "y \ carrier R" + and y_left_inv: "y \\<^bsub>R\<^esub> x = \\<^bsub>R\<^esub>" + using f_def by blast + hence y_right_inv: "x \\<^bsub>R\<^esub> y = \\<^bsub>R\<^esub>" + by (metis DiffD1 a cring_simprules(14)) + show "x \ Units R" + using y_carrier y_left_inv y_right_inv + by (metis DiffD1 a divides_one factor_def) + qed + thus "?rhs \ ?lhs" by auto +qed + +text \The following theorem can be found in Lidl and Niederreiter~\cite[Theorem 1.31]{lidl1986}.\ + +theorem finite_domains_are_fields: + assumes "domain R" + assumes "finite (carrier R)" + shows "finite_field R" +proof - + interpret domain R using assms by auto + have "Units R = carrier R - {\\<^bsub>R\<^esub>}" + using finite_domain_units[OF assms(2)] by simp + then have "field R" + by (simp add: assms(1) field.intro field_axioms.intro) + thus ?thesis + using assms(2) finite_fieldI by auto +qed + +definition zfact_iso :: "nat \ nat \ int set" where + "zfact_iso p k = Idl\<^bsub>\\<^esub> {int p} +>\<^bsub>\\<^esub> (int k)" + +context + fixes n :: nat + assumes n_gt_0: "n > 0" +begin + +private abbreviation I where "I \ Idl\<^bsub>\\<^esub> {int n}" + +private lemma ideal_I: "ideal I \" + by (simp add: int.genideal_ideal) + +lemma int_cosetI: + assumes "u mod (int n) = v mod (int n)" + shows "Idl\<^bsub>\\<^esub> {int n} +>\<^bsub>\\<^esub> u = Idl\<^bsub>\\<^esub> {int n} +>\<^bsub>\\<^esub> v" +proof - + have "u - v \ I" + by (metis Idl_subset_eq_dvd assms int_Idl_subset_ideal mod_eq_dvd_iff) + thus ?thesis + using ideal_I int.quotient_eq_iff_same_a_r_cos by simp +qed + +lemma zfact_iso_inj: + "inj_on (zfact_iso n) {.. {.. {..\<^bsub>\\<^esub> (int x) = I +>\<^bsub>\\<^esub> (int y)" + by (simp add:zfact_iso_def) + hence "int x - int y \ I" + by (subst int.quotient_eq_iff_same_a_r_cos[OF ideal_I], auto) + hence "int x mod int n = int y mod int n" + by (meson Idl_subset_eq_dvd int_Idl_subset_ideal mod_eq_dvd_iff) + thus "x = y" + using a by simp +qed + +lemma zfact_iso_ran: + "zfact_iso n ` {.. carrier (ZFact (int n))" + unfolding zfact_iso_def ZFact_def FactRing_simps + using int.a_rcosetsI by auto + moreover have "x \ zfact_iso n ` {.. carrier (ZFact (int n))" for x + proof - + obtain y where y_def: "x = I +>\<^bsub>\\<^esub> y" + using a unfolding ZFact_def FactRing_simps by auto + obtain z where z_def: "(int z) mod (int n) = y mod (int n)" "z < n" + by (metis Euclidean_Division.pos_mod_sign mod_mod_trivial + nonneg_int_cases of_nat_0_less_iff of_nat_mod n_gt_0 + unique_euclidean_semiring_numeral_class.pos_mod_bound) + have "x = I +>\<^bsub>\\<^esub> y" + by (simp add:y_def) + also have "... = I +>\<^bsub>\\<^esub> (int z)" + by (intro int_cosetI, simp add:z_def) + also have "... = zfact_iso n z" + by (simp add:zfact_iso_def) + finally have "x = zfact_iso n z" + by simp + thus "x \ zfact_iso n ` {.. 0" using assms(1) prime_gt_0_nat by simp + have "Factorial_Ring.prime (int p)" + using assms by simp + moreover have "finite (carrier (ZFact (int p)))" + using fin_zfact[OF p_gt_0] by simp + ultimately show ?thesis + by (intro finite_domains_are_fields ZFact_prime_is_domain, auto) +qed + +definition int_embed :: "_ \ int \ _" where + "int_embed R k = add_pow R k \\<^bsub>R\<^esub>" + +lemma (in ring) add_pow_consistent: + fixes i :: "int" + assumes "subring K R" + assumes "k \ K" + shows "add_pow R i k = add_pow (R \ carrier := K \) i k" + (is "?lhs = ?rhs") +proof - + have a:"subgroup K (add_monoid R)" + using assms(1) subring.axioms by auto + have "add_pow R i k = k [^]\<^bsub>add_monoid R\carrier := K\\<^esub> i" + using add.int_pow_consistent[OF a assms(2)] by simp + also have "... = ?rhs" + unfolding add_pow_def by simp + finally show ?thesis by simp +qed + +lemma (in ring) int_embed_consistent: + assumes "subring K R" + shows "int_embed R i = int_embed (R \ carrier := K \) i" +proof - + have a:"\ = \\<^bsub>R \ carrier := K \\<^esub>" by simp + have b:"\\<^bsub>R\carrier := K\\<^esub> \ K" + using assms subringE(3) by auto + show ?thesis + unfolding int_embed_def a using b add_pow_consistent[OF assms(1)] by simp +qed + +lemma (in ring) int_embed_closed: + "int_embed R k \ carrier R" + unfolding int_embed_def using add.int_pow_closed by simp + +lemma (in ring) int_embed_range: + assumes "subring K R" + shows "int_embed R k \ K" +proof - + let ?R' = "R \ carrier := K \" + interpret x:ring ?R' + using subring_is_ring[OF assms] by simp + have "int_embed R k = int_embed ?R' k" + using int_embed_consistent[OF assms] by simp + also have "... \ K" + using x.int_embed_closed by simp + finally show ?thesis by simp +qed + +lemma (in ring) int_embed_zero: + "int_embed R 0 = \\<^bsub>R\<^esub>" + by (simp add:int_embed_def add_pow_def) + +lemma (in ring) int_embed_one: + "int_embed R 1 = \\<^bsub>R\<^esub>" + by (simp add:int_embed_def) + +lemma (in ring) int_embed_add: + "int_embed R (x+y) = int_embed R x \\<^bsub>R\<^esub> int_embed R y" + by (simp add:int_embed_def add.int_pow_mult) + +lemma (in ring) int_embed_inv: + "int_embed R (-x) = \\<^bsub>R\<^esub> int_embed R x" (is "?lhs = ?rhs") +proof - + have "?lhs = int_embed R (-x) \ (int_embed R x \ int_embed R x)" + using int_embed_closed by simp + also have + "... = int_embed R (-x) \ int_embed R x \ (\ int_embed R x)" + using int_embed_closed by (subst a_minus_def, subst a_assoc, auto) + also have "... = int_embed R (-x +x) \ (\ int_embed R x)" + by (subst int_embed_add, simp) + also have "... = ?rhs" + using int_embed_closed + by (simp add:int_embed_zero) + finally show ?thesis by simp +qed + +lemma (in ring) int_embed_diff: + "int_embed R (x-y) = int_embed R x \\<^bsub>R\<^esub> int_embed R y" + (is "?lhs = ?rhs") +proof - + have "?lhs = int_embed R (x + (-y))" by simp + also have "... = ?rhs" + by (subst int_embed_add, simp add:a_minus_def int_embed_inv) + finally show ?thesis by simp +qed + +lemma (in ring) int_embed_mult_aux: + "int_embed R (x*int y) = int_embed R x \ int_embed R y" +proof (induction y) + case 0 + then show ?case by (simp add:int_embed_closed int_embed_zero) +next + case (Suc y) + have "int_embed R (x * int (Suc y)) = int_embed R (x + x * int y)" + by (simp add:algebra_simps) + also have "... = int_embed R x \ int_embed R (x * int y)" + by (subst int_embed_add, simp) + also have + "... = int_embed R x \ \ \ int_embed R x \ int_embed R y" + using int_embed_closed + by (subst Suc, simp) + also have "... = int_embed R x \ (int_embed R 1 \ int_embed R y)" + using int_embed_closed by (subst r_distr, simp_all add:int_embed_one) + also have "... = int_embed R x \ int_embed R (1+int y)" + by (subst int_embed_add, simp) + also have "... = int_embed R x \ int_embed R (Suc y)" + by simp + finally show ?case by simp +qed + +lemma (in ring) int_embed_mult: + "int_embed R (x*y) = int_embed R x \\<^bsub>R\<^esub> int_embed R y" +proof (cases "y \ 0") + case True + then obtain y' where y_def: "y = int y'" + using nonneg_int_cases by auto + have "int_embed R (x * y) = int_embed R (x * int y')" + unfolding y_def by simp + also have "... = int_embed R x \ int_embed R y'" + by (subst int_embed_mult_aux, simp) + also have "... = int_embed R x \ int_embed R y" + unfolding y_def by simp + finally show ?thesis by simp +next + case False + then obtain y' where y_def: "y = - int y'" + by (meson nle_le nonpos_int_cases) + have "int_embed R (x * y) = int_embed R (-(x * int y'))" + unfolding y_def by simp + also have "... = \ (int_embed R (x * int y'))" + by (subst int_embed_inv, simp) + also have "... = \ (int_embed R x \ int_embed R y')" + by (subst int_embed_mult_aux, simp) + also have "... = int_embed R x \ \ int_embed R y'" + using int_embed_closed by algebra + also have "... = int_embed R x \ int_embed R (-y')" + by (subst int_embed_inv, simp) + also have "... = int_embed R x \ int_embed R y" + unfolding y_def by simp + finally show ?thesis by simp +qed + +lemma (in ring) int_embed_ring_hom: + "ring_hom_ring int_ring R (int_embed R)" +proof (rule ring_hom_ringI) + show "ring int_ring" using int.is_ring by simp + show "ring R" using ring_axioms by simp + show "int_embed R x \ carrier R" if "x \ carrier \" for x + using int_embed_closed by simp + show "int_embed R (x\\<^bsub>\\<^esub>y) = int_embed R x \ int_embed R y" + if "x \ carrier \" "y \ carrier \" for x y + using int_embed_mult by simp + show "int_embed R (x\\<^bsub>\\<^esub>y) = int_embed R x \ int_embed R y" + if "x \ carrier \" "y \ carrier \" for x y + using int_embed_add by simp + show "int_embed R \\<^bsub>\\<^esub> = \" + by (simp add:int_embed_one) +qed + +abbreviation char_subring where + "char_subring R \ int_embed R ` UNIV" + +definition char where + "char R = card (char_subring R)" + +text \This is a non-standard definition for the characteristic of a ring. + +Commonly~\cite[Definition 1.43]{lidl1986} it is defined to be the smallest natural number $n$ such +that n-times repeated addition of any number is zero. If no such number exists then it is defined +to be $0$. In the case of rings with unit elements --- not that the locale @{locale "ring"} requires +unit elements --- the above definition can be simplified to the number of times the unit elements +needs to be repeatedly added to reach $0$. + +The following three lemmas imply that the definition of the characteristic here coincides with the +latter definition.\ + +lemma (in ring) char_bound: + assumes "x > 0" + assumes "int_embed R (int x) = \" + shows "char R \ x" "char R > 0" +proof - + have "char_subring R \ int_embed R ` ({0.. UNIV" + define u where "u = y div (int x)" + define v where "v = y mod (int x)" + have "int x > 0" using assms by simp + hence y_exp: "y = u * int x + v" "v \ 0" "v < int x" + unfolding u_def v_def by simp_all + have "int_embed R y = int_embed R v" + using int_embed_closed unfolding y_exp + by (simp add:int_embed_mult int_embed_add assms(2)) + also have "... \ int_embed R ` ({0.. int_embed R ` {0.. card {0.. x" by simp + have "1 = card {int_embed R 0}" by simp + also have "... \ card (int_embed R ` {0.. 0" by simp +qed + +lemma (in ring) embed_char_eq_0: + "int_embed R (int (char R)) = \" +proof (cases "finite (char_subring R)") + case True + interpret h: ring_hom_ring "int_ring" R "(int_embed R)" + using int_embed_ring_hom by simp + + define A where "A = {0..int (char R)}" + have "card (int_embed R ` A) \ card (char_subring R)" + by (intro card_mono[OF True] image_subsetI, simp) + also have "... = char R" + unfolding char_def by simp + also have "... < card A" + unfolding A_def by simp + finally have "card (int_embed R ` A) < card A" by simp + hence "\inj_on (int_embed R) A" + using pigeonhole by simp + then obtain x y where xy: + "x \ A" "y \ A" "x \ y" "int_embed R x = int_embed R y" + unfolding inj_on_def by auto + define v where "v = nat (max x y - min x y)" + have a:"int_embed R v = \" + using xy int_embed_closed + by (cases "x < y", simp_all add:int_embed_diff v_def) + moreover have "v > 0" + using xy by (cases "x < y", simp_all add:v_def) + ultimately have "char R \ v" using char_bound by simp + moreover have "v \ char R" + using xy v_def A_def by (cases "x < y", simp_all) + ultimately have "char R = v" by simp + then show ?thesis using a by simp +next + case False + hence "char R = 0" + unfolding char_def by simp + then show ?thesis by (simp add:int_embed_zero) +qed + +lemma (in ring) embed_char_eq_0_iff: + fixes n :: int + shows "int_embed R n = \ \ char R dvd n" +proof (cases "char R > 0") + case True + define r where "r = n mod char R" + define s where "s = n div char R" + have rs: "r < char R" "r \ 0" "n = r + s * char R" + using True by (simp_all add:r_def s_def) + + have "int_embed R n = int_embed R r" + using int_embed_closed unfolding rs(3) + by (simp add: int_embed_add int_embed_mult embed_char_eq_0) + + moreover have "nat r < char R" using rs by simp + hence "int_embed R (nat r) \ \ \ nat r = 0" + using True char_bound not_less by blast + hence "int_embed R r \ \ \ r = 0" + using rs by simp + + ultimately have "int_embed R n = \ \ r = 0" + using int_embed_zero by auto + also have "r = 0 \ char R dvd n" + using r_def by auto + finally show ?thesis by simp +next + case False + hence "char R = 0" by simp + hence a:"x > 0 \ int_embed R (int x) \ \" for x + using char_bound by auto + + have c:"int_embed R (abs x) \ \ \ int_embed R x \ \" for x + using int_embed_closed + by (cases "x > 0", simp, simp add:int_embed_inv) + + have "int_embed R x \ \" if b:"x \ 0" for x + proof - + have "nat (abs x) > 0" using b by simp + hence "int_embed R (nat (abs x)) \ \" + using a by blast + hence "int_embed R (abs x) \ \" by simp + thus ?thesis using c by simp + qed + hence "int_embed R n = \ \ n = 0" + using int_embed_zero by auto + also have "n = 0 \ char R dvd n" using False by simp + finally show ?thesis by simp +qed + +text \This result can be found in \cite[Theorem 1.44]{lidl1986}.\ + +lemma (in domain) characteristic_is_prime: + assumes "char R > 0" + shows "prime (char R)" +proof (rule ccontr) + have "\(char R = 1)" + using embed_char_eq_0 int_embed_one by auto + hence "\(char R dvd 1)" using assms(1) by simp + moreover assume "\(prime (char R))" + hence "\(irreducible (char R))" + using irreducible_imp_prime_elem_gcd prime_elem_nat_iff by blast + ultimately obtain p q where pq_def: "p * q = char R" "p > 1" "q > 1" + using assms + unfolding Factorial_Ring.irreducible_def by auto + have "int_embed R p \ int_embed R q = \" + using embed_char_eq_0 pq_def + by (subst int_embed_mult[symmetric]) (metis of_nat_mult) + hence "int_embed R p = \ \ int_embed R q = \" + using integral int_embed_closed by simp + hence "p*q \ p \ p*q \ q" + using char_bound pq_def by auto + thus "False" + using pq_def(2,3) by simp +qed + +lemma (in ring) char_ring_is_subring: + "subring (char_subring R) R" +proof - + have "subring (int_embed R ` carrier int_ring) R" + by (intro ring.carrier_is_subring int.is_ring + ring_hom_ring.img_is_subring[OF int_embed_ring_hom]) + thus ?thesis by simp +qed + +lemma (in cring) char_ring_is_subcring: + "subcring (char_subring R) R" + using subcringI'[OF char_ring_is_subring] by auto + +lemma (in domain) char_ring_is_subdomain: + "subdomain (char_subring R) R" + using subdomainI'[OF char_ring_is_subring] by auto + +lemma image_set_eqI: + assumes "\x. x \ A \ f x \ B" + assumes "\x. x \ B \ g x \ A \ f (g x) = x" + shows "f ` A = B" + using assms by force + +text \This is the binomial expansion theorem for commutative rings.\ + +lemma (in cring) binomial_expansion: + fixes n :: nat + assumes [simp]: "x \ carrier R" "y \ carrier R" + shows "(x \ y) [^] n = + (\k \ {..n}. int_embed R (n choose k) \ x [^] k \ y [^] (n-k))" +proof - + define A where "A = (\k. {A. A \ {.. card A = k})" + + have fin_A: "finite (A i)" for i + unfolding A_def by simp + have disj_A: "pairwise (\i j. disjnt (A i) (A j)) {..n}" + unfolding pairwise_def disjnt_def A_def by auto + have card_A: "B \ A i \ card B = i" if " i \ {..n}" for i B + unfolding A_def by simp + have card_A2: "card (A i) = (n choose i)" if "i \ {..n}" for i + unfolding A_def using n_subsets[where A="{.. n" + if "A \ {.. {..<(n::nat)}" for n A + using finite_subset that by (subst card_insert_disjoint, auto) + + have embed_distr: "[m] \ y = int_embed R (int m) \ y" + if "y \ carrier R" for m y + unfolding int_embed_def add_pow_def using that + by (simp add:add_pow_def[symmetric] int_pow_int add_pow_ldistr) + + have "(x \ y) [^] n = + (\A \ Pow {.. y [^] (n-card A))" + proof (induction n) + case 0 + then show ?case by simp + next + case (Suc n) + have s1: + "insert n ` Pow {.. {.. n \ A}" + by (intro image_set_eqI[where g="\x. x \ {.. {.. n \ A}" + using lessThan_Suc by auto + + have "(x \ y) [^] Suc n = (x \ y) [^] n \ (x \ y)" by simp + also have "... = + (\A \ Pow {.. y [^] (n-card A)) \ + (x \ y)" + by (subst Suc, simp) + also have "... = + (\A \ Pow {.. y [^] (n-card A)) \ x \ + (\A \ Pow {.. y [^] (n-card A)) \ y" + by (subst r_distr, auto) + also have "... = + (\A \ Pow {.. y [^] (n-card A) \ x) \ + (\A \ Pow {.. y [^] (n-card A) \ y)" + by (simp add:finsum_ldistr) + also have "... = + (\A \ Pow {.. y [^] (n-card A)) \ + (\A \ Pow {.. y [^] (n-card A+1))" + using m_assoc m_comm + by (intro arg_cong2[where f="(\)"] finsum_cong', auto) + also have "... = + (\A \ Pow {.. y [^] (n+1-card (insert n A))) \ + (\A \ Pow {.. y [^] (n+1-card A))" + using finite_subset card_bound card_insert Suc_diff_le + by (intro arg_cong2[where f="(\)"] finsum_cong', simp_all) + also have "... = + (\A \ insert n ` Pow {.. y [^] (n+1-card A)) \ + (\A \ Pow {.. y [^] (n+1-card A))" + by (subst finsum_reindex, auto simp add:inj_on_def) + also have "... = + (\A \ {A. A \ {.. n \ A}. + x [^] (card A) \ y [^] (n+1-card A)) \ + (\A \ {A. A \ {.. n \ A}. + x [^] (card A) \ y [^] (n+1-card A))" + by (intro arg_cong2[where f="(\)"] finsum_cong' s1 s2, simp_all) + also have "... = (\A \ + {A. A \ {.. n \ A} \ {A. A \ {.. n \ A}. + x [^] (card A) \ y [^] (n+1-card A))" + by (subst finsum_Un_disjoint, auto) + also have "... = + (\A \ Pow {.. y [^] (n+1-card A))" + by (intro finsum_cong', auto) + finally show ?case by simp + qed + also have "... = + (\A \ (\ (A ` {..n})). x [^] (card A) \ y [^] (n-card A))" + using card_bound by (intro finsum_cong', auto simp add:A_def) + also have "... = + (\ k \ {..n}. (\ A \ A k. x [^] (card A) \ y [^] (n-card A)))" + using fin_A disj_A by (subst add.finprod_UN_disjoint, auto) + also have "... = (\ k \ {..n}. (\ A \ A k. x [^] k \ y [^] (n-k)))" + using card_A by (intro finsum_cong', auto) + also have "... = + (\ k \ {..n}. int_embed R (card (A k)) \ x [^] k \ y [^] (n-k))" + using int_embed_closed + by (subst add.finprod_const, simp_all add:embed_distr m_assoc) + also have "... = + (\ k \ {..n}. int_embed R (n choose k) \ x [^] k \ y [^] (n-k))" + using int_embed_closed card_A2 by (intro finsum_cong', simp_all) + finally show ?thesis by simp +qed + +lemma bin_prime_factor: + assumes "prime p" + assumes "k > 0" "k < p" + shows "p dvd (p choose k)" +proof - + have "p dvd fact p" + using assms(1) prime_dvd_fact_iff by auto + hence "p dvd fact k * fact (p - k) * (p choose k)" + using binomial_fact_lemma assms by simp + hence "p dvd fact k \ p dvd fact (p-k) \ p dvd (p choose k)" + by (simp add: assms(1) prime_dvd_mult_eq_nat) + thus "p dvd (p choose k)" + using assms(1,2,3) prime_dvd_fact_iff by auto +qed + +theorem (in domain) freshmans_dream: + assumes "char R > 0" + assumes [simp]: "x \ carrier R" "y \ carrier R" + shows "(x \ y) [^] (char R) = x [^] char R \ y [^] char R" + (is "?lhs = ?rhs") +proof - + have c:"prime (char R)" + using assms(1) characteristic_is_prime by auto + have a:"int_embed R (char R choose i) = \" + if "i \ {..char R} - {0, char R}" for i + proof - + have "i > 0" "i < char R" using that by auto + hence "char R dvd char R choose i" + using c bin_prime_factor by simp + thus ?thesis using embed_char_eq_0_iff by simp + qed + + have "?lhs = (\k \ {..char R}. int_embed R (char R choose k) + \ x [^] k \ y [^] (char R-k))" + using binomial_expansion[OF assms(2,3)] by simp + also have "... = (\k \ {0,char R}.int_embed R (char R choose k) + \ x [^] k \ y [^] (char R-k))" + using a int_embed_closed + by (intro add.finprod_mono_neutral_cong_right, simp, simp_all) + also have "... = ?rhs" + using int_embed_closed assms(1) by (simp add:int_embed_one a_comm) + finally show ?thesis by simp +qed + +text \The following theorem is somtimes called Freshman's dream for obvious reasons, +it can be found in Lidl and Niederreiter~\cite[Theorem 1.46]{lidl1986}.\ + +lemma (in domain) freshmans_dream_ext: + fixes m + assumes "char R > 0" + assumes [simp]: "x \ carrier R" "y \ carrier R" + defines "n \ char R^m" + shows "(x \ y) [^] n = x [^] n \ y [^] n" + (is "?lhs = ?rhs") + unfolding n_def +proof (induction m) + case 0 + then show ?case by simp +next + case (Suc m) + have "(x \ y) [^] (char R^(m+1)) = + (x \ y) [^] (char R^m * char R)" + by (simp add:mult.commute) + also have "... = ((x \ y) [^] (char R^m)) [^] char R" + using nat_pow_pow by simp + also have "... = (x [^] (char R^m) \ y [^] (char R^m)) [^] char R" + by (subst Suc, simp) + also have "... = + (x [^] (char R^m)) [^] char R \ (y [^] (char R^m)) [^] char R" + by (subst freshmans_dream[OF assms(1), symmetric], simp_all) + also have "... = + x [^] (char R^m * char R) \ y [^] (char R^m * char R)" + by (simp add:nat_pow_pow) + also have "... = x [^] (char R^Suc m) \ y [^] (char R^Suc m)" + by (simp add:mult.commute) + finally show ?case by simp +qed + +text \The following is a generalized version of the Frobenius homomorphism. The classic version +of the theorem is the case where @{term "(k::nat) = 1"}.\ + +theorem (in domain) frobenius_hom: + assumes "char R > 0" + assumes "m = char R ^ k" + shows "ring_hom_cring R R (\x. x [^] m)" +proof - + have a:"(x \ y) [^] m = x [^] m \ y [^] m" + if b:"x \ carrier R" "y \ carrier R" for x y + using b nat_pow_distrib by simp + have b:"(x \ y) [^] m = x [^] m \ y [^] m" + if b:"x \ carrier R" "y \ carrier R" for x y + unfolding assms(2) freshmans_dream_ext[OF assms(1) b] + by simp + + have "ring_hom_ring R R (\x. x [^] m)" + by (intro ring_hom_ringI a b is_ring, simp_all) + + thus "?thesis" + using RingHom.ring_hom_cringI is_cring by blast +qed + +lemma (in domain) char_ring_is_subfield: + assumes "char R > 0" + shows "subfield (char_subring R) R" +proof - + interpret d:domain "R \ carrier := char_subring R \" + using char_ring_is_subdomain subdomain_is_domain by simp + + have "finite (char_subring R)" + using char_def assms by (metis card_ge_0_finite) + hence "Units (R \ carrier := char_subring R \) + = char_subring R - {\}" + using d.finite_domain_units by simp + + thus ?thesis + using subfieldI[OF char_ring_is_subcring] by simp +qed + +lemma card_lists_length_eq': + fixes A :: "'a set" + shows "card {xs. set xs \ A \ length xs = n} = card A ^ n" +proof (cases "finite A") + case True + then show ?thesis using card_lists_length_eq by auto +next + case False + hence inf_A: "infinite A" by simp + show ?thesis + proof (cases "n = 0") + case True + hence "card {xs. set xs \ A \ length xs = n} = card {([] :: 'a list)}" + by (intro arg_cong[where f="card"], auto simp add:set_eq_iff) + also have "... = 1" by simp + also have "... = card A^n" using True inf_A by simp + finally show ?thesis by simp + next + case False + hence "inj (replicate n)" + by (meson inj_onI replicate_eq_replicate) + hence "inj_on (replicate n) A" using inj_on_subset + by (metis subset_UNIV) + hence "infinite (replicate n ` A)" + using inf_A finite_image_iff by auto + moreover have + "replicate n ` A \ {xs. set xs \ A \ length xs = n}" + by (intro image_subsetI, auto) + ultimately have "infinite {xs. set xs \ A \ length xs = n}" + using infinite_super by auto + hence "card {xs. set xs \ A \ length xs = n} = 0" by simp + then show ?thesis using inf_A False by simp + qed +qed + +lemma (in ring) card_span: + assumes "subfield K R" + assumes "independent K w" + assumes "set w \ carrier R" + shows "card (Span K w) = card K^(length w)" +proof - + define A where "A = {x. set x \ K \ length x = length w}" + define f where "f = (\x. combine x w)" + + have "x \ f ` A" if a:"x \ Span K w" for x + proof - + obtain y where "y \ A" "x = f y" + unfolding A_def f_def + using unique_decomposition[OF assms(1,2) a] by auto + thus ?thesis by simp + qed + moreover have "f x \ Span K w" if a: "x \ A" for x + using Span_eq_combine_set[OF assms(1,3)] a + unfolding A_def f_def by auto + ultimately have b:"Span K w = f ` A" by auto + + have "False" if a: "x \ A" "y \ A" "f x = f y" "x \ y" for x y + proof - + have "f x \ Span K w" using b a by simp + thus "False" + using a unique_decomposition[OF assms(1,2)] + unfolding f_def A_def by blast + qed + hence f_inj: "inj_on f A" + unfolding inj_on_def by auto + + have "card (Span K w) = card (f ` A)" using b by simp + also have "... = card A" by (intro card_image f_inj) + also have "... = card K^length w" + unfolding A_def by (intro card_lists_length_eq') + finally show ?thesis by simp +qed + +lemma (in ring) finite_carr_imp_char_ge_0: + assumes "finite (carrier R)" + shows "char R > 0" +proof - + have "char_subring R \ carrier R" + using int_embed_closed by auto + hence "finite (char_subring R)" + using finite_subset assms by auto + hence "card (char_subring R) > 0" + using card_range_greater_zero by simp + thus "char R > 0" + unfolding char_def by simp +qed + +lemma (in ring) char_consistent: + assumes "subring H R" + shows "char (R \ carrier := H \) = char R" +proof - + show ?thesis + using int_embed_consistent[OF assms(1)] + unfolding char_def by simp +qed + +lemma (in ring_hom_ring) char_consistent: + assumes "inj_on h (carrier R)" + shows "char R = char S" +proof - + have a:"h (int_embed R (int n)) = int_embed S (int n)" for n + using R.int_embed_range[OF R.carrier_is_subring] + using R.int_embed_range[OF R.carrier_is_subring] + using S.int_embed_one R.int_embed_one + using S.int_embed_zero R.int_embed_zero + using S.int_embed_add R.int_embed_add + by (induction n, simp_all) + + have b:"h (int_embed R (-(int n))) = int_embed S (-(int n))" for n + using R.int_embed_range[OF R.carrier_is_subring] + using S.int_embed_range[OF S.carrier_is_subring] a + by (simp add:R.int_embed_inv S.int_embed_inv) + + have c:"h (int_embed R n) = int_embed S n" for n + proof (cases "n \ 0") + case True + then obtain m where "n = int m" + using nonneg_int_cases by auto + then show ?thesis + by (simp add:a) + next + case False + hence "n \ 0" by simp + then obtain m where "n = -int m" + using nonpos_int_cases by auto + then show ?thesis by (simp add:b) + qed + + have "char S = card (h ` char_subring R)" + unfolding char_def image_image c by simp + also have "... = card (char_subring R)" + using R.int_embed_range[OF R.carrier_is_subring] + by (intro card_image inj_on_subset[OF assms(1)]) auto + also have "... = char R" unfolding char_def by simp + finally show ?thesis + by simp +qed + +definition char_iso :: "_ \ int set \ 'a" + where "char_iso R x = the_elem (int_embed R ` x)" + +text \The function @{term "char_iso R"} denotes the isomorphism between @{term "ZFact (char R)"} and +the characteristic subring.\ + +lemma (in ring) char_iso: "char_iso R \ + ring_iso (ZFact (char R)) (R\carrier := char_subring R\)" +proof - + interpret h: ring_hom_ring "int_ring" "R" "int_embed R" + using int_embed_ring_hom by simp + + have "a_kernel \ R (int_embed R) = {x. int_embed R x = \}" + unfolding a_kernel_def kernel_def by simp + also have "... = {x. char R dvd x}" + using embed_char_eq_0_iff by simp + also have "... = PIdl\<^bsub>\\<^esub> (int (char R))" + unfolding cgenideal_def by auto + also have "... = Idl\<^bsub>\\<^esub> {int (char R)}" + using int.cgenideal_eq_genideal by simp + finally have a:"a_kernel \ R (int_embed R) = Idl\<^bsub>\\<^esub> {int (char R)}" + by simp + show "?thesis" + unfolding char_iso_def ZFact_def a[symmetric] + by (intro h.FactRing_iso_set_aux) +qed + +text \The size of a finite field must be a prime power. +This can be found in Ireland and Rosen~\cite[Proposition 7.1.3]{ireland1982}.\ + +theorem (in finite_field) finite_field_order: + "\n. order R = char R ^ n \ n > 0" +proof - + have a:"char R > 0" + using finite_carr_imp_char_ge_0[OF finite_carrier] + by simp + let ?CR = "char_subring R" + + obtain v where v_def: "set v = carrier R" + using finite_carrier finite_list by auto + hence b:"set v \ carrier R" by auto + + have "carrier R = set v" using v_def by simp + also have "... \ Span ?CR v" + using Span_base_incl[OF char_ring_is_subfield[OF a] b] by simp + finally have "carrier R \ Span ?CR v" by simp + moreover have "Span ?CR v \ carrier R" + using int_embed_closed v_def by (intro Span_in_carrier, auto) + ultimately have Span_v: "Span ?CR v = carrier R" by simp + + obtain w where w_def: + "set w \ carrier R" + "independent ?CR w" + "Span ?CR v = Span ?CR w" + using b filter_base[OF char_ring_is_subfield[OF a]] + by metis + + have Span_w: "Span ?CR w = carrier R" + using w_def(3) Span_v by simp + + hence "order R = card (Span ?CR w)" by (simp add:order_def) + also have "... = card ?CR^length w" + by (intro card_span char_ring_is_subfield[OF a] w_def(1,2)) + finally have c: + "order R = char R^(length w)" + by (simp add:char_def) + have "length w > 0" + using finite_field_min_order c by auto + thus ?thesis using c by auto +qed + +end diff --git a/thys/Finite_Fields/document/root.bib b/thys/Finite_Fields/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/document/root.bib @@ -0,0 +1,42 @@ +@book{ireland1982, + author = {Kenneth Ireland and + Michael Rosen}, + title = {A classical introduction to modern number theory}, + series = {Graduate texts in mathematics}, + volume = {84}, + publisher = {Springer}, + year = {1982}, + isbn = {978-0-387-90625-6}, + timestamp = {Fri, 28 Jun 2019 12:45:52 +0200}, + biburl = {https://dblp.org/rec/books/daglib/0068082.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{lidl1986, +author = {Lidl, Rudolf and Niederreiter, Harald}, +title = {Introduction to Finite Fields and Their Applications}, +year = {1986}, +isbn = {0521307066}, +publisher = {Cambridge University Press}, +address = {USA} +} + +@article{chebolu2010, + title={Counting Irreducible Polynomials over Finite Fields Using the Inclusion-Exclusion Principle}, + author={Sunil K. Chebolu and J{\'a}n Min{\'a}{\v{c}}}, + journal={Mathematics Magazine}, + year={2010}, + volume={84}, + pages={369 - 371} +} + +@article{Dirichlet_Series-AFP, + author = {Manuel Eberl}, + title = {Dirichlet Series}, + journal = {Archive of Formal Proofs}, + month = oct, + year = 2017, + note = {\url{https://isa-afp.org/entries/Dirichlet_Series.html}, + Formal proof development}, + ISSN = {2150-914x}, +} \ No newline at end of file diff --git a/thys/Finite_Fields/document/root.tex b/thys/Finite_Fields/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/document/root.tex @@ -0,0 +1,37 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amssymb} +\usepackage{pdfsetup} +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Finite Fields} +\author{Emin Karayel} +\maketitle + +\abstract{This entry formalizes the classification of the finite fields (also called Galois fields): +For each prime power $p^n$ there exists exactly one (up to isomorphisms) finite field of that size +and there are no other finite fields. +The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism, +formal differentiation for polynomials in HOL-Algebra and Gauss' formula for the number of +monic irreducible polynomials over finite fields: +\[ +\frac{1}{n} \sum_{d | n} \mu(d) p^{n/d} \textrm{.} +\] +The proofs are based on the books from Ireland and Rosen~\cite{ireland1982}, as well as, +Lidl and Niederreiter~\cite{lidl1986}. +} + +\parindent 0pt\parskip 0.5ex + +\tableofcontents + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} \ No newline at end of file diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,685 +1,686 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF +Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL