Theory Algebraic_Transitivity
section ‹Finite-dimensional extensions and transitivity of algebraicity›
theory Algebraic_Transitivity
imports Finite_Extension
begin
text ‹With the vector-space bridge of ‹Extension_Vector_Space› in place, the
Steinitz cardinality bound @{thm [source] Vector_Space.independent_le_span} yields the classical
chain
▪ a finite-dimensional extension is ∗‹algebraic› (every element satisfies a polynomial: its powers
cannot all be independent);
▪ ∗‹transitivity of algebraicity› --- if @{term a} is algebraic over @{term K} and @{term b} is
algebraic over the simple extension ‹K(a)›, then @{term b} is algebraic over @{term K}.
This is the last field-theoretic prerequisite of the quintic finish: it upgrades ``a radical is
algebraic over the immediate base'' to ``a radical is algebraic over the ground field'', so the
normal closure can be taken as the splitting field of a single ground-field polynomial.›
notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax
subsection ‹A finite-dimensional extension is algebraic›
text ‹If the extension @{term L} of @{term K} is spanned over @{term K} by a finite set @{term B},
then every element of @{term L} is algebraic over @{term K}. For @{term "y ∈ L"} the
@{term "card B + 1"} powers @{term "y ^ i"} (with ‹i ≤ card B›) all lie in the span of @{term B},
so by the Steinitz bound they are linearly dependent: some nontrivial @{term K}-combination
vanishes, i.e.\ a nonzero polynomial over @{term K} kills @{term y}.›
lemma (in subfield_tower) findim_imp_algebraic:
assumes finB: "finite B" and BL: "B ⊆ L" and span: "L ⊆ vs.span B" and y: "y ∈ L"
shows "algebraic_over K y"
proof (cases "inj_on (λi. y ^ i) {..card B}")
case False
then obtain i j where ij: "i ∈ {..card B}" "j ∈ {..card B}" "i ≠ j" "y ^ i = y ^ j"
by (auto simp: inj_on_def)
define p where "p = (monom 1 i - monom 1 j :: 'a poly)"
have p_over: "p ∈ poly_over K"
unfolding p_def by (intro base.poly_over_diff base.poly_over_monom base.one_closed)
have p_root: "poly p y = 0"
unfolding p_def using ij(4) by (simp add: poly_monom)
have p_nz: "p ≠ 0"
unfolding p_def by (meson eq_iff_diff_eq_0 monom_eq_iff' one_neq_zero ‹i ≠ j›)
show ?thesis unfolding algebraic_over_def using p_over p_nz p_root by blast
next
case True
define n where "n ≡ card B"
define P where "P ≡ (λi. y ^ i) ` {..n}"
have injn: "inj_on (λi. y ^ i) {..n}" using True by (simp add: n_def)
have yp_L: "⋀i. y ^ i ∈ L" using y by (intro ext.power_closed)
have PL: "P ⊆ L" using yp_L by (auto simp: P_def)
have finP: "finite P" by (simp add: P_def)
have Pspan: "P ⊆ vs.span B" using PL span by blast
have cardP: "card P = n + 1" using injn by (simp add: P_def card_image)
have "¬ vs.lin_indep P"
using BL Pspan cardP finB n_def vs.independent_le_span by fastforce
then obtain c where cPiE: "c ∈ P →⇩E K" and lc0: "vs.lincomb c P = 0"
and nz: "¬ (∀v∈P. c v = 0)"
using finP PL by (auto simp: vs.lin_indep_def)
have cK: "⋀v. v ∈ P ⟹ c v ∈ K" using cPiE by auto
have sum0: "(∑v∈P. c v * v) = 0" using vs_lincomb_eq_sum[OF finP PL cK] lc0 by simp
define d where "d ≡ (λi. c (y ^ i))"
have "(∑v∈P. c v * v) = (∑i≤n. c (y ^ i) * y ^ i)"
unfolding P_def by (subst sum.reindex[OF injn]) (simp add: o_def)
then have sumd0: "(∑i≤n. d i * y ^ i) = 0" using sum0 by (simp add: d_def)
define p where "p ≡ (∑i≤n. monom (d i) i :: 'a poly)"
have dK: "⋀i. i ≤ n ⟹ d i ∈ K" using cK by (auto simp: d_def P_def)
have p_over: "p ∈ poly_over K"
unfolding p_def
by (intro base.poly_over_sum base.poly_over_monom) (simp add: dK)
have p_root: "poly p y = 0"
unfolding p_def by (simp add: poly_sum poly_monom sumd0)
have p_nz: "p ≠ 0"
proof -
from nz obtain v where v: "v ∈ P" "c v ≠ 0" by blast
then obtain i where i: "i ≤ n" "v = y ^ i" by (auto simp: P_def)
have "coeff p i = d i"
unfolding p_def using i by (simp add: coeff_sum coeff_monom)
then show ?thesis
using d_def i(2) v(2) by fastforce
qed
show ?thesis unfolding algebraic_over_def using p_over p_nz p_root by blast
qed
text ‹Finite-dimensionality makes every target element algebraic over the base. This bridge belongs
with the finite-dimensional algebraicity theorem, so clients need not import primitive-element
constructions merely to use it.›
lemma (in finite_subfield_tower) finite_extension_algebraic:
assumes aL: "a ∈ L"
shows "algebraic_over K a"
proof -
obtain B where B: "vs.basis B" using finite_basis_exists by blast
have finB: "finite B" using B unfolding vs.basis_def by (rule conjunct1)
have BL: "B ⊆ L"
using B vs.basis_def by blast
have mod_span: "vs.mod.spanning B"
using vs.basis_spanning[OF B] by (simp add: vs.spanning_iff_mod_spanning[OF finB BL])
have spanL: "L ⊆ vs.span B"
using mod_span vs.mod.spanning_def by force
show ?thesis using findim_imp_algebraic[OF finB BL spanL aL] .
qed
subsection ‹Transitivity of algebraicity›
text ‹∗‹Transitivity.› If @{term a} is algebraic over @{term K} and @{term b} is algebraic over the
simple extension @{term "eval_img K a"}, then @{term b} is algebraic over @{term K}.
The two-step tower ‹K ⊆ K(a) ⊆ K(a)(b)› is spanned over @{term K} by the finite set of
products @{term "a ^ i * b ^ j"} (@{thm [source] tower_power_basis_span}); so
‹K(a)(b)› is a finite-dimensional extension of @{term K}, and @{term b}, being one of its
elements, is algebraic over @{term K} by @{thm [source] subfield_tower.findim_imp_algebraic}.›
theorem algebraic_over_transitive:
assumes K: "Subfield K"
and alg_a: "algebraic_over K a"
and alg_b: "algebraic_over (eval_img K a) b"
shows "algebraic_over K b"
proof -
define E where "E ≡ eval_img K a"
define L where "L ≡ eval_img E b"
have subE: "Subfield E" unfolding E_def by (rule Subfield.subfield_eval_img[OF K alg_a])
have algbE: "algebraic_over E b" using alg_b by (simp add: E_def)
have subL: "Subfield L" unfolding L_def by (rule Subfield.subfield_eval_img[OF subE algbE])
interpret KL: subfield_tower K L
using subfield_tower.intro[OF K subL]
by (metis E_def K L_def subE Subfield.eval_img_base subfield_tower_axioms.intro subsetI)
define da where "da ≡ ext_degree K a"
define db where "db ≡ ext_degree E b"
define B where "B ≡ (λ(j,i). a ^ i * b ^ j) ` ({..<db} × {..<da})"
have finB: "finite B" by (simp add: B_def)
have aE: "a ∈ E" unfolding E_def by (rule Subfield.eval_img_self[OF K])
obtain aL: "a ∈ L" and bL: "b ∈ L"
using L_def aE subE Subfield.eval_img_base Subfield.eval_img_self by blast
have prodL: "⋀i j. a ^ i * b ^ j ∈ L"
using aL bL by (intro KL.ext.mult_closed KL.ext.power_closed)
have BL: "B ⊆ L" using prodL by (auto simp: B_def)
have spanL: "L ⊆ KL.vs.span B"
proof
fix y assume "y ∈ L"
then
obtain c where cK: "⋀i j. i < da ⟹ j < db ⟹ c i j ∈ K"
and yeq: "y = (∑j < db. ∑i < da. c i j * (a ^ i * b ^ j))"
using tower_power_basis_span[OF K alg_a alg_b]
using E_def L_def da_def db_def by blast
then have yeq': "y = (∑ji∈{..<db} × {..<da}.
(λ(j,i). c i j) ji * (λ(j,i). a ^ i * b ^ j) ji)"
by (force simp: sum.cartesian_product intro: sum.cong)
then show "y ∈ KL.vs.span B"
unfolding yeq' B_def
by (intro KL.sum_scale_in_span) (auto simp: prodL cK)
qed
show "algebraic_over K b" using KL.findim_imp_algebraic[OF finB BL spanL bL] .
qed
subsection ‹Algebraicity along a radical/simple tower›
text ‹Every element of a simple algebraic extension @{term "eval_img K a"} is itself algebraic over
@{term K}: the extension is spanned over @{term K} by the finite power basis @{term "a ^ i"}
(@{thm [source] Subfield.power_basis_span}), so @{thm [source] subfield_tower.findim_imp_algebraic}
applies.›
theorem simple_ext_algebraic:
assumes K: "Subfield K" and alg_a: "algebraic_over K a" and y: "y ∈ eval_img K a"
shows "algebraic_over K y"
proof -
define L where "L ≡ eval_img K a"
define d where "d ≡ ext_degree K a"
have subL: "Subfield L" unfolding L_def by (rule Subfield.subfield_eval_img[OF K alg_a])
have KL: "K ⊆ L" unfolding L_def using Subfield.eval_img_base[OF K] by blast
interpret KL: subfield_tower K L by (rule subfield_tower.intro[OF K subL]) (unfold_locales, rule KL)
define B where "B = (λi. a ^ i) ` {..<d}"
have finB: "finite B" by (simp add: B_def)
have aL: "a ∈ L" unfolding L_def by (rule Subfield.eval_img_self[OF K])
have powL: "⋀i. a ^ i ∈ L" using aL by (intro KL.ext.power_closed)
have spanL: "L ⊆ KL.vs.span B"
proof
fix z assume "z ∈ L"
then obtain c where cK: "⋀i. i < d ⟹ c i ∈ K" and zc: "z = (∑i<d. c i * a ^ i)"
using Subfield.power_basis_span[OF K alg_a] by (auto simp: L_def d_def)
then show "z ∈ KL.vs.span B"
unfolding B_def
by (metis (full_types) KL.sum_scale_in_span finite_lessThan lessThan_iff powL)
qed
have BL: "B ⊆ L" using powL by (auto simp: B_def)
show ?thesis using KL.findim_imp_algebraic[OF finB BL spanL] y by (simp add: L_def)
qed
text ‹Two successive simple algebraic extensions are algebraic over the original base. This
interface is useful when proving closure of the algebraic elements under field operations: the
operation is first placed in the two-step generated field, and this lemma supplies its
algebraicity over the base.›
lemma algebraic_over_two_step:
fixes F :: "'a :: field set" and a b y :: 'a
assumes sfF: "Subfield F"
and alg_a: "algebraic_over F a"
and alg_b: "algebraic_over F b"
and y: "y ∈ eval_img (eval_img F a) b"
shows "algebraic_over F y"
proof -
have sfE: "Subfield (eval_img F a)"
by (rule Subfield.subfield_eval_img[OF sfF alg_a])
have FE: "F ⊆ eval_img F a"
using Subfield.eval_img_base[OF sfF] by blast
have alg_bE: "algebraic_over (eval_img F a) b"
by (rule algebraic_over_mono[OF alg_b FE])
have alg_yE: "algebraic_over (eval_img F a) y"
by (rule simple_ext_algebraic[OF sfE alg_bE y])
show ?thesis
by (rule algebraic_over_transitive[OF sfF alg_a alg_yE])
qed
definition algebraic_elements :: "'a :: field set ⇒ 'a set" where
"algebraic_elements F = {a. algebraic_over F a}"
text ‹Algebraic elements over a subfield form a subfield. Addition and multiplication are
handled through @{thm [source] algebraic_over_two_step}; negation and inversion already lie in
the corresponding simple extension.›
lemma subfield_algebraic_elements:
fixes F :: "'a :: field set"
assumes sfF: "Subfield F"
shows "Subfield (algebraic_elements F)"
proof
show "0 ∈ algebraic_elements F" "1 ∈ algebraic_elements F"
using Subfield.algebraic_over_self Subfield_def algebraic_elements_def sfF by blast+
next
fix a b
assume a: "a ∈ algebraic_elements F" and b: "b ∈ algebraic_elements F"
have alg_a: "algebraic_over F a"
using a by (simp add: algebraic_elements_def)
have sfE: "Subfield (eval_img F a)"
by (rule Subfield.subfield_eval_img[OF sfF alg_a])
have aE: "a ∈ eval_img F a"
by (rule Subfield.eval_img_self[OF sfF])
have negE: "-a ∈ eval_img F a"
using sfE aE by (rule Subfield.uminus_closed)
show "-a ∈ algebraic_elements F"
using simple_ext_algebraic[OF sfF alg_a negE]
by (simp add: algebraic_elements_def)
have invE: "inverse a ∈ eval_img F a"
using sfE aE by (rule Subfield.inverse_closed)
show "inverse a ∈ algebraic_elements F"
using simple_ext_algebraic[OF sfF alg_a invE]
by (simp add: algebraic_elements_def)
have aL: "a ∈ eval_img (eval_img F a) b"
using Subfield.eval_img_base[OF sfE aE] .
have bL: "b ∈ eval_img (eval_img F a) b"
by (rule Subfield.eval_img_self[OF sfE])
have sumL: "a + b ∈ eval_img (eval_img F a) b"
by (rule Subfield.eval_img_add[OF sfE aL bL])
have alg_b: "algebraic_over F b"
using b by (simp add: algebraic_elements_def)
show "a + b ∈ algebraic_elements F"
using algebraic_over_two_step[OF sfF alg_a alg_b sumL]
by (simp add: algebraic_elements_def)
have multL: "a * b ∈ eval_img (eval_img F a) b"
by (rule Subfield.eval_img_mult[OF sfE aL bL])
show "a * b ∈ algebraic_elements F"
using algebraic_over_two_step[OF sfF alg_a alg_b multL]
by (simp add: algebraic_elements_def)
qed
text ‹Generation by algebraic elements preserves algebraicity. The generated field is
contained in the subfield of all elements algebraic over the base, so no representation of
generated elements or basis choice is exposed to clients.›
lemma generated_algebraic:
fixes F A :: "'a :: field set"
assumes sfF: "Subfield F"
and algA: "⋀a. a ∈ A ⟹ algebraic_over F a"
and x: "x ∈ generate_field (F ∪ A)"
shows "algebraic_over F x"
proof -
have FA: "F ∪ A ⊆ algebraic_elements F"
by (simp add: Subfield.algebraic_over_self algA algebraic_elements_def sfF subsetI)
have gen: "generate_field (F ∪ A) ⊆ algebraic_elements F"
by (rule generate_field_least[OF subfield_algebraic_elements[OF sfF] FA])
show ?thesis
using x algebraic_elements_def gen by blast
qed
end