Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Embedded_Algebras.thy Sprache: Isabelle

Original von: 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 \ '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)
 \<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) \<Rightarrow> 'a) list"
 where "\ P = map indexed_const P"

definition (in ring) extensions :: "((('a list \ nat) multiset) \ 'a) ring set"
 where "extensions \ { L \ \such that\.
 \<comment> \<open>i\<close> (field L) \<and>
 \<comment> \<open>ii\<close> (indexed_const \<in> ring_hom R L) \<and>
 \<comment> \<open>iii\<close> (\<forall>\ \<in> carrier L. carrier_coeff \) \<and>
 \<comment> \<open>iv\<close> (\<forall>\ \<in> carrier L. \<forall>P \<in> carrier (poly_ring R). \<forall>i.
 \<not> index_free \ (P, i) \<longrightarrow>
 \<X>\<^bsub>(P, i)\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>L\<^esub>) }"

abbreviation (in ring) restrict_extensions :: "((('a list \ nat) multiset) \ 'a) ring set" ("\")
 where "\ ~~\ law_restrict ` extensions"~~

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) = (\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 \<open>carrier A = carrier B\<close> 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 \<open>Partial Order\<close>

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 \ nat) 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 \ ~~(relation_of (\) \)"~~
 using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_relation_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 \<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 \ 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 \<times> nat) multiset) \<Rightarrow> 'a" and P and i
 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, i)" for P i
 unfolding index_free_def indexed_const_def by auto
 thus "\ index_free \
(P, i) \ \\<^bsub>(P, i)\<^esub> \ carrier (image_ring indexed_const R)"
 and "\ index_free \
(P, i) \ ring.eval (image_ring indexed_const R) (\ P) \\<^bsub>(P, i)\<^esub> = \\<^bsub>image_ring indexed_const R\<^esub>"
 by auto
 from \<open>k \<in> carrier R\<close> and \<open>\ = indexed_const k\<close> show "carrier_coeff \"
 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 \ 'a ring"
 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) a b)),
 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) = (\(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 \<open>R \<in> C\<close> show "\<exists>y \<in> carrier (union_ring C). y \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^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 \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> 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 \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> 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 \<open>Zorn\<close>

lemma (in ring) exists_core_chain:
 assumes "C \ Chains (relation_of (\) \~~)" obtains C' where "C' \ extensions" and "C = law_restrict ` C'"~~
 using Chains_relation_of[OF assms] by (meson subset_image_iff)

lemma (in ring) core_chain_is_chain:
 assumes "law_restrict ` C \ Chains (relation_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 relation_of_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])
 fix C assume C: "C \ Chains (relation_of (\) \)"
 show "\L \ \~~. \R \ C. R \ L"~~
 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' \ extensions" "C = law_restrict ` 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: "\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 \<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' \ extensions"
 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 \ 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 i
 assume "\
\ carrier (union_ring C')"
 and P: "P \ carrier (poly_ring R)"
 and not_index_free: "\ index_free \
(P, i)"
 from \<open>\ \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\ \<in> carrier T"
 using exists_superset_carrier[of C' "{ \
}"] core_chain by auto
 hence "\\<^bsub>(P, i)\<^esub> \ carrier T" and "(ring.eval T) (\ P) \\<^bsub>(P, i)\<^esub> = \\<^bsub>T\<^esub>"
 and field: "field T" and hom: "indexed_const \ ring_hom R T"
 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 \ carrier R"
 using P unfolding sym[OF univ_poly_carrier] polynomial_def by auto
 hence "set (\ P) \ carrier T"
 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>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
 show "(ring.eval (union_ring C')) (\ P) \\<^bsub>(P, i)\<^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

subsection \<open>Existence of roots\<close>

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 \<open>p \<in> carrier (poly_ring R)\<close> have "set p \<subseteq> carrier R" and lc: "p \<noteq> [] \<Longrightarrow> lead_coeff p \<noteq> \<zero>\<^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 \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
 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)"
 shows "(ring.splitted M) (\ P)"
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: "\ (ring.splitted M) (\ P)"
 have "(\ P) \ carrier (poly_ring M)"
 using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \<sigma>_def by simp
 then obtain Q
 where Q: "Q \ carrier (poly_ring M)" "pirreducible\<^bsub>M\<^esub> (carrier M) Q" "Q pdivides\<^bsub>M\<^esub> (\ P)"
 and degree_gt: "degree Q > 1"
 using M.trivial_factors_imp_splitted[of "\ P"] not_splitted by force

 from \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> have "(\<sigma> P) \<noteq> []"
 using M.degree_zero_imp_splitted[of "\ P"] not_splitted unfolding \_def by auto

 have "\i. \\
~~\ carrier M. index_free \~~
(P, i)"
 proof (rule ccontr)
 assume "\i. \\
~~\ carrier M. index_free \~~
(P, i)"
 then have "\\<^bsub>(P, i)\<^esub> \ carrier M" and "(ring.eval M) (\ P) \\<^bsub>(P, i)\<^esub> = \\<^bsub>M\<^esub>" for i
 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) \<subseteq> { a. (ring.is_root M) (\<sigma> P) a }"
 unfolding M.is_root_def by auto
 moreover have "inj (\i :: nat. \\<^bsub>(P, i)\<^esub>)"
 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 ((\i :: nat. \\<^bsub>(P, i)\<^esub>) ` UNIV)"
 unfolding infinite_iff_countable_subset by auto
 ultimately have "infinite { a. (ring.is_root M) (\ P) a }"
 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 "\\
~~\ carrier M. index_free \~~
(P, i)"
 by blast

 then have hyps:
 \<comment> \<open>i\<close> "field M"
 \<comment> \<open>ii\<close> "\<And>\. \ \<in> carrier M \<Longrightarrow> carrier_coeff \"
 \<comment> \<open>iii\<close> "\<And>\. \ \<in> carrier M \<Longrightarrow> index_free \ (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 M)"
 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 \ extensions"
 proof (auto simp add: extensions_def is_field)
 fix \ assume "\ \<in> carrier image_poly"
 then obtain R where \: "\ = 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 \ 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 \<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 \ S j
 assume A: "\
~~\ carrier image_poly" "\ index_free \~~
(S, j)" "S \ carrier (poly_ring R)"
 have "\\<^bsub>(S, j)\<^esub> \ carrier image_poly \ Id.eval (\ S) \\<^bsub>(S, j)\<^esub> = \\<^bsub>image_poly\<^esub>"
 proof (cases)
 assume "(P, i) \ (S, j)"
 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 "\\<^bsub>(S, j)\<^esub> \ carrier M" and "M.eval (\ S) \\<^bsub>(S, j)\<^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 \<sigma>_def .
 ultimately show ?thesis
 using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto
 next
 assume "\ (P, i) \ (S, j)" hence S: "(P, i) = (S, j)"
 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, j)\<^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, j)\<^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) S unfolding 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 \<sigma>_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, j)\<^esub> \ carrier image_poly" and "Id.eval (\ S) \\<^bsub>(S, j)\<^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, i)\<^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, i)\<^esub> \ carrier M"
 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 "\L \ extensions. \P \ carrier (poly_ring R). (ring.splitted L) (\ P)"
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 \<open>Existence of Algebraic Closure\<close>

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]) \ splitted P"

locale algebraically_closed = field L for L (structure) +
 assumes roots_over_carrier: "P \ carrier (poly_ring L) \ splitted P"

definition (in field) alg_closure :: "(('a list \ nat) multiset \ 'a) ring"
 where "alg_closure = (SOME L \ \such that\.
 \<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 \ 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 \ nat) 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) \ (ring.splitted L) (\ P)"
 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 \<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 \ carrier := ?K \ = ?M \ carrier := ?K \"
 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 \ carrier := ?K \)"
 by simp
 next
 show "?K \ carrier ?M"
 proof
 fix x :: "(('a list \ nat) 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 \<open>subfield ?K L\<close> and \<open>x \<in> ?K\<close> 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 "Id.R.splitted P" if "P \ carrier (?K[X]\<^bsub>?M\<^esub>)" for 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\<^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: \<sigma>_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 \<sigma>_def by auto
 hence "set (q # Q) \ carrier R" and "\ (q # Q) = (p # P)"
 unfolding \<sigma>_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 \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
 unfolding \<sigma>_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 \<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 \ carrier (poly_ring R)"
 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 \ carrier (poly_ring ?M)" "pirreducible\<^bsub>?M\<^esub> (carrier ?M) R" and "R pdivides\<^bsub>?M\<^esub> P"

 from \<open>P \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
 have "P \ carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)" and "R \ carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
 unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by auto
 hence in_carrier: "P \ carrier (poly_ring L)" "R \ carrier (poly_ring L)"
 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]\<^bsub>L\<^esub>)\<^esub> P"
 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 ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
 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 \ 1"
 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 \ carrier L" and "a \# Id.S.roots R"
 and "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] \ carrier (poly_ring L)" and pdiv: "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] pdivides\<^bsub>L\<^esub> R"
 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 = \\<^bsub>L\<^esub>"
 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 = \<zero>\<^bsub>L\<^esub>"
 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 "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] \ carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
 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 "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] \ carrier (poly_ring ?M)"
 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]\<^bsub>L\<^esub>)\<close>
 and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
 have "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] divides\<^bsub>(?set_of_algs)[X]\<^bsub>L\<^esub>\<^esub> R"
 using pdiv domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs] by simp
 hence "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R"
 unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]]
 by simp

 have "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] \ Units (poly_ring ?M)"
 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> and \<open>R \<in> carrier (poly_ring ?M)\<close>
 and \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R\<close>
 have "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ] \\<^bsub>poly_ring ?M\<^esub> R"
 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> and \<open>R \<in> carrier (poly_ring ?M)\<close>
 have "degree R = 1"
 using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
 Id.R.carrier_is_subring, of "[ \\<^bsub>L\<^esub>, \\<^bsub>L\<^esub> a ]" R] by force
 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 \ 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) alg_closureE:
 shows "algebraic_closure alg_closure (indexed_const ` (carrier R))"
 and "indexed_const \ ring_hom R alg_closure"
 using exists_closure unfolding alg_closure_def
 by (metis (mono_tags, lifting) someI2)+

