(* Title: HOL/Algebra/Finite_Extensions.thy Author: Paulo Emílio de Vilhena *) theory Finite_Extensions imports Embedded_Algebras Polynomials Polynomial_Divisibility begin section ‹Finite Extensions› subsection ‹Definitions› definition (in ring) transcendental :: "'a set ⇒ 'a ⇒ bool" where "transcendental K x ⟷ inj_on (λp. eval p x) (carrier (K[X]))" abbreviation (in ring) algebraic :: "'a set ⇒ 'a ⇒ bool" where "algebraic K x ≡ ¬ transcendental K x" definition (in ring) Irr :: "'a set ⇒ 'a ⇒ 'a list" where "Irr K x = (THE p. p ∈ carrier (K[X]) ∧ pirreducible K p ∧ eval p x = 𝟬 ∧ lead_coeff p = 𝟭)" inductive_set (in ring) simple_extension :: "'a set ⇒ 'a ⇒ 'a set" for K and x where zero [simp, intro]: "𝟬 ∈ simple_extension K x" | lin: "⟦ k1 ∈ simple_extension K x; k2 ∈ K ⟧ ⟹ (k1 ⊗ x) ⊕ k2 ∈ simple_extension K x" fun (in ring) finite_extension :: "'a set ⇒ 'a list ⇒ 'a set" where "finite_extension K xs = foldr (λx K'. simple_extension K' x) xs K" subsection ‹Basic Properties› lemma (in ring) transcendental_consistent: assumes "subring K R" shows "transcendental = ring.transcendental (R ⦇ carrier := K ⦈)" unfolding transcendental_def ring.transcendental_def[OF subring_is_ring[OF assms]] univ_poly_consistent[OF assms] eval_consistent[OF assms] .. lemma (in ring) algebraic_consistent: assumes "subring K R" shows "algebraic = ring.algebraic (R ⦇ carrier := K ⦈)" unfolding over_def transcendental_consistent[OF assms] .. lemma (in ring) eval_transcendental: assumes "(transcendental over K) x" "p ∈ carrier (K[X])" "eval p x = 𝟬" shows "p = []" proof - have "[] ∈ carrier (K[X])" and "eval [] x = 𝟬" by (auto simp add: univ_poly_def) thus ?thesis using assms unfolding over_def transcendental_def inj_on_def by auto qed lemma (in ring) transcendental_imp_trivial_ker: shows "(transcendental over K) x ⟹ a_kernel (K[X]) R (λp. eval p x) = { [] }" using eval_transcendental unfolding a_kernel_def' by (auto simp add: univ_poly_def) lemma (in ring) non_trivial_ker_imp_algebraic: shows "a_kernel (K[X]) R (λp. eval p x) ≠ { [] } ⟹ (algebraic over K) x" using transcendental_imp_trivial_ker unfolding over_def by auto lemma (in domain) trivial_ker_imp_transcendental: assumes "subring K R" and "x ∈ carrier R" shows "a_kernel (K[X]) R (λp. eval p x) = { [] } ⟹ (transcendental over K) x" using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] unfolding transcendental_def over_def by (simp add: univ_poly_zero) lemma (in domain) algebraic_imp_non_trivial_ker: assumes "subring K R" and "x ∈ carrier R" shows "(algebraic over K) x ⟹ a_kernel (K[X]) R (λp. eval p x) ≠ { [] }" using trivial_ker_imp_transcendental[OF assms] unfolding over_def by auto lemma (in domain) algebraicE: assumes "subring K R" and "x ∈ carrier R" "(algebraic over K) x" obtains p where "p ∈ carrier (K[X])" "p ≠ []" "eval p x = 𝟬" proof - have "[] ∈ a_kernel (K[X]) R (λp. eval p x)" unfolding a_kernel_def' univ_poly_def by auto then obtain p where "p ∈ carrier (K[X])" "p ≠ []" "eval p x = 𝟬" using algebraic_imp_non_trivial_ker[OF assms] unfolding a_kernel_def' by blast thus thesis using that by auto qed lemma (in ring) algebraicI: assumes "p ∈ carrier (K[X])" "p ≠ []" and "eval p x = 𝟬" shows "(algebraic over K) x" using assms non_trivial_ker_imp_algebraic unfolding a_kernel_def' by auto lemma (in ring) transcendental_mono: assumes "K ⊆ K'" "(transcendental over K') x" shows "(transcendental over K) x" proof - have "carrier (K[X]) ⊆ carrier (K'[X])" using assms(1) unfolding univ_poly_def polynomial_def by auto thus ?thesis using assms unfolding over_def transcendental_def by (metis inj_on_subset) qed corollary (in ring) algebraic_mono: assumes "K ⊆ K'" "(algebraic over K) x" shows "(algebraic over K') x" using transcendental_mono[OF assms(1)] assms(2) unfolding over_def by blast lemma (in domain) zero_is_algebraic: assumes "subring K R" shows "(algebraic over K) 𝟬" using algebraicI[OF var_closed(1)[OF assms]] unfolding var_def by auto lemma (in domain) algebraic_self: assumes "subring K R" and "k ∈ K" shows "(algebraic over K) k" proof (rule algebraicI[of "[ 𝟭, ⊖ k ]"]) show "[ 𝟭, ⊖ k ] ∈ carrier (K [X])" and "[ 𝟭, ⊖ k ] ≠ []" using subringE(2-3,5)[OF assms(1)] assms(2) unfolding univ_poly_def polynomial_def by auto have "k ∈ carrier R" using subringE(1)[OF assms(1)] assms(2) by auto thus "eval [ 𝟭, ⊖ k ] k = 𝟬" by (auto, algebra) qed lemma (in domain) ker_diff_carrier: assumes "subring K R" shows "a_kernel (K[X]) R (λp. eval p x) ≠ carrier (K[X])" proof - have "eval [ 𝟭 ] x ≠ 𝟬" and "[ 𝟭 ] ∈ carrier (K[X])" using subringE(3)[OF assms] unfolding univ_poly_def polynomial_def by auto thus ?thesis unfolding a_kernel_def' by blast qed subsection ‹Minimal Polynomial› lemma (in domain) minimal_polynomial_is_unique: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" shows "∃!p ∈ carrier (K[X]). pirreducible K p ∧ eval p x = 𝟬 ∧ lead_coeff p = 𝟭" (is "∃!p. ?minimal_poly p") proof - interpret UP: principal_domain "K[X]" using univ_poly_is_principal[OF assms(1)] . let ?ker_gen = "λp. p ∈ carrier (K[X]) ∧ pirreducible K p ∧ lead_coeff p = 𝟭 ∧ a_kernel (K[X]) R (λp. eval p x) = PIdl⇘K[X]⇙ p" obtain p where p: "?ker_gen p" and unique: "⋀q. ?ker_gen q ⟹ q = p" using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)] algebraic_imp_non_trivial_ker[OF _ assms(2-3)] ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto hence "?minimal_poly p" using UP.cgenideal_self p unfolding a_kernel_def' by auto moreover have "⋀q. ?minimal_poly q ⟹ q = p" proof - fix q assume q: "?minimal_poly q" then have "q ∈ PIdl⇘K[X]⇙ p" using p unfolding a_kernel_def' by auto hence "p ∼⇘K[X]⇙ q" using cgenideal_pirreducible[OF assms(1)] p q by simp hence "a_kernel (K[X]) R (λp. eval p x) = PIdl⇘K[X]⇙ q" using UP.associated_iff_same_ideal q p by simp thus "q = p" using unique q by simp qed ultimately show ?thesis by blast qed lemma (in domain) IrrE: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" shows "Irr K x ∈ carrier (K[X])" and "pirreducible K (Irr K x)" and "lead_coeff (Irr K x) = 𝟭" and "eval (Irr K x) x = 𝟬" using theI'[OF minimal_polynomial_is_unique[OF assms]] unfolding Irr_def by auto lemma (in domain) Irr_generates_ker: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" shows "a_kernel (K[X]) R (λp. eval p x) = PIdl⇘K[X]⇙ (Irr K x)" proof - obtain q where q: "q ∈ carrier (K[X])" "pirreducible K q" and ker: "a_kernel (K[X]) R (λp. eval p x) = PIdl⇘K[X]⇙ q" using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)] algebraic_imp_non_trivial_ker[OF _ assms(2-3)] ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto have "Irr K x ∈ PIdl⇘K[X]⇙ q" using IrrE(1,4)[OF assms] ker unfolding a_kernel_def' by auto thus ?thesis using cgenideal_pirreducible[OF assms(1) q(1-2) IrrE(2)[OF assms]] q(1) IrrE(1)[OF assms] cring.associated_iff_same_ideal[OF univ_poly_is_cring[OF subfieldE(1)[OF assms(1)]]] unfolding ker by simp qed lemma (in domain) Irr_minimal: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" and "p ∈ carrier (K[X])" "eval p x = 𝟬" shows "(Irr K x) pdivides p" proof - interpret UP: principal_domain "K[X]" using univ_poly_is_principal[OF assms(1)] . have "p ∈ PIdl⇘K[X]⇙ (Irr K x)" using Irr_generates_ker[OF assms(1-3)] assms(4-5) unfolding a_kernel_def' by auto hence "(Irr K x) divides⇘K[X]⇙ p" using UP.to_contain_is_to_divide IrrE(1)[OF assms(1-3)] by (meson UP.cgenideal_ideal UP.cgenideal_minimal assms(4)) thus ?thesis unfolding pdivides_iff_shell[OF assms(1) IrrE(1)[OF assms(1-3)] assms(4)] . qed lemma (in domain) rupture_of_Irr: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" shows "field (Rupt K (Irr K x))" using rupture_is_field_iff_pirreducible[OF assms(1)] IrrE(1-2)[OF assms] by simp subsection ‹Simple Extensions› lemma (in ring) simple_extension_consistent: assumes "subring K R" shows "ring.simple_extension (R ⦇ carrier := K ⦈) = simple_extension" proof - interpret K: ring "R ⦇ carrier := K ⦈" using subring_is_ring[OF assms] . have "⋀K' x. K.simple_extension K' x ⊆ simple_extension K' x" proof fix K' x a show "a ∈ K.simple_extension K' x ⟹ a ∈ simple_extension K' x" by (induction rule: K.simple_extension.induct) (auto simp add: simple_extension.lin) qed moreover have "⋀K' x. simple_extension K' x ⊆ K.simple_extension K' x" proof fix K' x a assume a: "a ∈ simple_extension K' x" thus "a ∈ K.simple_extension K' x" using K.simple_extension.zero K.simple_extension.lin by (induction rule: simple_extension.induct) (simp)+ qed ultimately show ?thesis by blast qed lemma (in ring) mono_simple_extension: assumes "K ⊆ K'" shows "simple_extension K x ⊆ simple_extension K' x" proof fix a assume "a ∈ simple_extension K x" thus "a ∈ simple_extension K' x" proof (induct a rule: simple_extension.induct, simp) case lin thus ?case using simple_extension.lin assms by blast qed qed lemma (in ring) simple_extension_incl: assumes "K ⊆ carrier R" and "x ∈ carrier R" shows "K ⊆ simple_extension K x" proof fix k assume "k ∈ K" thus "k ∈ simple_extension K x" using simple_extension.lin[OF simple_extension.zero, of k K x] assms by auto qed lemma (in ring) simple_extension_mem: assumes "subring K R" and "x ∈ carrier R" shows "x ∈ simple_extension K x" proof - have "𝟭 ∈ simple_extension K x" using simple_extension_incl[OF _ assms(2)] subringE(1,3)[OF assms(1)] by auto thus ?thesis using simple_extension.lin[OF _ subringE(2)[OF assms(1)], of 𝟭 x] assms(2) by auto qed lemma (in ring) simple_extension_carrier: assumes "x ∈ carrier R" shows "simple_extension (carrier R) x = carrier R" proof show "carrier R ⊆ simple_extension (carrier R) x" using simple_extension_incl[OF _ assms] by auto next show "simple_extension (carrier R) x ⊆ carrier R" proof fix a assume "a ∈ simple_extension (carrier R) x" thus "a ∈ carrier R" by (induct a rule: simple_extension.induct) (auto simp add: assms) qed qed lemma (in ring) simple_extension_in_carrier: assumes "K ⊆ carrier R" and "x ∈ carrier R" shows "simple_extension K x ⊆ carrier R" using mono_simple_extension[OF assms(1), of x] simple_extension_carrier[OF assms(2)] by auto lemma (in ring) simple_extension_subring_incl: assumes "subring K' R" and "K ⊆ K'" "x ∈ K'" shows "simple_extension K x ⊆ K'" using ring.simple_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3) unfolding simple_extension_consistent[OF assms(1)] by simp lemma (in ring) simple_extension_as_eval_img: assumes "K ⊆ carrier R" "x ∈ carrier R" shows "simple_extension K x = (λp. eval p x) ` carrier (K[X])" proof show "simple_extension K x ⊆ (λp. eval p x) ` carrier (K[X])" proof fix a assume "a ∈ simple_extension K x" thus "a ∈ (λp. eval p x) ` carrier (K[X])" proof (induction rule: simple_extension.induct) case zero have "polynomial K []" and "eval [] x = 𝟬" unfolding polynomial_def by simp+ thus ?case unfolding univ_poly_carrier by force next case (lin k1 k2) then obtain p where p: "p ∈ carrier (K[X])" "polynomial K p" "eval p x = k1" by (auto simp add: univ_poly_carrier) hence "set p ⊆ carrier R" and "k2 ∈ carrier R" using assms(1) lin(2) unfolding polynomial_def by auto hence "eval (normalize (p @ [ k2 ])) x = k1 ⊗ x ⊕ k2" using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto moreover have "set (p @ [k2]) ⊆ K" using polynomial_incl[OF p(2)] ‹k2 ∈ K› by auto then have "local.normalize (p @ [k2]) ∈ carrier (K [X])" using normalize_gives_polynomial univ_poly_carrier by blast ultimately show ?case unfolding univ_poly_carrier by force qed qed next show "(λp. eval p x) ` carrier (K[X]) ⊆ simple_extension K x" proof fix a assume "a ∈ (λp. eval p x) ` carrier (K[X])" then obtain p where p: "set p ⊆ K" "eval p x = a" using polynomial_incl unfolding univ_poly_def by auto thus "a ∈ simple_extension K x" proof (induct "length p" arbitrary: p a) case 0 thus ?case using simple_extension.zero by simp next case (Suc n) obtain p' k where p: "p = p' @ [ k ]" using Suc(2) by (metis list.size(3) nat.simps(3) rev_exhaust) hence "a = (eval p' x) ⊗ x ⊕ k" using eval_append_aux[of p' k x] Suc(3-4) assms unfolding p by auto moreover have "eval p' x ∈ simple_extension K x" using Suc(1-3) unfolding p by auto ultimately show ?case using simple_extension.lin Suc(3) unfolding p by auto qed qed qed corollary (in domain) simple_extension_is_subring: assumes "subring K R" "x ∈ carrier R" shows "subring (simple_extension K x) R" using ring_hom_ring.img_is_subring[OF eval_ring_hom[OF assms] ring.carrier_is_subring[OF univ_poly_is_ring[OF assms(1)]]] simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)] by simp corollary (in domain) simple_extension_minimal: assumes "subring K R" "x ∈ carrier R" shows "simple_extension K x = ⋂ { K'. subring K' R ∧ K ⊆ K' ∧ x ∈ K' }" using simple_extension_is_subring[OF assms] simple_extension_mem[OF assms] simple_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] simple_extension_subring_incl by blast corollary (in domain) simple_extension_isomorphism: assumes "subring K R" "x ∈ carrier R" shows "(K[X]) Quot (a_kernel (K[X]) R (λp. eval p x)) ≃ R ⦇ carrier := simple_extension K x ⦈" using ring_hom_ring.FactRing_iso_set_aux[OF eval_ring_hom[OF assms]] simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)] unfolding is_ring_iso_def by auto corollary (in domain) simple_extension_of_algebraic: assumes "subfield K R" and "x ∈ carrier R" "(algebraic over K) x" shows "Rupt K (Irr K x) ≃ R ⦇ carrier := simple_extension K x ⦈" using simple_extension_isomorphism[OF subfieldE(1)[OF assms(1)] assms(2)] unfolding Irr_generates_ker[OF assms] rupture_def by simp corollary (in domain) simple_extension_of_transcendental: assumes "subring K R" and "x ∈ carrier R" "(transcendental over K) x" shows "K[X] ≃ R ⦇ carrier := simple_extension K x ⦈" using simple_extension_isomorphism[OF _ assms(2), of K] assms(1) ring_iso_trans[OF ring.FactRing_zeroideal(2)[OF univ_poly_is_ring]] unfolding transcendental_imp_trivial_ker[OF assms(3)] univ_poly_zero by auto proposition (in domain) simple_extension_subfield_imp_algebraic: assumes "subring K R" "x ∈ carrier R" shows "subfield (simple_extension K x) R ⟹ (algebraic over K) x" proof - assume simple_ext: "subfield (simple_extension K x) R" show "(algebraic over K) x" proof (rule ccontr) assume "¬ (algebraic over K) x" then have "(transcendental over K) x" unfolding over_def by simp then obtain h where h: "h ∈ ring_iso (R ⦇ carrier := simple_extension K x ⦈) (K[X])" using ring_iso_sym[OF univ_poly_is_ring simple_extension_of_transcendental] assms unfolding is_ring_iso_def by blast then interpret Hom: ring_hom_ring "R ⦇ carrier := simple_extension K x ⦈" "K[X]" h using subring_is_ring[OF simple_extension_is_subring[OF assms]] univ_poly_is_ring[OF assms(1)] assms h by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def) have "field (K[X])" using field.ring_iso_imp_img_field[OF subfield_iff(2)[OF simple_ext] h] unfolding Hom.hom_one Hom.hom_zero by simp moreover have "¬ field (K[X])" using univ_poly_not_field[OF assms(1)] . ultimately show False by simp qed qed proposition (in domain) simple_extension_is_subfield: assumes "subfield K R" "x ∈ carrier R" shows "subfield (simple_extension K x) R ⟷ (algebraic over K) x" proof assume alg: "(algebraic over K) x" then obtain h where h: "h ∈ ring_iso (Rupt K (Irr K x)) (R ⦇ carrier := simple_extension K x ⦈)" using simple_extension_of_algebraic[OF assms] unfolding is_ring_iso_def by blast have rupt_field: "field (Rupt K (Irr K x))" and "ring (R ⦇ carrier := simple_extension K x ⦈)" using subring_is_ring[OF simple_extension_is_subring[OF subfieldE(1)]] rupture_of_Irr[OF assms alg] assms by simp+ then interpret Hom: ring_hom_ring "Rupt K (Irr K x)" "R ⦇ carrier := simple_extension K x ⦈" h using h cring.axioms(1)[OF domain.axioms(1)[OF field.axioms(1)]] by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def) show "subfield (simple_extension K x) R" using field.ring_iso_imp_img_field[OF rupt_field h] subfield_iff(1)[OF _ simple_extension_in_carrier[OF subfieldE(3)[OF assms(1)] assms(2)]] by simp next assume simple_ext: "subfield (simple_extension K x) R" thus "(algebraic over K) x" using simple_extension_subfield_imp_algebraic[OF subfieldE(1)[OF assms(1)] assms(2)] by simp qed subsection ‹Link between dimension of K-algebras and algebraic extensions› lemma (in domain) exp_base_independent: assumes "subfield K R" "x ∈ carrier R" "(algebraic over K) x" shows "independent K (exp_base x (degree (Irr K x)))" proof - have "⋀n. n ≤ degree (Irr K x) ⟹ independent K (exp_base x n)" proof - fix n show "n ≤ degree (Irr K x) ⟹ independent K (exp_base x n)" proof (induct n, simp add: exp_base_def) case (Suc n) have "x [^] n ∉ Span K (exp_base x n)" proof (rule ccontr) assume "¬ x [^] n ∉ Span K (exp_base x n)" then obtain a Ks where Ks: "a ∈ K - { 𝟬 }" "set Ks ⊆ K" "length Ks = n" "combine (a # Ks) (exp_base x (Suc n)) = 𝟬" using Span_mem_imp_non_trivial_combine[OF assms(1) exp_base_closed[OF assms(2), of n]] by (auto simp add: exp_base_def) hence "eval (a # Ks) x = 𝟬" using combine_eq_eval by (auto simp add: exp_base_def) moreover have "(a # Ks) ∈ carrier (K[X]) - { [] }" unfolding univ_poly_def polynomial_def using Ks(1-2) by auto ultimately have "degree (Irr K x) ≤ n" using pdivides_imp_degree_le[OF subfieldE(1)[OF assms(1)] IrrE(1)[OF assms] _ _ Irr_minimal[OF assms, of "a # Ks"]] Ks(3) by auto from ‹Suc n ≤ degree (Irr K x)› and this show False by simp qed thus ?case using independent.li_Cons assms(2) Suc by (auto simp add: exp_base_def) qed qed thus ?thesis by simp qed lemma (in ring) Span_eq_eval_img: assumes "subfield K R" "x ∈ carrier R" shows "Span K (exp_base x n) = (λp. eval p x) ` { p ∈ carrier (K[X]). length p ≤ n }" (is "?Span = ?eval_img") proof show "?Span ⊆ ?eval_img" proof fix u assume "u ∈ Span K (exp_base x n)" then obtain Ks where Ks: "set Ks ⊆ K" "length Ks = n" "u = combine Ks (exp_base x n)" using Span_eq_combine_set_length_version[OF assms(1) exp_base_closed[OF assms(2)]] by (auto simp add: exp_base_def) hence "u = eval (normalize Ks) x" using combine_eq_eval eval_normalize[OF _ assms(2)] subfieldE(3)[OF assms(1)] by auto moreover have "normalize Ks ∈ carrier (K[X])" using normalize_gives_polynomial[OF Ks(1)] unfolding univ_poly_def by auto moreover have "length (normalize Ks) ≤ n" using normalize_length_le[of Ks] Ks(2) by auto ultimately show "u ∈ ?eval_img" by auto qed next show "?eval_img ⊆ ?Span" proof fix u assume "u ∈ ?eval_img" then obtain p where p: "p ∈ carrier (K[X])" "length p ≤ n" "u = eval p x" by blast hence "combine p (exp_base x (length p)) = u" using combine_eq_eval by auto moreover have set_p: "set p ⊆ K" using polynomial_incl[of K p] p(1) unfolding univ_poly_carrier by auto hence "set p ⊆ carrier R" using subfieldE(3)[OF assms(1)] by auto moreover have "drop (n - length p) (exp_base x n) = exp_base x (length p)" using p(2) drop_exp_base by auto ultimately have "combine ((replicate (n - length p) 𝟬) @ p) (exp_base x n) = u" using combine_prepend_replicate[OF _ exp_base_closed[OF assms(2), of n]] by auto moreover have "set ((replicate (n - length p) 𝟬) @ p) ⊆ K" using subringE(2)[OF subfieldE(1)[OF assms(1)]] set_p by auto ultimately show "u ∈ ?Span" using Span_eq_combine_set[OF assms(1) exp_base_closed[OF assms(2), of n]] by blast qed qed lemma (in domain) Span_exp_base: assumes "subfield K R" "x ∈ carrier R" "(algebraic over K) x" shows "Span K (exp_base x (degree (Irr K x))) = simple_extension K x" unfolding simple_extension_as_eval_img[OF subfieldE(3)[OF assms(1)] assms(2)] Span_eq_eval_img[OF assms(1-2)] proof (auto) interpret UP: principal_domain "K[X]" using univ_poly_is_principal[OF assms(1)] . note hom_simps = ring_hom_memE[OF eval_is_hom[OF subfieldE(1)[OF assms(1)] assms(2)]] fix p assume p: "p ∈ carrier (K[X])" have Irr: "Irr K x ∈ carrier (K[X])" "Irr K x ≠ []" using IrrE(1-2)[OF assms] unfolding ring_irreducible_def univ_poly_zero by auto then obtain q r where q: "q ∈ carrier (K[X])" and r: "r ∈ carrier (K[X])" and dvd: "p = Irr K x ⊗⇘K [X]⇙ q ⊕⇘K [X]⇙ r" "r = [] ∨ degree r < degree (Irr K x)" using subfield_long_division_theorem_shell[OF assms(1) p Irr(1)] unfolding univ_poly_zero by auto hence "eval p x = (eval (Irr K x) x) ⊗ (eval q x) ⊕ (eval r x)" using hom_simps(2-3) Irr(1) by simp hence "eval p x = eval r x" using hom_simps(1) q r unfolding IrrE(4)[OF assms] by simp moreover have "length r < length (Irr K x)" using dvd(2) Irr(2) by auto ultimately show "eval p x ∈ (λp. local.eval p x) ` { p ∈ carrier (K [X]). length p ≤ length (Irr K x) - Suc 0 }" using r by auto qed corollary (in domain) dimension_simple_extension: assumes "subfield K R" "x ∈ carrier R" "(algebraic over K) x" shows "dimension (degree (Irr K x)) K (simple_extension K x)" using dimension_independent[OF exp_base_independent[OF assms]] Span_exp_base[OF assms] by (simp add: exp_base_def) lemma (in ring) finite_dimension_imp_algebraic: assumes "subfield K R" "subring F R" and "finite_dimension K F" shows "x ∈ F ⟹ (algebraic over K) x" proof - let ?Us = "λn. map (λi. x [^] i) (rev [0..< Suc n])" assume x: "x ∈ F" then have in_carrier: "x ∈ carrier R" using subringE[OF assms(2)] by auto obtain n where n: "dimension n K F" using assms(3) by auto have set_Us: "set (?Us n) ⊆ F" using x subringE(3,6)[OF assms(2)] by (induct n) (auto) hence "set (?Us n) ⊆ carrier R" using subringE(1)[OF assms(2)] by auto moreover have "dependent K (?Us n)" using independent_length_le_dimension[OF assms(1) n _ set_Us] by auto ultimately obtain Ks where Ks: "length Ks = Suc n" "combine Ks (?Us n) = 𝟬" "set Ks ⊆ K" "set Ks ≠ { 𝟬 }" using dependent_imp_non_trivial_combine[OF assms(1), of "?Us n"] by auto have "set Ks ⊆ carrier R" using subring_props(1)[OF assms(1)] Ks(3) by auto hence "eval (normalize Ks) x = 𝟬" using combine_eq_eval[of Ks] eval_normalize[OF _ in_carrier] Ks(1-2) by (simp add: exp_base_def) moreover have "normalize Ks = [] ⟹ set Ks ⊆ { 𝟬 }" by (induct Ks) (auto, meson list.discI, metis all_not_in_conv list.discI list.sel(3) singletonD subset_singletonD) hence "normalize Ks ≠ []" using Ks(1,4) by (metis list.size(3) nat.distinct(1) set_empty subset_singleton_iff) moreover have "normalize Ks ∈ carrier (K[X])" using normalize_gives_polynomial[OF Ks(3)] unfolding univ_poly_def by auto ultimately show ?thesis using algebraicI by auto qed corollary (in domain) simple_extension_dim: assumes "subfield K R" "x ∈ carrier R" "(algebraic over K) x" shows "(dim over K) (simple_extension K x) = degree (Irr K x)" using dimI[OF assms(1) dimension_simple_extension[OF assms]] . corollary (in domain) finite_dimension_simple_extension: assumes "subfield K R" "x ∈ carrier R" shows "finite_dimension K (simple_extension K x) ⟷ (algebraic over K) x" using finite_dimensionI[OF dimension_simple_extension[OF assms]] finite_dimension_imp_algebraic[OF _ simple_extension_is_subring[OF subfieldE(1)]] simple_extension_mem[OF subfieldE(1)] assms by auto subsection ‹Finite Extensions› lemma (in ring) finite_extension_consistent: assumes "subring K R" shows "ring.finite_extension (R ⦇ carrier := K ⦈) = finite_extension" proof - have "⋀K' xs. ring.finite_extension (R ⦇ carrier := K ⦈) K' xs = finite_extension K' xs" proof - fix K' xs show "ring.finite_extension (R ⦇ carrier := K ⦈) K' xs = finite_extension K' xs" using ring.finite_extension.simps[OF subring_is_ring[OF assms]] simple_extension_consistent[OF assms] by (induct xs) (auto) qed thus ?thesis by blast qed lemma (in ring) mono_finite_extension: assumes "K ⊆ K'" shows "finite_extension K xs ⊆ finite_extension K' xs" using mono_simple_extension assms by (induct xs) (auto) lemma (in ring) finite_extension_carrier: assumes "set xs ⊆ carrier R" shows "finite_extension (carrier R) xs = carrier R" using assms simple_extension_carrier by (induct xs) (auto) lemma (in ring) finite_extension_in_carrier: assumes "K ⊆ carrier R" and "set xs ⊆ carrier R" shows "finite_extension K xs ⊆ carrier R" using assms simple_extension_in_carrier by (induct xs) (auto) lemma (in ring) finite_extension_subring_incl: assumes "subring K' R" and "K ⊆ K'" "set xs ⊆ K'" shows "finite_extension K xs ⊆ K'" using ring.finite_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3) unfolding finite_extension_consistent[OF assms(1)] by simp lemma (in ring) finite_extension_incl_aux: assumes "K ⊆ carrier R" and "x ∈ carrier R" "set xs ⊆ carrier R" shows "finite_extension K xs ⊆ finite_extension K (x # xs)" using simple_extension_incl[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp lemma (in ring) finite_extension_incl: assumes "K ⊆ carrier R" and "set xs ⊆ carrier R" shows "K ⊆ finite_extension K xs" using finite_extension_incl_aux[OF assms(1)] assms(2) by (induct xs) (auto) lemma (in ring) finite_extension_as_eval_img: assumes "K ⊆ carrier R" and "x ∈ carrier R" "set xs ⊆ carrier R" shows "finite_extension K (x # xs) = (λp. eval p x) ` carrier ((finite_extension K xs) [X])" using simple_extension_as_eval_img[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp lemma (in domain) finite_extension_is_subring: assumes "subring K R" "set xs ⊆ carrier R" shows "subring (finite_extension K xs) R" using assms simple_extension_is_subring by (induct xs) (auto) corollary (in domain) finite_extension_mem: assumes subring: "subring K R" shows "set xs ⊆ carrier R ⟹ set xs ⊆ finite_extension K xs" proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) from Cons(2) have a: "a ∈ carrier R" and xs: "set xs ⊆ carrier R" by auto show ?case proof fix x assume "x ∈ set (a # xs)" then consider "x = a" | "x ∈ set xs" by auto then show "x ∈ finite_extension K (a # xs)" proof cases case 1 with a have "x ∈ carrier R" by simp with xs have "x ∈ finite_extension K (x # xs)" using simple_extension_mem[OF finite_extension_is_subring[OF subring]] by simp with 1 show ?thesis by simp next case 2 with Cons have *: "x ∈ finite_extension K xs" by auto from a xs have "finite_extension K xs ⊆ finite_extension K (a # xs)" by (rule finite_extension_incl_aux[OF subringE(1)[OF subring]]) with * show ?thesis by auto qed qed qed corollary (in domain) finite_extension_minimal: assumes "subring K R" "set xs ⊆ carrier R" shows "finite_extension K xs = ⋂ { K'. subring K' R ∧ K ⊆ K' ∧ set xs ⊆ K' }" using finite_extension_is_subring[OF assms] finite_extension_mem[OF assms] finite_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] finite_extension_subring_incl by blast corollary (in domain) finite_extension_same_set: assumes "subring K R" "set xs ⊆ carrier R" "set xs = set ys" shows "finite_extension K xs = finite_extension K ys" using finite_extension_minimal[OF assms(1)] assms(2-3) by auto text ‹The reciprocal is also true, but it is more subtle.› proposition (in domain) finite_extension_is_subfield: assumes "subfield K R" "set xs ⊆ carrier R" shows "(⋀x. x ∈ set xs ⟹ (algebraic over K) x) ⟹ subfield (finite_extension K xs) R" using simple_extension_is_subfield algebraic_mono assms by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1)) proposition (in domain) finite_extension_finite_dimension: assumes "subfield K R" "set xs ⊆ carrier R" shows "(⋀x. x ∈ set xs ⟹ (algebraic over K) x) ⟹ finite_dimension K (finite_extension K xs)" and "finite_dimension K (finite_extension K xs) ⟹ (⋀x. x ∈ set xs ⟹ (algebraic over K) x)" proof - show "finite_dimension K (finite_extension K xs) ⟹ (⋀x. x ∈ set xs ⟹ (algebraic over K) x)" using finite_dimension_imp_algebraic[OF assms(1) finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]] finite_extension_mem[OF subfieldE(1)[OF assms(1)] assms(2)] by auto next show "(⋀x. x ∈ set xs ⟹ (algebraic over K) x) ⟹ finite_dimension K (finite_extension K xs)" using assms(2) proof (induct xs, simp add: finite_dimensionI[OF dimension_one[OF assms(1)]]) case (Cons x xs) hence "finite_dimension K (finite_extension K xs)" by auto moreover have "(algebraic over (finite_extension K xs)) x" using algebraic_mono[OF finite_extension_incl[OF subfieldE(3)[OF assms(1)]]] Cons(2-3) by auto moreover have "subfield (finite_extension K xs) R" using finite_extension_is_subfield[OF assms(1)] Cons(2-3) by auto ultimately show ?case using telescopic_base_dim(1)[OF assms(1) _ _ finite_dimensionI[OF dimension_simple_extension, of _ x]] Cons(3) by auto qed qed corollary (in domain) finite_extesion_mem_imp_algebraic: assumes "subfield K R" "set xs ⊆ carrier R" and "⋀x. x ∈ set xs ⟹ (algebraic over K) x" shows "y ∈ finite_extension K xs ⟹ (algebraic over K) y" using finite_dimension_imp_algebraic[OF assms(1) finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]] finite_extension_finite_dimension(1)[OF assms(1-2)] assms(3) by auto corollary (in domain) simple_extesion_mem_imp_algebraic: assumes "subfield K R" "x ∈ carrier R" "(algebraic over K) x" shows "y ∈ simple_extension K x ⟹ (algebraic over K) y" using finite_extesion_mem_imp_algebraic[OF assms(1), of "[ x ]"] assms(2-3) by auto subsection ‹Arithmetic of algebraic numbers› text ‹We show that the set of algebraic numbers of a field over a subfield K is a subfield itself.› lemma (in field) subfield_of_algebraics: assumes "subfield K R" shows "subfield { x ∈ carrier R. (algebraic over K) x } R" proof - let ?set_of_algebraics = "{ x ∈ carrier R. (algebraic over K) x }" show ?thesis proof (rule subfieldI'[OF subringI]) show "?set_of_algebraics ⊆ carrier R" and "𝟭 ∈ ?set_of_algebraics" using algebraic_self[OF _ subringE(3)] subfieldE(1)[OF assms(1)] by auto next fix x y assume x: "x ∈ ?set_of_algebraics" and y: "y ∈ ?set_of_algebraics" have "⊖ x ∈ simple_extension K x" using subringE(5)[OF simple_extension_is_subring[OF subfieldE(1)]] simple_extension_mem[OF subfieldE(1)] assms(1) x by auto thus "⊖ x ∈ ?set_of_algebraics" using simple_extesion_mem_imp_algebraic[OF assms] x by auto have "x ⊕ y ∈ finite_extension K [ x, y ]" and "x ⊗ y ∈ finite_extension K [ x, y ]" using subringE(6-7)[OF finite_extension_is_subring[OF subfieldE(1)[OF assms(1)]], of "[ x, y ]"] finite_extension_mem[OF subfieldE(1)[OF assms(1)], of "[ x, y ]"] x y by auto thus "x ⊕ y ∈ ?set_of_algebraics" and "x ⊗ y ∈ ?set_of_algebraics" using finite_extesion_mem_imp_algebraic[OF assms, of "[ x, y ]"] x y by auto next fix z assume z: "z ∈ ?set_of_algebraics - { 𝟬 }" have "inv z ∈ simple_extension K z" using subfield_m_inv(1)[of "simple_extension K z"] simple_extension_is_subfield[OF assms, of z] simple_extension_mem[OF subfieldE(1)] assms(1) z by auto thus "inv z ∈ ?set_of_algebraics" using simple_extesion_mem_imp_algebraic[OF assms] field_Units z by auto qed qed end