# HG changeset patch # User paulson # Date 1555239617 -3600 # Node ID 6152339771557d64222ee866bc8a393bc01fd1d3 # Parent 57503fe1b0ff293b56bf416d84f9e46e7e66b93d# Parent 13b10ca7115021fc1a548364b234a303ea6acb75 merged diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Algebra.thy --- a/src/HOL/Algebra/Algebra.thy Sat Apr 13 22:06:40 2019 +0200 +++ b/src/HOL/Algebra/Algebra.thy Sun Apr 14 12:00:17 2019 +0100 @@ -2,6 +2,6 @@ theory Algebra imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups - Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials + Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure begin end diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Algebraic_Closure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Algebraic_Closure.thy Sun Apr 14 12:00:17 2019 +0100 @@ -0,0 +1,768 @@ +(* Title: HOL/Algebra/Algebraic_Closure.thy + Author: Paulo Emílio de Vilhena + +With contributions by Martin Baillon. +*) + +theory Algebraic_Closure + imports Indexed_Polynomials Polynomial_Divisibility Pred_Zorn Finite_Extensions + +begin + +section \Algebraic Closure\ + +subsection \Definitions\ + +inductive iso_incl :: "'a ring \ 'a ring \ bool" (infixl "\" 65) for A B + where iso_inclI [intro]: "id \ ring_hom A B \ iso_incl A B" + +definition law_restrict :: "('a, 'b) ring_scheme \ 'a ring" + where "law_restrict R \ (ring.truncate R) + \ mult := (\a \ carrier R. \b \ carrier R. a \\<^bsub>R\<^esub> b), + add := (\a \ carrier R. \b \ carrier R. a \\<^bsub>R\<^esub> b) \" + +definition (in ring) \ :: "'a list \ (('a list multiset) \ 'a) list" + where "\ P = map indexed_const P" + +definition (in ring) extensions :: "(('a list multiset) \ 'a) ring set" + where "extensions \ { L \ \such that\. + \ \i\ (field L) \ + \ \ii\ (indexed_const \ ring_hom R L) \ + \ \iii\ (\\