lemma (in field) algebraically_closedI':
 assumes "\p. \ p \ carrier (poly_ring R); degree p > 1 \ \ splitted p"
 shows "algebraically_closed R"
proof
 fix p assume "p \ carrier (poly_ring R)" show "splitted p"
 proof (cases "degree p \ 1")
 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 "\p. \ p \ carrier (poly_ring R); degree p > 1 \ \ \x \ carrier R. eval p x = \"
 shows "algebraically_closed R"
proof
 fix p assume "p \ carrier (poly_ring R)" thus "splitted p"
 proof (induction "degree p" arbitrary: p rule: less_induct)
 case less show ?case
 proof (cases "degree p \ 1")
 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 \ carrier R" "a \# roots p"
 and pdiv: "[ \, \ a ] pdivides p" and in_carrier: "[ \, \ a ] \ carrier (poly_ring R)"
 using less(2) by blast
 then obtain q where q: "q \ carrier (poly_ring R)" and p: "p = [ \, \ a ] \\<^bsub>poly_ring R\<^esub> 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, of q]
 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 \ carrier (poly_ring L)" and gt_one: "degree P > 1"
 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 \ carrier (A[X])"
 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 simp

 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 \ carrier := A \" "Rupt A P" "rupture_surj A P \ poly_of_const"
 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 \ poly_of_const"

 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]) \ carrier (A[X])"
 using subsetI[of "carrier (K[X])" "carrier (A[X])"] incl
 unfolding sym[OF univ_poly_carrier] polynomial_def by auto
 hence "id \ ring_hom (K[X]) (A[X])"
 unfolding ring_hom_def unfolding univ_poly_mult univ_poly_add univ_poly_one by (simp add: subsetD)
 hence "rupture_surj A P \ ring_hom (K[X]) (Rupt 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(3)]]
 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 \<subseteq> carrier (A[X])"
 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 ` carrier (K[X])) (Rupt A P)"
 using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp

 moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
 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 A P))"
 using Rupt.finite_dimensionI[OF rupture_dimension[OF A P gt_zero]] .
 next
 let ?h = "rupture_surj A P \ poly_of_const"

 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_extension
 unfolding A_def by auto
 then obtain Us where Us: "set Us \ carrier L" "A = Span K 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) \ carrier (Rupt A P)"
 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 A P ` poly_of_const ` A)"
 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[X]) \<subseteq> carrier (Rupt A P)"
 by auto

 ultimately
 have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
 using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp

 hence "\ inj_on (rupture_surj A P) (carrier (K[X]))"
 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 subfield_axioms]]
 univ_poly_subfield_of_consts[OF subfield_axioms]
 by auto
 then obtain Q where Q: "Q \ carrier (K[X])" "Q \ []" and "rupture_surj A P Q = \\<^bsub>Rupt A P\<^esub>"
 using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero by blast
 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 \ carrier (A[X])" and "Q = R \\<^bsub>A[X]\<^esub> P"
 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.47 Sekunden (vorverarbeitet) ¤~~

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Embedded_Algebras.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©