Theory Finite_Extensions
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