\ carrier L. carrier_coeff \

) \ + \ \iv\ (\\

\ carrier L. \P \ carrier (poly_ring R). + \ index_free \

P \ \\<^bsub>P\<^esub> \ carrier L \ (ring.eval L) (\ P) \\<^bsub>P\<^esub> = \\<^bsub>L\<^esub>) }" + +abbreviation (in ring) restrict_extensions :: "(('a list multiset) \ 'a) ring set" ("\") + where "\ \ law_restrict ` extensions" + + +subsection \Basic Properties\ + +(* ========== *) +lemma (in field) is_ring: "ring R" + using ring_axioms . +(* ========== *) + +lemma law_restrict_carrier: "carrier (law_restrict R) = carrier R" + by (simp add: law_restrict_def ring.defs) + +lemma law_restrict_one: "one (law_restrict R) = one R" + by (simp add: law_restrict_def ring.defs) + +lemma law_restrict_zero: "zero (law_restrict R) = zero R" + by (simp add: law_restrict_def ring.defs) + +lemma law_restrict_mult: "monoid.mult (law_restrict R) = (\a \ carrier R. \b \ carrier R. a \\<^bsub>R\<^esub> b)" + by (simp add: law_restrict_def ring.defs) + +lemma law_restrict_add: "add (law_restrict R) = (\a \ carrier R. \b \ carrier R. a \\<^bsub>R\<^esub> b)" + by (simp add: law_restrict_def ring.defs) + +lemma (in ring) law_restrict_is_ring: "ring (law_restrict R)" + by (unfold_locales) (auto simp add: law_restrict_def Units_def ring.defs, + simp_all add: a_assoc a_comm m_assoc l_distr r_distr a_lcomm) + +lemma (in field) law_restrict_is_field: "field (law_restrict R)" +proof - + have "comm_monoid_axioms (law_restrict R)" + using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto + then interpret L: cring "law_restrict R" + using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto + have "Units R = Units (law_restrict R)" + unfolding Units_def law_restrict_carrier law_restrict_mult law_restrict_one by auto + thus ?thesis + using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp +qed + +lemma law_restrict_iso_imp_eq: + assumes "id \ ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B" + shows "law_restrict A = law_restrict B" +proof - + have "carrier A = carrier B" + using ring_iso_memE(5)[OF assms(1)] unfolding bij_betw_def law_restrict_def by (simp add: ring.defs) + hence mult: "a \\<^bsub>law_restrict A\<^esub> b = a \\<^bsub>law_restrict B\<^esub> b" + and add: "a \\<^bsub>law_restrict A\<^esub> b = a \\<^bsub>law_restrict B\<^esub> b" for a b + using ring_iso_memE(2-3)[OF assms(1)] unfolding law_restrict_def by (auto simp add: ring.defs) + have "monoid.mult (law_restrict A) = monoid.mult (law_restrict B)" + using mult by auto + moreover have "add (law_restrict A) = add (law_restrict B)" + using add by auto + moreover from \carrier A = carrier B\ have "carrier (law_restrict A) = carrier (law_restrict B)" + unfolding law_restrict_def by (simp add: ring.defs) + moreover have "\\<^bsub>law_restrict A\<^esub> = \\<^bsub>law_restrict B\<^esub>" + using ring_hom_zero[OF _ assms(2-3)[THEN ring.law_restrict_is_ring]] assms(1) + unfolding ring_iso_def by auto + moreover have "\\<^bsub>law_restrict A\<^esub> = \\<^bsub>law_restrict B\<^esub>" + using ring_iso_memE(4)[OF assms(1)] by simp + ultimately show ?thesis by simp +qed + +lemma law_restrict_hom: "h \ ring_hom A B \ h \ ring_hom (law_restrict A) (law_restrict B)" +proof + assume "h \ ring_hom A B" thus "h \ ring_hom (law_restrict A) (law_restrict B)" + by (auto intro!: ring_hom_memI dest: ring_hom_memE simp: law_restrict_def ring.defs) +next + assume h: "h \ ring_hom (law_restrict A) (law_restrict B)" show "h \ ring_hom A B" + using ring_hom_memE[OF h] by (auto intro!: ring_hom_memI simp: law_restrict_def ring.defs) +qed + +lemma iso_incl_hom: "A \ B \ (law_restrict A) \ (law_restrict B)" + using law_restrict_hom iso_incl.simps by blast + + +subsection \Partial Order\ + +lemma iso_incl_backwards: + assumes "A \ B" shows "id \ ring_hom A B" + using assms by cases + +lemma iso_incl_antisym_aux: + assumes "A \ B" and "B \ A" shows "id \ ring_iso A B" +proof - + have hom: "id \ ring_hom A B" "id \ ring_hom B A" + using assms(1-2)[THEN iso_incl_backwards] by auto + thus ?thesis + using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def) +qed + +lemma iso_incl_refl: "A \ A" + by (rule iso_inclI[OF ring_hom_memI], auto) + +lemma iso_incl_trans: + assumes "A \ B" and "B \ C" shows "A \ C" + using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto + +lemma (in ring) iso_incl_antisym: + assumes "A \ \" "B \ \" and "A \ B" "B \ A" shows "A = B" +proof - + obtain A' B' :: "('a list multiset \ 'a) ring" + where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'" + using assms(1-2) field.is_ring by (auto simp add: extensions_def) + thus ?thesis + using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp +qed + +lemma (in ring) iso_incl_partial_order: "partial_order_on \ (rel_of (\) \)" + using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_rel_ofI) + +lemma iso_inclE: + assumes "ring A" and "ring B" and "A \ B" shows "ring_hom_ring A B id" + using iso_incl_backwards[OF assms(3)] ring_hom_ring.intro[OF assms(1-2)] + unfolding symmetric[OF ring_hom_ring_axioms_def] by simp + +lemma iso_incl_imp_same_eval: + assumes "ring A" and "ring B" and "A \ B" and "a \ carrier A" and "set p \ carrier A" + shows "(ring.eval A) p a = (ring.eval B) p a" + using ring_hom_ring.eval_hom'[OF iso_inclE[OF assms(1-3)] assms(4-5)] by simp + + +subsection \Extensions Non Empty\ + +lemma (in ring) indexed_const_is_inj: "inj indexed_const" + unfolding indexed_const_def by (rule inj_onI, metis) + +lemma (in ring) indexed_const_inj_on: "inj_on indexed_const (carrier R)" + unfolding indexed_const_def by (rule inj_onI, metis) + +lemma (in field) extensions_non_empty: "\ \ {}" +proof - + have "image_ring indexed_const R \ extensions" + proof (auto simp add: extensions_def) + show "field (image_ring indexed_const R)" + using inj_imp_image_ring_is_field[OF indexed_const_inj_on] . + next + show "indexed_const \ ring_hom R (image_ring indexed_const R)" + using inj_imp_image_ring_iso[OF indexed_const_inj_on] unfolding ring_iso_def by auto + next + fix \

:: "('a list multiset) \ 'a" and P + assume "\

\ carrier (image_ring indexed_const R)" + then obtain k where "k \ carrier R" and "\

= indexed_const k" + unfolding image_ring_carrier by blast + hence "index_free \

P" for P + unfolding index_free_def indexed_const_def by auto + thus "\ index_free \

P \ \\<^bsub>P\<^esub> \ carrier (image_ring indexed_const R)" + and "\ index_free \

P \ ring.eval (image_ring indexed_const R) (\ P) \\<^bsub>P\<^esub> = \\<^bsub>image_ring indexed_const R\<^esub>" + by auto + from \k \ carrier R\ and \\

= indexed_const k\ show "carrier_coeff \

" + unfolding indexed_const_def carrier_coeff_def by auto + qed + thus ?thesis + by blast +qed + + +subsection \Chains\ + +definition union_ring :: "(('a, 'c) ring_scheme) set \ 'a ring" + where "union_ring C = + \ carrier = (\(carrier ` C)), + monoid.mult = (\a b. (monoid.mult (SOME R. R \ C \ a \ carrier R \ b \ carrier R) a b)), + one = one (SOME R. R \ C), + zero = zero (SOME R. R \ C), + add = (\a b. (add (SOME R. R \ C \ a \ carrier R \ b \ carrier R) a b)) \" + + +lemma union_ring_carrier: "carrier (union_ring C) = (\(carrier ` C))" + unfolding union_ring_def by simp + +context + fixes C :: "'a ring set" + assumes field_chain: "\R. R \ C \ field R" and chain: "\R S. \ R \ C; S \ C \ \ R \ S \ S \ R" +begin + +lemma ring_chain: "R \ C \ ring R" + using field.is_ring[OF field_chain] by blast + +lemma same_one_same_zero: + assumes "R \ C" shows "\\<^bsub>union_ring C\<^esub> = \\<^bsub>R\<^esub>" and "\\<^bsub>union_ring C\<^esub> = \\<^bsub>R\<^esub>" +proof - + have "\\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>" if "R \ C" and "S \ C" for R S + using ring_hom_one[of id] chain[OF that] unfolding iso_incl.simps by auto + moreover have "\\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>" if "R \ C" and "S \ C" for R S + using chain[OF that] ring_hom_zero[OF _ ring_chain ring_chain] that unfolding iso_incl.simps by auto + ultimately have "one (SOME R. R \ C) = \\<^bsub>R\<^esub>" and "zero (SOME R. R \ C) = \\<^bsub>R\<^esub>" + using assms by (metis (mono_tags) someI)+ + thus "\\<^bsub>union_ring C\<^esub> = \\<^bsub>R\<^esub>" and "\\<^bsub>union_ring C\<^esub> = \\<^bsub>R\<^esub>" + unfolding union_ring_def by auto +qed + +lemma same_laws: + assumes "R \ C" and "a \ carrier R" and "b \ carrier R" + shows "a \\<^bsub>union_ring C\<^esub> b = a \\<^bsub>R\<^esub> b" and "a \\<^bsub>union_ring C\<^esub> b = a \\<^bsub>R\<^esub> b" +proof - + have "a \\<^bsub>R\<^esub> b = a \\<^bsub>S\<^esub> b" + if "R \ C" "a \ carrier R" "b \ carrier R" and "S \ C" "a \ carrier S" "b \ carrier S" for R S + using ring_hom_memE(2)[of id R S] ring_hom_memE(2)[of id S R] that chain[OF that(1,4)] + unfolding iso_incl.simps by auto + moreover have "a \\<^bsub>R\<^esub> b = a \\<^bsub>S\<^esub> b" + if "R \ C" "a \ carrier R" "b \ carrier R" and "S \ C" "a \ carrier S" "b \ carrier S" for R S + using ring_hom_memE(3)[of id R S] ring_hom_memE(3)[of id S R] that chain[OF that(1,4)] + unfolding iso_incl.simps by auto + ultimately + have "monoid.mult (SOME R. R \ C \ a \ carrier R \ b \ carrier R) a b = a \\<^bsub>R\<^esub> b" + and "add (SOME R. R \ C \ a \ carrier R \ b \ carrier R) a b = a \\<^bsub>R\<^esub> b" + using assms by (metis (mono_tags, lifting) someI)+ + thus "a \\<^bsub>union_ring C\<^esub> b = a \\<^bsub>R\<^esub> b" and "a \\<^bsub>union_ring C\<^esub> b = a \\<^bsub>R\<^esub> b" + unfolding union_ring_def by auto +qed + +lemma exists_superset_carrier: + assumes "finite S" and "S \ {}" and "S \ carrier (union_ring C)" + shows "\R \ C. S \ carrier R" + using assms +proof (induction, simp) + case (insert s S) + obtain R where R: "s \ carrier R" "R \ C" + using insert(5) unfolding union_ring_def by auto + show ?case + proof (cases) + assume "S = {}" thus ?thesis + using R by blast + next + assume "S \ {}" + then obtain T where T: "S \ carrier T" "T \ C" + using insert(3,5) by blast + have "carrier R \ carrier T \ carrier T \ carrier R" + using ring_hom_memE(1)[of id R] ring_hom_memE(1)[of id T] chain[OF R(2) T(2)] + unfolding iso_incl.simps by auto + thus ?thesis + using R T by auto + qed +qed + +lemma union_ring_is_monoid: + assumes "C \ {}" shows "comm_monoid (union_ring C)" +proof + fix a b c + assume "a \ carrier (union_ring C)" "b \ carrier (union_ring C)" "c \ carrier (union_ring C)" + then obtain R where R: "R \ C" "a \ carrier R" "b \ carrier R" "c \ carrier R" + using exists_superset_carrier[of "{ a, b, c }"] by auto + then interpret field R + using field_chain by simp + + show "a \\<^bsub>union_ring C\<^esub> b \ carrier (union_ring C)" + using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto + show "(a \\<^bsub>union_ring C\<^esub> b) \\<^bsub>union_ring C\<^esub> c = a \\<^bsub>union_ring C\<^esub> (b \\<^bsub>union_ring C\<^esub> c)" + and "a \\<^bsub>union_ring C\<^esub> b = b \\<^bsub>union_ring C\<^esub> a" + and "\\<^bsub>union_ring C\<^esub> \\<^bsub>union_ring C\<^esub> a = a" + and "a \\<^bsub>union_ring C\<^esub> \\<^bsub>union_ring C\<^esub> = a" + using same_one_same_zero[OF R(1)] same_laws(1)[OF R(1)] R(2-4) m_assoc m_comm by auto +next + show "\\<^bsub>union_ring C\<^esub> \ carrier (union_ring C)" + using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1) + unfolding union_ring_carrier by auto +qed + +lemma union_ring_is_abelian_group: + assumes "C \ {}" shows "cring (union_ring C)" +proof (rule cringI[OF abelian_groupI union_ring_is_monoid[OF assms]]) + fix a b c + assume "a \ carrier (union_ring C)" "b \ carrier (union_ring C)" "c \ carrier (union_ring C)" + then obtain R where R: "R \ C" "a \ carrier R" "b \ carrier R" "c \ carrier R" + using exists_superset_carrier[of "{ a, b, c }"] by auto + then interpret field R + using field_chain by simp + + show "a \\<^bsub>union_ring C\<^esub> b \ carrier (union_ring C)" + using R(1-3) unfolding same_laws(2)[OF R(1-3)] unfolding union_ring_def by auto + show "(a \\<^bsub>union_ring C\<^esub> b) \\<^bsub>union_ring C\<^esub> c = (a \\<^bsub>union_ring C\<^esub> c) \\<^bsub>union_ring C\<^esub> (b \\<^bsub>union_ring C\<^esub> c)" + and "(a \\<^bsub>union_ring C\<^esub> b) \\<^bsub>union_ring C\<^esub> c = a \\<^bsub>union_ring C\<^esub> (b \\<^bsub>union_ring C\<^esub> c)" + and "a \\<^bsub>union_ring C\<^esub> b = b \\<^bsub>union_ring C\<^esub> a" + and "\\<^bsub>union_ring C\<^esub> \\<^bsub>union_ring C\<^esub> a = a" + using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto + have "\a' \ carrier R. a' \\<^bsub>union_ring C\<^esub> a = \\<^bsub>union_ring C\<^esub>" + using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp + with \R \ C\ show "\y \ carrier (union_ring C). y \\<^bsub>union_ring C\<^esub> a = \\<^bsub>union_ring C\<^esub>" + unfolding union_ring_carrier by auto +next + show "\\<^bsub>union_ring C\<^esub> \ carrier (union_ring C)" + using ring.ring_simprules(2)[OF ring_chain] assms same_one_same_zero(2) + unfolding union_ring_carrier by auto +qed + +lemma union_ring_is_field : + assumes "C \ {}" shows "field (union_ring C)" +proof (rule cring.cring_fieldI[OF union_ring_is_abelian_group[OF assms]]) + have "carrier (union_ring C) - { \\<^bsub>union_ring C\<^esub> } \ Units (union_ring C)" + proof + fix a assume "a \ carrier (union_ring C) - { \\<^bsub>union_ring C\<^esub> }" + hence "a \ carrier (union_ring C)" and "a \ \\<^bsub>union_ring C\<^esub>" + by auto + then obtain R where R: "R \ C" "a \ carrier R" + using exists_superset_carrier[of "{ a }"] by auto + then interpret field R + using field_chain by simp + + from \a \ carrier R\ and \a \ \\<^bsub>union_ring C\<^esub>\ have "a \ Units R" + unfolding same_one_same_zero[OF R(1)] field_Units by auto + hence "\a' \ carrier R. a' \\<^bsub>union_ring C\<^esub> a = \\<^bsub>union_ring C\<^esub> \ a \\<^bsub>union_ring C\<^esub> a' = \\<^bsub>union_ring C\<^esub>" + using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto + with \R \ C\ and \a \ carrier (union_ring C)\ show "a \ Units (union_ring C)" + unfolding Units_def union_ring_carrier by auto + qed + moreover have "\\<^bsub>union_ring C\<^esub> \ Units (union_ring C)" + proof (rule ccontr) + assume "\ \\<^bsub>union_ring C\<^esub> \ Units (union_ring C)" + then obtain a where a: "a \ carrier (union_ring C)" "a \\<^bsub>union_ring C\<^esub> \\<^bsub>union_ring C\<^esub> = \\<^bsub>union_ring C\<^esub>" + unfolding Units_def by auto + then obtain R where R: "R \ C" "a \ carrier R" + using exists_superset_carrier[of "{ a }"] by auto + then interpret field R + using field_chain by simp + have "\\<^bsub>R\<^esub> = \\<^bsub>R\<^esub>" + using a R same_laws(1)[OF R(1)] same_one_same_zero[OF R(1)] by auto + thus False + using one_not_zero by simp + qed + hence "Units (union_ring C) \ carrier (union_ring C) - { \\<^bsub>union_ring C\<^esub> }" + unfolding Units_def by auto + ultimately show "Units (union_ring C) = carrier (union_ring C) - { \\<^bsub>union_ring C\<^esub> }" + by simp +qed + +lemma union_ring_is_upper_bound: + assumes "R \ C" shows "R \ union_ring C" + using ring_hom_memI[of R id "union_ring C"] same_laws[of R] same_one_same_zero[of R] assms + unfolding union_ring_carrier by auto + +end + + +subsection \Zorn\ + +lemma (in ring) exists_core_chain: + assumes "C \ Chains (rel_of (\) \)" obtains C' where "C' \ extensions" and "C = law_restrict ` C'" + using Chains_rel_of[OF assms] by (meson subset_image_iff) + +lemma (in ring) core_chain_is_chain: + assumes "law_restrict ` C \ Chains (rel_of (\) \)" shows "\R S. \ R \ C; S \ C \ \ R \ S \ S \ R" +proof - + fix R S assume "R \ C" and "S \ C" thus "R \ S \ S \ R" + using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def by auto +qed + +lemma (in field) exists_maximal_extension: + shows "\M \ \. \L \ \. M \ L \ L = M" +proof (rule predicate_Zorn[OF iso_incl_partial_order]) + show "\C \ Chains (rel_of (\) \). \L \ \. \R \ C. R \ L" + proof + fix C assume C: "C \ Chains (rel_of (\) \)" + show "\L \ \. \R \ C. R \ L" + proof (cases) + assume "C = {}" thus ?thesis + using extensions_non_empty by auto + next + assume "C \ {}" + from \C \ Chains (rel_of (\) \)\ + obtain C' where C': "C' \ extensions" "C = law_restrict ` C'" + using exists_core_chain by auto + with \C \ {}\ obtain S where S: "S \ C'" and "C' \ {}" + by auto + + have core_chain: "\R. R \ C' \ field R" "\R S. \ R \ C'; S \ C' \ \ R \ S \ S \ R" + using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto + from \C' \ {}\ interpret Union: field "union_ring C'" + using union_ring_is_field[OF core_chain] C'(1) by blast + + have "union_ring C' \ extensions" + proof (auto simp add: extensions_def) + show "field (union_ring C')" + using Union.field_axioms . + next + from \S \ C'\ have "indexed_const \ ring_hom R S" + using C'(1) unfolding extensions_def by auto + thus "indexed_const \ ring_hom R (union_ring C')" + using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S] + unfolding iso_incl.simps by auto + next + show "a \ carrier (union_ring C') \ carrier_coeff a" for a + using C'(1) unfolding union_ring_carrier extensions_def by auto + next + fix \

P + assume "\

\ carrier (union_ring C')" and P: "P \ carrier (poly_ring R)" "\ index_free \

P" + from \\

\ carrier (union_ring C')\ obtain T where T: "T \ C'" "\

\ carrier T" + using exists_superset_carrier[of C' "{ \

}"] core_chain by auto + hence "\\<^bsub>P\<^esub> \ carrier T" and "(ring.eval T) (\ P) \\<^bsub>P\<^esub> = \\<^bsub>T\<^esub>" + and field: "field T" and hom: "indexed_const \ ring_hom R T" + using P C'(1) unfolding extensions_def by auto + with \T \ C'\ show "\\<^bsub>P\<^esub> \ carrier (union_ring C')" + unfolding union_ring_carrier by auto + have "set P \ carrier R" + using P(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "set (\ P) \ carrier T" + using ring_hom_memE(1)[OF hom] unfolding \_def by (induct P) (auto) + with \\\<^bsub>P\<^esub> \ carrier T\ and \(ring.eval T) (\ P) \\<^bsub>P\<^esub> = \\<^bsub>T\<^esub>\ + show "(ring.eval (union_ring C')) (\ P) \\<^bsub>P\<^esub> = \\<^bsub>union_ring C'\<^esub>" + using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring + union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)] + by auto + qed + moreover have "R \ law_restrict (union_ring C')" if "R \ C" for R + using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto + ultimately show ?thesis + by blast + qed + qed +qed + + +subsection \Existence of roots\ + +lemma polynomial_hom: + assumes "h \ ring_hom R S" and "field R" and "field S" + shows "p \ carrier (poly_ring R) \ (map h p) \ carrier (poly_ring S)" +proof - + assume "p \ carrier (poly_ring R)" + interpret ring_hom_ring R S h + using ring_hom_ringI2[OF assms(2-3)[THEN field.is_ring] assms(1)] . + + from \p \ carrier (poly_ring R)\ have "set p \ carrier R" and lc: "p \ [] \ lead_coeff p \ \\<^bsub>R\<^esub>" + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "set (map h p) \ carrier S" + by (induct p) (auto) + moreover have "h a = \\<^bsub>S\<^esub> \ a = \\<^bsub>R\<^esub>" if "a \ carrier R" for a + using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp + with \set p \ carrier R\ have "lead_coeff (map h p) \ \\<^bsub>S\<^esub>" if "p \ []" + using lc[OF that] that by (cases p) (auto) + ultimately show ?thesis + unfolding sym[OF univ_poly_carrier] polynomial_def by auto +qed + +lemma (in ring_hom_ring) subfield_polynomial_hom: + assumes "subfield K R" and "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>" + shows "p \ carrier (K[X]\<^bsub>R\<^esub>) \ (map h p) \ carrier ((h ` K)[X]\<^bsub>S\<^esub>)" +proof - + assume "p \ carrier (K[X]\<^bsub>R\<^esub>)" + hence "p \ carrier (poly_ring (R \ carrier := K \))" + using R.univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] by simp + moreover have "h \ ring_hom (R \ carrier := K \) (S \ carrier := h ` K \)" + using hom_mult subfieldE(3)[OF assms(1)] unfolding ring_hom_def subset_iff by auto + moreover have "field (R \ carrier := K \)" and "field (S \ carrier := (h ` K) \)" + using R.subfield_iff(2)[OF assms(1)] S.subfield_iff(2)[OF img_is_subfield(2)[OF assms]] by simp+ + ultimately have "(map h p) \ carrier (poly_ring (S \ carrier := h ` K \))" + using polynomial_hom[of h "R \ carrier := K \" "S \ carrier := h ` K \"] by auto + thus ?thesis + using S.univ_poly_consistent[OF subfieldE(1)[OF img_is_subfield(2)[OF assms]]] by simp +qed + +lemma (in field) exists_root: + assumes "M \ extensions" and "\L. \ L \ extensions; M \ L \ \ law_restrict L = law_restrict M" + and "P \ carrier (poly_ring R)" and "degree P > 0" + shows "\x \ carrier M. (ring.eval M) (\ P) x = \\<^bsub>M\<^esub>" +proof (rule ccontr) + from \M \ extensions\ interpret M: field M + Hom: ring_hom_ring R M "indexed_const" + using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto + interpret UP: principal_domain "poly_ring M" + using M.univ_poly_is_principal[OF M.carrier_is_subfield] . + + assume no_roots: "\ (\x \ carrier M. M.eval (\ P) x = \\<^bsub>M\<^esub>)" + have "(\ P) \ carrier (poly_ring M)" + using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \_def by simp + moreover have "(\ P) \ Units (poly_ring M)" and "(\ P) \ \\<^bsub>poly_ring M\<^esub>" + using assms(4) unfolding M.univ_poly_carrier_units \_def univ_poly_zero by auto + ultimately obtain Q + where Q: "Q \ carrier (poly_ring M)" "pirreducible\<^bsub>M\<^esub> (carrier M) Q" "Q pdivides\<^bsub>M\<^esub> (\ P)" + using UP.exists_irreducible_divisor[of "\ P"] unfolding pdivides_def by blast + + have hyps: + \ \i\ "field M" + \ \ii\ "\\

. \

\ carrier M \ carrier_coeff \

" + \ \iii\ "\\

. \

\ carrier M \ index_free \

P" + \ \iv\ "\\<^bsub>M\<^esub> = indexed_const \" + using assms(1,3) no_roots unfolding extensions_def by auto + have degree_gt: "degree Q > 1" + proof (rule ccontr) + assume "\ degree Q > 1" hence "degree Q = 1" + using M.pirreducible_degree[OF M.carrier_is_subfield Q(1-2)] by simp + then obtain x where "x \ carrier M" and "M.eval Q x = \\<^bsub>M\<^esub>" + using M.degree_one_root[OF M.carrier_is_subfield Q(1)] M.add.inv_closed by blast + hence "M.eval (\ P) x = \\<^bsub>M\<^esub>" + using M.pdivides_imp_root_sharing[OF Q(1,3)] by simp + with \x \ carrier M\ show False + using no_roots by simp + qed + + define image_poly where "image_poly = image_ring (eval_pmod M P Q) (poly_ring M)" + with \degree Q > 1\ have "M \ image_poly" + using image_poly_iso_incl[OF hyps Q(1)] by auto + moreover have is_field: "field image_poly" + using image_poly_is_field[OF hyps Q(1-2)] unfolding image_poly_def by simp + moreover have "image_poly \ extensions" + proof (auto simp add: extensions_def is_field) + fix \

assume "\

\ carrier image_poly" + then obtain R where \

: "\

= eval_pmod M P Q R" and "R \ carrier (poly_ring M)" + unfolding image_poly_def image_ring_carrier by auto + hence "M.pmod R Q \ carrier (poly_ring M)" + using M.long_division_closed(2)[OF M.carrier_is_subfield _ Q(1)] by simp + hence "list_all carrier_coeff (M.pmod R Q)" + using hyps(2) unfolding sym[OF univ_poly_carrier] list_all_iff polynomial_def by auto + thus "carrier_coeff \

" + using indexed_eval_in_carrier[of "M.pmod R Q"] unfolding \

by simp + next + from \M \ image_poly\ show "indexed_const \ ring_hom R image_poly" + using ring_hom_trans[OF Hom.homh, of id] unfolding iso_incl.simps by simp + next + from \M \ image_poly\ interpret Id: ring_hom_ring M image_poly id + using iso_inclE[OF M.ring_axioms field.is_ring[OF is_field]] by simp + + fix \

S + assume A: "\

\ carrier image_poly" "\ index_free \

S" "S \ carrier (poly_ring R)" + have "\\<^bsub>S\<^esub> \ carrier image_poly \ Id.eval (\ S) \\<^bsub>S\<^esub> = \\<^bsub>image_poly\<^esub>" + proof (cases) + assume "P \ S" + then obtain Q' where "Q' \ carrier M" and "\ index_free Q' S" + using A(1) image_poly_index_free[OF hyps Q(1) _ A(2)] unfolding image_poly_def by auto + hence "\\<^bsub>S\<^esub> \ carrier M" and "M.eval (\ S) \\<^bsub>S\<^esub> = \\<^bsub>M\<^esub>" + using assms(1) A(3) unfolding extensions_def by auto + moreover have "\ S \ carrier (poly_ring M)" + using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \_def . + ultimately show ?thesis + using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto + next + assume "\ P \ S" hence S: "P = S" + by simp + have poly_hom: "R \ carrier (poly_ring image_poly)" if "R \ carrier (poly_ring M)" for R + using polynomial_hom[OF Id.homh M.field_axioms is_field that] by simp + have "\\<^bsub>S\<^esub> \ carrier image_poly" + using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def S by simp + moreover have "Id.eval Q \\<^bsub>S\<^esub> = \\<^bsub>image_poly\<^esub>" + using image_poly_eval_indexed_var[OF hyps Hom.homh Q(1) degree_gt Q(2)] unfolding image_poly_def S by simp + moreover have "Q pdivides\<^bsub>image_poly\<^esub> (\ S)" + proof - + obtain R where R: "R \ carrier (poly_ring M)" "\ S = Q \\<^bsub>poly_ring M\<^esub> R" + using Q(3) unfolding S pdivides_def by auto + moreover have "set Q \ carrier M" and "set R \ carrier M" + using Q(1) R(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto + ultimately have "Id.normalize (\ S) = Q \\<^bsub>poly_ring image_poly\<^esub> R" + using Id.poly_mult_hom'[of Q R] unfolding univ_poly_mult by simp + moreover have "\ S \ carrier (poly_ring M)" + using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \_def . + hence "\ S \ carrier (poly_ring image_poly)" + using polynomial_hom[OF Id.homh M.field_axioms is_field] by simp + hence "Id.normalize (\ S) = \ S" + using Id.normalize_polynomial unfolding sym[OF univ_poly_carrier] by simp + ultimately show ?thesis + using poly_hom[OF Q(1)] poly_hom[OF R(1)] + unfolding pdivides_def factor_def univ_poly_mult by auto + qed + moreover have "Q \ carrier (poly_ring (image_poly))" + using poly_hom[OF Q(1)] by simp + ultimately show ?thesis + using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF is_field], of Q] by auto + qed + thus "\\<^bsub>S\<^esub> \ carrier image_poly" and "Id.eval (\ S) \\<^bsub>S\<^esub> = \\<^bsub>image_poly\<^esub>" + by auto + qed + ultimately have "law_restrict M = law_restrict image_poly" + using assms(2) by simp + hence "carrier M = carrier image_poly" + unfolding law_restrict_def by (simp add:ring.defs) + moreover have "\\<^bsub>P\<^esub> \ carrier image_poly" + using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp + moreover have "\\<^bsub>P\<^esub> \ carrier M" + using indexed_var_not_index_free[of P] hyps(3) by blast + ultimately show False by simp +qed + +lemma (in field) exists_extension_with_roots: + shows "\L \ extensions. \P \ carrier (poly_ring R). + degree P > 0 \ (\x \ carrier L. (ring.eval L) (\ P) x = \\<^bsub>L\<^esub>)" +proof - + obtain M where "M \ extensions" and "\L \ extensions. M \ L \ law_restrict L = law_restrict M" + using exists_maximal_extension iso_incl_hom by blast + thus ?thesis + using exists_root[of M] by auto +qed + + +subsection \Existence of Algebraic Closure\ + +locale algebraic_closure = field L + subfield K L for L (structure) and K + + assumes algebraic_extension: "x \ carrier L \ (algebraic over K) x" + and roots_over_subfield: "\ P \ carrier (K[X]); degree P > 0 \ \ \x \ carrier L. eval P x = \\<^bsub>L\<^esub>" + +locale algebraically_closed = field L for L (structure) + + assumes roots_over_carrier: "\ P \ carrier (poly_ring L); degree P > 0 \ \ \x \ carrier L. eval P x = \\<^bsub>L\<^esub>" + +definition (in field) closure :: "(('a list) multiset \ 'a) ring" ("\") + where "closure = (SOME L \ \such that\. + \ \i\ algebraic_closure L (indexed_const ` (carrier R)) \ + \ \ii\ indexed_const \ ring_hom R L)" + + +lemma algebraic_hom: + assumes "h \ ring_hom R S" and "field R" and "field S" and "subfield K R" and "x \ carrier R" + shows "((ring.algebraic R) over K) x \ ((ring.algebraic S) over (h ` K)) (h x)" +proof - + interpret Hom: ring_hom_ring R S h + using ring_hom_ringI2[OF assms(2-3)[THEN field.is_ring] assms(1)] . + assume "(Hom.R.algebraic over K) x" + then obtain p where p: "p \ carrier (K[X]\<^bsub>R\<^esub>)" and "p \ []" and eval: "Hom.R.eval p x = \\<^bsub>R\<^esub>" + using domain.algebraicE[OF field.axioms(1) subfieldE(1), of R K x] assms(2,4-5) by auto + hence "(map h p) \ carrier ((h ` K)[X]\<^bsub>S\<^esub>)" and "(map h p) \ []" + using Hom.subfield_polynomial_hom[OF assms(4) one_not_zero[OF assms(3)]] by auto + moreover have "Hom.S.eval (map h p) (h x) = \\<^bsub>S\<^esub>" + using Hom.eval_hom[OF subfieldE(1)[OF assms(4)] assms(5) p] unfolding eval by simp + ultimately show ?thesis + using Hom.S.non_trivial_ker_imp_algebraic[of "h ` K" "h x"] unfolding a_kernel_def' by auto +qed + +lemma (in field) exists_closure: + obtains L :: "(('a list multiset) \ 'a) ring" + where "algebraic_closure L (indexed_const ` (carrier R))" and "indexed_const \ ring_hom R L" +proof - + obtain L where "L \ extensions" + and roots: "\P. \ P \ carrier (poly_ring R); degree P > 0 \ \ + \x \ carrier L. (ring.eval L) (\ P) x = \\<^bsub>L\<^esub>" + using exists_extension_with_roots by auto + + let ?K = "indexed_const ` (carrier R)" + let ?set_of_algs = "{ x \ carrier L. ((ring.algebraic L) over ?K) x }" + let ?M = "L \ carrier := ?set_of_algs \" + + from \L \ extensions\ + have L: "field L" and hom: "ring_hom_ring R L indexed_const" + using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto + have "subfield ?K L" + using ring_hom_ring.img_is_subfield(2)[OF hom carrier_is_subfield + domain.one_not_zero[OF field.axioms(1)[OF L]]] by auto + hence set_of_algs: "subfield ?set_of_algs L" + using field.subfield_of_algebraics[OF L, of ?K] by simp + have M: "field ?M" + using ring.subfield_iff(2)[OF field.is_ring[OF L] set_of_algs] by simp + + interpret Id: ring_hom_ring ?M L id + using ring_hom_ringI[OF field.is_ring[OF M] field.is_ring[OF L]] by auto + + have is_subfield: "subfield ?K ?M" + proof (intro ring.subfield_iff(1)[OF field.is_ring[OF M]]) + have "L \ carrier := ?K \ = ?M \ carrier := ?K \" + by simp + moreover from \subfield ?K L\ have "field (L \ carrier := ?K \)" + using ring.subfield_iff(2)[OF field.is_ring[OF L]] by simp + ultimately show "field (?M \ carrier := ?K \)" + by simp + next + show "?K \ carrier ?M" + proof + fix x :: "('a list multiset) \ 'a" + assume "x \ ?K" + hence "x \ carrier L" + using ring_hom_memE(1)[OF ring_hom_ring.homh[OF hom]] by auto + moreover from \subfield ?K L\ and \x \ ?K\ have "(Id.S.algebraic over ?K) x" + using domain.algebraic_self[OF field.axioms(1)[OF L] subfieldE(1)] by auto + ultimately show "x \ carrier ?M" + by auto + qed + qed + + have "algebraic_closure ?M ?K" + proof (intro algebraic_closure.intro[OF M is_subfield]) + have "(Id.R.algebraic over ?K) x" if "x \ carrier ?M" for x + using that Id.S.algebraic_consistent[OF subfieldE(1)[OF set_of_algs]] by simp + moreover have "\x \ carrier ?M. Id.R.eval P x = \\<^bsub>?M\<^esub>" + if "P \ carrier (?K[X]\<^bsub>?M\<^esub>)" and "degree P > 0" for P + proof - + from \P \ carrier (?K[X]\<^bsub>?M\<^esub>)\ have "P \ carrier (?K[X]\<^bsub>L\<^esub>)" + unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] . + hence "set P \ ?K" + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "\Q. set Q \ carrier R \ P = \ Q" + proof (induct P, simp add: \_def) + case (Cons p P) + then obtain q Q where "q \ carrier R" "set Q \ carrier R" and "\ Q = P""indexed_const q = p" + unfolding \_def by auto + hence "set (q # Q) \ carrier R" and "\ (q # Q) = (p # P)" + unfolding \_def by auto + thus ?case + by metis + qed + then obtain Q where "set Q \ carrier R" and "\ Q = P" + by auto + moreover have "lead_coeff Q \ \" + proof (rule ccontr) + assume "\ lead_coeff Q \ \" then have "lead_coeff Q = \" + by simp + with \\ Q = P\ and \degree P > 0\ have "lead_coeff P = indexed_const \" + unfolding \_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3)) + hence "lead_coeff P = \\<^bsub>L\<^esub>" + using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto + with \degree P > 0\ have "\ P \ carrier (?K[X]\<^bsub>?M\<^esub>)" + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + with \P \ carrier (?K[X]\<^bsub>?M\<^esub>)\ show False + by simp + qed + ultimately have "Q \ carrier (poly_ring R)" + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + moreover from \degree P > 0\ and \\ Q = P\ have "degree Q > 0" + unfolding \_def by auto + ultimately obtain x where "x \ carrier L" and "Id.S.eval P x = \\<^bsub>L\<^esub>" + using roots[of Q] unfolding \\ Q = P\ by auto + hence "Id.R.eval P x = \\<^bsub>?M\<^esub>" + unfolding Id.S.eval_consistent[OF subfieldE(1)[OF set_of_algs]] by simp + moreover from \degree P > 0\ have "P \ []" + by auto + with \P \ carrier (?K[X]\<^bsub>L\<^esub>)\ and \Id.S.eval P x = \\<^bsub>L\<^esub>\ have "(Id.S.algebraic over ?K) x" + using Id.S.non_trivial_ker_imp_algebraic[of ?K x] unfolding a_kernel_def' by auto + with \x \ carrier L\ have "x \ carrier ?M" + by auto + ultimately show ?thesis + by auto + qed + ultimately show "algebraic_closure_axioms ?M ?K" + unfolding algebraic_closure_axioms_def by auto + qed + moreover have "indexed_const \ ring_hom R ?M" + using ring_hom_ring.homh[OF hom] subfieldE(3)[OF is_subfield] + unfolding subset_iff ring_hom_def by auto + ultimately show thesis + using that by auto +qed + +lemma (in field) closureE: + shows "algebraic_closure \ (indexed_const ` (carrier R))" and "indexed_const \ ring_hom R \" + using exists_closure unfolding closure_def + by (metis (mono_tags, lifting) someI2)+ + +end + diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Embedded_Algebras.thy --- a/src/HOL/Algebra/Embedded_Algebras.thy Sat Apr 13 22:06:40 2019 +0200 +++ b/src/HOL/Algebra/Embedded_Algebras.thy Sun Apr 14 12:00:17 2019 +0100 @@ -49,6 +49,16 @@ subsection \Basic Properties - First Part\ +lemma line_extension_consistent: + assumes "subring K R" shows "ring.line_extension (R \ carrier := K \) = line_extension" + unfolding ring.line_extension_def[OF subring_is_ring[OF assms]] line_extension_def + by (simp add: set_add_def set_mult_def) + +lemma Span_consistent: + assumes "subring K R" shows "ring.Span (R \ carrier := K \) = Span" + unfolding ring.Span.simps[OF subring_is_ring[OF assms]] Span.simps + line_extension_consistent[OF assms] by simp + lemma combine_in_carrier [simp, intro]: "\ set Ks \ carrier R; set Us \ carrier R \ \ combine Ks Us \ carrier R" by (induct Ks Us rule: combine.induct) (auto) @@ -71,6 +81,31 @@ "set Us \ carrier R \ combine (replicate (length Us) \) Us = \" by (induct Us) (auto) +lemma combine_take: + "combine (take (length Us) Ks) Us = combine Ks Us" + by (induct Us arbitrary: Ks) + (auto, metis combine.simps(1) list.exhaust take.simps(1) take_Suc_Cons) + +lemma combine_append_zero: + "set Us \ carrier R \ combine (Ks @ [ \ ]) Us = combine Ks Us" +proof (induct Ks arbitrary: Us) + case Nil thus ?case by (induct Us) (auto) +next + case Cons thus ?case by (cases Us) (auto) +qed + +lemma combine_prepend_replicate: + "\ set Ks \ carrier R; set Us \ carrier R \ \ + combine ((replicate n \) @ Ks) Us = combine Ks (drop n Us)" +proof (induct n arbitrary: Us, simp) + case (Suc n) thus ?case + by (cases Us) (auto, meson combine_in_carrier ring_simprules(8) set_drop_subset subset_trans) +qed + +lemma combine_append_replicate: + "set Us \ carrier R \ combine (Ks @ (replicate n \)) Us = combine Ks Us" + by (induct n) (auto, metis append.assoc combine_append_zero replicate_append_same) + lemma combine_append: assumes "length Ks = length Us" and "set Ks \ carrier R" "set Us \ carrier R" @@ -119,6 +154,36 @@ finally show ?case . qed +lemma combine_normalize: + assumes "set Ks \ carrier R" "set Us \ carrier R" "combine Ks Us = a" + obtains Ks' + where "set (take (length Us) Ks) \ set Ks'" "set Ks' \ set (take (length Us) Ks) \ { \ }" + and "length Ks' = length Us" "combine Ks' Us = a" +proof - + define Ks' + where "Ks' = (if length Ks \ length Us + then Ks @ (replicate (length Us - length Ks) \) else take (length Us) Ks)" + hence "set (take (length Us) Ks) \ set Ks'" "set Ks' \ set (take (length Us) Ks) \ { \ }" + "length Ks' = length Us" "a = combine Ks' Us" + using combine_append_replicate[OF assms(2)] combine_take assms(3) by auto + thus thesis + using that by blast +qed + +lemma line_extension_mem_iff: "u \ line_extension K a E \ (\k \ K. \v \ E. u = k \ a \ v)" + unfolding line_extension_def set_add_def'[of R "K #> a" E] unfolding r_coset_def by blast + +lemma line_extension_in_carrier: + assumes "K \ carrier R" "a \ carrier R" "E \ carrier R" + shows "line_extension K a E \ carrier R" + using set_add_closed[OF r_coset_subset_G[OF assms(1-2)] assms(3)] + by (simp add: line_extension_def) + +lemma Span_in_carrier: + assumes "K \ carrier R" "set Us \ carrier R" + shows "Span K Us \ carrier R" + using assms by (induct Us) (auto simp add: line_extension_in_carrier) + subsection \Some Basic Properties of Linear Independence\ @@ -131,10 +196,18 @@ "independent K (u # Us) \ u \ carrier R" by (cases rule: independent.cases, auto)+ +lemma dimension_independent [intro]: "independent K Us \ dimension (length Us) K (Span K Us)" +proof (induct Us) + case Nil thus ?case by simp +next + case Cons thus ?case + using Suc_dim independent_backwards[OF Cons(2)] by auto +qed + text \Now, we fix K, a subfield of the ring. Many lemmas would also be true for weaker structures, but our interest is to work with subfields, so generalization could - be the subjuct of a future work.\ + be the subject of a future work.\ context fixes K :: "'a set" assumes K: "subfield K R" @@ -146,9 +219,6 @@ lemmas subring_props [simp] = subringE[OF subfieldE(1)[OF K]] -lemma line_extension_mem_iff: "u \ line_extension K a E \ (\k \ K. \v \ E. u = k \ a \ v)" - unfolding line_extension_def set_add_def'[of R "K #> a" E] unfolding r_coset_def by blast - lemma line_extension_is_subgroup: assumes "subgroup E (add_monoid R)" "a \ carrier R" shows "subgroup (line_extension K a E) (add_monoid R)" @@ -325,6 +395,28 @@ subsubsection \Corollaries\ +corollary Span_mem_iff_length_version: + assumes "set Us \ carrier R" + shows "a \ Span K Us \ (\Ks. set Ks \ K \ length Ks = length Us \ a = combine Ks Us)" + using Span_eq_combine_set_length_version[OF assms] by blast + +corollary Span_mem_imp_non_trivial_combine: + assumes "set Us \ carrier R" and "a \ Span K Us" + obtains k Ks + where "k \ K - { \ }" "set Ks \ K" "length Ks = length Us" "combine (k # Ks) (a # Us) = \" +proof - + obtain Ks where Ks: "set Ks \ K" "length Ks = length Us" "a = combine Ks Us" + using Span_mem_iff_length_version[OF assms(1)] assms(2) by auto + hence "((\ \) \ a) \ a = combine ((\ \) # Ks) (a # Us)" + by auto + moreover have "((\ \) \ a) \ a = \" + using assms(2) Span_subgroup_props(1)[OF assms(1)] l_minus l_neg by auto + moreover have "\ \ \ \" + using subfieldE(6)[OF K] l_neg by force + ultimately show ?thesis + using that subring_props(3,5) Ks(1-2) by (force simp del: combine.simps) +qed + corollary Span_mem_iff: assumes "set Us \ carrier R" and "a \ carrier R" shows "a \ Span K Us \ (\k \ K - { \ }. \Ks. set Ks \ K \ combine (k # Ks) (a # Us) = \)" @@ -355,11 +447,6 @@ using Span_m_inv_simprule[OF assms(1) _ assms(2), of k] k by auto qed -corollary Span_mem_iff_length_version: - assumes "set Us \ carrier R" - shows "a \ Span K Us \ (\Ks. set Ks \ K \ length Ks = length Us \ a = combine Ks Us)" - using Span_eq_combine_set_length_version[OF assms] by blast - subsection \Span as the minimal subgroup that contains \<^term>\K <#> (set Us)\\ @@ -525,7 +612,7 @@ fix v assume "v \ line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)" then obtain k u' v' where v: "k \ K" "u' \ Span K Us" "v' \ Span K Vs" "v = k \ u \ (u' \ v')" - using line_extension_mem_iff[of v u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"] + using line_extension_mem_iff[of v _ u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"] unfolding set_add_def' by blast hence "v = (k \ u \ u') \ v'" using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1) @@ -541,12 +628,12 @@ fix v assume "v \ Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs" then obtain k u' v' where v: "k \ K" "u' \ Span K Us" "v' \ Span K Vs" "v = (k \ u \ u') \ v'" - using line_extension_mem_iff[of _ u "Span K Us"] unfolding set_add_def' by auto + using line_extension_mem_iff[of _ _ u "Span K Us"] unfolding set_add_def' by auto hence "v = (k \ u) \ (u' \ v')" using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1) by (metis (no_types, lifting) rev_subsetD ring_simprules(5,7)) thus "v \ line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)" - using line_extension_mem_iff[of "(k \ u) \ (u' \ v')" u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"] + using line_extension_mem_iff[of "(k \ u) \ (u' \ v')" K u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"] unfolding set_add_def' using v by auto qed qed @@ -571,7 +658,7 @@ by auto qed -lemma independent_strinct_incl: +lemma independent_strict_incl: assumes "independent K (u # Us)" shows "Span K Us \ Span K (u # Us)" proof - have "u \ Span K (u # Us)" @@ -588,7 +675,7 @@ proof - assume "Span K (u # Us) \ Span K Vs" hence "Span K Us \ Span K Vs" - using independent_strinct_incl[OF assms(1)] by auto + using independent_strict_incl[OF assms(1)] by auto then obtain v where v: "v \ set Vs" "v \ Span K Us" using Span_strict_incl[of Us Vs] assms[THEN independent_in_carrier] by auto thus ?thesis @@ -638,7 +725,7 @@ where u': "u' \ Span K Us" "u' \ carrier R" and v': "v' \ Span K Vs" "v' \ carrier R" "v' \ \" and k: "k \ K" "(k \ u \ u') = v'" - using line_extension_mem_iff[of _ u "Span K Us"] in_carrier(2-3)[THEN Span_subgroup_props(1)] + using line_extension_mem_iff[of _ _ u "Span K Us"] in_carrier(2-3)[THEN Span_subgroup_props(1)] subring_props(1) by force hence "v' = \" if "k = \" using in_carrier(1) that IH by auto @@ -735,6 +822,11 @@ qed qed +lemma non_trivial_combine_imp_dependent: + assumes "set Ks \ K" and "combine Ks Us = \" and "\ set (take (length Us) Ks) \ { \ }" + shows "dependent K Us" + using independent_imp_trivial_combine[OF _ assms(1-2)] assms(3) by blast + lemma trivial_combine_imp_independent: assumes "set Us \ carrier R" and "\Ks. \ set Ks \ K; combine Ks Us = \ \ \ set (take (length Us) Ks) \ { \ }" @@ -773,6 +865,27 @@ using li_Cons[OF u] by simp qed +corollary dependent_imp_non_trivial_combine: + assumes "set Us \ carrier R" and "dependent K Us" + obtains Ks where "length Ks = length Us" "combine Ks Us = \" "set Ks \ K" "set Ks \ { \ }" +proof - + obtain Ks + where Ks: "set Ks \ carrier R" "set Ks \ K" "combine Ks Us = \" "\ set (take (length Us) Ks) \ { \ }" + using trivial_combine_imp_independent[OF assms(1)] assms(2) subring_props(1) by blast + obtain Ks' + where Ks': "set (take (length Us) Ks) \ set Ks'" "set Ks' \ set (take (length Us) Ks) \ { \ }" + "length Ks' = length Us" "combine Ks' Us = \" + using combine_normalize[OF Ks(1) assms(1) Ks(3)] by metis + have "set (take (length Us) Ks) \ set Ks" + by (simp add: set_take_subset) + hence "set Ks' \ K" + using Ks(2) Ks'(2) subring_props(2) Un_commute by blast + moreover have "set Ks' \ { \ }" + using Ks'(1) Ks(4) by auto + ultimately show thesis + using that Ks' by blast +qed + corollary unique_decomposition: assumes "independent K Us" shows "a \ Span K Us \ \!Ks. set Ks \ K \ length Ks = length Us \ a = combine Ks Us" @@ -964,7 +1077,7 @@ thus ?case by blast qed -lemma dimension_zero [intro]: "dimension 0 K E \ E = { \ }" +lemma dimension_zero: "dimension 0 K E \ E = { \ }" proof - assume "dimension 0 K E" then obtain Vs where "length Vs = 0" "Span K Vs = E" @@ -973,12 +1086,12 @@ by auto qed -lemma dimension_independent [intro]: "independent K Us \ dimension (length Us) K (Span K Us)" -proof (induct Us) - case Nil thus ?case by simp -next - case Cons thus ?case - using Suc_dim[OF independent_backwards(3,1)[OF Cons(2)]] by auto +lemma dimension_one [iff]: "dimension 1 K K" +proof - + have "K = Span K [ \ ]" + using line_extension_mem_iff[of _ K \ "{ \ }"] subfieldE(3)[OF K] by (auto simp add: rev_subsetD) + thus ?thesis + using dimension.Suc_dim[OF one_closed _ dimension.zero_dim, of K] subfieldE(6)[OF K] by auto qed lemma dimensionI: @@ -1081,6 +1194,37 @@ using aux_lemma[OF _ assms(2-3)] by auto qed +lemma filter_base: + assumes "set Us \ carrier R" + obtains Vs where "set Vs \ carrier R" and "independent K Vs" and "Span K Vs = Span K Us" +proof - + from \set Us \ carrier R\ have "\Vs. independent K Vs \ Span K Vs = Span K Us" + proof (induction Us) + case Nil thus ?case by auto + next + case (Cons u Us) + then obtain Vs where Vs: "independent K Vs" "Span K Vs = Span K Us" + by auto + show ?case + proof (cases "u \ Span K Us") + case True + hence "Span K (u # Us) = Span K Us" + using Span_base_incl mono_Span_subset + by (metis Cons.prems insert_subset list.simps(15) subset_antisym) + thus ?thesis + using Vs by blast + next + case False + hence "Span K (u # Vs) = Span K (u # Us)" and "independent K (u # Vs)" + using li_Cons[of u K Vs] Cons(2) Vs by auto + thus ?thesis + by blast + qed + qed + thus ?thesis + using independent_in_carrier that by auto +qed + lemma dimension_backwards: "dimension (Suc n) K E \ \v \ carrier R. \E'. dimension n K E' \ v \ E' \ E = line_extension K v E'" by (cases rule: dimension.cases) (auto) @@ -1123,7 +1267,7 @@ hence dim: "dimension (n + m - k) K (Span K (Us @ (Vs @ Bs)))" using independent_append[OF independent_split(2)[OF Us(2)] Vs(2)] Us(1) Vs(1) Bs(2) - dimension_independent[of "Us @ (Vs @ Bs)"] by auto + dimension_independent[of K "Us @ (Vs @ Bs)"] by auto have "(Span K Us) <+>\<^bsub>R\<^esub> F \ E <+>\<^bsub>R\<^esub> F" using mono_Span_append(1)[OF in_carrier(1) Bs(1)] Us(3) unfolding set_add_def' by auto @@ -1149,9 +1293,10 @@ thus ?thesis using dim by simp qed -end +end (* of fixed K context. *) -end +end (* of ring context. *) + lemma (in ring) telescopic_base_aux: assumes "subfield K R" "subfield F R" @@ -1186,7 +1331,7 @@ proof fix v assume "v \ E" then obtain f where f: "f \ F" "v = f \ u \ \" - using u(1,3) line_extension_mem_iff[OF assms(2)] by auto + using u(1,3) line_extension_mem_iff by auto then obtain Ks where Ks: "set Ks \ K" "f = combine Ks Us" using Span_eq_combine_set[OF assms(1) Us(1)] Us(4) by auto have "v = f \ u" @@ -1209,7 +1354,7 @@ ultimately have "v = (combine Ks Us) \ u \ \" and "combine Ks Us \ F" using subring_props(1)[OF assms(2)] u(1) by auto thus "v \ E" - using u(3) line_extension_mem_iff[OF assms(2)] by auto + using u(3) line_extension_mem_iff by auto qed ultimately have "Span K (map (\u'. u' \ u) Us) = E" by auto thus ?thesis @@ -1234,9 +1379,9 @@ hence li: "independent F [ v ]" "independent F Vs'" and inter: "Span F [ v ] \ Span F Vs' = { \ }" using Vs(3) independent_split[OF assms(2), of "[ v ]" Vs'] by auto have "dimension n K (Span F [ v ])" - using dimension_independent[OF assms(2) li(1)] telescopic_base_aux[OF assms(1-3)] by simp + using dimension_independent[OF li(1)] telescopic_base_aux[OF assms(1-3)] by simp moreover have "dimension (n * m) K (Span F Vs')" - using Suc(1) dimension_independent[OF assms(2) li(2)] Vs(2) unfolding v by auto + using Suc(1) dimension_independent[OF li(2)] Vs(2) unfolding v by auto ultimately have "dimension (n * Suc m) K (Span F [ v ] <+>\<^bsub>R\<^esub> Span F Vs')" using dimension_direct_sum_space[OF assms(1) _ _ inter] by auto thus "dimension (n * Suc m) K E" @@ -1244,70 +1389,387 @@ qed -(* -lemma combine_take: - assumes "set Ks \ carrier R" "set Us \ carrier R" - shows "length Ks \ length Us \ combine Ks Us = combine Ks (take (length Ks) Us)" - and "length Us \ length Ks \ combine Ks Us = combine (take (length Us) Ks) Us" +context ring_hom_ring +begin + +lemma combine_hom: + "\ set Ks \ carrier R; set Us \ carrier R \ \ combine (map h Ks) (map h Us) = h (R.combine Ks Us)" + by (induct Ks Us rule: R.combine.induct) (auto) + +lemma line_extension_hom: + assumes "K \ carrier R" "a \ carrier R" "E \ carrier R" + shows "line_extension (h ` K) (h a) (h ` E) = h ` R.line_extension K a E" + using set_add_hom[OF homh R.r_coset_subset_G[OF assms(1-2)] assms(3)] + coset_hom(2)[OF ring_hom_in_hom(1)[OF homh] assms(1-2)] + unfolding R.line_extension_def S.line_extension_def + by simp + +lemma Span_hom: + assumes "K \ carrier R" "set Us \ carrier R" + shows "Span (h ` K) (map h Us) = h ` R.Span K Us" + using assms line_extension_hom R.Span_in_carrier by (induct Us) (auto) + +lemma inj_on_subgroup_iff_trivial_ker: + assumes "subgroup H (add_monoid R)" + shows "inj_on h H \ a_kernel (R \ carrier := H \) S h = { \ }" + using group_hom.inj_on_subgroup_iff_trivial_ker[OF a_group_hom assms] + unfolding a_kernel_def[of "R \ carrier := H \" S h] by simp + +corollary inj_on_Span_iff_trivial_ker: + assumes "subfield K R" "set Us \ carrier R" + shows "inj_on h (R.Span K Us) \ a_kernel (R \ carrier := R.Span K Us \) S h = { \ }" + using inj_on_subgroup_iff_trivial_ker[OF R.Span_is_add_subgroup[OF assms]] . + + +context + fixes K :: "'a set" assumes K: "subfield K R" and one_zero: "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>" +begin + +lemma inj_hom_preserves_independent: + assumes "inj_on h (R.Span K Us)" + and "R.independent K Us" shows "independent (h ` K) (map h Us)" +proof (rule ccontr) + have in_carrier: "set Us \ carrier R" "set (map h Us) \ carrier S" + using R.independent_in_carrier[OF assms(2)] by auto + + assume ld: "dependent (h ` K) (map h Us)" + obtain Ks :: "'c list" + where Ks: "length Ks = length Us" "combine Ks (map h Us) = \\<^bsub>S\<^esub>" "set Ks \ h ` K" "set Ks \ { \\<^bsub>S\<^esub> }" + using dependent_imp_non_trivial_combine[OF img_is_subfield(2)[OF K one_zero] in_carrier(2) ld] + by (metis length_map) + obtain Ks' where Ks': "set Ks' \ K" "Ks = map h Ks'" + using Ks(3) by (induct Ks) (auto, metis insert_subset list.simps(15,9)) + hence "h (R.combine Ks' Us) = \\<^bsub>S\<^esub>" + using combine_hom[OF _ in_carrier(1)] Ks(2) subfieldE(3)[OF K] by (metis subset_trans) + moreover have "R.combine Ks' Us \ R.Span K Us" + using R.Span_eq_combine_set[OF K in_carrier(1)] Ks'(1) by auto + ultimately have "R.combine Ks' Us = \" + using assms hom_zero R.Span_subgroup_props(2)[OF K in_carrier(1)] by (auto simp add: inj_on_def) + hence "set Ks' \ { \ }" + using R.independent_imp_trivial_combine[OF K assms(2)] Ks' Ks(1) + by (metis length_map order_refl take_all) + hence "set Ks \ { \\<^bsub>S\<^esub> }" + unfolding Ks' using hom_zero by (induct Ks') (auto) + hence "Ks = []" + using Ks(4) by (metis set_empty2 subset_singletonD) + hence "independent (h ` K) (map h Us)" + using independent.li_Nil Ks(1) by simp + from \dependent (h ` K) (map h Us)\ and this show False by simp +qed + +corollary inj_hom_dimension: + assumes "inj_on h E" + and "R.dimension n K E" shows "dimension n (h ` K) (h ` E)" +proof - + obtain Us + where Us: "set Us \ carrier R" "R.independent K Us" "length Us = n" "R.Span K Us = E" + using R.exists_base[OF K assms(2)] by blast + hence "dimension n (h ` K) (Span (h ` K) (map h Us))" + using dimension_independent[OF inj_hom_preserves_independent[OF _ Us(2)]] assms(1) by auto + thus ?thesis + using Span_hom[OF subfieldE(3)[OF K] Us(1)] Us(4) by simp +qed + +corollary rank_nullity_theorem: + assumes "R.dimension n K E" and "R.dimension m K (a_kernel (R \ carrier := E \) S h)" + shows "dimension (n - m) (h ` K) (h ` E)" proof - - assume len: "length Ks \ length Us" - hence Us: "Us = (take (length Ks) Us) @ (drop (length Ks) Us)" by auto - hence set_t: "set (take (length Ks) Us) \ carrier R" and set_d: "set (drop (length Ks) Us) \ carrier R" - using assms(2) len by (metis le_sup_iff set_append)+ - hence "combine Ks Us = (combine Ks (take (length Ks) Us)) \ \" - using combine_append[OF _ assms(1), of "take (length Ks) Us" "[]" "drop (length Ks) Us"] len by auto - also have " ... = combine Ks (take (length Ks) Us)" - using combine_in_carrier[OF assms(1) set_t] by auto - finally show "combine Ks Us = combine Ks (take (length Ks) Us)" . -next - assume len: "length Us \ length Ks" - hence Us: "Ks = (take (length Us) Ks) @ (drop (length Us) Ks)" by auto - hence set_t: "set (take (length Us) Ks) \ carrier R" and set_d: "set (drop (length Us) Ks) \ carrier R" - using assms(1) len by (metis le_sup_iff set_append)+ - hence "combine Ks Us = (combine (take (length Us) Ks) Us) \ \" - using combine_append[OF _ _ assms(2), of "take (length Us) Ks" "drop (length Us) Ks" "[]"] len by auto - also have " ... = combine (take (length Us) Ks) Us" - using combine_in_carrier[OF set_t assms(2)] by auto - finally show "combine Ks Us = combine (take (length Us) Ks) Us" . + obtain Us + where Us: "set Us \ carrier R" "R.independent K Us" "length Us = m" + "R.Span K Us = a_kernel (R \ carrier := E \) S h" + using R.exists_base[OF K assms(2)] by blast + obtain Vs + where Vs: "R.independent K (Vs @ Us)" "length (Vs @ Us) = n" "R.Span K (Vs @ Us) = E" + using R.complete_base[OF K assms(1) Us(2)] R.Span_base_incl[OF K Us(1)] Us(4) + unfolding a_kernel_def' by auto + have set_Vs: "set Vs \ carrier R" + using R.independent_in_carrier[OF Vs(1)] by auto + have "R.Span K Vs \ a_kernel (R \ carrier := E \) S h = { \ }" + using R.independent_split[OF K Vs(1)] Us(4) by simp + moreover have "R.Span K Vs \ E" + using R.mono_Span_append(1)[OF K set_Vs Us(1)] Vs(3) by auto + ultimately have "a_kernel (R \ carrier := R.Span K Vs \) S h \ { \ }" + unfolding a_kernel_def' by (simp del: R.Span.simps, blast) + hence "a_kernel (R \ carrier := R.Span K Vs \) S h = { \ }" + using R.Span_subgroup_props(2)[OF K set_Vs] + unfolding a_kernel_def' by (auto simp del: R.Span.simps) + hence "inj_on h (R.Span K Vs)" + using inj_on_Span_iff_trivial_ker[OF K set_Vs] by simp + moreover have "R.dimension (n - m) K (R.Span K Vs)" + using R.dimension_independent[OF R.independent_split(2)[OF K Vs(1)]] Vs(2) Us(3) by auto + ultimately have "dimension (n - m) (h ` K) (h ` (R.Span K Vs))" + using assms(1) inj_hom_dimension by simp + + have "h ` E = h ` (R.Span K Vs <+>\<^bsub>R\<^esub> R.Span K Us)" + using R.Span_append_eq_set_add[OF K set_Vs Us(1)] Vs(3) by simp + hence "h ` E = h ` (R.Span K Vs) <+>\<^bsub>S\<^esub> h ` (R.Span K Us)" + using R.Span_subgroup_props(1)[OF K] set_Vs Us(1) set_add_hom[OF homh] by auto + moreover have "h ` (R.Span K Us) = { \\<^bsub>S\<^esub> }" + using R.space_subgroup_props(2)[OF K assms(1)] unfolding Us(4) a_kernel_def' by force + ultimately have "h ` E = h ` (R.Span K Vs) <+>\<^bsub>S\<^esub> { \\<^bsub>S\<^esub> }" + by simp + hence "h ` E = h ` (R.Span K Vs)" + using R.Span_subgroup_props(1-2)[OF K set_Vs] unfolding set_add_def' by force + + from \dimension (n - m) (h ` K) (h ` (R.Span K Vs))\ and this show ?thesis by simp qed -*) + +end (* of fixed K context. *) + +end (* of ring_hom_ring context. *) + +lemma (in ring_hom_ring) + assumes "subfield K R" and "set Us \ carrier R" and "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>" + and "independent (h ` K) (map h Us)" shows "R.independent K Us" +proof (rule ccontr) + assume "R.dependent K Us" + then obtain Ks + where "length Ks = length Us" and "R.combine Ks Us = \" and "set Ks \ K" and "set Ks \ { \ }" + using R.dependent_imp_non_trivial_combine[OF assms(1-2)] by metis + hence "combine (map h Ks) (map h Us) = \\<^bsub>S\<^esub>" + using combine_hom[OF _ assms(2), of Ks] subfieldE(3)[OF assms(1)] by simp + moreover from \set Ks \ K\ have "set (map h Ks) \ h ` K" + by (induction Ks) (auto) + moreover have "\ set (map h Ks) \ { h \ }" + proof (rule ccontr) + assume "\ \ set (map h Ks) \ { h \ }" then have "set (map h Ks) \ { h \ }" + by simp + moreover from \R.dependent K Us\ and \length Ks = length Us\ have "Ks \ []" + by auto + ultimately have "set (map h Ks) = { h \ }" + using subset_singletonD by fastforce + with \set Ks \ K\ have "set Ks = { \ }" + using inj_onD[OF _ _ _ subringE(2)[OF subfieldE(1)[OF assms(1)]], of h] + img_is_subfield(1)[OF assms(1,3)] subset_singletonD + by (induction Ks) (auto simp add: subset_singletonD, fastforce) + with \set Ks \ { \ }\ show False + by simp + qed + with \length Ks = length Us\ have "\ set (take (length (map h Us)) (map h Ks)) \ { h \ }" + by auto + ultimately have "dependent (h ` K) (map h Us)" + using non_trivial_combine_imp_dependent[OF img_is_subfield(2)[OF assms(1,3)], of "map h Ks"] by simp + with \independent (h ` K) (map h Us)\ show False + by simp +qed + + +subsection \Finite Dimension\ + +definition (in ring) finite_dimension :: "'a set \ 'a set \ bool" + where "finite_dimension K E \ (\n. dimension n K E)" + +abbreviation (in ring) infinite_dimension :: "'a set \ 'a set \ bool" + where "infinite_dimension K E \ \ finite_dimension K E" + +definition (in ring) dim :: "'a set \ 'a set \ nat" + where "dim K E = (THE n. dimension n K E)" + +locale subalgebra = subgroup V "add_monoid R" for K and V and R (structure) + + assumes smult_closed: "\ k \ K; v \ V \ \ k \ v \ V" + + +subsubsection \Basic Properties\ + +lemma (in ring) unique_dimension: + assumes "subfield K R" and "finite_dimension K E" shows "\!n. dimension n K E" + using assms(2) dimension_is_inj[OF assms(1)] unfolding finite_dimension_def by auto + +lemma (in ring) finite_dimensionI: + assumes "dimension n K E" shows "finite_dimension K E" + using assms unfolding finite_dimension_def by auto -(* -lemma combine_normalize: - assumes "set Ks \ K" "set Us \ carrier R" "a = combine Ks Us" - shows "\Ks'. set Ks' \ K \ length Ks' = length Us \ a = combine Ks' Us" -proof (cases "length Ks \ length Us") - assume "\ length Ks \ length Us" - hence len: "length Us < length Ks" by simp - hence "length (take (length Us) Ks) = length Us" and "set (take (length Us) Ks) \ K" - using assms(1) by (auto, metis contra_subsetD in_set_takeD) - thus ?thesis - using combine_take(2)[OF _ assms(2), of Ks] assms(1,3) subring_props(1) len - by (metis dual_order.trans nat_less_le) +lemma (in ring) finite_dimensionE: + assumes "subfield K R" and "finite_dimension K E" shows "dimension ((dim over K) E) K E" + using theI'[OF unique_dimension[OF assms]] unfolding over_def dim_def by simp + +lemma (in ring) dimI: + assumes "subfield K R" and "dimension n K E" shows "(dim over K) E = n" + using finite_dimensionE[OF assms(1) finite_dimensionI] dimension_is_inj[OF assms(1)] assms(2) + unfolding over_def dim_def by auto + +lemma (in ring) finite_dimensionE' [elim]: + assumes "finite_dimension K E" and "\n. dimension n K E \ P" shows P + using assms unfolding finite_dimension_def by auto + +lemma (in ring) Span_finite_dimension: + assumes "subfield K R" and "set Us \ carrier R" + shows "finite_dimension K (Span K Us)" + using filter_base[OF assms] finite_dimensionI[OF dimension_independent[of K]] by metis + +lemma (in ring) carrier_is_subalgebra: + assumes "K \ carrier R" shows "subalgebra K (carrier R) R" + using assms subalgebra.intro[OF add.group_incl_imp_subgroup[of "carrier R"], of K] add.group_axioms + unfolding subalgebra_axioms_def by auto + +lemma (in ring) subalgebra_in_carrier: + assumes "subalgebra K V R" shows "V \ carrier R" + using subgroup.subset[OF subalgebra.axioms(1)[OF assms]] by simp + +lemma (in ring) subalgebra_inter: + assumes "subalgebra K V R" and "subalgebra K V' R" shows "subalgebra K (V \ V') R" + using add.subgroups_Inter_pair assms unfolding subalgebra_def subalgebra_axioms_def by auto + +lemma (in ring_hom_ring) img_is_subalgebra: + assumes "K \ carrier R" and "subalgebra K V R" shows "subalgebra (h ` K) (h ` V) S" +proof (intro subalgebra.intro) + have "group_hom (add_monoid R) (add_monoid S) h" + using ring_hom_in_hom(2)[OF homh] R.add.group_axioms add.group_axioms + unfolding group_hom_def group_hom_axioms_def by auto + thus "subgroup (h ` V) (add_monoid S)" + using group_hom.subgroup_img_is_subgroup[OF _ subalgebra.axioms(1)[OF assms(2)]] by force next - assume len: "length Ks \ length Us" - have Ks: "set Ks \ carrier R" and set_r: "set (replicate (length Us - length Ks) \) \ carrier R" - using assms subring_props(1) zero_closed by (metis dual_order.trans, auto) - moreover - have set_t: "set (take (length Ks) Us) \ carrier R" - and set_d: "set (drop (length Ks) Us) \ carrier R" - using assms(2) len dual_order.trans by (metis set_take_subset, metis set_drop_subset) - ultimately - have "combine (Ks @ (replicate (length Us - length Ks) \)) Us = - (combine Ks (take (length Ks) Us)) \ - (combine (replicate (length Us - length Ks) \) (drop (length Ks) Us))" - using combine_append[OF _ Ks set_t set_r set_d] len by auto - also have " ... = combine Ks (take (length Ks) Us)" - using combine_replicate[OF set_d] combine_in_carrier[OF Ks set_t] by auto - also have " ... = a" - using combine_take(1)[OF Ks assms(2) len] assms(3) by simp - finally have "combine (Ks @ (replicate (length Us - length Ks) \)) Us = a" . - moreover have "set (Ks @ (replicate (length Us - length Ks) \)) \ K" - using assms(1) subring_props(2) by auto - moreover have "length (Ks @ (replicate (length Us - length Ks) \)) = length Us" - using len by simp - ultimately show ?thesis by blast + show "subalgebra_axioms (h ` K) (h ` V) S" + using R.subalgebra_in_carrier[OF assms(2)] subalgebra.axioms(2)[OF assms(2)] assms(1) + unfolding subalgebra_axioms_def + by (auto, metis hom_mult image_eqI subset_iff) +qed + +lemma (in ring) ideal_is_subalgebra: + assumes "K \ carrier R" "ideal I R" shows "subalgebra K I R" + using ideal.axioms(1)[OF assms(2)] ideal.I_l_closed[OF assms(2)] assms(1) + unfolding subalgebra_def subalgebra_axioms_def additive_subgroup_def by auto + +lemma (in ring) Span_is_subalgebra: + assumes "subfield K R" "set Us \ carrier R" shows "subalgebra K (Span K Us) R" + using Span_smult_closed[OF assms] Span_is_add_subgroup[OF assms] + unfolding subalgebra_def subalgebra_axioms_def by auto + +lemma (in ring) finite_dimension_imp_subalgebra: + assumes "subfield K R" "finite_dimension K E" shows "subalgebra K E R" + using exists_base[OF assms(1) finite_dimensionE[OF assms]] Span_is_subalgebra[OF assms(1)] by auto + +lemma (in ring) subalgebra_Span_incl: + assumes "subfield K R" and "subalgebra K V R" "set Us \ V" shows "Span K Us \ V" +proof - + have "K <#> (set Us) \ V" + using subalgebra.smult_closed[OF assms(2)] assms(3) unfolding set_mult_def by blast + moreover have "set Us \ carrier R" + using subalgebra_in_carrier[OF assms(2)] assms(3) by auto + ultimately show ?thesis + using subalgebra.axioms(1)[OF assms(2)] Span_min[OF assms(1)] by blast +qed + +lemma (in ring) Span_subalgebra_minimal: + assumes "subfield K R" "set Us \ carrier R" + shows "Span K Us = \ { V. subalgebra K V R \ set Us \ V }" + using Span_is_subalgebra[OF assms] Span_base_incl[OF assms] subalgebra_Span_incl[OF assms(1)] + by blast + +lemma (in ring) Span_subalgebraI: + assumes "subfield K R" + and "subalgebra K E R" "set Us \ E" + and "\V. \ subalgebra K V R; set Us \ V \ \ E \ V" + shows "E = Span K Us" +proof - + have "\ { V. subalgebra K V R \ set Us \ V } = E" + using assms(2-4) by auto + thus "E = Span K Us" + using Span_subalgebra_minimal subalgebra_in_carrier[of K E] assms by auto qed -*) + +lemma (in ring) subalbegra_incl_imp_finite_dimension: + assumes "subfield K R" and "finite_dimension K E" + and "subalgebra K V R" "V \ E" shows "finite_dimension K V" +proof - + obtain n where n: "dimension n K E" + using assms(2) by auto + + define S where "S = { Us. set Us \ V \ independent K Us }" + have "length ` S \ {..n}" + unfolding S_def using independent_length_le_dimension[OF assms(1) n] assms(4) by auto + moreover have "[] \ S" + unfolding S_def by simp + hence "length ` S \ {}" by blast + ultimately obtain m where m: "m \ length ` S" and greatest: "\k. k \ length ` S \ k \ m" + by (meson Max_ge Max_in finite_atMost rev_finite_subset) + then obtain Us where Us: "set Us \ V" "independent K Us" "m = length Us" + unfolding S_def by auto + have "Span K Us = V" + proof (rule ccontr) + assume "\ Span K Us = V" then have "Span K Us \ V" + using subalgebra_Span_incl[OF assms(1,3) Us(1)] by blast + then obtain v where v:"v \ V" "v \ Span K Us" + by blast + hence "independent K (v # Us)" + using independent.li_Cons[OF _ _ Us(2)] subalgebra_in_carrier[OF assms(3)] by auto + hence "(v # Us) \ S" + unfolding S_def using Us(1) v(1) by auto + hence "length (v # Us) \ m" + using greatest by blast + moreover have "length (v # Us) = Suc m" + using Us(3) by auto + ultimately show False by simp + qed + thus ?thesis + using finite_dimensionI[OF dimension_independent[OF Us(2)]] by simp +qed + +lemma (in ring_hom_ring) infinite_dimension_hom: + assumes "subfield K R" and "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>" and "inj_on h E" and "subalgebra K E R" + shows "R.infinite_dimension K E \ infinite_dimension (h ` K) (h ` E)" +proof - + note subfield = img_is_subfield(2)[OF assms(1-2)] + + assume "R.infinite_dimension K E" + show "infinite_dimension (h ` K) (h ` E)" + proof (rule ccontr) + assume "\ infinite_dimension (h ` K) (h ` E)" + then obtain Vs where "set Vs \ carrier S" and "Span (h ` K) Vs = h ` E" + using exists_base[OF subfield] by blast + hence "set Vs \ h ` E" + using Span_base_incl[OF subfield] by blast + hence "\Us. set Us \ E \ Vs = map h Us" + by (induct Vs) (auto, metis insert_subset list.simps(9,15)) + then obtain Us where "set Us \ E" and "Vs = map h Us" + by blast + with \Span (h ` K) Vs = h ` E\ have "h ` (R.Span K Us) = h ` E" + using R.subalgebra_in_carrier[OF assms(4)] Span_hom assms(1) by auto + moreover from \set Us \ E\ have "R.Span K Us \ E" + using R.subalgebra_Span_incl assms(1-4) by blast + ultimately have "R.Span K Us = E" + proof (auto simp del: R.Span.simps) + fix a assume "a \ E" + with \h ` (R.Span K Us) = h ` E\ obtain b where "b \ R.Span K Us" and "h a = h b" + by auto + with \R.Span K Us \ E\ and \a \ E\ have "a = b" + using inj_onD[OF assms(3)] by auto + with \b \ R.Span K Us\ show "a \ R.Span K Us" + by simp + qed + with \set Us \ E\ have "R.finite_dimension K E" + using R.Span_finite_dimension[OF assms(1)] R.subalgebra_in_carrier[OF assms(4)] by auto + with \R.infinite_dimension K E\ show False + by simp + qed +qed + + +subsubsection \Reformulation of some lemmas in this new language.\ + +lemma (in ring) sum_space_dim: + assumes "subfield K R" "finite_dimension K E" "finite_dimension K F" + shows "finite_dimension K (E <+>\<^bsub>R\<^esub> F)" + and "((dim over K) (E <+>\<^bsub>R\<^esub> F)) = ((dim over K) E) + ((dim over K) F) - ((dim over K) (E \ F))" +proof - + obtain n m k where n: "dimension n K E" and m: "dimension m K F" and k: "dimension k K (E \ F)" + using assms(2-3) subalbegra_incl_imp_finite_dimension[OF assms(1-2) + subalgebra_inter[OF assms(2-3)[THEN finite_dimension_imp_subalgebra[OF assms(1)]]]] + by (meson inf_le1 finite_dimension_def) + hence "dimension (n + m - k) K (E <+>\<^bsub>R\<^esub> F)" + using dimension_sum_space[OF assms(1)] by simp + thus "finite_dimension K (E <+>\<^bsub>R\<^esub> F)" + and "((dim over K) (E <+>\<^bsub>R\<^esub> F)) = ((dim over K) E) + ((dim over K) F) - ((dim over K) (E \ F))" + using finite_dimensionI dimI[OF assms(1)] n m k by auto +qed + +lemma (in ring) telescopic_base_dim: + assumes "subfield K R" "subfield F R" and "finite_dimension K F" and "finite_dimension F E" + shows "finite_dimension K E" and "(dim over K) E = ((dim over K) F) * ((dim over F) E)" + using telescopic_base[OF assms(1-2) + finite_dimensionE[OF assms(1,3)] + finite_dimensionE[OF assms(2,4)]] + dimI[OF assms(1)] finite_dimensionI + by auto end diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Finite_Extensions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Finite_Extensions.thy Sun Apr 14 12:00:17 2019 +0100 @@ -0,0 +1,810 @@ +(* Title: HOL/Algebra/Finite_Extensions.thy + Author: Paulo Emílio de Vilhena +*) + +theory Finite_Extensions + imports Embedded_Algebras Polynomials Polynomial_Divisibility + +begin + +section \Finite Extensions\ + +subsection \Definitions\ + +definition (in ring) transcendental :: "'a set \ 'a \ bool" + where "transcendental K x \ inj_on (\p. eval p x) (carrier (K[X]))" + +abbreviation (in ring) algebraic :: "'a set \ 'a \ bool" + where "algebraic K x \ \ transcendental K x" + +definition (in ring) Irr :: "'a set \ 'a \ 'a list" + where "Irr K x = (THE p. p \ carrier (K[X]) \ pirreducible K p \ eval p x = \ \ lead_coeff p = \)" + +inductive_set (in ring) simple_extension :: "'a set \ 'a \ 'a set" + for K and x where + zero [simp, intro]: "\ \ simple_extension K x" | + lin: "\ k1 \ simple_extension K x; k2 \ K \ \ (k1 \ x) \ k2 \ simple_extension K x" + +fun (in ring) finite_extension :: "'a set \ 'a list \ 'a set" + where "finite_extension K xs = foldr (\x K'. simple_extension K' x) xs K" + + +subsection \Basic Properties\ + +lemma (in ring) transcendental_consistent: + assumes "subring K R" shows "transcendental = ring.transcendental (R \ carrier := K \)" + unfolding transcendental_def ring.transcendental_def[OF subring_is_ring[OF assms]] + univ_poly_consistent[OF assms] eval_consistent[OF assms] .. + +lemma (in ring) algebraic_consistent: + assumes "subring K R" shows "algebraic = ring.algebraic (R \ carrier := K \)" + unfolding over_def transcendental_consistent[OF assms] .. + +lemma (in ring) eval_transcendental: + assumes "(transcendental over K) x" "p \ carrier (K[X])" "eval p x = \" shows "p = []" +proof - + have "[] \ carrier (K[X])" and "eval [] x = \" + by (auto simp add: univ_poly_def) + thus ?thesis + using assms unfolding over_def transcendental_def inj_on_def by auto +qed + +lemma (in ring) transcendental_imp_trivial_ker: + shows "(transcendental over K) x \ a_kernel (K[X]) R (\p. eval p x) = { [] }" + using eval_transcendental unfolding a_kernel_def' by (auto simp add: univ_poly_def) + +lemma (in ring) non_trivial_ker_imp_algebraic: + shows "a_kernel (K[X]) R (\p. eval p x) \ { [] } \ (algebraic over K) x" + using transcendental_imp_trivial_ker unfolding over_def by auto + +lemma (in domain) trivial_ker_imp_transcendental: + assumes "subring K R" and "x \ carrier R" + shows "a_kernel (K[X]) R (\p. eval p x) = { [] } \ (transcendental over K) x" + using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] + unfolding transcendental_def over_def by (simp add: univ_poly_zero) + +lemma (in domain) algebraic_imp_non_trivial_ker: + assumes "subring K R" and "x \ carrier R" + shows "(algebraic over K) x \ a_kernel (K[X]) R (\p. eval p x) \ { [] }" + using trivial_ker_imp_transcendental[OF assms] unfolding over_def by auto + +lemma (in domain) algebraicE: + assumes "subring K R" and "x \ carrier R" "(algebraic over K) x" + obtains p where "p \ carrier (K[X])" "p \ []" "eval p x = \" +proof - + have "[] \ a_kernel (K[X]) R (\p. eval p x)" + unfolding a_kernel_def' univ_poly_def by auto + then obtain p where "p \ carrier (K[X])" "p \ []" "eval p x = \" + using algebraic_imp_non_trivial_ker[OF assms] unfolding a_kernel_def' by blast + thus thesis using that by auto +qed + +lemma (in ring) algebraicI: + assumes "p \ carrier (K[X])" "p \ []" and "eval p x = \" shows "(algebraic over K) x" + using assms non_trivial_ker_imp_algebraic unfolding a_kernel_def' by auto + +lemma (in ring) transcendental_mono: + assumes "K \ K'" "(transcendental over K') x" shows "(transcendental over K) x" +proof - + have "carrier (K[X]) \ carrier (K'[X])" + using assms(1) unfolding univ_poly_def polynomial_def by auto + thus ?thesis + using assms unfolding over_def transcendental_def by (metis inj_on_subset) +qed + +corollary (in ring) algebraic_mono: + assumes "K \ K'" "(algebraic over K) x" shows "(algebraic over K') x" + using transcendental_mono[OF assms(1)] assms(2) unfolding over_def by blast + +lemma (in domain) zero_is_algebraic: + assumes "subring K R" shows "(algebraic over K) \" + using algebraicI[OF var_closed(1)[OF assms]] unfolding var_def by auto + +lemma (in domain) algebraic_self: + assumes "subring K R" and "k \ K" shows "(algebraic over K) k" +proof (rule algebraicI[of "[ \, \ k ]"]) + show "[ \, \ k ] \ carrier (K [X])" and "[ \, \ k ] \ []" + using subringE(2-3,5)[OF assms(1)] assms(2) unfolding univ_poly_def polynomial_def by auto + have "k \ carrier R" + using subringE(1)[OF assms(1)] assms(2) by auto + thus "eval [ \, \ k ] k = \" + by (auto, algebra) +qed + +lemma (in domain) ker_diff_carrier: + assumes "subring K R" + shows "a_kernel (K[X]) R (\p. eval p x) \ carrier (K[X])" +proof - + have "eval [ \ ] x \ \" and "[ \ ] \ carrier (K[X])" + using subringE(3)[OF assms] unfolding univ_poly_def polynomial_def by auto + thus ?thesis + unfolding a_kernel_def' by blast +qed + + +subsection \Minimal Polynomial\ + +lemma (in domain) minimal_polynomial_is_unique: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" + shows "\!p \ carrier (K[X]). pirreducible K p \ eval p x = \ \ lead_coeff p = \" + (is "\!p. ?minimal_poly p") +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + let ?ker_gen = "\p. p \ carrier (K[X]) \ pirreducible K p \ lead_coeff p = \ \ + a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> p" + + obtain p where p: "?ker_gen p" and unique: "\q. ?ker_gen q \ q = p" + using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)] + algebraic_imp_non_trivial_ker[OF _ assms(2-3)] + ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto + hence "?minimal_poly p" + using UP.cgenideal_self p unfolding a_kernel_def' by auto + moreover have "\q. ?minimal_poly q \ q = p" + proof - + fix q assume q: "?minimal_poly q" + then have "q \ PIdl\<^bsub>K[X]\<^esub> p" + using p unfolding a_kernel_def' by auto + hence "p \\<^bsub>K[X]\<^esub> q" + using cgenideal_pirreducible[OF assms(1)] p q by simp + hence "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> q" + using UP.associated_iff_same_ideal q p by simp + thus "q = p" + using unique q by simp + qed + ultimately show ?thesis by blast +qed + +lemma (in domain) IrrE: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" + shows "Irr K x \ carrier (K[X])" and "pirreducible K (Irr K x)" + and "lead_coeff (Irr K x) = \" and "eval (Irr K x) x = \" + using theI'[OF minimal_polynomial_is_unique[OF assms]] unfolding Irr_def by auto + +lemma (in domain) Irr_generates_ker: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" + shows "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> (Irr K x)" +proof - + obtain q + where q: "q \ carrier (K[X])" "pirreducible K q" + and ker: "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> q" + using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)] + algebraic_imp_non_trivial_ker[OF _ assms(2-3)] + ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto + have "Irr K x \ PIdl\<^bsub>K[X]\<^esub> q" + using IrrE(1,4)[OF assms] ker unfolding a_kernel_def' by auto + thus ?thesis + using cgenideal_pirreducible[OF assms(1) q(1-2) IrrE(2)[OF assms]] q(1) IrrE(1)[OF assms] + cring.associated_iff_same_ideal[OF univ_poly_is_cring[OF subfieldE(1)[OF assms(1)]]] + unfolding ker + by simp +qed + +lemma (in domain) Irr_minimal: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" + and "p \ carrier (K[X])" "eval p x = \" shows "(Irr K x) pdivides p" +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + have "p \ PIdl\<^bsub>K[X]\<^esub> (Irr K x)" + using Irr_generates_ker[OF assms(1-3)] assms(4-5) unfolding a_kernel_def' by auto + hence "(Irr K x) divides\<^bsub>K[X]\<^esub> p" + using UP.to_contain_is_to_divide IrrE(1)[OF assms(1-3)] + by (meson UP.cgenideal_ideal UP.cgenideal_minimal assms(4)) + thus ?thesis + unfolding pdivides_iff_shell[OF assms(1) IrrE(1)[OF assms(1-3)] assms(4)] . +qed + +lemma (in domain) rupture_of_Irr: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" shows "field (Rupt K (Irr K x))" + using rupture_is_field_iff_pirreducible[OF assms(1)] IrrE(1-2)[OF assms] by simp + + +subsection \Simple Extensions\ + +lemma (in ring) simple_extension_consistent: + assumes "subring K R" shows "ring.simple_extension (R \ carrier := K \) = simple_extension" +proof - + interpret K: ring "R \ carrier := K \" + using subring_is_ring[OF assms] . + + have "\K' x. K.simple_extension K' x \ simple_extension K' x" + proof + fix K' x a show "a \ K.simple_extension K' x \ a \ simple_extension K' x" + by (induction rule: K.simple_extension.induct) (auto simp add: simple_extension.lin) + qed + moreover + have "\K' x. simple_extension K' x \ K.simple_extension K' x" + proof + fix K' x a assume a: "a \ simple_extension K' x" thus "a \ K.simple_extension K' x" + using K.simple_extension.zero K.simple_extension.lin + by (induction rule: simple_extension.induct) (simp)+ + qed + ultimately show ?thesis by blast +qed + +lemma (in ring) mono_simple_extension: + assumes "K \ K'" shows "simple_extension K x \ simple_extension K' x" +proof + fix a assume "a \ simple_extension K x" thus "a \ simple_extension K' x" + proof (induct a rule: simple_extension.induct, simp) + case lin thus ?case using simple_extension.lin assms by blast + qed +qed + +lemma (in ring) simple_extension_incl: + assumes "K \ carrier R" and "x \ carrier R" shows "K \ simple_extension K x" +proof + fix k assume "k \ K" thus "k \ simple_extension K x" + using simple_extension.lin[OF simple_extension.zero, of k K x] assms by auto +qed + +lemma (in ring) simple_extension_mem: + assumes "subring K R" and "x \ carrier R" shows "x \ simple_extension K x" +proof - + have "\ \ simple_extension K x" + using simple_extension_incl[OF _ assms(2)] subringE(1,3)[OF assms(1)] by auto + thus ?thesis + using simple_extension.lin[OF _ subringE(2)[OF assms(1)], of \ x] assms(2) by auto +qed + +lemma (in ring) simple_extension_carrier: + assumes "x \ carrier R" shows "simple_extension (carrier R) x = carrier R" +proof + show "carrier R \ simple_extension (carrier R) x" + using simple_extension_incl[OF _ assms] by auto +next + show "simple_extension (carrier R) x \ carrier R" + proof + fix a assume "a \ simple_extension (carrier R) x" thus "a \ carrier R" + by (induct a rule: simple_extension.induct) (auto simp add: assms) + qed +qed + +lemma (in ring) simple_extension_in_carrier: + assumes "K \ carrier R" and "x \ carrier R" shows "simple_extension K x \ carrier R" + using mono_simple_extension[OF assms(1), of x] simple_extension_carrier[OF assms(2)] by auto + +lemma (in ring) simple_extension_subring_incl: + assumes "subring K' R" and "K \ K'" "x \ K'" shows "simple_extension K x \ K'" + using ring.simple_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3) + unfolding simple_extension_consistent[OF assms(1)] by simp + +lemma (in ring) simple_extension_as_eval_img: + assumes "K \ carrier R" "x \ carrier R" + shows "simple_extension K x = (\p. eval p x) ` carrier (K[X])" +proof + show "simple_extension K x \ (\p. eval p x) ` carrier (K[X])" + proof + fix a assume "a \ simple_extension K x" thus "a \ (\p. eval p x) ` carrier (K[X])" + proof (induction rule: simple_extension.induct) + case zero + have "polynomial K []" and "eval [] x = \" + unfolding polynomial_def by simp+ + thus ?case + unfolding univ_poly_carrier by force + next + case (lin k1 k2) + then obtain p where p: "p \ carrier (K[X])" "polynomial K p" "eval p x = k1" + by (auto simp add: univ_poly_carrier) + hence "set p \ carrier R" and "k2 \ carrier R" + using assms(1) lin(2) unfolding polynomial_def by auto + hence "eval (normalize (p @ [ k2 ])) x = k1 \ x \ k2" + using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto + thus ?case + using normalize_gives_polynomial[of "p @ [ k2 ]"] polynomial_incl[OF p(2)] lin(2) + unfolding univ_poly_carrier by force + qed + qed +next + show "(\p. eval p x) ` carrier (K[X]) \ simple_extension K x" + proof + fix a assume "a \ (\p. eval p x) ` carrier (K[X])" + then obtain p where p: "set p \ K" "eval p x = a" + using polynomial_incl unfolding univ_poly_def by auto + thus "a \ simple_extension K x" + proof (induct "length p" arbitrary: p a) + case 0 thus ?case + using simple_extension.zero by simp + next + case (Suc n) + obtain p' k where p: "p = p' @ [ k ]" + using Suc(2) by (metis list.size(3) nat.simps(3) rev_exhaust) + hence "a = (eval p' x) \ x \ k" + using eval_append_aux[of p' k x] Suc(3-4) assms unfolding p by auto + moreover have "eval p' x \ simple_extension K x" + using Suc(1-3) unfolding p by auto + ultimately show ?case + using simple_extension.lin Suc(3) unfolding p by auto + qed + qed +qed + +corollary (in domain) simple_extension_is_subring: + assumes "subring K R" "x \ carrier R" shows "subring (simple_extension K x) R" + using ring_hom_ring.img_is_subring[OF eval_ring_hom[OF assms] + ring.carrier_is_subring[OF univ_poly_is_ring[OF assms(1)]]] + simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)] + by simp + +corollary (in domain) simple_extension_minimal: + assumes "subring K R" "x \ carrier R" + shows "simple_extension K x = \ { K'. subring K' R \ K \ K' \ x \ K' }" + using simple_extension_is_subring[OF assms] simple_extension_mem[OF assms] + simple_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] simple_extension_subring_incl + by blast + +corollary (in domain) simple_extension_isomorphism: + assumes "subring K R" "x \ carrier R" + shows "(K[X]) Quot (a_kernel (K[X]) R (\p. eval p x)) \ R \ carrier := simple_extension K x \" + using ring_hom_ring.FactRing_iso_set_aux[OF eval_ring_hom[OF assms]] + simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)] + unfolding is_ring_iso_def by auto + +corollary (in domain) simple_extension_of_algebraic: + assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" + shows "Rupt K (Irr K x) \ R \ carrier := simple_extension K x \" + using simple_extension_isomorphism[OF subfieldE(1)[OF assms(1)] assms(2)] + unfolding Irr_generates_ker[OF assms] rupture_def by simp + +corollary (in domain) simple_extension_of_transcendental: + assumes "subring K R" and "x \ carrier R" "(transcendental over K) x" + shows "K[X] \ R \ carrier := simple_extension K x \" + using simple_extension_isomorphism[OF _ assms(2), of K] assms(1) + ring_iso_trans[OF ring.FactRing_zeroideal(2)[OF univ_poly_is_ring]] + unfolding transcendental_imp_trivial_ker[OF assms(3)] univ_poly_zero + by auto + +proposition (in domain) simple_extension_subfield_imp_algebraic: + assumes "subring K R" "x \ carrier R" + shows "subfield (simple_extension K x) R \ (algebraic over K) x" +proof - + assume simple_ext: "subfield (simple_extension K x) R" show "(algebraic over K) x" + proof (rule ccontr) + assume "\ (algebraic over K) x" then have "(transcendental over K) x" + unfolding over_def by simp + then obtain h where h: "h \ ring_iso (R \ carrier := simple_extension K x \) (K[X])" + using ring_iso_sym[OF univ_poly_is_ring simple_extension_of_transcendental] assms + unfolding is_ring_iso_def by blast + then interpret Hom: ring_hom_ring "R \ carrier := simple_extension K x \" "K[X]" h + using subring_is_ring[OF simple_extension_is_subring[OF assms]] + univ_poly_is_ring[OF assms(1)] assms h + by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def) + have "field (K[X])" + using field.ring_iso_imp_img_field[OF subfield_iff(2)[OF simple_ext] h] + unfolding Hom.hom_one Hom.hom_zero by simp + moreover have "\ field (K[X])" + using univ_poly_not_field[OF assms(1)] . + ultimately show False by simp + qed +qed + +proposition (in domain) simple_extension_is_subfield: + assumes "subfield K R" "x \ carrier R" + shows "subfield (simple_extension K x) R \ (algebraic over K) x" +proof + assume alg: "(algebraic over K) x" + then obtain h where h: "h \ ring_iso (Rupt K (Irr K x)) (R \ carrier := simple_extension K x \)" + using simple_extension_of_algebraic[OF assms] unfolding is_ring_iso_def by blast + have rupt_field: "field (Rupt K (Irr K x))" and "ring (R \ carrier := simple_extension K x \)" + using subring_is_ring[OF simple_extension_is_subring[OF subfieldE(1)]] + rupture_of_Irr[OF assms alg] assms by simp+ + then interpret Hom: ring_hom_ring "Rupt K (Irr K x)" "R \ carrier := simple_extension K x \" h + using h cring.axioms(1)[OF domain.axioms(1)[OF field.axioms(1)]] + by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def) + show "subfield (simple_extension K x) R" + using field.ring_iso_imp_img_field[OF rupt_field h] subfield_iff(1)[OF _ + simple_extension_in_carrier[OF subfieldE(3)[OF assms(1)] assms(2)]] + by simp +next + assume simple_ext: "subfield (simple_extension K x) R" thus "(algebraic over K) x" + using simple_extension_subfield_imp_algebraic[OF subfieldE(1)[OF assms(1)] assms(2)] by simp +qed + + +subsection \Link between dimension of K-algebras and algebraic extensions\ + +lemma (in domain) exp_base_independent: + assumes "subfield K R" "x \ carrier R" "(algebraic over K) x" + shows "independent K (exp_base x (degree (Irr K x)))" +proof - + have "\n. n \ degree (Irr K x) \ independent K (exp_base x n)" + proof - + fix n show "n \ degree (Irr K x) \ independent K (exp_base x n)" + proof (induct n, simp add: exp_base_def) + case (Suc n) + have "x [^] n \ Span K (exp_base x n)" + proof (rule ccontr) + assume "\ x [^] n \ Span K (exp_base x n)" + then obtain a Ks + where Ks: "a \ K - { \ }" "set Ks \ K" "length Ks = n" "combine (a # Ks) (exp_base x (Suc n)) = \" + using Span_mem_imp_non_trivial_combine[OF assms(1) exp_base_closed[OF assms(2), of n]] + by (auto simp add: exp_base_def) + hence "eval (a # Ks) x = \" + using combine_eq_eval by (auto simp add: exp_base_def) + moreover have "(a # Ks) \ carrier (K[X]) - { [] }" + unfolding univ_poly_def polynomial_def using Ks(1-2) by auto + ultimately have "degree (Irr K x) \ n" + using pdivides_imp_degree_le[OF subfieldE(1)[OF assms(1)] + IrrE(1)[OF assms] _ _ Irr_minimal[OF assms, of "a # Ks"]] Ks(3) by auto + from \Suc n \ degree (Irr K x)\ and this show False by simp + qed + thus ?case + using independent.li_Cons assms(2) Suc by (auto simp add: exp_base_def) + qed + qed + thus ?thesis + by simp +qed + +lemma (in ring) Span_eq_eval_img: + assumes "subfield K R" "x \ carrier R" + shows "Span K (exp_base x n) = (\p. eval p x) ` { p \ carrier (K[X]). length p \ n }" + (is "?Span = ?eval_img") +proof + show "?Span \ ?eval_img" + proof + fix u assume "u \ Span K (exp_base x n)" + then obtain Ks where Ks: "set Ks \ K" "length Ks = n" "u = combine Ks (exp_base x n)" + using Span_eq_combine_set_length_version[OF assms(1) exp_base_closed[OF assms(2)]] + by (auto simp add: exp_base_def) + hence "u = eval (normalize Ks) x" + using combine_eq_eval eval_normalize[OF _ assms(2)] subfieldE(3)[OF assms(1)] by auto + moreover have "normalize Ks \ carrier (K[X])" + using normalize_gives_polynomial[OF Ks(1)] unfolding univ_poly_def by auto + moreover have "length (normalize Ks) \ n" + using normalize_length_le[of Ks] Ks(2) by auto + ultimately show "u \ ?eval_img" by auto + qed +next + show "?eval_img \ ?Span" + proof + fix u assume "u \ ?eval_img" + then obtain p where p: "p \ carrier (K[X])" "length p \ n" "u = eval p x" + by blast + hence "combine p (exp_base x (length p)) = u" + using combine_eq_eval by auto + moreover have set_p: "set p \ K" + using polynomial_incl[of K p] p(1) unfolding univ_poly_carrier by auto + hence "set p \ carrier R" + using subfieldE(3)[OF assms(1)] by auto + moreover have "drop (n - length p) (exp_base x n) = exp_base x (length p)" + using p(2) drop_exp_base by auto + ultimately have "combine ((replicate (n - length p) \) @ p) (exp_base x n) = u" + using combine_prepend_replicate[OF _ exp_base_closed[OF assms(2), of n]] by auto + moreover have "set ((replicate (n - length p) \) @ p) \ K" + using subringE(2)[OF subfieldE(1)[OF assms(1)]] set_p by auto + ultimately show "u \ ?Span" + using Span_eq_combine_set[OF assms(1) exp_base_closed[OF assms(2), of n]] by blast + qed +qed + +lemma (in domain) Span_exp_base: + assumes "subfield K R" "x \ carrier R" "(algebraic over K) x" + shows "Span K (exp_base x (degree (Irr K x))) = simple_extension K x" + unfolding simple_extension_as_eval_img[OF subfieldE(3)[OF assms(1)] assms(2)] + Span_eq_eval_img[OF assms(1-2)] +proof (auto) + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + note hom_simps = ring_hom_memE[OF eval_is_hom[OF subfieldE(1)[OF assms(1)] assms(2)]] + + fix p assume p: "p \ carrier (K[X])" + have Irr: "Irr K x \ carrier (K[X])" "Irr K x \ []" + using IrrE(1-2)[OF assms] unfolding ring_irreducible_def univ_poly_zero by auto + then obtain q r + where q: "q \ carrier (K[X])" and r: "r \ carrier (K[X])" + and dvd: "p = Irr K x \\<^bsub>K [X]\<^esub> q \\<^bsub>K [X]\<^esub> r" "r = [] \ degree r < degree (Irr K x)" + using subfield_long_division_theorem_shell[OF assms(1) p Irr(1)] unfolding univ_poly_zero by auto + hence "eval p x = (eval (Irr K x) x) \ (eval q x) \ (eval r x)" + using hom_simps(2-3) Irr(1) by simp + hence "eval p x = eval r x" + using hom_simps(1) q r unfolding IrrE(4)[OF assms] by simp + moreover have "length r < length (Irr K x)" + using dvd(2) Irr(2) by auto + ultimately + show "eval p x \ (\p. local.eval p x) ` { p \ carrier (K [X]). length p \ length (Irr K x) - Suc 0 }" + using r by auto +qed + +corollary (in domain) dimension_simple_extension: + assumes "subfield K R" "x \ carrier R" "(algebraic over K) x" + shows "dimension (degree (Irr K x)) K (simple_extension K x)" + using dimension_independent[OF exp_base_independent[OF assms]] Span_exp_base[OF assms] + by (simp add: exp_base_def) + +lemma (in ring) finite_dimension_imp_algebraic: + assumes "subfield K R" "subring F R" and "finite_dimension K F" + shows "x \ F \ (algebraic over K) x" +proof - + let ?Us = "\n. map (\i. x [^] i) (rev [0..< Suc n])" + + assume x: "x \ F" then have in_carrier: "x \ carrier R" + using subringE[OF assms(2)] by auto + obtain n where n: "dimension n K F" + using assms(3) by auto + have set_Us: "set (?Us n) \ F" + using x subringE(3,6)[OF assms(2)] by (induct n) (auto) + hence "set (?Us n) \ carrier R" + using subringE(1)[OF assms(2)] by auto + moreover have "dependent K (?Us n)" + using independent_length_le_dimension[OF assms(1) n _ set_Us] by auto + ultimately + obtain Ks where Ks: "length Ks = Suc n" "combine Ks (?Us n) = \" "set Ks \ K" "set Ks \ { \ }" + using dependent_imp_non_trivial_combine[OF assms(1), of "?Us n"] by auto + have "set Ks \ carrier R" + using subring_props(1)[OF assms(1)] Ks(3) by auto + hence "eval (normalize Ks) x = \" + using combine_eq_eval[of Ks] eval_normalize[OF _ in_carrier] Ks(1-2) by (simp add: exp_base_def) + moreover have "normalize Ks = [] \ set Ks \ { \ }" + by (induct Ks) (auto, meson list.discI, + metis all_not_in_conv list.discI list.sel(3) singletonD subset_singletonD) + hence "normalize Ks \ []" + using Ks(1,4) by (metis list.size(3) nat.distinct(1) set_empty subset_singleton_iff) + moreover have "normalize Ks \ carrier (K[X])" + using normalize_gives_polynomial[OF Ks(3)] unfolding univ_poly_def by auto + ultimately show ?thesis + using algebraicI by auto +qed + +corollary (in domain) simple_extension_dim: + assumes "subfield K R" "x \ carrier R" "(algebraic over K) x" + shows "(dim over K) (simple_extension K x) = degree (Irr K x)" + using dimI[OF assms(1) dimension_simple_extension[OF assms]] . + +corollary (in domain) finite_dimension_simple_extension: + assumes "subfield K R" "x \ carrier R" + shows "finite_dimension K (simple_extension K x) \ (algebraic over K) x" + using finite_dimensionI[OF dimension_simple_extension[OF assms]] + finite_dimension_imp_algebraic[OF _ simple_extension_is_subring[OF subfieldE(1)]] + simple_extension_mem[OF subfieldE(1)] assms + by auto + + +subsection \Finite Extensions\ + +lemma (in ring) finite_extension_consistent: + assumes "subring K R" shows "ring.finite_extension (R \ carrier := K \) = finite_extension" +proof - + have "\K' xs. ring.finite_extension (R \ carrier := K \) K' xs = finite_extension K' xs" + proof - + fix K' xs show "ring.finite_extension (R \ carrier := K \) K' xs = finite_extension K' xs" + using ring.finite_extension.simps[OF subring_is_ring[OF assms]] + simple_extension_consistent[OF assms] by (induct xs) (auto) + qed + thus ?thesis by blast +qed + +lemma (in ring) mono_finite_extension: + assumes "K \ K'" shows "finite_extension K xs \ finite_extension K' xs" + using mono_simple_extension assms by (induct xs) (auto) + +lemma (in ring) finite_extension_carrier: + assumes "set xs \ carrier R" shows "finite_extension (carrier R) xs = carrier R" + using assms simple_extension_carrier by (induct xs) (auto) + +lemma (in ring) finite_extension_in_carrier: + assumes "K \ carrier R" and "set xs \ carrier R" shows "finite_extension K xs \ carrier R" + using assms simple_extension_in_carrier by (induct xs) (auto) + +lemma (in ring) finite_extension_subring_incl: + assumes "subring K' R" and "K \ K'" "set xs \ K'" shows "finite_extension K xs \ K'" + using ring.finite_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3) + unfolding finite_extension_consistent[OF assms(1)] by simp + +lemma (in ring) finite_extension_incl_aux: + assumes "K \ carrier R" and "x \ carrier R" "set xs \ carrier R" + shows "finite_extension K xs \ finite_extension K (x # xs)" + using simple_extension_incl[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp + +lemma (in ring) finite_extension_incl: + assumes "K \ carrier R" and "set xs \ carrier R" shows "K \ finite_extension K xs" + using finite_extension_incl_aux[OF assms(1)] assms(2) by (induct xs) (auto) + +lemma (in ring) finite_extension_as_eval_img: + assumes "K \ carrier R" and "x \ carrier R" "set xs \ carrier R" + shows "finite_extension K (x # xs) = (\p. eval p x) ` carrier ((finite_extension K xs) [X])" + using simple_extension_as_eval_img[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp + +lemma (in domain) finite_extension_is_subring: + assumes "subring K R" "set xs \ carrier R" shows "subring (finite_extension K xs) R" + using assms simple_extension_is_subring by (induct xs) (auto) + +corollary (in domain) finite_extension_mem: + assumes "subring K R" "set xs \ carrier R" shows "set xs \ finite_extension K xs" +proof - + { fix x xs assume "x \ carrier R" "set xs \ carrier R" + hence "x \ finite_extension K (x # xs)" + using simple_extension_mem[OF finite_extension_is_subring[OF assms(1), of xs]] by simp } + note aux_lemma = this + show ?thesis + using aux_lemma finite_extension_incl_aux[OF subringE(1)[OF assms(1)]] assms(2) + by (induct xs) (simp, smt insert_subset list.simps(15) subset_trans) +qed + +corollary (in domain) finite_extension_minimal: + assumes "subring K R" "set xs \ carrier R" + shows "finite_extension K xs = \ { K'. subring K' R \ K \ K' \ set xs \ K' }" + using finite_extension_is_subring[OF assms] finite_extension_mem[OF assms] + finite_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] finite_extension_subring_incl + by blast + +corollary (in domain) finite_extension_same_set: + assumes "subring K R" "set xs \ carrier R" "set xs = set ys" + shows "finite_extension K xs = finite_extension K ys" + using finite_extension_minimal[OF assms(1)] assms(2-3) by auto + +text \The reciprocal is also true, but it is more subtle.\ +proposition (in domain) finite_extension_is_subfield: + assumes "subfield K R" "set xs \ carrier R" + shows "(\x. x \ set xs \ (algebraic over K) x) \ subfield (finite_extension K xs) R" + using simple_extension_is_subfield algebraic_mono assms + by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1)) + +proposition (in domain) finite_extension_finite_dimension: + assumes "subfield K R" "set xs \ carrier R" + shows "(\x. x \ set xs \ (algebraic over K) x) \ finite_dimension K (finite_extension K xs)" + and "finite_dimension K (finite_extension K xs) \ (\x. x \ set xs \ (algebraic over K) x)" +proof - + show "finite_dimension K (finite_extension K xs) \ (\x. x \ set xs \ (algebraic over K) x)" + using finite_dimension_imp_algebraic[OF assms(1) + finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]] + finite_extension_mem[OF subfieldE(1)[OF assms(1)] assms(2)] by auto +next + show "(\x. x \ set xs \ (algebraic over K) x) \ finite_dimension K (finite_extension K xs)" + using assms(2) + proof (induct xs, simp add: finite_dimensionI[OF dimension_one[OF assms(1)]]) + case (Cons x xs) + hence "finite_dimension K (finite_extension K xs)" + by auto + moreover have "(algebraic over (finite_extension K xs)) x" + using algebraic_mono[OF finite_extension_incl[OF subfieldE(3)[OF assms(1)]]] Cons(2-3) by auto + moreover have "subfield (finite_extension K xs) R" + using finite_extension_is_subfield[OF assms(1)] Cons(2-3) by auto + ultimately show ?case + using telescopic_base_dim(1)[OF assms(1) _ _ + finite_dimensionI[OF dimension_simple_extension, of _ x]] Cons(3) by auto + qed +qed + +corollary (in domain) finite_extesion_mem_imp_algebraic: + assumes "subfield K R" "set xs \ carrier R" and "\x. x \ set xs \ (algebraic over K) x" + shows "y \ finite_extension K xs \ (algebraic over K) y" + using finite_dimension_imp_algebraic[OF assms(1) + finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]] + finite_extension_finite_dimension(1)[OF assms(1-2)] assms(3) by auto + +corollary (in domain) simple_extesion_mem_imp_algebraic: + assumes "subfield K R" "x \ carrier R" "(algebraic over K) x" + shows "y \ simple_extension K x \ (algebraic over K) y" + using finite_extesion_mem_imp_algebraic[OF assms(1), of "[ x ]"] assms(2-3) by auto + + +subsection \Arithmetic of algebraic numbers\ + +text \We show that the set of algebraic numbers of a field + over a subfield K is a subfield itself.\ + +lemma (in field) subfield_of_algebraics: + assumes "subfield K R" shows "subfield { x \ carrier R. (algebraic over K) x } R" +proof - + let ?set_of_algebraics = "{ x \ carrier R. (algebraic over K) x }" + + show ?thesis + proof (rule subfieldI'[OF subringI]) + show "?set_of_algebraics \ carrier R" and "\ \ ?set_of_algebraics" + using algebraic_self[OF _ subringE(3)] subfieldE(1)[OF assms(1)] by auto + next + fix x y assume x: "x \ ?set_of_algebraics" and y: "y \ ?set_of_algebraics" + have "\ x \ simple_extension K x" + using subringE(5)[OF simple_extension_is_subring[OF subfieldE(1)]] + simple_extension_mem[OF subfieldE(1)] assms(1) x by auto + thus "\ x \ ?set_of_algebraics" + using simple_extesion_mem_imp_algebraic[OF assms] x by auto + + have "x \ y \ finite_extension K [ x, y ]" and "x \ y \ finite_extension K [ x, y ]" + using subringE(6-7)[OF finite_extension_is_subring[OF subfieldE(1)[OF assms(1)]], of "[ x, y ]"] + finite_extension_mem[OF subfieldE(1)[OF assms(1)], of "[ x, y ]"] x y by auto + thus "x \ y \ ?set_of_algebraics" and "x \ y \ ?set_of_algebraics" + using finite_extesion_mem_imp_algebraic[OF assms, of "[ x, y ]"] x y by auto + next + fix z assume z: "z \ ?set_of_algebraics - { \ }" + have "inv z \ simple_extension K z" + using subfield_m_inv(1)[of "simple_extension K z"] + simple_extension_is_subfield[OF assms, of z] + simple_extension_mem[OF subfieldE(1)] assms(1) z by auto + thus "inv z \ ?set_of_algebraics" + using simple_extesion_mem_imp_algebraic[OF assms] field_Units z by auto + qed +qed + + +(* +proposition (in domain) finite_extension_is_subfield: + assumes "subfield K R" "set xs \ carrier R" + shows "subfield (finite_extension K xs) R \ (algebraic_set over K) (set xs)" +proof + have "(\x. x \ set xs \ (algebraic over K) x) \ subfield (finite_extension K xs) R" + using simple_extension_is_subfield algebraic_mono assms + by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1)) + thus "(algebraic_set over K) (set xs) \ subfield (finite_extension K xs) R" + unfolding algebraic_set_def over_def by auto +next + { fix x xs + assume x: "x \ carrier R" and xs: "set xs \ carrier R" + and is_subfield: "subfield (finite_extension K (x # xs)) R" + hence "(algebraic over K) x" sorry } + + assume "subfield (finite_extension K xs) R" thus "(algebraic_set over K) (set xs)" + using assms(2) + proof (induct xs) + case Nil thus ?case + unfolding algebraic_set_def over_def by simp + next + case (Cons x xs) + have "(algebraic over K) x" + using simple_extension_subfield_imp_algebraic[OF + finite_extension_is_subring[of K xs], of x] + + then show ?case sorry + qed +qed +*) + +(* +lemma (in ring) transcendental_imp_trivial_ker: + assumes "x \ carrier R" + shows "(transcendental over K) x \ (\p. \ polynomial R p; set p \ K \ \ eval p x = \ \ p = [])" +proof - + fix p assume "(transcendental over K) x" "polynomial R p" "eval p x = \" "set p \ K" + moreover have "eval [] x = \" and "polynomial R []" + using assms zero_is_polynomial by auto + ultimately show "p = []" + unfolding over_def transcendental_def inj_on_def by auto +qed + +lemma (in domain) trivial_ker_imp_transcendental: + assumes "subring K R" and "x \ carrier R" + shows "(\p. \ polynomial R p; set p \ K \ \ eval p x = \ \ p = []) \ (transcendental over K) x" +proof - + assume "\p. \ polynomial R p; set p \ K \ \ eval p x = \ \ p = []" + hence "a_kernel (univ_poly (R \ carrier := K \)) R (\p. local.eval p x) = { [] }" + unfolding a_kernel_def' univ_poly_subring_def'[OF assms(1)] by auto + moreover have "[] = \\<^bsub>(univ_poly (R \ carrier := K \))\<^esub>" + unfolding univ_poly_def by auto + ultimately have "inj_on (\p. local.eval p x) (carrier (univ_poly (R \ carrier := K \)))" + using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] by auto + thus "(transcendental over K) x" + unfolding over_def transcendental_def univ_poly_subring_def'[OF assms(1)] by simp +qed + +lemma (in ring) non_trivial_ker_imp_algebraic: + assumes "x \ carrier R" + and "p \ []" "polynomial R p" "set p \ K" "eval p x = \" + shows "(algebraic over K) x" + using transcendental_imp_trivial_ker[OF assms(1) _ assms(3-5)] assms(2) + unfolding over_def algebraic_def by auto + +lemma (in domain) algebraic_imp_non_trivial_ker: + assumes "subring K R" "x \ carrier R" + shows "(algebraic over K) x \ (\p \ []. polynomial R p \ set p \ K \ eval p x = \)" + using trivial_ker_imp_transcendental[OF assms] + unfolding over_def algebraic_def by auto + +lemma (in domain) algebraic_iff: + assumes "subring K R" "x \ carrier R" + shows "(algebraic over K) x \ (\p \ []. polynomial R p \ set p \ K \ eval p x = \)" + using non_trivial_ker_imp_algebraic[OF assms(2)] algebraic_imp_non_trivial_ker[OF assms] by auto +*) + + +(* +lemma (in field) + assumes "subfield K R" + shows "subfield (simple_extension K x) R \ (algebraic over K) x" + sorry + +*) +end \ No newline at end of file diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Indexed_Polynomials.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Indexed_Polynomials.thy Sun Apr 14 12:00:17 2019 +0100 @@ -0,0 +1,549 @@ +(* Title: HOL/Algebra/Indexed_Polynomials.thy + Author: Paulo Emílio de Vilhena +*) + +theory Indexed_Polynomials + imports Weak_Morphisms "HOL-Library.Multiset" Polynomial_Divisibility + +begin + +section \Indexed Polynomials\ + +text \In this theory, we build a basic framework to the study of polynomials on letters + indexed by a set. The main interest is to then apply these concepts to the construction + of the algebraic closure of a field. \ + + +subsection \Definitions\ + +text \We formalize indexed monomials as multisets with its support a subset of the index set. + On top of those, we build indexed polynomials which are simply functions mapping a monomial + to its coefficient. \ + +definition (in ring) indexed_const :: "'a \ ('c multiset \ 'a)" + where "indexed_const k = (\m. if m = {#} then k else \)" + +definition (in ring) indexed_pmult :: "('c multiset \ 'a) \ 'c \ ('c multiset \ 'a)" (infixl "\" 65) + where "indexed_pmult P i = (\m. if i \# m then P (m - {# i #}) else \)" + +definition (in ring) indexed_padd :: "_ \ _ \ ('c multiset \ 'a)" (infixl "\" 65) + where "indexed_padd P Q = (\m. (P m) \ (Q m))" + +definition (in ring) indexed_var :: "'c \ ('c multiset \ 'a)" ("\\") + where "indexed_var i = (indexed_const \) \ i" + +definition (in ring) index_free :: "('c multiset \ 'a) \ 'c \ bool" + where "index_free P i \ (\m. i \# m \ P m = \)" + +definition (in ring) carrier_coeff :: "('c multiset \ 'a) \ bool" + where "carrier_coeff P \ (\m. P m \ carrier R)" + +inductive_set (in ring) indexed_pset :: "'c set \ 'a set \ ('c multiset \ 'a) set" ("_ [\\]" 80) + for I and K where + indexed_const: "k \ K \ indexed_const k \ (K[\\<^bsub>I\<^esub>])" + | indexed_padd: "\ P \ (K[\\<^bsub>I\<^esub>]); Q \ (K[\\<^bsub>I\<^esub>]) \ \ P \ Q \ (K[\\<^bsub>I\<^esub>])" + | indexed_pmult: "\ P \ (K[\\<^bsub>I\<^esub>]); i \ I \ \ P \ i \ (K[\\<^bsub>I\<^esub>])" + +fun (in ring) indexed_eval_aux :: "('c multiset \ 'a) list \ 'c \ ('c multiset \ 'a)" + where "indexed_eval_aux Ps i = foldr (\P Q. (Q \ i) \ P) Ps (indexed_const \)" + +fun (in ring) indexed_eval :: "('c multiset \ 'a) list \ 'c \ ('c multiset \ 'a)" + where "indexed_eval Ps i = indexed_eval_aux (rev Ps) i" + + +subsection \Basic Properties\ + +lemma (in ring) carrier_coeffE: + assumes "carrier_coeff P" shows "P m \ carrier R" + using assms unfolding carrier_coeff_def by simp + +lemma (in ring) indexed_zero_def: "indexed_const \ = (\_. \)" + unfolding indexed_const_def by simp + +lemma (in ring) indexed_const_index_free: "index_free (indexed_const k) i" + unfolding index_free_def indexed_const_def by auto + +lemma (in domain) indexed_var_not_index_free: "\ index_free \\<^bsub>i\<^esub> i" +proof - + have "\\<^bsub>i\<^esub> {# i #} = \" + unfolding indexed_var_def indexed_pmult_def indexed_const_def by simp + thus ?thesis + using one_not_zero unfolding index_free_def by fastforce +qed + +lemma (in ring) indexed_pmult_zero [simp]: + shows "indexed_pmult (indexed_const \) i = indexed_const \" + unfolding indexed_zero_def indexed_pmult_def by auto + +lemma (in ring) indexed_padd_zero: + assumes "carrier_coeff P" shows "P \ (indexed_const \) = P" and "(indexed_const \) \ P = P" + using assms unfolding carrier_coeff_def indexed_zero_def indexed_padd_def by auto + +lemma (in ring) indexed_padd_const: + shows "(indexed_const k1) \ (indexed_const k2) = indexed_const (k1 \ k2)" + unfolding indexed_padd_def indexed_const_def by auto + +lemma (in ring) indexed_const_in_carrier: + assumes "K \ carrier R" and "k \ K" shows "\m. (indexed_const k) m \ carrier R" + using assms unfolding indexed_const_def by auto + +lemma (in ring) indexed_padd_in_carrier: + assumes "carrier_coeff P" and "carrier_coeff Q" shows "carrier_coeff (indexed_padd P Q)" + using assms unfolding carrier_coeff_def indexed_padd_def by simp + +lemma (in ring) indexed_pmult_in_carrier: + assumes "carrier_coeff P" shows "carrier_coeff (P \ i)" + using assms unfolding carrier_coeff_def indexed_pmult_def by simp + +lemma (in ring) indexed_eval_aux_in_carrier: + assumes "list_all carrier_coeff Ps" shows "carrier_coeff (indexed_eval_aux Ps i)" + using assms unfolding carrier_coeff_def + by (induct Ps) (auto simp add: indexed_zero_def indexed_padd_def indexed_pmult_def) + +lemma (in ring) indexed_eval_in_carrier: + assumes "list_all carrier_coeff Ps" shows "carrier_coeff (indexed_eval Ps i)" + using assms indexed_eval_aux_in_carrier[of "rev Ps"] by auto + +lemma (in ring) indexed_pset_in_carrier: + assumes "K \ carrier R" and "P \ (K[\\<^bsub>I\<^esub>])" shows "carrier_coeff P" + using assms(2,1) indexed_const_in_carrier unfolding carrier_coeff_def + by (induction) (auto simp add: indexed_zero_def indexed_padd_def indexed_pmult_def) + + +subsection \Indexed Eval\ + +lemma (in ring) exists_indexed_eval_aux_monomial: + assumes "carrier_coeff P" and "list_all carrier_coeff Qs" + and "count n i = k" and "P n \ \" and "list_all (\Q. index_free Q i) Qs" + obtains m where "count m i = length Qs + k" and "(indexed_eval_aux (Qs @ [ P ]) i) m \ \" +proof - + from assms(2,5) have "\m. count m i = length Qs + k \ (indexed_eval_aux (Qs @ [ P ]) i) m \ \" + proof (induct Qs) + case Nil thus ?case + using indexed_padd_zero(2)[OF assms(1)] assms(3-4) by auto + next + case (Cons Q Qs) + then obtain m where m: "count m i = length Qs + k" "(indexed_eval_aux (Qs @ [ P ]) i) m \ \" + by auto + define m' where "m' = m + {# i #}" + hence "Q m' = \" + using Cons(3) unfolding index_free_def by simp + moreover have "(indexed_eval_aux (Qs @ [ P ]) i) m \ carrier R" + using indexed_eval_aux_in_carrier[of "Qs @ [ P ]" i] Cons(2) assms(1) carrier_coeffE by auto + hence "((indexed_eval_aux (Qs @ [ P ]) i) \ i) m' \ carrier R - { \ }" + using m unfolding indexed_pmult_def m'_def by simp + ultimately have "(indexed_eval_aux (Q # (Qs @ [ P ])) i) m' \ \" + by (auto simp add: indexed_padd_def) + moreover from \count m i = length Qs + k\ have "count m' i = length (Q # Qs) + k" + unfolding m'_def by simp + ultimately show ?case + by auto + qed + thus thesis + using that by blast +qed + +lemma (in ring) indexed_eval_aux_monomial_degree_le: + assumes "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + and "(indexed_eval_aux Ps i) m \ \" shows "count m i \ length Ps - 1" + using assms(1-3) +proof (induct Ps arbitrary: m, simp add: indexed_zero_def) + case (Cons P Ps) show ?case + proof (cases "count m i = 0", simp) + assume "count m i \ 0" + hence "P m = \" + using Cons(3) unfolding index_free_def by simp + moreover have "(indexed_eval_aux Ps i) m \ carrier R" + using carrier_coeffE[OF indexed_eval_aux_in_carrier[of Ps i]] Cons(2) by simp + ultimately have "((indexed_eval_aux Ps i) \ i) m \ \" + using Cons(4) by (auto simp add: indexed_padd_def) + with \count m i \ 0\ have "(indexed_eval_aux Ps i) (m - {# i #}) \ \" + unfolding indexed_pmult_def by (auto simp del: indexed_eval_aux.simps) + hence "count m i - 1 \ length Ps - 1" + using Cons(1)[of "m - {# i #}"] Cons(2-3) by auto + moreover from \(indexed_eval_aux Ps i) (m - {# i #}) \ \\ have "length Ps > 0" + by (auto simp add: indexed_zero_def) + moreover from \count m i \ 0\ have "count m i > 0" + by simp + ultimately show ?thesis + by (simp add: Suc_leI le_diff_iff) + qed +qed + +lemma (in ring) indexed_eval_aux_is_inj: + assumes "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + and "list_all carrier_coeff Qs" and "list_all (\Q. index_free Q i) Qs" + and "indexed_eval_aux Ps i = indexed_eval_aux Qs i" and "length Ps = length Qs" + shows "Ps = Qs" + using assms +proof (induct Ps arbitrary: Qs, simp) + case (Cons P Ps) + from \length (P # Ps) = length Qs\ obtain Q' Qs' where Qs: "Qs = Q' # Qs'" and "length Ps = length Qs'" + by (metis Suc_length_conv) + + have in_carrier: + "((indexed_eval_aux Ps i) \ i) m \ carrier R" "P m \ carrier R" + "((indexed_eval_aux Qs' i) \ i) m \ carrier R" "Q' m \ carrier R" for m + using indexed_eval_aux_in_carrier[of Ps i] + indexed_eval_aux_in_carrier[of Qs' i] Cons(2,4) carrier_coeffE + unfolding Qs indexed_pmult_def by auto + + have "(indexed_eval_aux (P # Ps) i) m = (indexed_eval_aux (Q' # Qs') i) m" for m + using Cons(6) unfolding Qs by simp + hence eq: "((indexed_eval_aux Ps i) \ i) m \ P m = ((indexed_eval_aux Qs' i) \ i) m \ Q' m" for m + by (simp add: indexed_padd_def) + + have "P m = Q' m" if "i \# m" for m + using that Cons(3,5) unfolding index_free_def Qs by auto + moreover have "P m = Q' m" if "i \# m" for m + using in_carrier(2,4) eq[of m] that by (auto simp add: indexed_pmult_def) + ultimately have "P = Q'" + by auto + + hence "(indexed_eval_aux Ps i) m = (indexed_eval_aux Qs' i) m" for m + using eq[of "m + {# i #}"] in_carrier[of "m + {# i #}"] unfolding indexed_pmult_def by auto + with \length Ps = length Qs'\ have "Ps = Qs'" + using Cons(1)[of Qs'] Cons(2-5) unfolding Qs by auto + with \P = Q'\ show ?case + unfolding Qs by simp +qed + +lemma (in ring) indexed_eval_aux_is_inj': + assumes "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + and "list_all carrier_coeff Qs" and "list_all (\Q. index_free Q i) Qs" + and "carrier_coeff P" and "index_free P i" "P \ indexed_const \" + and "carrier_coeff Q" and "index_free Q i" "Q \ indexed_const \" + and "indexed_eval_aux (Ps @ [ P ]) i = indexed_eval_aux (Qs @ [ Q ]) i" + shows "Ps = Qs" and "P = Q" +proof - + obtain m n where "P m \ \" and "Q n \ \" + using assms(7,10) unfolding indexed_zero_def by blast + hence "count m i = 0" and "count n i = 0" + using assms(6,9) unfolding index_free_def by (meson count_inI)+ + with \P m \ \\ and \Q n \ \\ obtain m' n' + where m': "count m' i = length Ps" "(indexed_eval_aux (Ps @ [ P ]) i) m' \ \" + and n': "count n' i = length Qs" "(indexed_eval_aux (Qs @ [ Q ]) i) n' \ \" + using exists_indexed_eval_aux_monomial[of P Ps m i 0] + exists_indexed_eval_aux_monomial[of Q Qs n i 0] assms(1-5,8) + by (metis (no_types, lifting) add.right_neutral) + have "(indexed_eval_aux (Qs @ [ Q ]) i) m' \ \" + using m'(2) assms(11) by simp + with \count m' i = length Ps\ have "length Ps \ length Qs" + using indexed_eval_aux_monomial_degree_le[of "Qs @ [ Q ]" i m'] assms(3-4,8-9) by auto + moreover have "(indexed_eval_aux (Ps @ [ P ]) i) n' \ \" + using n'(2) assms(11) by simp + with \count n' i = length Qs\ have "length Qs \ length Ps" + using indexed_eval_aux_monomial_degree_le[of "Ps @ [ P ]" i n'] assms(1-2,5-6) by auto + ultimately have same_len: "length (Ps @ [ P ]) = length (Qs @ [ Q ])" + by simp + thus "Ps = Qs" and "P = Q" + using indexed_eval_aux_is_inj[of "Ps @ [ P ]" i "Qs @ [ Q ]"] assms(1-6,8-9,11) by auto +qed + +lemma (in ring) exists_indexed_eval_monomial: + assumes "carrier_coeff P" and "list_all carrier_coeff Qs" + and "P n \ \" and "list_all (\Q. index_free Q i) Qs" + obtains m where "count m i = length Qs + (count n i)" and "(indexed_eval (P # Qs) i) m \ \" + using exists_indexed_eval_aux_monomial[OF assms(1) _ _ assms(3), of "rev Qs"] assms(2,4) by auto + +corollary (in ring) exists_indexed_eval_monomial': + assumes "carrier_coeff P" and "list_all carrier_coeff Qs" + and "P \ indexed_const \" and "list_all (\Q. index_free Q i) Qs" + obtains m where "count m i \ length Qs" and "(indexed_eval (P # Qs) i) m \ \" +proof - + from \P \ indexed_const \\ obtain n where "P n \ \" + unfolding indexed_const_def by auto + then obtain m where "count m i = length Qs + (count n i)" and "(indexed_eval (P # Qs) i) m \ \" + using exists_indexed_eval_monomial[OF assms(1-2) _ assms(4)] by auto + thus thesis + using that by force +qed + +lemma (in ring) indexed_eval_monomial_degree_le: + assumes "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + and "(indexed_eval Ps i) m \ \" shows "count m i \ length Ps - 1" + using indexed_eval_aux_monomial_degree_le[of "rev Ps"] assms by auto + +lemma (in ring) indexed_eval_is_inj: + assumes "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + and "list_all carrier_coeff Qs" and "list_all (\Q. index_free Q i) Qs" + and "carrier_coeff P" and "index_free P i" "P \ indexed_const \" + and "carrier_coeff Q" and "index_free Q i" "Q \ indexed_const \" + and "indexed_eval (P # Ps) i = indexed_eval (Q # Qs) i" + shows "Ps = Qs" and "P = Q" +proof - + have rev_cond: + "list_all carrier_coeff (rev Ps)" "list_all (\P. index_free P i) (rev Ps)" + "list_all carrier_coeff (rev Qs)" "list_all (\Q. index_free Q i) (rev Qs)" + using assms(1-4) by auto + show "Ps = Qs" and "P = Q" + using indexed_eval_aux_is_inj'[OF rev_cond assms(5-10)] assms(11) by auto +qed + +lemma (in ring) indexed_eval_inj_on_carrier: + assumes "\P. P \ carrier L \ carrier_coeff P" and "\P. P \ carrier L \ index_free P i" and "\\<^bsub>L\<^esub> = indexed_const \" + shows "inj_on (\Ps. indexed_eval Ps i) (carrier (poly_ring L))" +proof - + { fix Ps + assume "Ps \ carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const \" + have "Ps = []" + proof (rule ccontr) + assume "Ps \ []" + then obtain P' Ps' where Ps: "Ps = P' # Ps'" + using list.exhaust by blast + with \Ps \ carrier (poly_ring L)\ + have "P' \ indexed_const \" and "list_all carrier_coeff Ps" and "list_all (\P. index_free P i) Ps" + using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def + by (simp add: list.pred_set subset_code(1))+ + then obtain m where "(indexed_eval Ps i) m \ \" + using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto + hence "indexed_eval Ps i \ indexed_const \" + unfolding indexed_const_def by auto + with \indexed_eval Ps i = indexed_const \\ show False by simp + qed } note aux_lemma = this + + show ?thesis + proof (rule inj_onI) + fix Ps Qs + assume "Ps \ carrier (poly_ring L)" and "Qs \ carrier (poly_ring L)" + show "indexed_eval Ps i = indexed_eval Qs i \ Ps = Qs" + proof (cases) + assume "Qs = []" and "indexed_eval Ps i = indexed_eval Qs i" + with \Ps \ carrier (poly_ring L)\ show "Ps = Qs" + using aux_lemma by simp + next + assume "Qs \ []" and eq: "indexed_eval Ps i = indexed_eval Qs i" + with \Qs \ carrier (poly_ring L)\ have "Ps \ []" + using aux_lemma by auto + from \Ps \ []\ and \Qs \ []\ obtain P' Ps' Q' Qs' where Ps: "Ps = P' # Ps'" and Qs: "Qs = Q' # Qs'" + using list.exhaust by metis + + from \Ps \ carrier (poly_ring L)\ and \Ps = P' # Ps'\ + have "carrier_coeff P'" and "index_free P' i" "P' \ indexed_const \" + and "list_all carrier_coeff Ps'" and "list_all (\P. index_free P i) Ps'" + using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def + by (simp add: list.pred_set subset_code(1))+ + moreover + from \Qs \ carrier (poly_ring L)\ and \Qs = Q' # Qs'\ + have "carrier_coeff Q'" and "index_free Q' i" "Q' \ indexed_const \" + and "list_all carrier_coeff Qs'" and "list_all (\P. index_free P i) Qs'" + using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def + by (simp add: list.pred_set subset_code(1))+ + ultimately show ?thesis + using indexed_eval_is_inj[of Ps' i Qs' P' Q'] eq unfolding Ps Qs by auto + qed + qed +qed + + +subsection \Link with Weak Morphisms\ + +text \We study some elements of the contradiction needed in the algebraic closure existence proof. \ + +context ring +begin + +lemma (in ring) indexed_padd_index_free: + assumes "index_free P i" and "index_free Q i" shows "index_free (P \ Q) i" + using assms unfolding indexed_padd_def index_free_def by auto + +lemma (in ring) indexed_pmult_index_free: + assumes "index_free P j" and "i \ j" shows "index_free (P \ i) j" + using assms unfolding index_free_def indexed_pmult_def + by (metis insert_DiffM insert_noteq_member) + +lemma (in ring) indexed_eval_index_free: + assumes "list_all (\P. index_free P j) Ps" and "i \ j" shows "index_free (indexed_eval Ps i) j" +proof - + { fix Ps assume "list_all (\P. index_free P j) Ps" hence "index_free (indexed_eval_aux Ps i) j" + using indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]] + by (induct Ps) (auto simp add: indexed_zero_def index_free_def) } + thus ?thesis + using assms(1) by auto +qed + +context + fixes L :: "(('c multiset) \ 'a) ring" and i :: 'c + assumes hyps: + \ \i\ "field L" + \ \ii\ "\P. P \ carrier L \ carrier_coeff P" + \ \iii\ "\P. P \ carrier L \ index_free P i" + \ \iv\ "\\<^bsub>L\<^esub> = indexed_const \" +begin + +interpretation L: field L + using \field L\ . + +interpretation UP: principal_domain "poly_ring L" + using L.univ_poly_is_principal[OF L.carrier_is_subfield] . + + +abbreviation eval_pmod + where "eval_pmod q \ (\p. indexed_eval (L.pmod p q) i)" + +abbreviation image_poly + where "image_poly q \ image_ring (eval_pmod q) (poly_ring L)" + + +lemma indexed_eval_is_weak_ring_morphism: + assumes "q \ carrier (poly_ring L)" shows "weak_ring_morphism (eval_pmod q) (PIdl\<^bsub>poly_ring L\<^esub> q) (poly_ring L)" +proof (rule weak_ring_morphismI) + show "ideal (PIdl\<^bsub>poly_ring L\<^esub> q) (poly_ring L)" + using UP.cgenideal_ideal[OF assms] . +next + fix a b assume in_carrier: "a \ carrier (poly_ring L)" "b \ carrier (poly_ring L)" + note ldiv_closed = in_carrier[THEN L.long_division_closed(2)[OF L.carrier_is_subfield _ assms]] + + have "(eval_pmod q) a = (eval_pmod q) b \ L.pmod a q = L.pmod b q" + using inj_onD[OF indexed_eval_inj_on_carrier[OF hyps(2-4)] _ ldiv_closed] by fastforce + also have " ... \ q pdivides\<^bsub>L\<^esub> (a \\<^bsub>poly_ring L\<^esub> b)" + unfolding L.same_pmod_iff_pdivides[OF L.carrier_is_subfield in_carrier assms] .. + also have " ... \ PIdl\<^bsub>poly_ring L\<^esub> (a \\<^bsub>poly_ring L\<^esub> b) \ PIdl\<^bsub>poly_ring L\<^esub> q" + unfolding UP.to_contain_is_to_divide[OF assms UP.minus_closed[OF in_carrier]] pdivides_def .. + also have " ... \ a \\<^bsub>poly_ring L\<^esub> b \ PIdl\<^bsub>poly_ring L\<^esub> q" + unfolding UP.cgenideal_eq_genideal[OF assms] UP.cgenideal_eq_genideal[OF UP.minus_closed[OF in_carrier]] + UP.Idl_subset_ideal'[OF UP.minus_closed[OF in_carrier] assms] .. + finally show "(eval_pmod q) a = (eval_pmod q) b \ a \\<^bsub>poly_ring L\<^esub> b \ PIdl\<^bsub>poly_ring L\<^esub> q" . +qed + +lemma eval_norm_eq_id: + assumes "q \ carrier (poly_ring L)" and "degree q > 0" and "a \ carrier L" + shows "((eval_pmod q) \ (ring.poly_of_const L)) a = a" +proof (cases) + assume "a = \\<^bsub>L\<^esub>" thus ?thesis + using L.long_division_zero(2)[OF L.carrier_is_subfield assms(1)] hyps(4) + unfolding ring.poly_of_const_def[OF L.ring_axioms] by auto +next + assume "a \ \\<^bsub>L\<^esub>" then have in_carrier: "[ a ] \ carrier (poly_ring L)" + using assms(3) unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def by simp + from \a \ \\<^bsub>L\<^esub>\ show ?thesis + using L.pmod_const(2)[OF L.carrier_is_subfield in_carrier assms(1)] assms(2) + indexed_padd_zero(2)[OF hyps(2)[OF assms(3)]] + unfolding ring.poly_of_const_def[OF L.ring_axioms] by auto +qed + +lemma image_poly_iso_incl: + assumes "q \ carrier (poly_ring L)" and "degree q > 0" shows "id \ ring_hom L (image_poly q)" +proof - + have "((eval_pmod q) \ L.poly_of_const) \ ring_hom L (image_poly q)" + using ring_hom_trans[OF L.canonical_embedding_is_hom[OF L.carrier_is_subring] + UP.weak_ring_morphism_is_hom[OF indexed_eval_is_weak_ring_morphism[OF assms(1)]]] + by simp + thus ?thesis + using eval_norm_eq_id[OF assms(1-2)] L.ring_hom_restrict[of _ "image_poly q" id] by auto +qed + +lemma image_poly_is_field: + assumes "q \ carrier (poly_ring L)" and "pirreducible\<^bsub>L\<^esub> (carrier L) q" shows "field (image_poly q)" + using UP.image_ring_is_field[OF indexed_eval_is_weak_ring_morphism[OF assms(1)]] assms(2) + unfolding sym[OF L.rupture_is_field_iff_pirreducible[OF L.carrier_is_subfield assms(1)]] rupture_def + by simp + +lemma image_poly_index_free: + assumes "q \ carrier (poly_ring L)" and "P \ carrier (image_poly q)" and "\ index_free P j" "i \ j" + obtains Q where "Q \ carrier L" and "\ index_free Q j" +proof - + from \P \ carrier (image_poly q)\ obtain p where p: "p \ carrier (poly_ring L)" and P: "P = (eval_pmod q) p" + unfolding image_ring_carrier by blast + from \\ index_free P j\ have "\ list_all (\P. index_free P j) (L.pmod p q)" + using indexed_eval_index_free[OF _ assms(4), of "L.pmod p q"] unfolding sym[OF P] by auto + then obtain Q where "Q \ set (L.pmod p q)" and "\ index_free Q j" + unfolding list_all_iff by auto + thus ?thesis + using L.long_division_closed(2)[OF L.carrier_is_subfield p assms(1)] that + unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def + by auto +qed + +lemma eval_pmod_var: + assumes "indexed_const \ ring_hom R L" and "q \ carrier (poly_ring L)" and "degree q > 1" + shows "(eval_pmod q) X\<^bsub>L\<^esub> = \\<^bsub>i\<^esub>" and "\\<^bsub>i\<^esub> \ carrier (image_poly q)" +proof - + have "X\<^bsub>L\<^esub> = [ indexed_const \, indexed_const \ ]" and "X\<^bsub>L\<^esub> \ carrier (poly_ring L)" + using ring_hom_one[OF assms(1)] hyps(4) L.var_closed(1) L.carrier_is_subring unfolding var_def by auto + thus "(eval_pmod q) X\<^bsub>L\<^esub> = \\<^bsub>i\<^esub>" + using L.pmod_const(2)[OF L.carrier_is_subfield _ assms(2), of "X\<^bsub>L\<^esub>"] assms(3) + by (auto simp add: indexed_pmult_def indexed_padd_def indexed_const_def indexed_var_def) + with \X\<^bsub>L\<^esub> \ carrier (poly_ring L)\ show "\\<^bsub>i\<^esub> \ carrier (image_poly q)" + using image_iff unfolding image_ring_carrier by fastforce +qed + +lemma image_poly_eval_indexed_var: + assumes "indexed_const \ ring_hom R L" + and "q \ carrier (poly_ring L)" and "degree q > 1" and "pirreducible\<^bsub>L\<^esub> (carrier L) q" + shows "(ring.eval (image_poly q)) q \\<^bsub>i\<^esub> = \\<^bsub>image_poly q\<^esub>" +proof - + let ?surj = "L.rupture_surj (carrier L) q" + let ?Rupt = "Rupt\<^bsub>L\<^esub> (carrier L) q" + let ?f = "eval_pmod q" + + interpret UP: ring "poly_ring L" + using L.univ_poly_is_ring[OF L.carrier_is_subring] . + from \pirreducible\<^bsub>L\<^esub> (carrier L) q\ interpret Rupt: field ?Rupt + using L.rupture_is_field_iff_pirreducible[OF L.carrier_is_subfield assms(2)] by simp + + have weak_morphism: "weak_ring_morphism ?f (PIdl\<^bsub>poly_ring L\<^esub> q) (poly_ring L)" + using indexed_eval_is_weak_ring_morphism[OF assms(2)] . + then interpret I: ideal "PIdl\<^bsub>poly_ring L\<^esub> q" "poly_ring L" + using weak_ring_morphism.axioms(1) by auto + interpret Hom: ring_hom_ring ?Rupt "image_poly q" "\x. the_elem (?f ` x)" + using ring_hom_ring.intro[OF I.quotient_is_ring UP.image_ring_is_ring[OF weak_morphism]] + UP.weak_ring_morphism_is_iso[OF weak_morphism] + unfolding ring_iso_def symmetric[OF ring_hom_ring_axioms_def] rupture_def + by auto + + have "set q \ carrier L" and lc: "q \ [] \ lead_coeff q \ carrier L - { \\<^bsub>L\<^esub> }" + using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by auto + + have map_surj: "set (map (?surj \ L.poly_of_const) q) \ carrier ?Rupt" + proof - + have "L.poly_of_const a \ carrier (poly_ring L)" if "a \ carrier L" for a + using that L.normalize_gives_polynomial[of "[ a ]"] + unfolding univ_poly_carrier ring.poly_of_const_def[OF L.ring_axioms] by simp + hence "(?surj \ L.poly_of_const) a \ carrier ?Rupt" if "a \ carrier L" for a + using ring_hom_memE(1)[OF L.rupture_surj_hom(1)[OF L.carrier_is_subring assms(2)]] that by simp + with \set q \ carrier L\ show ?thesis + by (induct q) (auto) + qed + + have "?surj X\<^bsub>L\<^esub> \ carrier ?Rupt" + using ring_hom_memE(1)[OF L.rupture_surj_hom(1)[OF _ assms(2)] L.var_closed(1)] L.carrier_is_subring by simp + moreover have "map (\x. the_elem (?f ` x)) (map (?surj \ L.poly_of_const) q) = q" + proof - + define g where "g = (?surj \ L.poly_of_const)" + define f where "f = (\x. the_elem (?f ` x))" + + have "the_elem (?f ` ((?surj \ L.poly_of_const) a)) = ((eval_pmod q) \ L.poly_of_const) a" + if "a \ carrier L" for a + using that L.normalize_gives_polynomial[of "[ a ]"] UP.weak_ring_morphism_range[OF weak_morphism] + unfolding univ_poly_carrier ring.poly_of_const_def[OF L.ring_axioms] by auto + hence "the_elem (?f ` ((?surj \ L.poly_of_const) a)) = a" if "a \ carrier L" for a + using eval_norm_eq_id[OF assms(2)] that assms(3) by simp + hence "f (g a) = a" if "a \ carrier L" for a + using that unfolding f_def g_def by simp + with \set q \ carrier L\ have "map f (map g q) = q" + by (induct q) (auto) + thus ?thesis + unfolding f_def g_def by simp + qed + moreover have "(\x. the_elem (?f ` x)) (?surj X\<^bsub>L\<^esub>) = \\<^bsub>i\<^esub>" + using UP.weak_ring_morphism_range[OF weak_morphism L.var_closed(1)[OF L.carrier_is_subring]] + unfolding eval_pmod_var(1)[OF assms(1-3)] by simp + ultimately have "Hom.S.eval q \\<^bsub>i\<^esub> = (\x. the_elem (?f ` x)) (Rupt.eval (map (?surj \ L.poly_of_const) q) (?surj X\<^bsub>L\<^esub>))" + using Hom.eval_hom'[OF _ map_surj] by auto + moreover have "\\<^bsub>?Rupt\<^esub> = ?surj \\<^bsub>poly_ring L\<^esub>" + unfolding rupture_def FactRing_def by (simp add: I.a_rcos_const) + hence "the_elem (?f ` \\<^bsub>?Rupt\<^esub>) = \\<^bsub>image_poly q\<^esub>" + using UP.weak_ring_morphism_range[OF weak_morphism UP.zero_closed] + unfolding image_ring_zero by simp + hence "(\x. the_elem (?f ` x)) (Rupt.eval (map (?surj \ L.poly_of_const) q) (?surj X\<^bsub>L\<^esub>)) = \\<^bsub>image_poly q\<^esub>" + using L.polynomial_rupture[OF L.carrier_is_subring assms(2)] by simp + ultimately show ?thesis + by simp +qed + +end (* of fixed L context. *) + +end (* of ring context. *) + +end \ No newline at end of file diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Polynomial_Divisibility.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Sun Apr 14 12:00:17 2019 +0100 @@ -0,0 +1,1221 @@ +(* Title: HOL/Algebra/Polynomial_Divisibility.thy + Author: Paulo Emílio de Vilhena +*) + +theory Polynomial_Divisibility + imports Polynomials Embedded_Algebras "HOL-Library.Multiset" + +begin + +section \Divisibility of Polynomials\ + +subsection \Definitions\ + +abbreviation poly_ring :: "_ \ ('a list) ring" + where "poly_ring R \ univ_poly R (carrier R)" + +abbreviation pirreducible :: "_ \ 'a set \ 'a list \ bool" ("pirreducible\") + where "pirreducible\<^bsub>R\<^esub> K p \ ring_irreducible\<^bsub>(univ_poly R K)\<^esub> p" + +abbreviation pprime :: "_ \ 'a set \ 'a list \ bool" ("pprime\") + where "pprime\<^bsub>R\<^esub> K p \ ring_prime\<^bsub>(univ_poly R K)\<^esub> p" + +definition pdivides :: "_ \ 'a list \ 'a list \ bool" (infix "pdivides\" 65) + where "p pdivides\<^bsub>R\<^esub> q = p divides\<^bsub>(univ_poly R (carrier R))\<^esub> q" + +definition rupture :: "_ \ 'a set \ 'a list \ (('a list) set) ring" ("Rupt\") + where "Rupt\<^bsub>R\<^esub> K p = (K[X]\<^bsub>R\<^esub>) Quot (PIdl\<^bsub>K[X]\<^bsub>R\<^esub>\<^esub> p)" + +abbreviation (in ring) rupture_surj :: "'a set \ 'a list \ 'a list \ ('a list) set" + where "rupture_surj K p \ (\q. (PIdl\<^bsub>K[X]\<^esub> p) +>\<^bsub>K[X]\<^esub> q)" + + +subsection \Basic Properties\ + +lemma (in ring) carrier_polynomial_shell [intro]: + assumes "subring K R" and "p \ carrier (K[X])" shows "p \ carrier (poly_ring R)" + using carrier_polynomial[OF assms(1), of p] assms(2) unfolding sym[OF univ_poly_carrier] by simp + +lemma (in domain) pdivides_zero: + assumes "subring K R" and "p \ carrier (K[X])" shows "p pdivides []" + using ring.divides_zero[OF univ_poly_is_ring[OF carrier_is_subring] + carrier_polynomial_shell[OF assms]] + unfolding univ_poly_zero pdivides_def . + +lemma (in domain) zero_pdivides_zero: "[] pdivides []" + using pdivides_zero[OF carrier_is_subring] univ_poly_carrier by blast + +lemma (in domain) zero_pdivides: + shows "[] pdivides p \ p = []" + using ring.zero_divides[OF univ_poly_is_ring[OF carrier_is_subring]] + unfolding univ_poly_zero pdivides_def . + +lemma (in domain) pprime_iff_pirreducible: + assumes "subfield K R" and "p \ carrier (K[X])" + shows "pprime K p \ pirreducible K p" + using principal_domain.primeness_condition[OF univ_poly_is_principal] assms by simp + +lemma (in domain) pirreducibleE: + assumes "subring K R" "p \ carrier (K[X])" "pirreducible K p" + shows "p \ []" "p \ Units (K[X])" + and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \ + p = q \\<^bsub>K[X]\<^esub> r \ q \ Units (K[X]) \ r \ Units (K[X])" + using domain.ring_irreducibleE[OF univ_poly_is_domain[OF assms(1)] _ assms(3)] assms(2) + by (auto simp add: univ_poly_zero) + +lemma (in domain) pirreducibleI: + assumes "subring K R" "p \ carrier (K[X])" "p \ []" "p \ Units (K[X])" + and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \ + p = q \\<^bsub>K[X]\<^esub> r \ q \ Units (K[X]) \ r \ Units (K[X])" + shows "pirreducible K p" + using domain.ring_irreducibleI[OF univ_poly_is_domain[OF assms(1)] _ assms(4)] assms(2-3,5) + by (auto simp add: univ_poly_zero) + +lemma (in domain) univ_poly_carrier_units_incl: + shows "Units ((carrier R) [X]) \ { [ k ] | k. k \ carrier R - { \ } }" +proof + fix p assume "p \ Units ((carrier R) [X])" + then obtain q + where p: "polynomial (carrier R) p" and q: "polynomial (carrier R) q" and pq: "poly_mult p q = [ \ ]" + unfolding Units_def univ_poly_def by auto + hence not_nil: "p \ []" and "q \ []" + using poly_mult_integral[OF carrier_is_subring p q] poly_mult_zero[OF polynomial_incl[OF p]] by auto + hence "degree p = 0" + using poly_mult_degree_eq[OF carrier_is_subring p q] unfolding pq by simp + hence "length p = 1" + using not_nil by (metis One_nat_def Suc_pred length_greater_0_conv) + then obtain k where k: "p = [ k ]" + by (metis One_nat_def length_0_conv length_Suc_conv) + hence "k \ carrier R - { \ }" + using p unfolding polynomial_def by auto + thus "p \ { [ k ] | k. k \ carrier R - { \ } }" + unfolding k by blast +qed + +lemma (in field) univ_poly_carrier_units: + "Units ((carrier R) [X]) = { [ k ] | k. k \ carrier R - { \ } }" +proof + show "Units ((carrier R) [X]) \ { [ k ] | k. k \ carrier R - { \ } }" + using univ_poly_carrier_units_incl by simp +next + show "{ [ k ] | k. k \ carrier R - { \ } } \ Units ((carrier R) [X])" + proof (auto) + fix k assume k: "k \ carrier R" "k \ \" + hence inv_k: "inv k \ carrier R" "inv k \ \" and "k \ inv k = \" "inv k \ k = \" + using subfield_m_inv[OF carrier_is_subfield, of k] by auto + hence "poly_mult [ k ] [ inv k ] = [ \ ]" and "poly_mult [ inv k ] [ k ] = [ \ ]" + by (auto simp add: k) + moreover have "polynomial (carrier R) [ k ]" and "polynomial (carrier R) [ inv k ]" + using const_is_polynomial k inv_k by auto + ultimately show "[ k ] \ Units ((carrier R) [X])" + unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps) + qed +qed + +lemma (in domain) univ_poly_units_incl: + assumes "subring K R" shows "Units (K[X]) \ { [ k ] | k. k \ K - { \ } }" + using domain.univ_poly_carrier_units_incl[OF subring_is_domain[OF assms]] + univ_poly_consistent[OF assms] by auto + +lemma (in ring) univ_poly_units: + assumes "subfield K R" shows "Units (K[X]) = { [ k ] | k. k \ K - { \ } }" + using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]] + univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto + +corollary (in domain) rupture_one_not_zero: + assumes "subfield K R" and "p \ carrier (K[X])" and "degree p > 0" + shows "\\<^bsub>Rupt K p\<^esub> \ \\<^bsub>Rupt K p\<^esub>" +proof (rule ccontr) + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + assume "\ \\<^bsub>Rupt K p\<^esub> \ \\<^bsub>Rupt K p\<^esub>" + then have "PIdl\<^bsub>K[X]\<^esub> p +>\<^bsub>K[X]\<^esub> \\<^bsub>K[X]\<^esub> = PIdl\<^bsub>K[X]\<^esub> p" + unfolding rupture_def FactRing_def by simp + hence "\\<^bsub>K[X]\<^esub> \ PIdl\<^bsub>K[X]\<^esub> p" + using ideal.rcos_const_imp_mem[OF UP.cgenideal_ideal[OF assms(2)]] by auto + then obtain q where "q \ carrier (K[X])" and "\\<^bsub>K[X]\<^esub> = q \\<^bsub>K[X]\<^esub> p" + using assms(2) unfolding cgenideal_def by auto + hence "p \ Units (K[X])" + unfolding Units_def using assms(2) UP.m_comm by auto + hence "degree p = 0" + unfolding univ_poly_units[OF assms(1)] by auto + with \degree p > 0\ show False + by simp +qed + +corollary (in ring) pirreducible_degree: + assumes "subfield K R" "p \ carrier (K[X])" "pirreducible K p" + shows "degree p \ 1" +proof (rule ccontr) + assume "\ degree p \ 1" then have "length p \ 1" + by simp + moreover have "p \ []" and "p \ Units (K[X])" + using assms(3) by (auto simp add: ring_irreducible_def irreducible_def univ_poly_zero) + ultimately obtain k where k: "p = [ k ]" + by (metis append_butlast_last_id butlast_take diff_is_0_eq le_refl self_append_conv2 take0 take_all) + hence "k \ K" and "k \ \" + using assms(2) by (auto simp add: polynomial_def univ_poly_def) + hence "p \ Units (K[X])" + using univ_poly_units[OF assms(1)] unfolding k by auto + from \p \ Units (K[X])\ and \p \ Units (K[X])\ show False by simp +qed + +corollary (in domain) univ_poly_not_field: + assumes "subring K R" shows "\ field (K[X])" +proof - + have "X \ carrier (K[X]) - { \\<^bsub>(K[X])\<^esub> }" and "X \ { [ k ] | k. k \ K - { \ } }" + using var_closed(1)[OF assms] unfolding univ_poly_zero var_def by auto + thus ?thesis + using field.field_Units[of "K[X]"] univ_poly_units_incl[OF assms] by blast +qed + +lemma (in domain) rupture_is_field_iff_pirreducible: + assumes "subfield K R" and "p \ carrier (K[X])" + shows "field (Rupt K p) \ pirreducible K p" +proof + assume "pirreducible K p" thus "field (Rupt K p)" + using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF assms(1)]] assms(2) + pprime_iff_pirreducible[OF assms] pirreducibleE(1)[OF subfieldE(1)[OF assms(1)]] + by (simp add: univ_poly_zero rupture_def) +next + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + assume field: "field (Rupt K p)" + have "p \ []" + proof (rule ccontr) + assume "\ p \ []" then have p: "p = []" + by simp + hence "Rupt K p \ (K[X])" + using UP.FactRing_zeroideal(1) UP.genideal_zero + UP.cgenideal_eq_genideal[OF UP.zero_closed] + by (simp add: rupture_def univ_poly_zero) + then obtain h where h: "h \ ring_iso (Rupt K p) (K[X])" + unfolding is_ring_iso_def by blast + moreover have "ring (Rupt K p)" + using field by (simp add: cring_def domain_def field_def) + ultimately interpret R: ring_hom_ring "Rupt K p" "K[X]" h + unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def + using UP.ring_axioms by simp + have "field (K[X])" + using field.ring_iso_imp_img_field[OF field h] by simp + thus False + using univ_poly_not_field[OF subfieldE(1)[OF assms(1)]] by simp + qed + thus "pirreducible K p" + using UP.field_iff_prime pprime_iff_pirreducible[OF assms] assms(2) field + by (simp add: univ_poly_zero rupture_def) +qed + +lemma (in domain) rupture_surj_hom: + assumes "subring K R" and "p \ carrier (K[X])" + shows "(rupture_surj K p) \ ring_hom (K[X]) (Rupt K p)" + and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)" +proof - + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF assms(1)] . + interpret I: ideal "PIdl\<^bsub>K[X]\<^esub> p" "K[X]" + using UP.cgenideal_ideal[OF assms(2)] . + show "(rupture_surj K p) \ ring_hom (K[X]) (Rupt K p)" + and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)" + using ring_hom_ring.intro[OF UP.ring_axioms I.quotient_is_ring] I.rcos_ring_hom + unfolding symmetric[OF ring_hom_ring_axioms_def] rupture_def by auto +qed + +corollary (in domain) rupture_surj_norm_is_hom: + assumes "subring K R" and "p \ carrier (K[X])" + shows "((rupture_surj K p) \ poly_of_const) \ ring_hom (R \ carrier := K \) (Rupt K p)" + using ring_hom_trans[OF canonical_embedding_is_hom[OF assms(1)] rupture_surj_hom(1)[OF assms]] . + +lemma (in domain) norm_map_in_poly_ring_carrier: + assumes "p \ carrier (poly_ring R)" and "\a. a \ carrier R \ f a \ carrier (poly_ring R)" + shows "ring.normalize (poly_ring R) (map f p) \ carrier (poly_ring (poly_ring R))" +proof - + have "set p \ carrier R" + using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "set (map f p) \ carrier (poly_ring R)" + using assms(2) by auto + thus ?thesis + using ring.normalize_gives_polynomial[OF univ_poly_is_ring[OF carrier_is_subring]] + unfolding univ_poly_carrier by simp +qed + +lemma (in domain) map_in_poly_ring_carrier: + assumes "p \ carrier (poly_ring R)" and "\a. a \ carrier R \ f a \ carrier (poly_ring R)" + and "\a. a \ \ \ f a \ []" + shows "map f p \ carrier (poly_ring (poly_ring R))" +proof - + interpret UP: ring "poly_ring R" + using univ_poly_is_ring[OF carrier_is_subring] . + have "lead_coeff p \ \" if "p \ []" + using that assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "ring.normalize (poly_ring R) (map f p) = map f p" + by (cases p) (simp_all add: assms(3) univ_poly_zero) + thus ?thesis + using norm_map_in_poly_ring_carrier[of p f] assms(1-2) by simp +qed + +lemma (in domain) map_norm_in_poly_ring_carrier: + assumes "subring K R" and "p \ carrier (K[X])" + shows "map poly_of_const p \ carrier (poly_ring (K[X]))" + using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]] +proof - + have "\a. a \ K \ poly_of_const a \ carrier (K[X])" + and "\a. a \ \ \ poly_of_const a \ []" + using ring_hom_memE(1)[OF canonical_embedding_is_hom[OF assms(1)]] + by (auto simp: poly_of_const_def) + thus ?thesis + using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]] assms(2) + unfolding univ_poly_consistent[OF assms(1)] by simp +qed + +lemma (in domain) polynomial_rupture: + assumes "subring K R" and "p \ carrier (K[X])" + shows "(ring.eval (Rupt K p)) (map ((rupture_surj K p) \ poly_of_const) p) (rupture_surj K p X) = \\<^bsub>Rupt K p\<^esub>" +proof - + let ?surj = "rupture_surj K p" + + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF assms(1)] . + interpret Hom: ring_hom_ring "K[X]" "Rupt K p" ?surj + using rupture_surj_hom(2)[OF assms] . + + have "(Hom.S.eval) (map (?surj \ poly_of_const) p) (?surj X) = ?surj ((UP.eval) (map poly_of_const p) X)" + using Hom.eval_hom[OF UP.carrier_is_subring var_closed(1)[OF assms(1)] + map_norm_in_poly_ring_carrier[OF assms]] by simp + also have " ... = ?surj p" + unfolding sym[OF eval_rewrite[OF assms]] .. + also have " ... = \\<^bsub>Rupt K p\<^esub>" + using UP.a_rcos_zero[OF UP.cgenideal_ideal[OF assms(2)] UP.cgenideal_self[OF assms(2)]] + unfolding rupture_def FactRing_def by simp + finally show ?thesis . +qed + + +subsection \Division\ + +definition (in ring) long_divides :: "'a list \ 'a list \ ('a list \ 'a list) \ bool" + where "long_divides p q t \ + \ \i\ (t \ carrier (poly_ring R) \ carrier (poly_ring R)) \ + \ \ii\ (p = (q \\<^bsub>poly_ring R\<^esub> (fst t)) \\<^bsub>poly_ring R\<^esub> (snd t)) \ + \ \iii\ (snd t = [] \ degree (snd t) < degree q)" + +definition (in ring) long_division :: "'a list \ 'a list \ ('a list \ 'a list)" + where "long_division p q = (THE t. long_divides p q t)" + +definition (in ring) pdiv :: "'a list \ 'a list \ 'a list" (infixl "pdiv" 65) + where "p pdiv q = (if q = [] then [] else fst (long_division p q))" + +definition (in ring) pmod :: "'a list \ 'a list \ 'a list" (infixl "pmod" 65) + where "p pmod q = (if q = [] then p else snd (long_division p q))" + + +lemma (in ring) long_dividesI: + assumes "b \ carrier (poly_ring R)" and "r \ carrier (poly_ring R)" + and "p = (q \\<^bsub>poly_ring R\<^esub> b) \\<^bsub>poly_ring R\<^esub> r" and "r = [] \ degree r < degree q" + shows "long_divides p q (b, r)" + using assms unfolding long_divides_def by auto + +lemma (in domain) exists_long_division: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []" + obtains b r where "b \ carrier (K[X])" and "r \ carrier (K[X])" and "long_divides p q (b, r)" + using subfield_long_division_theorem_shell[OF assms(1-3)] assms(4) + carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] + unfolding long_divides_def univ_poly_zero univ_poly_add univ_poly_mult by auto + +lemma (in domain) exists_unique_long_division: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []" + shows "\!t. long_divides p q t" +proof - + let ?padd = "\a b. a \\<^bsub>poly_ring R\<^esub> b" + let ?pmult = "\a b. a \\<^bsub>poly_ring R\<^esub> b" + let ?pminus = "\a b. a \\<^bsub>poly_ring R\<^esub> b" + + interpret UP: domain "poly_ring R" + using univ_poly_is_domain[OF carrier_is_subring] . + + obtain b r where ldiv: "long_divides p q (b, r)" + using exists_long_division[OF assms] by metis + + moreover have "(b, r) = (b', r')" if "long_divides p q (b', r')" for b' r' + proof - + have q: "q \ carrier (poly_ring R)" "q \ []" + using assms(3-4) carrier_polynomial[OF subfieldE(1)[OF assms(1)]] + unfolding univ_poly_carrier by auto + hence in_carrier: "q \ carrier (poly_ring R)" + "b \ carrier (poly_ring R)" "r \ carrier (poly_ring R)" + "b' \ carrier (poly_ring R)" "r' \ carrier (poly_ring R)" + using assms(3) that ldiv unfolding long_divides_def by auto + have "?pminus (?padd (?pmult q b) r) r' = ?pminus (?padd (?pmult q b') r') r'" + using ldiv and that unfolding long_divides_def by auto + hence eq: "?padd (?pmult q (?pminus b b')) (?pminus r r') = \\<^bsub>poly_ring R\<^esub>" + using in_carrier by algebra + have "b = b'" + proof (rule ccontr) + assume "b \ b'" + hence pminus: "?pminus b b' \ \\<^bsub>poly_ring R\<^esub>" "?pminus b b' \ carrier (poly_ring R)" + using in_carrier(2,4) by (metis UP.add.inv_closed UP.l_neg UP.minus_eq UP.minus_unique, algebra) + hence degree_ge: "degree (?pmult q (?pminus b b')) \ degree q" + using poly_mult_degree_eq[OF carrier_is_subring, of q "?pminus b b'"] q + unfolding univ_poly_zero univ_poly_carrier univ_poly_mult by simp + + have "?pminus b b' = \\<^bsub>poly_ring R\<^esub>" if "?pminus r r' = \\<^bsub>poly_ring R\<^esub>" + using eq pminus(2) q UP.integral univ_poly_zero unfolding that by auto + hence "?pminus r r' \ []" + using pminus(1) unfolding univ_poly_zero by blast + moreover have "?pminus r r' = []" if "r = []" and "r' = []" + using univ_poly_a_inv_def'[OF carrier_is_subring UP.zero_closed] that + unfolding a_minus_def univ_poly_add univ_poly_zero by auto + ultimately have "r \ [] \ r' \ []" + by blast + hence "max (degree r) (degree r') < degree q" + using ldiv and that unfolding long_divides_def by auto + moreover have "degree (?pminus r r') \ max (degree r) (degree r')" + using poly_add_degree[of r "map (a_inv R) r'"] + unfolding a_minus_def univ_poly_add univ_poly_a_inv_def'[OF carrier_is_subring in_carrier(5)] + by auto + ultimately have degree_lt: "degree (?pminus r r') < degree q" + by linarith + have is_poly: "polynomial (carrier R) (?pmult q (?pminus b b'))" "polynomial (carrier R) (?pminus r r')" + using in_carrier pminus(2) unfolding univ_poly_carrier by algebra+ + + have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = degree (?pmult q (?pminus b b'))" + using poly_add_degree_eq[OF carrier_is_subring is_poly] degree_ge degree_lt + unfolding univ_poly_carrier sym[OF univ_poly_add[of R "carrier R"]] max_def by simp + hence "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) > 0" + using degree_ge degree_lt by simp + moreover have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = 0" + using eq unfolding univ_poly_zero by simp + ultimately show False by simp + qed + hence "?pminus r r' = \\<^bsub>poly_ring R\<^esub>" + using in_carrier eq by algebra + hence "r = r'" + using in_carrier by (metis UP.add.inv_closed UP.add.right_cancel UP.minus_eq UP.r_neg) + with \b = b'\ show ?thesis + by simp + qed + + ultimately show ?thesis + by auto +qed + +lemma (in domain) long_divisionE: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []" + shows "long_divides p q (p pdiv q, p pmod q)" + using theI'[OF exists_unique_long_division[OF assms]] assms(4) + unfolding pmod_def pdiv_def long_division_def by auto + +lemma (in domain) long_divisionI: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []" + shows "long_divides p q (b, r) \ (b, r) = (p pdiv q, p pmod q)" + using exists_unique_long_division[OF assms] long_divisionE[OF assms] by metis + +lemma (in domain) long_division_closed: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])" +proof - + have "p pdiv q \ carrier (K[X]) \ p pmod q \ carrier (K[X])" + using assms univ_poly_zero_closed[of R] long_divisionI[of K] exists_long_division[OF assms] + by (cases "q = []") (simp add: pdiv_def pmod_def, metis Pair_inject)+ + thus "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])" + by auto +qed + +lemma (in domain) pdiv_pmod: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p = (q \\<^bsub>K[X]\<^esub> (p pdiv q)) \\<^bsub>K[X]\<^esub> (p pmod q)" +proof (cases) + interpret UP: ring "K[X]" + using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] . + assume "q = []" thus ?thesis + using assms(2) unfolding pdiv_def pmod_def sym[OF univ_poly_zero[of R K]] by simp +next + assume "q \ []" thus ?thesis + using long_divisionE[OF assms] unfolding long_divides_def univ_poly_mult univ_poly_add by simp +qed + +lemma (in domain) pmod_degree: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []" + shows "p pmod q = [] \ degree (p pmod q) < degree q" + using long_divisionE[OF assms] unfolding long_divides_def by auto + +lemma (in domain) pmod_const: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" and "degree q > degree p" + shows "p pdiv q = []" and "p pmod q = p" +proof - + have "p pdiv q = [] \ p pmod q = p" + proof (cases) + interpret UP: ring "K[X]" + using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] . + + assume "q \ []" + have "p = (q \\<^bsub>K[X]\<^esub> []) \\<^bsub>K[X]\<^esub> p" + using assms(2-3) unfolding sym[OF univ_poly_zero[of R K]] by simp + moreover have "([], p) \ carrier (poly_ring R) \ carrier (poly_ring R)" + using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] by auto + ultimately have "long_divides p q ([], p)" + using assms(4) unfolding long_divides_def univ_poly_mult univ_poly_add by auto + with \q \ []\ show ?thesis + using long_divisionI[OF assms(1-3)] by auto + qed (simp add: pmod_def pdiv_def) + thus "p pdiv q = []" and "p pmod q = p" + by auto +qed + +lemma (in domain) long_division_zero: + assumes "subfield K R" and "q \ carrier (K[X])" shows "[] pdiv q = []" and "[] pmod q = []" +proof - + interpret UP: ring "poly_ring R" + using univ_poly_is_ring[OF carrier_is_subring] . + + have "[] pdiv q = [] \ [] pmod q = []" + proof (cases) + assume "q \ []" + have "q \ carrier (poly_ring R)" + using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] . + hence "long_divides [] q ([], [])" + unfolding long_divides_def sym[OF univ_poly_zero[of R "carrier R"]] by auto + with \q \ []\ show ?thesis + using long_divisionI[OF assms(1) univ_poly_zero_closed assms(2)] by simp + qed (simp add: pmod_def pdiv_def) + thus "[] pdiv q = []" and "[] pmod q = []" + by auto +qed + +lemma (in domain) long_division_a_inv: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "((\\<^bsub>K[X]\<^esub> p) pdiv q) = \\<^bsub>K[X]\<^esub> (p pdiv q)" (is "?pdiv") + and "((\\<^bsub>K[X]\<^esub> p) pmod q) = \\<^bsub>K[X]\<^esub> (p pmod q)" (is "?pmod") +proof - + interpret UP: ring "K[X]" + using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] . + + have "?pdiv \ ?pmod" + proof (cases) + assume "q = []" thus ?thesis + unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp + next + assume not_nil: "q \ []" + have "\\<^bsub>K[X]\<^esub> p = \\<^bsub>K[X]\<^esub> ((q \\<^bsub>K[X]\<^esub> (p pdiv q)) \\<^bsub>K[X]\<^esub> (p pmod q))" + using pdiv_pmod[OF assms] by simp + hence "\\<^bsub>K[X]\<^esub> p = (q \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> (p pdiv q))) \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> (p pmod q))" + using assms(2-3) long_division_closed[OF assms] by algebra + moreover have "\\<^bsub>K[X]\<^esub> (p pdiv q) \ carrier (K[X])" "\\<^bsub>K[X]\<^esub> (p pmod q) \ carrier (K[X])" + using long_division_closed[OF assms] by algebra+ + hence "(\\<^bsub>K[X]\<^esub> (p pdiv q), \\<^bsub>K[X]\<^esub> (p pmod q)) \ carrier (poly_ring R) \ carrier (poly_ring R)" + using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto + moreover have "\\<^bsub>K[X]\<^esub> (p pmod q) = [] \ degree (\\<^bsub>K[X]\<^esub> (p pmod q)) < degree q" + using univ_poly_a_inv_length[OF subfieldE(1)[OF assms(1)] + long_division_closed(2)[OF assms]] pmod_degree[OF assms not_nil] + by auto + ultimately have "long_divides (\\<^bsub>K[X]\<^esub> p) q (\\<^bsub>K[X]\<^esub> (p pdiv q), \\<^bsub>K[X]\<^esub> (p pmod q))" + unfolding long_divides_def univ_poly_mult univ_poly_add by simp + thus ?thesis + using long_divisionI[OF assms(1) UP.a_inv_closed[OF assms(2)] assms(3) not_nil] by simp + qed + thus ?pdiv and ?pmod + by auto +qed + +lemma (in domain) long_division_add: + assumes "subfield K R" and "a \ carrier (K[X])" "b \ carrier (K[X])" "q \ carrier (K[X])" + shows "(a \\<^bsub>K[X]\<^esub> b) pdiv q = (a pdiv q) \\<^bsub>K[X]\<^esub> (b pdiv q)" (is "?pdiv") + and "(a \\<^bsub>K[X]\<^esub> b) pmod q = (a pmod q) \\<^bsub>K[X]\<^esub> (b pmod q)" (is "?pmod") +proof - + let ?pdiv_add = "(a pdiv q) \\<^bsub>K[X]\<^esub> (b pdiv q)" + let ?pmod_add = "(a pmod q) \\<^bsub>K[X]\<^esub> (b pmod q)" + + interpret UP: ring "K[X]" + using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] . + + have "?pdiv \ ?pmod" + proof (cases) + assume "q = []" thus ?thesis + using assms(2-3) unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp + next + note in_carrier = long_division_closed[OF assms(1,2,4)] + long_division_closed[OF assms(1,3,4)] + + assume "q \ []" + have "a \\<^bsub>K[X]\<^esub> b = ((q \\<^bsub>K[X]\<^esub> (a pdiv q)) \\<^bsub>K[X]\<^esub> (a pmod q)) \\<^bsub>K[X]\<^esub> + ((q \\<^bsub>K[X]\<^esub> (b pdiv q)) \\<^bsub>K[X]\<^esub> (b pmod q))" + using assms(2-3)[THEN pdiv_pmod[OF assms(1) _ assms(4)]] by simp + hence "a \\<^bsub>K[X]\<^esub> b = (q \\<^bsub>K[X]\<^esub> ?pdiv_add) \\<^bsub>K[X]\<^esub> ?pmod_add" + using assms(4) in_carrier by algebra + moreover have "(?pdiv_add, ?pmod_add) \ carrier (poly_ring R) \ carrier (poly_ring R)" + using in_carrier carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto + moreover have "?pmod_add = [] \ degree ?pmod_add < degree q" + proof (cases) + assume "?pmod_add \ []" + hence "a pmod q \ [] \ b pmod q \ []" + using in_carrier(2,4) unfolding sym[OF univ_poly_zero[of R K]] by auto + moreover from \q \ []\ + have "a pmod q = [] \ degree (a pmod q) < degree q" and "b pmod q = [] \ degree (b pmod q) < degree q" + using assms(2-3)[THEN pmod_degree[OF assms(1) _ assms(4)]] by auto + ultimately have "max (degree (a pmod q)) (degree (b pmod q)) < degree q" + by auto + thus ?thesis + using poly_add_degree le_less_trans unfolding univ_poly_add by blast + qed simp + ultimately have "long_divides (a \\<^bsub>K[X]\<^esub> b) q (?pdiv_add, ?pmod_add)" + unfolding long_divides_def univ_poly_mult univ_poly_add by simp + with \q \ []\ show ?thesis + using long_divisionI[OF assms(1) UP.a_closed[OF assms(2-3)] assms(4)] by simp + qed + thus ?pdiv and ?pmod + by auto +qed + +lemma (in domain) long_division_add_iff: + assumes "subfield K R" + and "a \ carrier (K[X])" "b \ carrier (K[X])" "c \ carrier (K[X])" "q \ carrier (K[X])" + shows "a pmod q = b pmod q \ (a \\<^bsub>K[X]\<^esub> c) pmod q = (b \\<^bsub>K[X]\<^esub> c) pmod q" +proof - + interpret UP: ring "K[X]" + using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] . + show ?thesis + using assms(2-4)[THEN long_division_closed(2)[OF assms(1) _ assms(5)]] + unfolding assms(2-3)[THEN long_division_add(2)[OF assms(1) _ assms(4-5)]] by auto +qed + +lemma (in domain) pdivides_iff: + assumes "subfield K R" and "polynomial K p" "polynomial K q" + shows "p pdivides q \ p divides\<^bsub>K[X]\<^esub> q" +proof + show "p divides\<^bsub>K [X]\<^esub> q \ p pdivides q" + using carrier_polynomial[OF subfieldE(1)[OF assms(1)]] + unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by auto +next + interpret UP: ring "poly_ring R" + using univ_poly_is_ring[OF carrier_is_subring] . + + have in_carrier: "p \ carrier (poly_ring R)" "q \ carrier (poly_ring R)" + using carrier_polynomial[OF subfieldE(1)[OF assms(1)]] assms + unfolding univ_poly_carrier by auto + + assume "p pdivides q" + then obtain b where "b \ carrier (poly_ring R)" and "q = p \\<^bsub>poly_ring R\<^esub> b" + unfolding pdivides_def factor_def by blast + show "p divides\<^bsub>K[X]\<^esub> q" + proof (cases) + assume "p = []" + with \b \ carrier (poly_ring R)\ and \q = p \\<^bsub>poly_ring R\<^esub> b\ have "q = []" + unfolding univ_poly_mult sym[OF univ_poly_carrier] + using poly_mult_zero(1)[OF polynomial_incl] by simp + with \p = []\ show ?thesis + using poly_mult_zero(2)[of "[]"] + unfolding factor_def univ_poly_mult by auto + next + interpret UP: ring "poly_ring R" + using univ_poly_is_ring[OF carrier_is_subring] . + + assume "p \ []" + from \p pdivides q\ obtain b where "b \ carrier (poly_ring R)" and "q = p \\<^bsub>poly_ring R\<^esub> b" + unfolding pdivides_def factor_def by blast + moreover have "p \ carrier (poly_ring R)" and "q \ carrier (poly_ring R)" + using assms carrier_polynomial[OF subfieldE(1)[OF assms(1)]] unfolding univ_poly_carrier by auto + ultimately have "q = (p \\<^bsub>poly_ring R\<^esub> b) \\<^bsub>poly_ring R\<^esub> \\<^bsub>poly_ring R\<^esub>" + by algebra + with \b \ carrier (poly_ring R)\ have "long_divides q p (b, [])" + unfolding long_divides_def univ_poly_zero by auto + with \p \ []\ have "b \ carrier (K[X])" + using long_divisionI[of K q p b] long_division_closed[of K q p] assms + unfolding univ_poly_carrier by auto + with \q = p \\<^bsub>poly_ring R\<^esub> b\ show ?thesis + unfolding factor_def univ_poly_mult by blast + qed +qed + +lemma (in domain) pdivides_iff_shell: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p pdivides q \ p divides\<^bsub>K[X]\<^esub> q" + using pdivides_iff assms by (simp add: univ_poly_carrier) + +lemma (in domain) pmod_zero_iff_pdivides: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p pmod q = [] \ q pdivides p" +proof - + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] . + + show ?thesis + proof + assume pmod: "p pmod q = []" + have "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])" + using long_division_closed[OF assms] by auto + hence "p = q \\<^bsub>K[X]\<^esub> (p pdiv q)" + using pdiv_pmod[OF assms] assms(3) unfolding pmod sym[OF univ_poly_zero[of R K]] by algebra + with \p pdiv q \ carrier (K[X])\ show "q pdivides p" + unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast + next + assume "q pdivides p" show "p pmod q = []" + proof (cases) + assume "q = []" with \q pdivides p\ show ?thesis + using zero_pdivides unfolding pmod_def by simp + next + assume "q \ []" + from \q pdivides p\ obtain r where "r \ carrier (K[X])" and "p = q \\<^bsub>K[X]\<^esub> r" + unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast + hence "p = (q \\<^bsub>K[X]\<^esub> r) \\<^bsub>K[X]\<^esub> []" + using assms(2) unfolding sym[OF univ_poly_zero[of R K]] by simp + moreover from \r \ carrier (K[X])\ have "r \ carrier (poly_ring R)" + using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto + ultimately have "long_divides p q (r, [])" + unfolding long_divides_def univ_poly_mult univ_poly_add by auto + with \q \ []\ show ?thesis + using long_divisionI[OF assms] by simp + qed + qed +qed + +lemma (in domain) same_pmod_iff_pdivides: + assumes "subfield K R" and "a \ carrier (K[X])" "b \ carrier (K[X])" "q \ carrier (K[X])" + shows "a pmod q = b pmod q \ q pdivides (a \\<^bsub>K[X]\<^esub> b)" +proof - + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] . + + have "a pmod q = b pmod q \ (a \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> b)) pmod q = (b \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> b)) pmod q" + using long_division_add_iff[OF assms(1-3) UP.a_inv_closed[OF assms(3)] assms(4)] . + also have " ... \ (a \\<^bsub>K[X]\<^esub> b) pmod q = \\<^bsub>K[X]\<^esub> pmod q" + using assms(2-3) by algebra + also have " ... \ q pdivides (a \\<^bsub>K[X]\<^esub> b)" + using pmod_zero_iff_pdivides[OF assms(1) UP.minus_closed[OF assms(2-3)] assms(4)] + unfolding univ_poly_zero long_division_zero(2)[OF assms(1,4)] . + finally show ?thesis . +qed + +lemma (in domain) pdivides_imp_degree_le: + assumes "subring K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" "q \ []" + shows "p pdivides q \ degree p \ degree q" +proof - + assume "p pdivides q" + then obtain r where r: "polynomial (carrier R) r" "q = poly_mult p r" + unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by blast + moreover have p: "polynomial (carrier R) p" + using assms(2) carrier_polynomial[OF assms(1)] unfolding univ_poly_carrier by auto + moreover have "p \ []" and "r \ []" + using poly_mult_zero(2)[OF polynomial_incl[OF p]] r(2) assms(4) by auto + ultimately show "degree p \ degree q" + using poly_mult_degree_eq[OF carrier_is_subring, of p r] by auto +qed + +lemma (in domain) pprimeE: + assumes "subfield K R" "p \ carrier (K[X])" "pprime K p" + shows "p \ []" "p \ Units (K[X])" + and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \ + p pdivides (q \\<^bsub>K[X]\<^esub> r) \ p pdivides q \ p pdivides r" + using assms(2-3) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)] + unfolding ring_prime_def prime_def + by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero) + +lemma (in domain) pprimeI: + assumes "subfield K R" "p \ carrier (K[X])" "p \ []" "p \ Units (K[X])" + and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \ + p pdivides (q \\<^bsub>K[X]\<^esub> r) \ p pdivides q \ p pdivides r" + shows "pprime K p" + using assms(2-5) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)] + unfolding ring_prime_def prime_def + by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero) + +lemma (in domain) associated_polynomials_iff: + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p \\<^bsub>K[X]\<^esub> q \ (\k \ K - { \ }. p = [ k ] \\<^bsub>K[X]\<^esub> q)" + using domain.ring_associated_iff[OF univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] assms(2-3)] + unfolding univ_poly_units[OF assms(1)] by auto + +corollary (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *) + assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + shows "p \\<^bsub>K[X]\<^esub> q \ length p = length q" + unfolding associated_polynomials_iff[OF assms] + using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)],of q] assms(3) + by (auto simp add: univ_poly_carrier univ_poly_mult simp del: poly_mult.simps) + + +subsection \Ideals\ + +lemma (in domain) exists_unique_gen: + assumes "subfield K R" "ideal I (K[X])" "I \ { [] }" + shows "\!p \ carrier (K[X]). lead_coeff p = \ \ I = PIdl\<^bsub>K[X]\<^esub> p" + (is "\!p. ?generator p") +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + obtain q where q: "q \ carrier (K[X])" "I = PIdl\<^bsub>K[X]\<^esub> q" + using UP.exists_gen[OF assms(2)] by blast + hence not_nil: "q \ []" + using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3) + by (auto simp add: univ_poly_zero) + hence "lead_coeff q \ K - { \ }" + using q(1) unfolding univ_poly_def polynomial_def by auto + hence inv_lc_q: "inv (lead_coeff q) \ K - { \ }" "inv (lead_coeff q) \ lead_coeff q = \" + using subfield_m_inv[OF assms(1)] by auto + + define p where "p = [ inv (lead_coeff q) ] \\<^bsub>K[X]\<^esub> q" + have is_poly: "polynomial K [ inv (lead_coeff q) ]" "polynomial K q" + using inv_lc_q(1) q(1) unfolding univ_poly_def polynomial_def by auto + hence in_carrier: "p \ carrier (K[X])" + using UP.m_closed unfolding univ_poly_carrier p_def by simp + have lc_p: "lead_coeff p = \" + using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)] is_poly _ not_nil] inv_lc_q(2) + unfolding p_def univ_poly_mult[of R K] by simp + moreover have PIdl_p: "I = PIdl\<^bsub>K[X]\<^esub> p" + using UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) inv_lc_q(1) p_def + associated_polynomials_iff[OF assms(1) in_carrier q(1)] + by auto + ultimately have "?generator p" + using in_carrier by simp + + moreover + have "\r. \ r \ carrier (K[X]); lead_coeff r = \; I = PIdl\<^bsub>K[X]\<^esub> r \ \ r = p" + proof - + fix r assume r: "r \ carrier (K[X])" "lead_coeff r = \" "I = PIdl\<^bsub>K[X]\<^esub> r" + obtain k where k: "k \ K - { \ }" "r = [ k ] \\<^bsub>K[X]\<^esub> p" + using UP.associated_iff_same_ideal[OF r(1) in_carrier] PIdl_p r(3) + associated_polynomials_iff[OF assms(1) r(1) in_carrier] + by auto + hence "polynomial K [ k ]" + unfolding polynomial_def by simp + moreover have "p \ []" + using not_nil UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) PIdl_p + associated_polynomials_imp_same_length[OF assms(1) in_carrier q(1)] by auto + ultimately have "lead_coeff r = k \ (lead_coeff p)" + using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)]] in_carrier k(2) + unfolding univ_poly_def by (auto simp del: poly_mult.simps) + hence "k = \" + using lc_p r(2) k(1) subfieldE(3)[OF assms(1)] by auto + hence "r = map ((\) \) p" + using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)] _ k(1), of p] in_carrier + unfolding k(2) univ_poly_carrier[of R K] univ_poly_mult[of R K] by auto + moreover have "set p \ carrier R" + using polynomial_in_carrier[OF subfieldE(1)[OF assms(1)]] + in_carrier univ_poly_carrier[of R K] by auto + hence "map ((\) \) p = p" + by (induct p) (auto) + ultimately show "r = p" by simp + qed + + ultimately show ?thesis by blast +qed + +proposition (in domain) exists_unique_pirreducible_gen: + assumes "subfield K R" "ring_hom_ring (K[X]) R h" + and "a_kernel (K[X]) R h \ { [] }" "a_kernel (K[X]) R h \ carrier (K[X])" + shows "\!p \ carrier (K[X]). pirreducible K p \ lead_coeff p = \ \ a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> p" + (is "\!p. ?generator p") +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + have "ideal (a_kernel (K[X]) R h) (K[X])" + using ring_hom_ring.kernel_is_ideal[OF assms(2)] . + then obtain p + where p: "p \ carrier (K[X])" "lead_coeff p = \" "a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> p" + and unique: + "\q. \ q \ carrier (K[X]); lead_coeff q = \; a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> q \ \ q = p" + using exists_unique_gen[OF assms(1) _ assms(3)] by metis + + have "p \ carrier (K[X]) - { [] }" + using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3) p(1,3) + by (auto simp add: univ_poly_zero) + hence "pprime K p" + using ring_hom_ring.primeideal_vimage[OF assms(2) UP.is_cring zeroprimeideal] + UP.primeideal_iff_prime[of p] + unfolding univ_poly_zero sym[OF p(3)] a_kernel_def' by simp + hence "pirreducible K p" + using pprime_iff_pirreducible[OF assms(1) p(1)] by simp + thus ?thesis + using p unique by metis +qed + +lemma (in domain) cgenideal_pirreducible: + assumes "subfield K R" and "p \ carrier (K[X])" "pirreducible K p" + shows "\ pirreducible K q; q \ PIdl\<^bsub>K[X]\<^esub> p \ \ p \\<^bsub>K[X]\<^esub> q" +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + assume q: "pirreducible K q" "q \ PIdl\<^bsub>K[X]\<^esub> p" + hence in_carrier: "q \ carrier (K[X])" + using additive_subgroup.a_subset[OF ideal.axioms(1)[OF UP.cgenideal_ideal[OF assms(2)]]] by auto + hence "p divides\<^bsub>K[X]\<^esub> q" + by (meson q assms(2) UP.cgenideal_ideal UP.cgenideal_minimal UP.to_contain_is_to_divide) + then obtain r where r: "r \ carrier (K[X])" "q = p \\<^bsub>K[X]\<^esub> r" + by auto + hence "r \ Units (K[X])" + using pirreducibleE(3)[OF _ in_carrier q(1) assms(2) r(1)] subfieldE(1)[OF assms(1)] + pirreducibleE(2)[OF _ assms(2-3)] by auto + thus "p \\<^bsub>K[X]\<^esub> q" + using UP.ring_associated_iff[OF in_carrier assms(2)] r(2) UP.associated_sym + unfolding UP.m_comm[OF assms(2) r(1)] by auto +qed + + +subsection \Roots and Multiplicity\ + +lemma (in domain) pdivides_imp_root_sharing: + assumes "p \ carrier (poly_ring R)" "p pdivides q" and "a \ carrier R" + shows "eval p a = \ \ eval q a = \" +proof - + from \p pdivides q\ obtain r where r: "q = p \\<^bsub>poly_ring R\<^esub> r" "r \ carrier (poly_ring R)" + unfolding pdivides_def factor_def by auto + hence "eval q a = (eval p a) \ (eval r a)" + using ring_hom_memE(2)[OF eval_is_hom[OF carrier_is_subring assms(3)] assms(1) r(2)] by simp + thus "eval p a = \ \ eval q a = \" + using ring_hom_memE(1)[OF eval_is_hom[OF carrier_is_subring assms(3)] r(2)] by auto +qed + +lemma (in domain) degree_one_root: + assumes "subfield K R" and "p \ carrier (K[X])" and "degree p = 1" + shows "eval p (\ (inv (lead_coeff p) \ (const_term p))) = \" + and "inv (lead_coeff p) \ (const_term p) \ K" +proof - + from \degree p = 1\ have "length p = Suc (Suc 0)" + by simp + then obtain a b where p: "p = [ a, b ]" + by (metis (no_types, hide_lams) Suc_length_conv length_0_conv) + hence "a \ K - { \ }" "b \ K" and in_carrier: "a \ carrier R" "b \ carrier R" + using assms(2) subfieldE(3)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence inv_a: "inv a \ carrier R" "a \ inv a = \" and "inv a \ K" + using subfield_m_inv(1-2)[OF assms(1), of a] subfieldE(3)[OF assms(1)] by auto + hence "eval p (\ (inv a \ b)) = a \ (\ (inv a \ b)) \ b" + using in_carrier unfolding p by simp + also have " ... = \ (a \ (inv a \ b)) \ b" + using inv_a in_carrier by (simp add: r_minus) + also have " ... = \" + using in_carrier(2) unfolding sym[OF m_assoc[OF in_carrier(1) inv_a(1) in_carrier(2)]] inv_a(2) by algebra + finally have "eval p (\ (inv a \ b)) = \" . + moreover have ct: "const_term p = b" + using in_carrier unfolding p const_term_def by auto + ultimately show "eval p (\ (inv (lead_coeff p) \ (const_term p))) = \" + unfolding p by simp + from \inv a \ K\ and \b \ K\ + show "inv (lead_coeff p) \ (const_term p) \ K" + using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto +qed + + +subsection \Link between @{term \(pmod)\} and @{term rupture_surj}\ + +lemma (in domain) rupture_surj_composed_with_pmod: + assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" + shows "rupture_surj K p q = rupture_surj K p (q pmod p)" +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + interpret Rupt: ring "Rupt K p" + using assms by (simp add: UP.cgenideal_ideal ideal.quotient_is_ring rupture_def) + + let ?h = "rupture_surj K p" + + have "?h q = (?h p \\<^bsub>Rupt K p\<^esub> ?h (q pdiv p)) \\<^bsub>Rupt K p\<^esub> ?h (q pmod p)" + and "?h (q pdiv p) \ carrier (Rupt K p)" "?h (q pmod p) \ carrier (Rupt K p)" + using pdiv_pmod[OF assms(1,3,2)] long_division_closed[OF assms(1,3,2)] assms UP.m_closed + ring_hom_memE[OF rupture_surj_hom(1)[OF subfieldE(1)[OF assms(1)] assms(2)]] + by metis+ + moreover have "?h p = PIdl\<^bsub>K[X]\<^esub> p" + using assms by (simp add: UP.a_rcos_zero UP.cgenideal_ideal UP.cgenideal_self) + hence "?h p = \\<^bsub>Rupt K p\<^esub>" + unfolding rupture_def FactRing_def by simp + ultimately show ?thesis + by simp +qed + +corollary (in domain) rupture_carrier_as_pmod_image: + assumes "subfield K R" and "p \ carrier (K[X])" + shows "(rupture_surj K p) ` ((\q. q pmod p) ` (carrier (K[X]))) = carrier (Rupt K p)" + (is "?lhs = ?rhs") +proof + have "(\q. q pmod p) ` carrier (K[X]) \ carrier (K[X])" + using long_division_closed(2)[OF assms(1) _ assms(2)] by auto + thus "?lhs \ ?rhs" + using ring_hom_memE(1)[OF rupture_surj_hom(1)[OF subfieldE(1)[OF assms(1)] assms(2)]] by auto +next + show "?rhs \ ?lhs" + proof + fix a assume "a \ carrier (Rupt K p)" + then obtain q where "q \ carrier (K[X])" and "a = rupture_surj K p q" + unfolding rupture_def FactRing_def A_RCOSETS_def' by auto + thus "a \ ?lhs" + using rupture_surj_composed_with_pmod[OF assms] by auto + qed +qed + +(* Move to Ideal.thy ========================================================= *) +lemma (in ring) quotient_eq_iff_same_a_r_cos: + assumes "ideal I R" and "a \ carrier R" and "b \ carrier R" + shows "a \ b \ I \ I +> a = I +> b" +proof + assume "I +> a = I +> b" + then obtain i where "i \ I" and "\ \ a = i \ b" + using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2) + unfolding a_r_coset_def' by blast + hence "a \ b = i" + using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero) + with \i \ I\ show "a \ b \ I" + by simp +next + assume "a \ b \ I" + then obtain i where "i \ I" and "a = i \ b" + using ideal.Icarr[OF assms(1)] assms(2-3) + by (metis a_minus_def add.inv_solve_right) + hence "I +> a = (I +> i) +> b" + using ideal.Icarr[OF assms(1)] assms(3) + by (simp add: a_coset_add_assoc subsetI) + with \i \ I\ show "I +> a = I +> b" + using a_rcos_zero[OF assms(1)] by simp +qed +(* ========================================================================== *) + +lemma (in domain) rupture_surj_inj_on: + assumes "subfield K R" and "p \ carrier (K[X])" + shows "inj_on (rupture_surj K p) ((\q. q pmod p) ` (carrier (K[X])))" +proof (intro inj_onI) + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + fix a b + assume "a \ (\q. q pmod p) ` carrier (K[X])" + and "b \ (\q. q pmod p) ` carrier (K[X])" + then obtain q s + where q: "q \ carrier (K[X])" "a = q pmod p" + and s: "s \ carrier (K[X])" "b = s pmod p" + by auto + moreover assume "rupture_surj K p a = rupture_surj K p b" + ultimately have "q \\<^bsub>K[X]\<^esub> s \ (PIdl\<^bsub>K[X]\<^esub> p)" + using UP.quotient_eq_iff_same_a_r_cos[OF UP.cgenideal_ideal[OF assms(2)], of q s] + rupture_surj_composed_with_pmod[OF assms] by auto + hence "p pdivides (q \\<^bsub>K[X]\<^esub> s)" + using assms q(1) s(1) UP.to_contain_is_to_divide pdivides_iff_shell + by (meson UP.cgenideal_ideal UP.cgenideal_minimal UP.minus_closed) + thus "a = b" + unfolding q s same_pmod_iff_pdivides[OF assms(1) q(1) s(1) assms(2)] . +qed + + +subsection \Dimension\ + +definition (in ring) exp_base :: "'a \ nat \ 'a list" + where "exp_base x n = map (\i. x [^] i) (rev [0..< n])" + +lemma (in ring) exp_base_closed: + assumes "x \ carrier R" shows "set (exp_base x n) \ carrier R" + using assms by (induct n) (auto simp add: exp_base_def) + +lemma (in ring) exp_base_append: + shows "exp_base x (n + m) = (map (\i. x [^] i) (rev [n..< n + m])) @ exp_base x n" + unfolding exp_base_def by (metis map_append rev_append upt_add_eq_append zero_le) + +lemma (in ring) drop_exp_base: + shows "drop n (exp_base x m) = exp_base x (m - n)" +proof - + have ?thesis if "n > m" + using that by (simp add: exp_base_def) + moreover have ?thesis if "n \ m" + using exp_base_append[of x "m - n" n] that by auto + ultimately show ?thesis + by linarith +qed + +lemma (in ring) combine_eq_eval: + shows "combine Ks (exp_base x (length Ks)) = eval Ks x" + unfolding exp_base_def by (induct Ks) (auto) + +lemma (in domain) pmod_image_characterization: + assumes "subfield K R" and "p \ carrier (K[X])" and "p \ []" + shows "(\q. q pmod p) ` carrier (K[X]) = { q \ carrier (K[X]). length q \ degree p }" +proof - + interpret UP: principal_domain "K[X]" + using univ_poly_is_principal[OF assms(1)] . + + show ?thesis + proof (intro no_atp(10)[OF subsetI subsetI]) + fix q assume "q \ { q \ carrier (K[X]). length q \ degree p }" + then have "q \ carrier (K[X])" and "length q \ degree p" + by simp+ + + show "q \ (\q. q pmod p) ` carrier (K[X])" + proof (cases "q = []") + case True + have "p pmod p = q" + unfolding True pmod_zero_iff_pdivides[OF assms(1,2,2)] + using assms(1-2) pdivides_iff_shell by auto + thus ?thesis + using assms(2) by blast + next + case False + with \length q \ degree p\ have "degree q < degree p" + using le_eq_less_or_eq by fastforce + with \q \ carrier (K[X])\ show ?thesis + using pmod_const(2)[OF assms(1) _ assms(2), of q] by (metis imageI) + qed + next + fix q assume "q \ (\q. q pmod p) ` carrier (K[X])" + then obtain q' where "q' \ carrier (K[X])" and "q = q' pmod p" + by auto + thus "q \ { q \ carrier (K[X]). length q \ degree p }" + using long_division_closed(2)[OF assms(1) _ assms(2), of q'] + pmod_degree[OF assms(1) _ assms(2-3), of q'] + by auto + qed +qed + +lemma (in domain) Span_var_pow_base: + assumes "subfield K R" + shows "ring.Span (K[X]) (poly_of_const ` K) (ring.exp_base (K[X]) X n) = + { q \ carrier (K[X]). length q \ n }" (is "?lhs = ?rhs") +proof - + note subring = subfieldE(1)[OF assms] + note subfield = univ_poly_subfield_of_consts[OF assms] + + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subring] . + + show ?thesis + proof (intro no_atp(10)[OF subsetI subsetI]) + fix q assume "q \ { q \ carrier (K[X]). length q \ n }" + then have q: "q \ carrier (K[X])" "length q \ n" + by simp+ + + let ?repl = "replicate (n - length q) \\<^bsub>K[X]\<^esub>" + let ?map = "map poly_of_const q" + let ?comb = "UP.combine" + define Ks where "Ks = ?repl @ ?map" + + have "q = ?comb ?map (UP.exp_base X (length q))" + using q eval_rewrite[OF subring q(1)] unfolding sym[OF UP.combine_eq_eval] by auto + moreover from \length q \ n\ + have "?comb (?repl @ Ks) (UP.exp_base X n) = ?comb Ks (UP.exp_base X (length q))" + if "set Ks \ carrier (K[X])" for Ks + using UP.combine_prepend_replicate[OF that UP.exp_base_closed[OF var_closed(1)[OF subring]]] + unfolding UP.drop_exp_base by auto + + moreover have "set ?map \ carrier (K[X])" + using map_norm_in_poly_ring_carrier[OF subring q(1)] + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + + moreover have "?repl = map poly_of_const (replicate (n - length q) \)" + unfolding poly_of_const_def univ_poly_zero by (induct "n - length q") (auto) + hence "set ?repl \ poly_of_const ` K" + using subringE(2)[OF subring] by auto + moreover from \q \ carrier (K[X])\ have "set q \ K" + unfolding sym[OF univ_poly_carrier] polynomial_def by auto + hence "set ?map \ poly_of_const ` K" + by auto + + ultimately have "q = ?comb Ks (UP.exp_base X n)" and "set Ks \ poly_of_const ` K" + by (simp add: Ks_def)+ + thus "q \ UP.Span (poly_of_const ` K) (UP.exp_base X n)" + using UP.Span_eq_combine_set[OF subfield UP.exp_base_closed[OF var_closed(1)[OF subring]]] by auto + next + fix q assume "q \ UP.Span (poly_of_const ` K) (UP.exp_base X n)" + thus "q \ { q \ carrier (K[X]). length q \ n }" + proof (induction n arbitrary: q) + case 0 thus ?case + unfolding UP.exp_base_def by (auto simp add: univ_poly_zero) + next + case (Suc n) + then obtain k p where k: "k \ K" and p: "p \ UP.Span (poly_of_const ` K) (UP.exp_base X n)" + and q: "q = ((poly_of_const k) \\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> n)) \\<^bsub>K[X]\<^esub> p" + unfolding UP.exp_base_def using UP.line_extension_mem_iff by auto + have p_in_carrier: "p \ carrier (K[X])" and "length p \ n" + using Suc(1)[OF p] by simp+ + moreover from \k \ K\ have "poly_of_const k \ carrier (K[X])" + unfolding poly_of_const_def sym[OF univ_poly_carrier] polynomial_def by auto + ultimately have "q \ carrier (K[X])" + unfolding q using var_pow_closed[OF subring, of n] by algebra + + moreover have "poly_of_const k = \\<^bsub>K[X]\<^esub>" if "k = \" + unfolding poly_of_const_def that univ_poly_zero by simp + with \p \ carrier (K[X])\ have "q = p" if "k = \" + unfolding q using var_pow_closed[OF subring, of n] that by algebra + with \length p \ n\ have "length q \ Suc n" if "k = \" + using that by simp + + moreover have "poly_of_const k = [ k ]" if "k \ \" + unfolding poly_of_const_def using that by simp + hence monom: "monom k n = (poly_of_const k) \\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> n)" if "k \ \" + using that monom_eq_var_pow[OF subring] subfieldE(3)[OF assms] k by auto + with \p \ carrier (K[X])\ and \k \ K\ and \length p \ n\ + have "length q = Suc n" if "k \ \" + using that poly_add_length_eq[OF subring monom_is_polynomial[OF subring, of k n], of p] + unfolding univ_poly_carrier monom_def univ_poly_add sym[OF monom[OF that]] q by auto + ultimately show ?case + by (cases "k = \", auto) + qed + qed +qed + +lemma (in domain) var_pow_base_independent: + assumes "subfield K R" + shows "ring.independent (K[X]) (poly_of_const ` K) (ring.exp_base (K[X]) X n)" +proof - + note subring = subfieldE(1)[OF assms] + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subring] . + + show ?thesis + proof (induction n, simp add: UP.exp_base_def) + case (Suc n) + have "X [^]\<^bsub>K[X]\<^esub> n \ UP.Span (poly_of_const ` K) (ring.exp_base (K[X]) X n)" + unfolding sym[OF unitary_monom_eq_var_pow[OF subring]] monom_def + Span_var_pow_base[OF assms] by auto + moreover have "X [^]\<^bsub>K[X]\<^esub> n # UP.exp_base X n = UP.exp_base X (Suc n)" + unfolding UP.exp_base_def by simp + ultimately show ?case + using UP.li_Cons[OF var_pow_closed[OF subring, of n] _Suc] by simp + qed +qed + +lemma (in domain) bounded_degree_dimension: + assumes "subfield K R" + shows "ring.dimension (K[X]) n (poly_of_const ` K) { q \ carrier (K[X]). length q \ n }" +proof - + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subfieldE(1)[OF assms]] . + have "length (UP.exp_base X n) = n" + unfolding UP.exp_base_def by simp + thus ?thesis + using UP.dimension_independent[OF var_pow_base_independent[OF assms], of n] + unfolding Span_var_pow_base[OF assms] by simp +qed + +corollary (in domain) univ_poly_infinite_dimension: + assumes "subfield K R" shows "ring.infinite_dimension (K[X]) (poly_of_const ` K) (carrier (K[X]))" +proof (rule ccontr) + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subfieldE(1)[OF assms]] . + + assume "\ UP.infinite_dimension (poly_of_const ` K) (carrier (K[X]))" + then obtain n where n: "UP.dimension n (poly_of_const ` K) (carrier (K[X]))" + by blast + show False + using UP.independent_length_le_dimension[OF univ_poly_subfield_of_consts[OF assms] n + var_pow_base_independent[OF assms, of "Suc n"] + UP.exp_base_closed[OF var_closed(1)[OF subfieldE(1)[OF assms]]]] + unfolding UP.exp_base_def by simp +qed + +corollary (in domain) rupture_dimension: + assumes "subfield K R" and "p \ carrier (K[X])" and "degree p > 0" + shows "ring.dimension (Rupt K p) (degree p) ((rupture_surj K p) ` poly_of_const ` K) (carrier (Rupt K p))" +proof - + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] . + interpret Hom: ring_hom_ring "K[X]" "Rupt K p" "rupture_surj K p" + using rupture_surj_hom(2)[OF subfieldE(1)[OF assms(1)] assms(2)] . + + have not_nil: "p \ []" + using assms(3) by auto + + show ?thesis + using Hom.inj_hom_dimension[OF univ_poly_subfield_of_consts rupture_one_not_zero + rupture_surj_inj_on] bounded_degree_dimension assms + unfolding sym[OF rupture_carrier_as_pmod_image[OF assms(1-2)]] + pmod_image_characterization[OF assms(1-2) not_nil] + by simp +qed + +end \ No newline at end of file diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Polynomials.thy --- a/src/HOL/Algebra/Polynomials.thy Sat Apr 13 22:06:40 2019 +0200 +++ b/src/HOL/Algebra/Polynomials.thy Sun Apr 14 12:00:17 2019 +0100 @@ -57,9 +57,11 @@ then (lead_coeff p, degree p) # (dense_repr (tl p)) else (dense_repr (tl p)))" -fun (in ring) of_dense :: "('a \ nat) list \ 'a list" - where "of_dense dl = foldr (\(a, n) l. poly_add (monom a n) l) dl []" +fun (in ring) poly_of_dense :: "('a \ nat) list \ 'a list" + where "poly_of_dense dl = foldr (\(a, n) l. poly_add (monom a n) l) dl []" +definition (in ring) poly_of_const :: "'a \ 'a list" + where "poly_of_const = (\k. normalize [ k ])" subsection \Basic Properties\ @@ -324,15 +326,17 @@ qed qed +corollary normalize_trick: + shows "p = (replicate (length p - length (normalize p)) \) @ (normalize p)" + using normalize_def'(1)[of p] unfolding sym[OF normalize_def'(2)] . + lemma normalize_coeff: "coeff p = coeff (normalize p)" proof (induction p) case Nil thus ?case by simp next case (Cons a p) have "coeff (normalize p) (length p) = \" - using normalize_length_le[of p] coeff_degree[of "normalize p"] - by (metis One_nat_def coeff.simps(1) diff_less length_0_conv - less_imp_diff_less nat_neq_iff neq0_conv not_le zero_less_Suc) + using normalize_length_le[of p] coeff_degree[of "normalize p"] coeff_length by blast then show ?case using Cons by (cases "a = \") (auto) qed @@ -456,8 +460,7 @@ lemma poly_add_degree_eq: assumes "polynomial K p1" "polynomial K p2" and "degree p1 \ degree p2" shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)" - using poly_add_length_eq[of p1 p2] assms - by (metis (no_types, lifting) diff_le_mono max.absorb_iff1 max_def) + using poly_add_length_eq[OF assms(1-2)] assms(3) by simp end (* of fixed K context. *) (* ========================================================================== *) @@ -724,7 +727,7 @@ lemma monom_decomp: assumes "subring K R" "polynomial K p" - shows "p = of_dense (dense_repr p)" + shows "p = poly_of_dense (dense_repr p)" using assms(2) proof (induct "length p" arbitrary: p rule: less_induct) case less thus ?case @@ -739,12 +742,12 @@ also have " ... = poly_add (monom a (degree (a # l))) (normalize l)" using poly_add_normalize(2)[of "monom a (degree (a # l))", OF _ l(1)] a unfolding monom_def by force - also have " ... = poly_add (monom a (degree (a # l))) (of_dense (dense_repr (normalize l)))" + also have " ... = poly_add (monom a (degree (a # l))) (poly_of_dense (dense_repr (normalize l)))" using less(1)[OF _ normalize_gives_polynomial[OF l(2)]] normalize_length_le[of l] unfolding Cons by simp - also have " ... = of_dense ((a, degree (a # l)) # dense_repr (normalize l))" + also have " ... = poly_of_dense ((a, degree (a # l)) # dense_repr (normalize l))" by simp - also have " ... = of_dense (dense_repr (a # l))" + also have " ... = poly_of_dense (dense_repr (a # l))" using polynomial_dense_repr[OF less(2)] unfolding Cons by simp finally show ?thesis unfolding Cons by simp @@ -1383,6 +1386,11 @@ unfolding univ_poly_def by simp +(* NEW ========== *) +lemma univ_poly_zero_closed [intro]: "[] \ carrier (K[X]\<^bsub>R\<^esub>)" + unfolding sym[OF univ_poly_carrier] polynomial_def by simp + + context domain begin @@ -1575,8 +1583,7 @@ declare poly_add.simps[simp] lemma univ_poly_a_inv_def': - assumes "p \ carrier (K[X])" - shows "\\<^bsub>K[X]\<^esub> p = map (\a. \ a) p" + assumes "p \ carrier (K[X])" shows "\\<^bsub>K[X]\<^esub> p = map (\a. \ a) p" proof - have aux_lemma: "\p. p \ carrier (K[X]) \ p \\<^bsub>K[X]\<^esub> (map (\a. \ a) p) = []" @@ -1619,6 +1626,16 @@ using assms by simp qed +(* NEW ========== *) +corollary univ_poly_a_inv_length: + assumes "p \ carrier (K[X])" shows "length (\\<^bsub>K[X]\<^esub> p) = length p" + unfolding univ_poly_a_inv_def'[OF assms] by simp + +(* NEW ========== *) +corollary univ_poly_a_inv_degree: + assumes "p \ carrier (K[X])" shows "degree (\\<^bsub>K[X]\<^esub> p) = degree p" + using univ_poly_a_inv_length[OF assms] by simp + subsection \Long Division Theorem\ @@ -1712,7 +1729,8 @@ end (* of domain context. *) -lemma (in field) field_long_division_theorem: +(* PROOF ========== *) +lemma (in domain) field_long_division_theorem: assumes "subfield K R" "polynomial K p" and "polynomial K b" "b \ []" shows "\q r. polynomial K q \ polynomial K r \ p = (b \\<^bsub>K[X]\<^esub> q) \\<^bsub>K[X]\<^esub> r \ (r = [] \ degree r < degree b)" @@ -1720,8 +1738,9 @@ subfield.subfield_Units[OF assms(1)] lead_coeff_not_zero[of K "hd b" "tl b"] by simp +(* PROOF ========== *) text \The same theorem as above, but now, everything is in a shell. \ -lemma (in field) field_long_division_theorem_shell: +lemma (in domain) field_long_division_theorem_shell: assumes "subfield K R" "p \ carrier (K[X])" and "b \ carrier (K[X])" "b \ \\<^bsub>K[X]\<^esub>" shows "\q r. q \ carrier (K[X]) \ r \ carrier (K[X]) \ p = (b \\<^bsub>K[X]\<^esub> q) \\<^bsub>K[X]\<^esub> r \ (r = \\<^bsub>K[X]\<^esub> \ degree r < degree b)" @@ -1807,13 +1826,14 @@ subsubsection \Corollaries\ +(* PROOF ========== *) corollary (in ring) subfield_long_division_theorem_shell: assumes "subfield K R" "p \ carrier (K[X])" and "b \ carrier (K[X])" "b \ \\<^bsub>K[X]\<^esub>" shows "\q r. q \ carrier (K[X]) \ r \ carrier (K[X]) \ p = (b \\<^bsub>K[X]\<^esub> q) \\<^bsub>K[X]\<^esub> r \ (r = \\<^bsub>K[X]\<^esub> \ degree r < degree b)" - using field.field_long_division_theorem_shell[OF subfield_iff(2)[OF assms(1)] - field.carrier_is_subfield[OF subfield_iff(2)[OF assms(1)]]] - univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] assms(2-4) + using domain.field_long_division_theorem_shell[OF subdomain_is_domain[OF subfield.axioms(1)] + field.carrier_is_subfield[OF subfield_iff(2)[OF assms(1)]]] assms(1-4) + unfolding univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] by auto corollary (in domain) univ_poly_is_euclidean: @@ -2016,6 +2036,79 @@ unfolding ring_hom_cring_def ring_hom_cring_axioms_def cring_def by auto +subsection \Homomorphisms\ + +lemma (in ring_hom_ring) eval_hom': + assumes "a \ carrier R" and "set p \ carrier R" + shows "h (R.eval p a) = eval (map h p) (h a)" + using assms by (induct p, auto simp add: R.eval_in_carrier hom_nat_pow) + +lemma (in ring_hom_ring) eval_hom: + assumes "subring K R" and "a \ carrier R" and "p \ carrier (K[X])" + shows "h (R.eval p a) = eval (map h p) (h a)" +proof - + have "set p \ carrier R" + using subringE(1)[OF assms(1)] R.polynomial_incl assms(3) + unfolding sym[OF univ_poly_carrier[of R]] by auto + thus ?thesis + using eval_hom'[OF assms(2)] by simp +qed + +lemma (in ring_hom_ring) coeff_hom': + assumes "set p \ carrier R" shows "h (R.coeff p i) = coeff (map h p) i" + using assms by (induct p) (auto) + +lemma (in ring_hom_ring) poly_add_hom': + assumes "set p \ carrier R" and "set q \ carrier R" + shows "normalize (map h (R.poly_add p q)) = poly_add (map h p) (map h q)" +proof - + have set_map: "set (map h s) \ carrier S" if "set s \ carrier R" for s + using that by auto + have "coeff (normalize (map h (R.poly_add p q))) = coeff (map h (R.poly_add p q))" + using S.normalize_coeff by auto + also have " ... = (\i. h ((R.coeff p i) \ (R.coeff q i)))" + using coeff_hom'[OF R.poly_add_in_carrier[OF assms]] R.poly_add_coeff[OF assms] by simp + also have " ... = (\i. (coeff (map h p) i) \\<^bsub>S\<^esub> (coeff (map h q) i))" + using assms[THEN R.coeff_in_carrier] assms[THEN coeff_hom'] by simp + also have " ... = (\i. coeff (poly_add (map h p) (map h q)) i)" + using S.poly_add_coeff[OF assms[THEN set_map]] by simp + finally have "coeff (normalize (map h (R.poly_add p q))) = (\i. coeff (poly_add (map h p) (map h q)) i)" . + thus ?thesis + unfolding coeff_iff_polynomial_cond[OF + normalize_gives_polynomial[OF set_map[OF R.poly_add_in_carrier[OF assms]]] + poly_add_is_polynomial[OF carrier_is_subring assms[THEN set_map]]] . +qed + +lemma (in ring_hom_ring) poly_mult_hom': + assumes "set p \ carrier R" and "set q \ carrier R" + shows "normalize (map h (R.poly_mult p q)) = poly_mult (map h p) (map h q)" + using assms(1) +proof (induct p, simp) + case (Cons a p) + have set_map: "set (map h s) \ carrier S" if "set s \ carrier R" for s + using that by auto + + let ?q_a = "(map ((\) a) q) @ (replicate (length p) \)" + have set_q_a: "set ?q_a \ carrier R" + using assms(2) Cons(2) by (induct q) (auto) + have q_a_simp: "map h ?q_a = (map ((\\<^bsub>S\<^esub>) (h a)) (map h q)) @ (replicate (length (map h p)) \\<^bsub>S\<^esub>)" + using assms(2) Cons(2) by (induct q) (auto) + + have "S.normalize (map h (R.poly_mult (a # p) q)) = + S.normalize (map h (R.poly_add ?q_a (R.poly_mult p q)))" + by simp + also have " ... = S.poly_add (map h ?q_a) (map h (R.poly_mult p q))" + using poly_add_hom'[OF set_q_a R.poly_mult_in_carrier[OF _ assms(2)]] Cons by simp + also have " ... = S.poly_add (map h ?q_a) (S.normalize (map h (R.poly_mult p q)))" + using poly_add_normalize(2)[OF set_map[OF set_q_a] set_map[OF R.poly_mult_in_carrier[OF _ assms(2)]]] Cons by simp + also have " ... = S.poly_add (map h ?q_a) (S.poly_mult (map h p) (map h q))" + using Cons by simp + also have " ... = S.poly_mult (map h (a # p)) (map h q)" + unfolding q_a_simp by simp + finally show ?case . +qed + + subsection \The X Variable\ definition var :: "_ \ 'a list" ("X\") @@ -2080,6 +2173,73 @@ finally show ?thesis . qed +lemma (in domain) eval_rewrite: + assumes "subring K R" and "p \ carrier (K[X])" + shows "p = (ring.eval (K[X])) (map poly_of_const p) X" +proof - + let ?map_norm = "\p. map poly_of_const p" + + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF assms(1)] . + + { fix l assume "set l \ K" + hence "poly_of_const a \ carrier (K[X])" if "a \ set l" for a + using that normalize_gives_polynomial[of "[ a ]" K] + unfolding univ_poly_carrier poly_of_const_def by auto + hence "set (?map_norm l) \ carrier (K[X])" + by auto } + note aux_lemma1 = this + + { fix q l assume set_l: "set l \ K" and q: "q \ carrier (K[X])" + from set_l have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \) @ l)) q" for n + proof (induct n, simp) + case (Suc n) + from \set l \ K\ have set_replicate: "set ((replicate n \) @ l) \ K" + using subringE(2)[OF assms(1)] by (induct n) (auto) + have step: "UP.eval (?map_norm l') q = UP.eval (?map_norm (\ # l')) q" if "set l' \ K" for l' + using UP.eval_in_carrier[OF aux_lemma1[OF that]] q unfolding poly_of_const_def + by (simp, simp add: sym[OF univ_poly_zero[of R K]]) + have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \) @ l)) q" + using Suc by simp + also have " ... = UP.eval (map poly_of_const ((replicate (Suc n) \) @ l)) q" + using step[OF set_replicate] by simp + finally show ?case . + qed } + note aux_lemma2 = this + + { fix q l assume "set l \ K" and q: "q \ carrier (K[X])" + from \set l \ K\ have set_norm: "set (normalize l) \ K" + by (induct l) (auto) + have "UP.eval (?map_norm l) q = UP.eval (?map_norm (normalize l)) q" + using aux_lemma2[OF set_norm q, of "length l - length (local.normalize l)"] + unfolding sym[OF normalize_trick[of l]] .. } + note aux_lemma3 = this + + from \p \ carrier (K[X])\ show ?thesis + proof (induct "length p" arbitrary: p rule: less_induct) + case less thus ?case + proof (cases p, simp add: univ_poly_zero) + case (Cons a l) + hence a: "a \ carrier R - { \ }" and set_l: "set l \ carrier R" "set l \ K" + using less(2) subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto + + have "a # l = poly_add (monom a (length l)) l" + using poly_add_monom[OF set_l(1) a] .. + also have " ... = poly_add (monom a (length l)) (normalize l)" + using poly_add_normalize(2)[OF monom_in_carrier[of a] set_l(1)] a by simp + also have " ... = poly_add (monom a (length l)) (UP.eval (?map_norm (normalize l)) X)" + using less(1)[of "normalize l"] normalize_gives_polynomial[OF set_l(2)] normalize_length_le[of l] + by (auto simp add: univ_poly_carrier Cons(1)) + also have " ... = poly_add ([ a ] \\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> (length l))) (UP.eval (?map_norm l) X)" + unfolding monom_eq_var_pow[OF assms(1) a] aux_lemma3[OF set_l(2) var_closed(1)[OF assms(1)]] .. + also have " ... = UP.eval (?map_norm (a # l)) X" + using a unfolding sym[OF univ_poly_add[of R K]] unfolding poly_of_const_def by auto + finally show ?thesis + unfolding Cons(1) . + qed + qed +qed + lemma (in ring) dense_repr_set_fst: assumes "set p \ K" shows "fst ` (set (dense_repr p)) \ K - { \ }" using assms by (induct p) (auto) @@ -2118,7 +2278,7 @@ have a: "a \ K - { \ }" using less(2) subringE(1)[OF assms(1)] unfolding Cons univ_poly_def polynomial_def by auto - hence "p = (monom a (length l)) \\<^bsub>K[X]\<^esub> (of_dense (dense_repr (normalize l)))" + hence "p = (monom a (length l)) \\<^bsub>K[X]\<^esub> (poly_of_dense (dense_repr (normalize l)))" using monom_decomp[OF assms(1), of p] less(2) dense_repr_normalize unfolding univ_poly_add univ_poly_carrier Cons by (auto simp del: poly_add.simps) also have " ... = (monom a (length l)) \\<^bsub>K[X]\<^esub> (normalize l)" @@ -2307,29 +2467,52 @@ subsection \The Canonical Embedding of K in K[X]\ -lemma (in field) univ_poly_carrier_subfield_of_consts: - "subfield { p \ carrier ((carrier R)[X]). degree p = 0 } ((carrier R)[X])" +lemma (in ring) poly_of_const_consistent: + assumes "subring K R" shows "ring.poly_of_const (R \ carrier := K \) = poly_of_const" + unfolding ring.poly_of_const_def[OF subring_is_ring[OF assms]] + normalize_consistent[OF assms] poly_of_const_def .. + +lemma (in domain) canonical_embedding_is_hom: + assumes "subring K R" shows "poly_of_const \ ring_hom (R \ carrier := K \) (K[X])" + using subringE(1)[OF assms] unfolding subset_iff poly_of_const_def + by (auto intro!: ring_hom_memI simp add: univ_poly_def) + +lemma (in domain) canonical_embedding_ring_hom: + assumes "subring K R" shows "ring_hom_ring (R \ carrier := K \) (K[X]) poly_of_const" + using canonical_embedding_is_hom[OF assms] unfolding symmetric[OF ring_hom_ring_axioms_def] + by (rule ring_hom_ring.intro[OF subring_is_ring[OF assms] univ_poly_is_ring[OF assms]]) + +lemma (in field) poly_of_const_over_carrier: + shows "poly_of_const ` (carrier R) = { p \ carrier ((carrier R)[X]). degree p = 0 }" proof - - have ring_hom: "ring_hom_ring R ((carrier R)[X]) (\k. normalize [ k ])" - by (rule ring_hom_ringI[OF ring_axioms univ_poly_is_ring[OF carrier_is_subring]]) - (auto simp add: univ_poly_def) - have subfield: "subfield ((\k. normalize [ k ]) ` (carrier R)) ((carrier R)[X])" - using ring_hom_ring.img_is_subfield(2)[OF ring_hom carrier_is_subfield] - unfolding univ_poly_def by auto - - have "(\k. normalize [ k ]) ` (carrier R) = insert [] { [ k ] | k. k \ carrier R - { \ } }" - by auto + have "poly_of_const ` (carrier R) = insert [] { [ k ] | k. k \ carrier R - { \ } }" + unfolding poly_of_const_def by auto also have " ... = { p \ carrier ((carrier R)[X]). degree p = 0 }" unfolding univ_poly_def polynomial_def by (auto, metis le_Suc_eq le_zero_eq length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subsetCE) - finally have "(\k. normalize [ k ]) ` (carrier R) = { p \ carrier ((carrier R)[X]). degree p = 0 }" . + finally show ?thesis . +qed + +lemma (in ring) poly_of_const_over_subfield: + assumes "subfield K R" shows "poly_of_const ` K = { p \ carrier (K[X]). degree p = 0 }" + using field.poly_of_const_over_carrier[OF subfield_iff(2)[OF assms]] + poly_of_const_consistent[OF subfieldE(1)[OF assms]] + univ_poly_consistent[OF subfieldE(1)[OF assms]] by simp + +lemma (in field) univ_poly_carrier_subfield_of_consts: + "subfield (poly_of_const ` (carrier R)) ((carrier R)[X])" +proof - + have ring_hom: "ring_hom_ring R ((carrier R)[X]) poly_of_const" + using canonical_embedding_ring_hom[OF carrier_is_subring] by simp thus ?thesis - using subfield by auto + using ring_hom_ring.img_is_subfield(2)[OF ring_hom carrier_is_subfield] + unfolding univ_poly_def by auto qed proposition (in ring) univ_poly_subfield_of_consts: - assumes "subfield K R" shows "subfield { p \ carrier (K[X]). degree p = 0 } (K[X])" + assumes "subfield K R" shows "subfield (poly_of_const ` K) (K[X])" using field.univ_poly_carrier_subfield_of_consts[OF subfield_iff(2)[OF assms]] - univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto + unfolding poly_of_const_consistent[OF subfieldE(1)[OF assms]] + univ_poly_consistent[OF subfieldE(1)[OF assms]] by simp end diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Pred_Zorn.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Pred_Zorn.thy Sun Apr 14 12:00:17 2019 +0100 @@ -0,0 +1,57 @@ +theory Pred_Zorn + imports HOL.Zorn + +begin + +(* ========== *) +lemma partial_order_onE: + assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r" + using assms unfolding partial_order_on_def preorder_on_def by auto +(* ========== *) + +abbreviation rel_of :: "('a \ 'a \ bool) \ 'a set \ ('a \ 'a) set" + where "rel_of P A \ { (a, b) \ A \ A. P a b }" + +lemma Field_rel_of: + assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A" + using assms unfolding refl_on_def Field_def by auto + +(* ========== *) +lemma Chains_rel_of: + assumes "C \ Chains (rel_of P A)" shows "C \ A" + using assms unfolding Chains_def by auto +(* ========== *) + +lemma partial_order_on_rel_ofI: + assumes refl: "\a. a \ A \ P a a" + and trans: "\a b c. \ a \ A; b \ A; c \ A \ \ P a b \ P b c \ P a c" + and antisym: "\a b. \ a \ A; b \ A \ \ P a b \ P b a \ a = b" + shows "partial_order_on A (rel_of P A)" +proof - + from refl have "refl_on A (rel_of P A)" + unfolding refl_on_def by auto + moreover have "trans (rel_of P A)" and "antisym (rel_of P A)" + by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym) + ultimately show ?thesis + unfolding partial_order_on_def preorder_on_def by simp +qed + +lemma Partial_order_rel_ofI: + assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)" + using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] . + +lemma predicate_Zorn: + assumes "partial_order_on A (rel_of P A)" + and "\C \ Chains (rel_of P A). \u \ A. \a \ C. P a u" + shows "\m \ A. \a \ A. P m a \ a = m" +proof - + have "a \ A" if "a \ C" and "C \ Chains (rel_of P A)" for C a + using that Chains_rel_of by auto + moreover have "(a, u) \ rel_of P A" if "a \ A" and "u \ A" and "P a u" for a u + using that by auto + ultimately show ?thesis + using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2) + unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto +qed + +end \ No newline at end of file diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Ring_Divisibility.thy --- a/src/HOL/Algebra/Ring_Divisibility.thy Sat Apr 13 22:06:40 2019 +0200 +++ b/src/HOL/Algebra/Ring_Divisibility.thy Sun Apr 14 12:00:17 2019 +0100 @@ -7,6 +7,23 @@ begin +(* TEMPORARY ====================================================================== *) +definition mult_of :: "('a, 'b) ring_scheme \ 'a monoid" where + "mult_of R \ \ carrier = carrier R - {\\<^bsub>R\<^esub>}, mult = mult R, one = \\<^bsub>R\<^esub>\" + +lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\\<^bsub>R\<^esub>}" + by (simp add: mult_of_def) + +lemma mult_mult_of [simp]: "mult (mult_of R) = mult R" + by (simp add: mult_of_def) + +lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \ nat \ _)" + by (simp add: mult_of_def fun_eq_iff nat_pow_def) + +lemma one_mult_of [simp]: "\\<^bsub>mult_of R\<^esub> = \\<^bsub>R\<^esub>" + by (simp add: mult_of_def) +(* ================================================================================ *) + section \The Arithmetic of Rings\ text \In this section we study the links between the divisibility theory and that of rings\ @@ -51,6 +68,11 @@ and "one (mult_of R) = one R" using factorial_monoid_axioms by auto +lemma (in ring) noetherian_ringI: + assumes "\I. ideal I R \ \A \ carrier R. finite A \ I = Idl A" + shows "noetherian_ring R" + using assms by unfold_locales auto + lemma (in domain) euclidean_domainI: assumes "\a b. \ a \ carrier R - { \ }; b \ carrier R - { \ } \ \ \q r. q \ carrier R \ r \ carrier R \ a = (b \ q) \ r \ ((r = \) \ (\ r < \ b))" @@ -529,7 +551,7 @@ lemma (in ring) trivial_ideal_chain_imp_noetherian: assumes "\C. \ C \ {}; subset.chain { I. ideal I R } C \ \ \C \ C" shows "noetherian_ring R" -proof (auto simp add: noetherian_ring_def noetherian_ring_axioms_def ring_axioms) +proof (rule noetherian_ringI) fix I assume I: "ideal I R" have in_carrier: "I \ carrier R" and add_subgroup: "additive_subgroup I R" using ideal.axioms(1)[OF I] additive_subgroup.a_subset by auto @@ -662,6 +684,26 @@ using C unfolding pred_on.maxchain_def by blast qed +lemma (in noetherian_domain) exists_irreducible_divisor: + assumes "a \ carrier R - { \ }" and "a \ Units R" + obtains b where "b \ carrier R" and "ring_irreducible b" and "b divides a" +proof - + obtain fs where set_fs: "set fs \ carrier (mult_of R)" and "wfactors (mult_of R) fs a" + using factorization_property[OF assms] by blast + hence "a \ Units R" if "fs = []" + using that assms(1) Units_cong assoc_iff_assoc_mult unfolding wfactors_def by (simp, blast) + hence "fs \ []" + using assms(2) by auto + then obtain f' fs' where fs: "fs = f' # fs'" + using list.exhaust by blast + from \wfactors (mult_of R) fs a\ have "f' divides a" + using mult_of.wfactors_dividesI[OF _ set_fs] assms(1) unfolding fs by auto + moreover from \wfactors (mult_of R) fs a\ have "ring_irreducible f'" and "f' \ carrier R" + using set_fs ring_irreducibleI'[of f'] unfolding wfactors_def fs by auto + ultimately show thesis + using that by blast +qed + subsection \Principal Domains\ diff -r 57503fe1b0ff -r 615233977155 src/HOL/Algebra/Subrings.thy --- a/src/HOL/Algebra/Subrings.thy Sat Apr 13 22:06:40 2019 +0200 +++ b/src/HOL/Algebra/Subrings.thy Sun Apr 14 12:00:17 2019 +0100 @@ -225,6 +225,11 @@ assumes "subring H R" shows "domain (R \ carrier := H \)" using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] . +(* NEW ====================== *) +lemma (in ring) subdomain_is_domain: + assumes "subdomain H R" shows "domain (R \ carrier := H \)" + using assms unfolding subdomain_iff[OF subdomainE(1)[OF assms]] . + subsubsection \Subfields\ @@ -338,6 +343,23 @@ using monoid.m_inv_monoid_consistent[OF monoid_axioms k K(2)] by auto qed +lemma (in ring) subfield_m_inv_simprule: + assumes "subfield K R" + shows "\ k \ K - { \ }; a \ carrier R \ \ k \ a \ K \ a \ K" +proof - + note subring_props = subringE[OF subfieldE(1)[OF assms]] + + assume A: "k \ K - { \ }" "a \ carrier R" "k \ a \ K" + then obtain k' where k': "k' \ K" "k \ a = k'" by blast + have inv_k: "inv k \ K" "inv k \ k = \" + using subfield_m_inv[OF assms A(1)] by auto + hence "inv k \ (k \ a) \ K" + using k' A(3) subring_props(6) by auto + thus "a \ K" + using m_assoc[of "inv k" k a] A(2) inv_k subring_props(1) + by (metis (no_types, hide_lams) A(1) Diff_iff l_one subsetCE) +qed + lemma (in ring) subfield_iff: shows "\ field (R \ carrier := K \); K \ carrier R \ \ subfield K R" and "subfield K R \ field (R \ carrier := K \)" @@ -433,4 +455,46 @@ using S.subfield_iff[of "h ` K"] K(1) ring_hom_memE(1)[OF homh] by blast qed +(* NEW ========================================================================== *) +lemma (in ring_hom_ring) induced_ring_hom: + assumes "subring K R" shows "ring_hom_ring (R \ carrier := K \) S h" +proof - + have "h \ ring_hom (R \ carrier := K \) S" + using homh subringE(1)[OF assms] unfolding ring_hom_def + by (auto, meson hom_mult hom_add subsetCE)+ + thus ?thesis + using R.subring_is_ring[OF assms] ring_axioms + unfolding ring_hom_ring_def ring_hom_ring_axioms_def by auto +qed + +(* NEW ========================================================================== *) +lemma (in ring_hom_ring) inj_on_subgroup_iff_trivial_ker: + assumes "subring K R" + shows "inj_on h K \ a_kernel (R \ carrier := K \) S h = { \ }" + using ring_hom_ring.inj_iff_trivial_ker[OF induced_ring_hom[OF assms]] by simp + +lemma (in ring_hom_ring) inv_ring_hom: + assumes "inj_on h K" and "subring K R" + shows "ring_hom_ring (S \ carrier := h ` K \) R (inv_into K h)" +proof (intro ring_hom_ringI[OF _ R.ring_axioms], auto) + show "ring (S \ carrier := h ` K \)" + using subring_is_ring[OF img_is_subring[OF assms(2)]] . +next + show "inv_into K h \\<^bsub>S\<^esub> = \\<^bsub>R\<^esub>" + using assms(1) subringE(3)[OF assms(2)] hom_one by (simp add: inv_into_f_eq) +next + fix k1 k2 + assume k1: "k1 \ K" and k2: "k2 \ K" + with \k1 \ K\ show "inv_into K h (h k1) \ carrier R" + using assms(1) subringE(1)[OF assms(2)] by (simp add: subset_iff) + + from \k1 \ K\ and \k2 \ K\ + have "h k1 \\<^bsub>S\<^esub> h k2 = h (k1 \\<^bsub>R\<^esub> k2)" and "k1 \\<^bsub>R\<^esub> k2 \ K" + and "h k1 \\<^bsub>S\<^esub> h k2 = h (k1 \\<^bsub>R\<^esub> k2)" and "k1 \\<^bsub>R\<^esub> k2 \ K" + using subringE(1,6,7)[OF assms(2)] by (simp add: subset_iff)+ + thus "inv_into K h (h k1 \\<^bsub>S\<^esub> h k2) = inv_into K h (h k1) \\<^bsub>R\<^esub> inv_into K h (h k2)" + and "inv_into K h (h k1 \\<^bsub>S\<^esub> h k2) = inv_into K h (h k1) \\<^bsub>R\<^esub> inv_into K h (h k2)" + using assms(1) k1 k2 by simp+ +qed + end