(* 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 ‹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 ⊗⇘R⇙ b), add := (λa ∈ carrier R. λb ∈ carrier R. a ⊕⇘R⇙ b) ⦈" definition (in ring) σ :: "'a list ⇒ ((('a list × nat) multiset) ⇒ 'a) list" where "σ P = map indexed_const P" definition (in ring) extensions :: "((('a list × nat) 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). ∀i. ¬ index_free 𝒫 (P, i) ⟶ 𝒳⇘(P, i)⇙ ∈ carrier L ∧ (ring.eval L) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘L⇙) }" abbreviation (in ring) restrict_extensions :: "((('a list × nat) multiset) ⇒ 'a) ring set" ("𝒮") where "𝒮 ≡ law_restrict ` extensions" subsection ‹Basic Properties› 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 ⊗⇘R⇙ b)" by (simp add: law_restrict_def ring.defs) lemma law_restrict_add: "add (law_restrict R) = (λa ∈ carrier R. λb ∈ carrier R. a ⊕⇘R⇙ 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 ⊗⇘law_restrict A⇙ b = a ⊗⇘law_restrict B⇙ b" and add: "a ⊕⇘law_restrict A⇙ b = a ⊕⇘law_restrict B⇙ 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 "𝟬⇘law_restrict A⇙ = 𝟬⇘law_restrict B⇙" using ring_hom_zero[OF _ assms(2-3)[THEN ring.law_restrict_is_ring]] assms(1) unfolding ring_iso_def by auto moreover have "𝟭⇘law_restrict A⇙ = 𝟭⇘law_restrict B⇙" 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 × 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 ‹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 × nat) multiset) ⇒ '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) ⟹ 𝒳⇘(P, i)⇙ ∈ carrier (image_ring indexed_const R)" and "¬ index_free 𝒫 (P, i) ⟹ ring.eval (image_ring indexed_const R) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘image_ring indexed_const R⇙" 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 "𝟭⇘union_ring C⇙ = 𝟭⇘R⇙" and "𝟬⇘union_ring C⇙ = 𝟬⇘R⇙" proof - have "𝟭⇘R⇙ = 𝟭⇘S⇙" 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 "𝟬⇘R⇙ = 𝟬⇘S⇙" 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) = 𝟭⇘R⇙" and "zero (SOME R. R ∈ C) = 𝟬⇘R⇙" using assms by (metis (mono_tags) someI)+ thus "𝟭⇘union_ring C⇙ = 𝟭⇘R⇙" and "𝟬⇘union_ring C⇙ = 𝟬⇘R⇙" unfolding union_ring_def by auto qed lemma same_laws: assumes "R ∈ C" and "a ∈ carrier R" and "b ∈ carrier R" shows "a ⊗⇘union_ring C⇙ b = a ⊗⇘R⇙ b" and "a ⊕⇘union_ring C⇙ b = a ⊕⇘R⇙ b" proof - have "a ⊗⇘R⇙ b = a ⊗⇘S⇙ 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 ⊕⇘R⇙ b = a ⊕⇘S⇙ 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 ⊗⇘R⇙ b" and "add (SOME R. R ∈ C ∧ a ∈ carrier R ∧ b ∈ carrier R) a b = a ⊕⇘R⇙ b" using assms by (metis (mono_tags, lifting) someI)+ thus "a ⊗⇘union_ring C⇙ b = a ⊗⇘R⇙ b" and "a ⊕⇘union_ring C⇙ b = a ⊕⇘R⇙ 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 ⊗⇘union_ring C⇙ 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 ⊗⇘union_ring C⇙ b) ⊗⇘union_ring C⇙ c = a ⊗⇘union_ring C⇙ (b ⊗⇘union_ring C⇙ c)" and "a ⊗⇘union_ring C⇙ b = b ⊗⇘union_ring C⇙ a" and "𝟭⇘union_ring C⇙ ⊗⇘union_ring C⇙ a = a" and "a ⊗⇘union_ring C⇙ 𝟭⇘union_ring C⇙ = 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 "𝟭⇘union_ring C⇙ ∈ 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 ⊕⇘union_ring C⇙ 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 ⊕⇘union_ring C⇙ b) ⊗⇘union_ring C⇙ c = (a ⊗⇘union_ring C⇙ c) ⊕⇘union_ring C⇙ (b ⊗⇘union_ring C⇙ c)" and "(a ⊕⇘union_ring C⇙ b) ⊕⇘union_ring C⇙ c = a ⊕⇘union_ring C⇙ (b ⊕⇘union_ring C⇙ c)" and "a ⊕⇘union_ring C⇙ b = b ⊕⇘union_ring C⇙ a" and "𝟬⇘union_ring C⇙ ⊕⇘union_ring C⇙ 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' ⊕⇘union_ring C⇙ a = 𝟬⇘union_ring C⇙" 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 ⊕⇘union_ring C⇙ a = 𝟬⇘union_ring C⇙" unfolding union_ring_carrier by auto next show "𝟬⇘union_ring C⇙ ∈ 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) - { 𝟬⇘union_ring C⇙ } ⊆ Units (union_ring C)" proof fix a assume "a ∈ carrier (union_ring C) - { 𝟬⇘union_ring C⇙ }" hence "a ∈ carrier (union_ring C)" and "a ≠ 𝟬⇘union_ring C⇙" 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 ≠ 𝟬⇘union_ring C⇙› have "a ∈ Units R" unfolding same_one_same_zero[OF R(1)] field_Units by auto hence "∃a' ∈ carrier R. a' ⊗⇘union_ring C⇙ a = 𝟭⇘union_ring C⇙ ∧ a ⊗⇘union_ring C⇙ a' = 𝟭⇘union_ring C⇙" 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 "𝟬⇘union_ring C⇙ ∉ Units (union_ring C)" proof (rule ccontr) assume "¬ 𝟬⇘union_ring C⇙ ∉ Units (union_ring C)" then obtain a where a: "a ∈ carrier (union_ring C)" "a ⊗⇘union_ring C⇙ 𝟬⇘union_ring C⇙ = 𝟭⇘union_ring C⇙" 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 "𝟭⇘R⇙ = 𝟬⇘R⇙" 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) - { 𝟬⇘union_ring C⇙ }" unfolding Units_def by auto ultimately show "Units (union_ring C) = carrier (union_ring C) - { 𝟬⇘union_ring C⇙ }" 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 (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 ‹C ∈ Chains (relation_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 i assume "𝒫 ∈ carrier (union_ring C')" and P: "P ∈ carrier (poly_ring R)" and not_index_free: "¬ index_free 𝒫 (P, i)" from ‹𝒫 ∈ carrier (union_ring C')› obtain T where T: "T ∈ C'" "𝒫 ∈ carrier T" using exists_superset_carrier[of C' "{ 𝒫 }"] core_chain by auto hence "𝒳⇘(P, i)⇙ ∈ carrier T" and "(ring.eval T) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘T⇙" 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 ‹T ∈ C'› show "𝒳⇘(P, i)⇙ ∈ 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 σ_def by (induct P) (auto) with ‹𝒳⇘(P, i)⇙ ∈ carrier T› and ‹(ring.eval T) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘T⇙› show "(ring.eval (union_ring C')) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘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(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 ‹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 ≠ 𝟬⇘R⇙" 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 = 𝟬⇘S⇙ ⟹ a = 𝟬⇘R⇙" 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) ≠ 𝟬⇘S⇙" 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 "𝟭⇘S⇙ ≠ 𝟬⇘S⇙" shows "p ∈ carrier (K[X]⇘R⇙) ⟹ (map h p) ∈ carrier ((h ` K)[X]⇘S⇙)" proof - assume "p ∈ carrier (K[X]⇘R⇙)" 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 ‹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 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 σ_def by simp then obtain Q where Q: "Q ∈ carrier (poly_ring M)" "pirreducible⇘M⇙ (carrier M) Q" "Q pdivides⇘M⇙ (σ P)" and degree_gt: "degree Q > 1" using M.trivial_factors_imp_splitted[of "σ P"] not_splitted by force from ‹(σ P) ∈ carrier (poly_ring M)› have "(σ P) ≠ []" 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 "𝒳⇘(P, i)⇙ ∈ carrier M" and "(ring.eval M) (σ P) 𝒳⇘(P, i)⇙ = 𝟬⇘M⇙" for i using assms(1,3) unfolding extensions_def by blast+ with ‹(σ P) ≠ []› have "((λi :: nat. 𝒳⇘(P, i)⇙) ` UNIV) ⊆ { a. (ring.is_root M) (σ P) a }" unfolding M.is_root_def by auto moreover have "inj (λi :: nat. 𝒳⇘(P, i)⇙)" 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. 𝒳⇘(P, i)⇙) ` UNIV)" unfolding infinite_iff_countable_subset by auto ultimately have "infinite { a. (ring.is_root M) (σ P) a }" using finite_subset by auto with ‹(σ P) ∈ carrier (poly_ring M)› 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: ― ‹i› "field M" ― ‹ii› "⋀𝒫. 𝒫 ∈ carrier M ⟹ carrier_coeff 𝒫" ― ‹iii› "⋀𝒫. 𝒫 ∈ carrier M ⟹ index_free 𝒫 (P, i)" ― ‹iv› "𝟬⇘M⇙ = indexed_const 𝟬" 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 ‹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, i) 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 j assume A: "𝒫 ∈ carrier image_poly" "¬ index_free 𝒫 (S, j)" "S ∈ carrier (poly_ring R)" have "𝒳⇘(S, j)⇙ ∈ carrier image_poly ∧ Id.eval (σ S) 𝒳⇘(S, j)⇙ = 𝟬⇘image_poly⇙" proof (cases) assume "(P, i) ≠ (S, j)" then obtain Q' where "Q' ∈ carrier M" and "¬ 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 "𝒳⇘(S, j)⇙ ∈ carrier M" and "M.eval (σ S) 𝒳⇘(S, j)⇙ = 𝟬⇘M⇙" 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, 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 "𝒳⇘(S, j)⇙ ∈ 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 𝒳⇘(S, j)⇙ = 𝟬⇘image_poly⇙" 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⇘image_poly⇙ (σ S)" proof - obtain R where R: "R ∈ carrier (poly_ring M)" "σ S = Q ⊗⇘poly_ring M⇙ 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 ⊗⇘poly_ring image_poly⇙ 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 "𝒳⇘(S, j)⇙ ∈ carrier image_poly" and "Id.eval (σ S) 𝒳⇘(S, j)⇙ = 𝟬⇘image_poly⇙" 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 "𝒳⇘(P, i)⇙ ∈ carrier image_poly" using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp moreover have "𝒳⇘(P, i)⇙ ∉ 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 ‹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]) ⟹ 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›. ― ‹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]⇘R⇙)" and "p ≠ []" and eval: "Hom.R.eval p x = 𝟬⇘R⇙" 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]⇘S⇙)" 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) = 𝟬⇘S⇙" 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 ‹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 × 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 ‹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 "Id.R.splitted P" if "P ∈ carrier (?K[X]⇘?M⇙)" for P proof - from ‹P ∈ carrier (?K[X]⇘?M⇙)› have "P ∈ 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 ‹P ∈ carrier (poly_ring ?M)› 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 ‹P ∈ carrier (?K[X]⇘?M⇙)› have "P ∈ carrier (?K[X]⇘L⇙)" 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 = 𝟬⇘L⇙" 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]⇘?M⇙)" unfolding sym[OF univ_poly_carrier] polynomial_def by auto with ‹P ∈ carrier (?K[X]⇘?M⇙)› show False by simp qed ultimately have "Q ∈ carrier (poly_ring R)" unfolding sym[OF univ_poly_carrier] polynomial_def by auto with ‹σ Q = P› have "Id.S.splitted P" using roots[of Q] by simp from ‹P ∈ carrier (poly_ring ?M)› show ?thesis proof (rule field.trivial_factors_imp_splitted[OF M]) fix R assume R: "R ∈ carrier (poly_ring ?M)" "pirreducible⇘?M⇙ (carrier ?M) R" and "R pdivides⇘?M⇙ P" from ‹P ∈ carrier (poly_ring ?M)› and ‹R ∈ carrier (poly_ring ?M)› have "P ∈ carrier ((?set_of_algs)[X]⇘L⇙)" and "R ∈ carrier ((?set_of_algs)[X]⇘L⇙)" 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 ‹R pdivides⇘?M⇙ P› have "R divides⇘((?set_of_algs)[X]⇘L⇙)⇙ P" unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp with ‹P ∈ carrier ((?set_of_algs)[X]⇘L⇙)› and ‹R ∈ carrier ((?set_of_algs)[X]⇘L⇙)› have "R pdivides⇘L⇙ P" using domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs, of R P] by simp with ‹Id.S.splitted P› and ‹degree P ≠ 0› 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 ‹Id.S.splitted R› show ?thesis unfolding Id.S.splitted_def by simp next case False with ‹R ∈ carrier (poly_ring L)› obtain a where "a ∈ carrier L" and "a ∈# Id.S.roots R" and "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier (poly_ring L)" and pdiv: "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] pdivides⇘L⇙ R" using domain.not_empty_rootsE[OF field.axioms(1)[OF L], of R] by blast from ‹P ∈ carrier (?K[X]⇘L⇙)› have "(Id.S.algebraic over ?K) a" proof (rule Id.S.algebraicI) from ‹degree P ≠ 0› show "P ≠ []" by auto next from ‹a ∈# Id.S.roots R› and ‹R ∈ carrier (poly_ring L)› have "Id.S.eval R a = 𝟬⇘L⇙" using domain.roots_mem_iff_is_root[OF field.axioms(1)[OF L]] unfolding Id.S.is_root_def by auto with ‹R pdivides⇘L⇙ P› and ‹a ∈ carrier L› show "Id.S.eval P a = 𝟬⇘L⇙" using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF L] in_carrier(2)] by simp qed with ‹a ∈ carrier L› have "a ∈ ?set_of_algs" by simp hence "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier ((?set_of_algs)[X]⇘L⇙)" 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 "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier (poly_ring ?M)" unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp from ‹[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier ((?set_of_algs)[X]⇘L⇙)› and ‹R ∈ carrier ((?set_of_algs)[X]⇘L⇙)› have "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] divides⇘(?set_of_algs)[X]⇘L⇙⇙ R" using pdiv domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs] by simp hence "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] divides⇘poly_ring ?M⇙ R" unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp have "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∉ Units (poly_ring ?M)" using Id.R.univ_poly_units[OF field.carrier_is_subfield[OF M]] by force with ‹[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier (poly_ring ?M)› and ‹R ∈ carrier (poly_ring ?M)› and ‹[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] divides⇘poly_ring ?M⇙ R› have "[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∼⇘poly_ring ?M⇙ R" using Id.R.divides_pirreducible_condition[OF R(2)] by auto with ‹[ 𝟭⇘L⇙, ⊖⇘L⇙ a ] ∈ carrier (poly_ring ?M)› and ‹R ∈ carrier (poly_ring ?M)› have "degree R = 1" using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M] Id.R.carrier_is_subring, of "[ 𝟭⇘L⇙, ⊖⇘L⇙ 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 ‹p ∈ carrier (poly_ring R)› show ?thesis using degree_zero_imp_splitted degree_one_imp_splitted by fastforce next case False with ‹p ∈ carrier (poly_ring R)› 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 ‹p ∈ carrier (poly_ring R)› show ?thesis using degree_zero_imp_splitted degree_one_imp_splitted by fastforce next case False then have "degree p > 1" by simp with ‹p ∈ carrier (poly_ring R)› have "roots p ≠ {#}" 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 ] ⊗⇘poly_ring R⇙ q" unfolding pdivides_def by blast with ‹degree p > 1› have not_zero: "q ≠ []" and "p ≠ []" 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 ⊆ 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 ‹P ∈ carrier (poly_ring L)› have "set P ⊆ 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 ‹set P ⊆ carrier L› have incl: "K ⊆ 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 ‹id ∈ ring_hom (K[X]) (A[X])› 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 ‹carrier (K[X]) ⊆ carrier (A[X])› have "poly_of_const ` K ⊆ 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 ‹set P ⊆ carrier L› 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 ‹carrier (K[X]) ⊆ carrier (A[X])› have "rupture_surj A P ` carrier (K[X]) ⊆ 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 = 𝟬⇘Rupt A P⇙" using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero by blast with ‹carrier (K[X]) ⊆ carrier (A[X])› have "Q ∈ PIdl⇘A[X]⇙ 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 ⊗⇘A[X]⇙ P" unfolding cgenideal_def by blast with ‹P ∈ carrier (A[X])› 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