| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Algebra/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 55 kB |
|
Quelle Algebraic_Closure.thy Sprache: Isabelle |
|||||||||
|
(* 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 Finite_Extensions begin section \<open>Algebraic Closure\<close> subsection \<open>Definitions\<close> inductive iso_incl :: "'a ring \ where iso_inclI [intro]: "id \ definition law_restrict :: "('a, 'b) ring_scheme \ where "law_restrict R \ \<lparr> mult := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b), add := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<oplus>\<^bsub>R\<^esub> b) \<rparr>" definition (in ring) \<sigma> :: "'a list \<Rightarrow> ((('a list \<times> nat) multiset) \<Rightar where "\ definition (in ring) extensions :: "((('a list \ where "extensions \ \<comment> \<open>i\<close> (field L) \<and> \<comment> \<open>ii\<close> (indexed_const \<in> ring_hom R L) \<and> \<comment> \<open>iii\<close> (\<forall>\<P> \<in> carrier L. carrier_coeff \<P>) \<and> \<comment> \<open>iv\<close> (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R). \<foral \<not> index_free \<P> (P, i) \<longrightarrow> \<X>\<^bsub>(P, i)\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero> abbreviation (in ring) restrict_extensions :: "((('a list \ where "\ subsection \<open>Basic Properties\<close> 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) = (\ by (simp add: law_restrict_def ring.defs) lemma law_restrict_add: "add (law_restrict R) = (\ 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 b 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 si qed lemma law_restrict_iso_imp_eq: assumes "id \ 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 hence mult: "a \ and add: "a \ using ring_iso_memE(2-3)[OF assms(1)] unfolding law_restrict_def by (auto simp add: ring. 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 \<open>carrier A = carrier B\<close> have "carrier (law_restrict A) = carrier (law_ unfolding law_restrict_def by (simp add: ring.defs) moreover have "\ using ring_hom_zero[OF _ assms(2-3)[THEN ring.law_restrict_is_ring]] assms(1) unfolding ring_iso_def by auto moreover have "\ using ring_iso_memE(4)[OF assms(1)] by simp ultimately show ?thesis by simp qed lemma law_restrict_hom: "h \ proof assume "h \ by (auto intro!: ring_hom_memI dest: ring_hom_memE simp: law_restrict_def ring.defs) next assume h: "h \ using ring_hom_memE[OF h] by (auto intro!: ring_hom_memI simp: law_restrict_def ring.defs qed lemma iso_incl_hom: "A \ using law_restrict_hom iso_incl.simps by blast subsection \<open>Partial Order\<close> lemma iso_incl_backwards: assumes "A \ using assms by cases lemma iso_incl_antisym_aux: assumes "A \ proof - have hom: "id \ 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 \ by (rule iso_inclI[OF ring_hom_memI], auto) lemma iso_incl_trans: assumes "A \ using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto lemma (in ring) iso_incl_antisym: assumes "A \ proof - obtain A' B' :: "(('a list \ 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 \ using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_relation lemma iso_inclE: assumes "ring A" and "ring B" and "A \ 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 \ 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 \<open>Extensions Non Empty\<close> 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 \ 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 \ using inj_imp_image_ring_iso[OF indexed_const_inj_on] unfolding ring_iso_def by auto next fix \<P> :: "(('a list \<times> nat) multiset) \<Rightarrow> 'a" and P and i assume "\ \ then obtain k where "k \ = indexed_const k" unfolding image_ring_carrier by blast hence "index_free \ (P, i)" for P i unfolding index_free_def indexed_const_def by auto thus "\ (P, i) \ and "\ (P, i) \ by auto from \<open>k \<in> carrier R\<close> and \<open>\<P> = indexed_const k\<close> show "carrier_coeff \<P>" unfolding indexed_const_def carrier_coeff_def by auto qed thus ?thesis by blast qed subsection \<open>Chains\<close> definition union_ring :: "(('a, 'c) ring_scheme) set \ where "union_ring C = \<lparr> carrier = (\<Union>(carrier ` C)), monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) one = one (SOME R. R \<in> C), zero = zero (SOME R. R \<in> C), add = (\<lambda>a b. (add (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)) \<rparr>" lemma union_ring_carrier: "carrier (union_ring C) = (\ unfolding union_ring_def by simp context fixes C :: "'a ring set" assumes field_chain: "\ begin lemma ring_chain: "R \ using field.is_ring[OF field_chain] by blast lemma same_one_same_zero: assumes "R \ proof - have "\ using ring_hom_one[of id] chain[OF that] unfolding iso_incl.simps by auto moreover have "\ using chain[OF that] ring_hom_zero[OF _ ring_chain ring_chain] that unfolding iso_incl.si ultimately have "one (SOME R. R \ using assms by (metis (mono_tags) someI)+ thus "\ unfolding union_ring_def by auto qed lemma same_laws: assumes "R \ shows "a \ proof - have "a \ if "R \ 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 \ if "R \ 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 \ and "add (SOME R. R \ using assms by (metis (mono_tags, lifting) someI)+ thus "a \ unfolding union_ring_def by auto qed lemma exists_superset_carrier: assumes "finite S" and "S \ shows "\ using assms proof (induction, simp) case (insert s S) obtain R where R: "s \ 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 \ using insert(3,5) by blast have "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 \ proof fix a b c assume "a \ then obtain R where R: "R \ using exists_superset_carrier[of "{ a, b, c }"] by auto then interpret field R using field_chain by simp show "a \ using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto show "(a \ and "a \ and "\ and "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 "\ 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 \ proof (rule cringI[OF abelian_groupI union_ring_is_monoid[OF assms]]) fix a b c assume "a \ then obtain R where R: "R \ using exists_superset_carrier[of "{ a, b, c }"] by auto then interpret field R using field_chain by simp show "a \ using R(1-3) unfolding same_laws(2)[OF R(1-3)] unfolding union_ring_def by auto show "(a \ and "(a \ and "a \ and "\ 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 "\ using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp with \<open>R \<in> C\<close> show "\<exists>y \<in> carrier (union_ring C). y \<oplus>\<^bsub>union_ring unfolding union_ring_carrier by auto next show "\ 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 \ proof (rule cring.cring_fieldI[OF union_ring_is_abelian_group[OF assms]]) have "carrier (union_ring C) - { \ proof fix a assume "a \ hence "a \ by auto then obtain R where R: "R \ using exists_superset_carrier[of "{ a }"] by auto then interpret field R using field_chain by simp from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have unfolding same_one_same_zero[OF R(1)] field_Units by auto hence "\ using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_r unfolding Units_def union_ring_carrier by auto qed moreover have "\ proof (rule ccontr) assume "\ then obtain a where a: "a \ unfolding Units_def by auto then obtain R where R: "R \ using exists_superset_carrier[of "{ a }"] by auto then interpret field R using field_chain by simp have "\ 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) \ unfolding Units_def by auto ultimately show "Units (union_ring C) = carrier (union_ring C) - { \ by simp qed lemma union_ring_is_upper_bound: assumes "R \ using ring_hom_memI[of R id "union_ring C"] same_laws[of R] same_one_same_zero[of R] assm unfolding union_ring_carrier by auto end subsection \<open>Zorn\<close> lemma (in ring) exists_core_chain: assumes "C \ using Chains_relation_of[OF assms] by (meson subset_image_iff) lemma (in ring) core_chain_is_chain: assumes "law_restrict ` C \ proof - fix R S assume "R \ using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def relation_of_de by auto qed lemma (in field) exists_maximal_extension: shows "\ proof (rule predicate_Zorn[OF iso_incl_partial_order]) fix C assume C: "C \ show "\ proof (cases) assume "C = {}" thus ?thesis using extensions_non_empty by auto next assume "C \ from \<open>C \<in> Chains (relation_of (\<lesssim>) \<S>)\<close> obtain C' where C': "C' \ using exists_core_chain by auto with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}" by auto have core_chain: "\ using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'" using union_ring_is_field[OF core_chain] C'(1) by blast have "union_ring C' \ proof (auto simp add: extensions_def) show "field (union_ring C')" using Union.field_axioms . next from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S" using C'(1) unfolding extensions_def by auto thus "indexed_const \ 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 \ using C'(1) unfolding union_ring_carrier extensions_def by auto next fix \<P> P i assume "\ \ and P: "P \ and not_index_free: "\ (P, i)" from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T" using exists_superset_carrier[of C' "{ \ }"] core_chain by auto hence "\ and field: "field T" and hom: "indexed_const \ using P not_index_free C'(1) unfolding extensions_def by auto with \<open>T \<in> C'\<close> show "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier (union_ring C')" unfolding union_ring_carrier by auto have "set P \ using P unfolding sym[OF univ_poly_carrier] polynomial_def by auto hence "set (\ using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto) with \<open>\<X>\<^bsub>(P, i)\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bs show "(ring.eval (union_ring C')) (\ 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( by auto qed moreover have "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 subsection \<open>Existence of roots\<close> lemma polynomial_hom: assumes "h \ shows "p \ proof - assume "p \ interpret ring_hom_ring R S h using ring_hom_ringI2[OF assms(2-3)[THEN field.is_ring] assms(1)] . from \<open>p \<in> carrier (poly_ring R)\<close> have "set p \<subseteq> carrier R" and lc: "p \<noteq> [ unfolding sym[OF univ_poly_carrier] polynomial_def by auto hence "set (map h p) \ by (induct p) (auto) moreover have "h a = \ using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^es 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 "\ shows "p \ proof - assume "p \ hence "p \ using R.univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] by simp moreover have "h \ using hom_mult subfieldE(3)[OF assms(1)] unfolding ring_hom_def subset_iff by auto moreover have "field (R \ using R.subfield_iff(2)[OF assms(1)] S.subfield_iff(2)[OF img_is_subfield(2)[OF assms ultimately have "(map h p) \ using polynomial_hom[of h "R \ 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 \ and "P \ shows "(ring.splitted M) (\ proof (rule ccontr) from \<open>M \<in> extensions\<close> 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 not_splitted: "\ have "(\ using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \<sigma> then obtain Q where Q: "Q \ and degree_gt: "degree Q > 1" using M.trivial_factors_imp_splitted[of "\ from \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> have "(\<sigma> P) \<noteq> []" using M.degree_zero_imp_splitted[of "\ have "\ \ (P, i)" proof (rule ccontr) assume "\ \ (P, i)" then have "\ using assms(1,3) unfolding extensions_def by blast+ with \<open>(\<sigma> P) \<noteq> []\<close> have "((\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>) ` UNIV) \< unfolding M.is_root_def by auto moreover have "inj (\ unfolding indexed_var_def indexed_const_def indexed_pmult_def inj_def by (metis (no_types, lifting) add_mset_eq_singleton_iff diff_single_eq_union multi_member_last prod.inject zero_not_one) hence "infinite ((\ unfolding infinite_iff_countable_subset by auto ultimately have "infinite { a. (ring.is_root M) (\ using finite_subset by auto with \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> show False using M.finite_number_of_roots by simp qed then obtain i :: nat where "\ \ (P, i)" by blast then have hyps: \<comment> \<open>i\<close> "field M" \<comment> \<open>ii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>" \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> (P, i)" \<comment> \<open>iv\<close> "\<zero>\<^bsub>M\<^esub> = indexed_const \<zero>" using assms(1,3) unfolding extensions_def by auto define image_poly where "image_poly = image_ring (eval_pmod M (P, i) Q) (poly_ring with \<open>degree Q > 1\<close> have "M \<lesssim> 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 \ proof (auto simp add: extensions_def is_field) fix \<P> assume "\<P> \<in> carrier image_poly" then obtain R where \<P>: "\<P> = eval_pmod M (P, i) Q R" and "R \<in> carrier (poly_ring M)" unfolding image_poly_def image_ring_carrier by auto hence "M.pmod R Q \ 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 \<P> by simp next from \<open>M \<lesssim> image_poly\<close> show "indexed_const \<in> ring_hom R image_poly" using ring_hom_trans[OF Hom.homh, of id] unfolding iso_incl.simps by simp next from \<open>M \<lesssim> image_poly\<close> 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 \<P> S j assume A: "\ \ (S, j)" "S \ have "\ proof (cases) assume "(P, i) \ then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' (S, j)" using A(1) image_poly_index_free[OF hyps Q(1) _ A(2)] unfolding image_poly_def by auto hence "\ using assms(1) A(3) unfolding extensions_def by auto moreover have "\ using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def ultimately show ?thesis using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto next assume "\ by simp have poly_hom: "R \ using polynomial_hom[OF Id.homh M.field_axioms is_field that] by simp have "\ 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 \ using image_poly_eval_indexed_var[OF hyps Hom.homh Q(1) degree_gt Q(2)] unfolding image_ moreover have "Q pdivides\<^bsub>image_poly\<^esub> (\ proof - obtain R where R: "R \ using Q(3) S unfolding pdivides_def by auto moreover have "set Q \ using Q(1) R(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto ultimately have "Id.normalize (\ using Id.poly_mult_hom'[of Q R] unfolding univ_poly_mult by simp moreover have "\ using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def hence "\ using polynomial_hom[OF Id.homh M.field_axioms is_field] by simp hence "Id.normalize (\ 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 \ 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 "\ 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 "\ using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp moreover have "\ using indexed_var_not_index_free[of "(P, i)"] hyps(3) by blast ultimately show False by simp qed lemma (in field) exists_extension_with_roots: shows "\ proof - obtain M where "M \ using exists_maximal_extension iso_incl_hom by blast thus ?thesis using exists_root[of M] by auto qed subsection \<open>Existence of Algebraic Closure\<close> locale algebraic_closure = field L + subfield K L for L (structure) and K + assumes algebraic_extension: "x \ and roots_over_subfield: "P \ locale algebraically_closed = field L for L (structure) + assumes roots_over_carrier: "P \ definition (in field) alg_closure :: "(('a list \ where "alg_closure = (SOME L \ \<comment> \<open>i\<close> algebraic_closure L (indexed_const ` (carrier R)) \<and> \<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)" lemma algebraic_hom: assumes "h \ shows "((ring.algebraic R) over K) 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 \ using domain.algebraicE[OF field.axioms(1) subfieldE(1), of R K x] assms(2,4-5) by auto hence "(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) = \ 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' b qed lemma (in field) exists_closure: obtains L :: "((('a list \ where "algebraic_closure L (indexed_const ` (carrier R))" and "indexed_const \ proof - obtain L where "L \ and roots: "\ using exists_extension_with_roots by auto let ?K = "indexed_const ` (carrier R)" let ?set_of_algs = "{ x \ let ?M = "L \ from \<open>L \<in> extensions\<close> 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 \ by simp moreover from \<open>subfield ?K L\<close> have "field (L \<lparr> carrier := ?K \<rparr>)" using ring.subfield_iff(2)[OF field.is_ring[OF L]] by simp ultimately show "field (?M \ by simp next show "?K \ proof fix x :: "(('a list \ assume "x \ hence "x \ using ring_hom_memE(1)[OF ring_hom_ring.homh[OF hom]] by auto moreover from \<open>subfield ?K L\<close> and \<open>x \<in> ?K\<close> have "(Id.S.algebraic over ?K using domain.algebraic_self[OF field.axioms(1)[OF L] subfieldE(1)] by auto ultimately show "x \ 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 \ using that Id.S.algebraic_consistent[OF subfieldE(1)[OF set_of_algs]] by simp moreover have "Id.R.splitted P" if "P \ proof - from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (poly_ring ?M)" using Id.R.carrier_polynomial_shell[OF subfieldE(1)[OF is_subfield]] by simp show ?thesis proof (cases "degree P = 0") case True with \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis using domain.degree_zero_imp_splitted[OF field.axioms(1)[OF M]] by fastforce next case False then have "degree P > 0" by simp from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^es unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] . hence "set P \ unfolding sym[OF univ_poly_carrier] polynomial_def by auto hence "\ proof (induct P, simp add: \<sigma>_def) case (Cons p P) then obtain q Q where "q \ and "\ unfolding \<sigma>_def by auto hence "set (q # Q) \ unfolding \<sigma>_def by auto thus ?case by metis qed then obtain Q where "set Q \ by auto moreover have "lead_coeff Q \ proof (rule ccontr) assume "\ by simp with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zer unfolding \<sigma>_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) li hence "lead_coeff P = \ using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" unfolding sym[OF univ_poly_carrier] polynomial_def by auto with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False by simp qed ultimately have "Q \ unfolding sym[OF univ_poly_carrier] polynomial_def by auto with \<open>\<sigma> Q = P\<close> have "Id.S.splitted P" using roots[of Q] by simp from \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis proof (rule field.trivial_factors_imp_splitted[OF M]) fix R assume R: "R \ from \<open>P \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close> have "P \ unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by auto hence in_carrier: "P \ using Id.S.carrier_polynomial_shell[OF subfieldE(1)[OF set_of_algs]] by auto from \<open>R pdivides\<^bsub>?M\<^esub> P\<close> have "R divides\<^bsub>((?set_of_algs)[X]\<^bs unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp with \<open>P \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close> and \<open>R \<in> carrier ((? have "R pdivides\<^bsub>L\<^esub> P" using domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs, of R P] by simp with \<open>Id.S.splitted P\<close> and \<open>degree P \<noteq> 0\<close> have "Id.S.splitted R" using field.pdivides_imp_splitted[OF L in_carrier(2,1)] by fastforce show "degree R \ proof (cases "Id.S.roots R = {#}") case True with \<open>Id.S.splitted R\<close> show ?thesis unfolding Id.S.splitted_def by simp next case False with \<open>R \<in> carrier (poly_ring L)\<close> obtain a where "a \ and "[ \ using domain.not_empty_rootsE[OF field.axioms(1)[OF L], of R] by blast from \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close> have "(Id.S.algebraic over ?K) a" proof (rule Id.S.algebraicI) from \<open>degree P \<noteq> 0\<close> show "P \<noteq> []" by auto next from \<open>a \<in># Id.S.roots R\<close> and \<open>R \<in> carrier (poly_ring L)\<close> have "Id.S.eval R a = \ using domain.roots_mem_iff_is_root[OF field.axioms(1)[OF L]] unfolding Id.S.is_root_def by auto with \<open>R pdivides\<^bsub>L\<^esub> P\<close> and \<open>a \<in> carrier L\<close> show "Id.S.eval P a using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF L] in_carrier(2)] by simp qed with \<open>a \<in> carrier L\<close> have "a \<in> ?set_of_algs" by simp hence "[ \ using subringE(3,5)[of ?set_of_algs L] subfieldE(1,6)[OF set_of_algs] unfolding sym[OF univ_poly_carrier] polynomial_def by simp hence "[ \ unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp from \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier ((?set_of_algs)[X]\<^ and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close> have "[ \ using pdiv domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs] by simp hence "[ \ unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp have "[ \ using Id.R.univ_poly_units[OF field.carrier_is_subfield[OF M]] by force with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> a and \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R have "[ \ using Id.R.divides_pirreducible_condition[OF R(2)] by auto with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> a have "degree R = 1" using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M] Id.R.carrier_is_subring, of "[ \ thus ?thesis by simp qed qed qed qed ultimately show "algebraic_closure_axioms ?M ?K" unfolding algebraic_closure_axioms_def by auto qed moreover have "indexed_const \ 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) alg_closureE: shows "algebraic_closure alg_closure (indexed_const ` (carrier R))" and "indexed_const \ using exists_closure unfolding alg_closure_def by (metis (mono_tags, lifting) someI2)+ lemma (in field) algebraically_closedI': assumes "\ shows "algebraically_closed R" proof fix p assume "p \ proof (cases "degree p \ case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis using degree_zero_imp_splitted degree_one_imp_splitted by fastforce next case False with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis using assms by fastforce qed qed lemma (in field) algebraically_closedI: assumes "\ shows "algebraically_closed R" proof fix p assume "p \ proof (induction "degree p" arbitrary: p rule: less_induct) case less show ?case proof (cases "degree p \ case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis using degree_zero_imp_splitted degree_one_imp_splitted by fastforce next case False then have "degree p > 1" by simp with \<open>p \<in> carrier (poly_ring R)\<close> have "roots p \<noteq> {#}" using assms[of p] roots_mem_iff_is_root[of p] unfolding is_root_def by force then obtain a where a: "a \ and pdiv: "[ \ using less(2) by blast then obtain q where q: "q \ unfolding pdivides_def by blast with \<open>degree p > 1\<close> have not_zero: "q \<noteq> []" and "p \<noteq> []" using domain.integral_iff[OF univ_poly_is_domain[OF carrier_is_subring] in_carrier, o by (auto simp add: univ_poly_zero[of R "carrier R"]) hence deg: "degree p = Suc (degree q)" using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q p unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto hence "splitted q" using less(1)[OF _ q] by simp moreover have "roots p = add_mset a (roots q)" using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp ultimately show ?thesis unfolding splitted_def deg by simp qed qed qed sublocale algebraic_closure \<subseteq> algebraically_closed proof (rule algebraically_closedI') fix P assume in_carrier: "P \ then have gt_zero: "degree P > 0" by simp define A where "A = finite_extension K P" from \<open>P \<in> carrier (poly_ring L)\<close> have "set P \<subseteq> carrier L" by (simp add: polynomial_incl univ_poly_carrier) hence A: "subfield A L" and P: "P \ using finite_extension_mem[OF subfieldE(1)[OF subfield_axioms], of P] in_carrier algebraic_extension finite_extension_is_subfield[OF subfield_axioms, of P] unfolding sym[OF A_def] sym[OF univ_poly_carrier] polynomial_def by auto from \<open>set P \<subseteq> carrier L\<close> have incl: "K \<subseteq> A" using finite_extension_incl[OF subfieldE(3)[OF subfield_axioms]] unfolding A_def by sim interpret UP_K: domain "K[X]" using univ_poly_is_domain[OF subfieldE(1)[OF subfield_axioms]] . interpret UP_A: domain "A[X]" using univ_poly_is_domain[OF subfieldE(1)[OF A]] . interpret Rupt: ring "Rupt A P" unfolding rupture_def using ideal.quotient_is_ring[OF UP_A.cgenideal_ideal[OF P]] . interpret Hom: ring_hom_ring "L \ using ring_hom_ringI2[OF subring_is_ring[OF subfieldE(1)] Rupt.ring_axioms rupture_surj_norm_is_hom[OF subfieldE(1) P]] A by simp let ?h = "rupture_surj A P \ have h_simp: "rupture_surj A P ` poly_of_const ` E = ?h ` E" for E by auto hence aux_lemmas: "subfield (rupture_surj A P ` poly_of_const ` K) (Rupt A P)" "subfield (rupture_surj A P ` poly_of_const ` A) (Rupt A P)" using Hom.img_is_subfield(2)[OF _ rupture_one_not_zero[OF A P gt_zero]] ring.subfield_iff(1)[OF subring_is_ring[OF subfieldE(1)[OF A]]] subfield_iff(2)[OF subfield_axioms] subfield_iff(2)[OF A] incl by auto have "carrier (K[X]) \ using subsetI[of "carrier (K[X])" "carrier (A[X])"] incl unfolding sym[OF univ_poly_carrier] polynomial_def by auto hence "id \ unfolding ring_hom_def unfolding univ_poly_mult univ_poly_add univ_poly_one by (simp add hence "rupture_surj A P \ using ring_hom_trans[OF _ rupture_surj_hom(1)[OF subfieldE(1)[OF A] P], of id] by simp then interpret Hom': ring_hom_ring "K[X]" "Rupt A P" "rupture_surj A P" using ring_hom_ringI2[OF UP_K.ring_axioms Rupt.ring_axioms] by simp from \<open>id \<in> ring_hom (K[X]) (A[X])\<close> have Id: "ring_hom_ring (K[X]) (A[X]) id" using ring_hom_ringI2[OF UP_K.ring_axioms UP_A.ring_axioms] by simp hence "subalgebra (poly_of_const ` K) (carrier (K[X])) (A[X])" using ring_hom_ring.img_is_subalgebra[OF Id _ UP_K.carrier_is_subalgebra[OF subfieldE univ_poly_subfield_of_consts[OF subfield_axioms] by auto moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<s using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp ultimately have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carri using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P] moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carri proof (intro Rupt.telescopic_base_dim(1)[where ?K = "rupture_surj A P ` poly_of_const ` K" and ?F = "rupture_surj A P ` poly_of_const ` A" and ?E = "carrier (Rupt A P)", OF aux_lemmas]) show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` A) (carrier (Rupt using Rupt.finite_dimensionI[OF rupture_dimension[OF A P gt_zero]] . next let ?h = "rupture_surj A P \ from \<open>set P \<subseteq> carrier L\<close> have "finite_dimension K A" using finite_extension_finite_dimension(1)[OF subfield_axioms, of P] algebraic_extens unfolding A_def by auto then obtain Us where Us: "set Us \ using exists_base subfield_axioms by blast hence "?h ` A = Rupt.Span (?h ` K) (map ?h Us)" using Hom.Span_hom[of K Us] incl Span_base_incl[OF subfield_axioms, of Us] unfolding Span_consistent[OF subfieldE(1)[OF A]] by simp moreover have "set (map ?h Us) \ using Span_base_incl[OF subfield_axioms Us(1)] ring_hom_memE(1)[OF Hom.homh] unfolding sym[OF Us(2)] by auto ultimately show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj using Rupt.Span_finite_dimension[OF aux_lemmas(1)] unfolding h_simp by simp qed moreover have "rupture_surj A P ` carrier (A[X]) = carrier (Rupt A P)" unfolding rupture_def FactRing_def A_RCOSETS_def' by auto with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "rupture_surj A P ` carrier (K[ by auto ultimately have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp hence "\ using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _ UP_K.carrier_is_subalgebra[OF subfieldE(3)] univ_poly_infinite_dimension[OF subfiel univ_poly_subfield_of_consts[OF subfield_axioms] by auto then obtain Q where Q: "Q \ using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "Q \<in> PIdl\<^bsub>A[X]\<^esub> P using ideal.rcos_const_imp_mem[OF UP_A.cgenideal_ideal[OF P]] unfolding rupture_def FactRing_def by auto then obtain R where "R \ unfolding cgenideal_def by blast with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q" using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp thus "splitted P" using pdivides_imp_splitted[OF in_carrier carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2) roots_over_subfield[OF Q(1)]] Q by simp qed end ¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28