Theory Finite_Extension_Tower
section ‹The tower law for finite field extensions›
theory Finite_Extension_Tower
imports Finite_Extension
begin
text ‹
A pair of finite field extensions ‹K ⊆ L ⊆ M› carries three native vector-space
interpretations. This theory proves that a basis of ‹L› over ‹K› and a basis of ‹M›
over ‹L› multiply to a basis of ‹M› over ‹K›. The resulting degree formula is
independent of the chosen bases and is the reusable tower-law interface for later Galois work.
›
locale finite_subfield_tower_chain =
KL: finite_subfield_tower K L + LM: finite_subfield_tower L M
for K L M :: "'a :: field set"
begin
lemma subfield_tower_KM: "subfield_tower K M"
proof (rule subfield_tower.intro)
show "Subfield K" by (rule KL.base.Subfield_axioms)
show "Subfield M" by (rule LM.ext.Subfield_axioms)
show "subfield_tower_axioms K M"
by unfold_locales (rule subset_trans[OF KL.base_subset LM.base_subset])
qed
sublocale KM: subfield_tower K M
by (rule subfield_tower_KM)
definition product_map :: "'a × 'a ⇒ 'a"
where "product_map z = snd z * fst z"
definition product_basis :: "'a set ⇒ 'a set ⇒ 'a set"
where "product_basis B C = {b * c | b c. b ∈ B ∧ c ∈ C}"
lemma product_basis_image:
"product_basis B C = product_map ` (C × B)"
proof -
have "product_basis B C = {b * c | b c. b ∈ B ∧ c ∈ C}"
by (simp add: product_basis_def)
also have "... = product_map ` (C × B)"
proof (rule equalityI)
show "{b * c | b c. b ∈ B ∧ c ∈ C} ⊆ product_map ` (C × B)"
proof
fix x
assume x: "x ∈ {b * c | b c. b ∈ B ∧ c ∈ C}"
then obtain b c where bB: "b ∈ B" and cC: "c ∈ C" and x: "x = b * c"
by blast
have pair: "(c, b) ∈ C × B" using cC bB by simp
have img: "product_map (c, b) ∈ product_map ` (C × B)"
by (rule imageI[OF pair])
have bc: "b * c ∈ product_map ` (C × B)"
using img by (simp add: product_map_def mult.commute)
show "x ∈ product_map ` (C × B)" using x bc by simp
qed
next
show "product_map ` (C × B) ⊆ {b * c | b c. b ∈ B ∧ c ∈ C}"
proof
fix x
assume x: "x ∈ product_map ` (C × B)"
then obtain z where z: "z ∈ C × B" and x: "x = product_map z" by blast
obtain c b where z: "z = (c, b)" and cC: "c ∈ C" and bB: "b ∈ B"
using z by (cases z) auto
show "x ∈ {b * c | b c. b ∈ B ∧ c ∈ C}"
using x z bB cC by (auto simp add: product_map_def mult.commute)
qed
qed
finally show ?thesis .
qed
lemma KL_basis_subset:
assumes "KL.vs.basis B"
shows "B ⊆ L"
using assms by (simp add: KL.vs.basis_def)
lemma LM_basis_subset:
assumes "LM.vs.basis C"
shows "C ⊆ M"
using assms by (simp add: LM.vs.basis_def)
lemma KM_product_map_inj:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "inj_on product_map (C × B)"
proof (rule inj_onI)
fix x y
assume x: "x ∈ C × B" and y: "y ∈ C × B"
and eq: "product_map x = product_map y"
obtain c b where x': "x = (c, b)" and cC: "c ∈ C" and bB: "b ∈ B"
using x by (cases x) auto
obtain c' b' where y': "y = (c', b')" and c'C: "c' ∈ C" and b'B: "b' ∈ B"
using y by (cases y) auto
have BL: "B ⊆ L" by (rule KL_basis_subset[OF B])
have bL: "b ∈ L" and b'L: "b' ∈ L" using BL bB b'B by blast+
have b0: "b ≠ 0"
proof
assume b0: "b = 0"
have bnot: "b ∉ KL.vs.span (B - {b})"
using KL.vs.lin_indep_not_in_span[OF KL.vs.basis_lin_indep[OF B] bB] .
have "b ∈ KL.vs.span (B - {b})" using b0 by (simp add: KL.vs.span_zero)
then show False using bnot by contradiction
qed
have c0: "c ≠ 0"
proof
assume c0: "c = 0"
have cnot: "c ∉ LM.vs.span (C - {c})"
using LM.vs.lin_indep_not_in_span[OF LM.vs.basis_lin_indep[OF C] cC] .
have "c ∈ LM.vs.span (C - {c})" using c0 by (simp add: LM.vs.span_zero)
then show False using cnot by contradiction
qed
have eq': "b * c = b' * c'"
using eq x' y' by (simp add: product_map_def)
have c_eq: "c = c'"
proof (rule ccontr)
assume cne: "c ≠ c'"
have ibL: "inverse b ∈ L"
using bL by (rule Subfield.inverse_closed[OF KL.ext.Subfield_axioms])
have rL: "inverse b * b' ∈ L"
using ibL b'L by (rule Subfield.mult_closed[OF KL.ext.Subfield_axioms])
have eqc: "c = (inverse b * b') * c'"
proof -
have "c = inverse b * (b * c)" using b0 by simp
also have "... = inverse b * (b' * c')" using eq' by simp
also have "... = (inverse b * b') * c'" by (simp add: mult.assoc)
finally show ?thesis .
qed
have c'other: "c' ∈ C - {c}" using c'C cne by blast
have CsubM: "C - {c} ⊆ M"
using LM_basis_subset[OF C] by blast
have c'span: "c' ∈ LM.vs.span (C - {c})"
by (rule LM.vs.span_incl[OF CsubM c'other])
have rspan: "(inverse b * b') * c' ∈ LM.vs.span (C - {c})"
by (rule LM.vs.span_scale[OF CsubM rL c'span])
have cspan: "c ∈ LM.vs.span (C - {c})" using eqc rspan by simp
have cnot: "c ∉ LM.vs.span (C - {c})"
using LM.vs.lin_indep_not_in_span[OF LM.vs.basis_lin_indep[OF C] cC] .
then show False using cspan by contradiction
qed
have b_eq: "b = b'"
proof -
have eqc': "b * c = b' * c" using eq' c_eq by simp
have "b = (b * c) * inverse c" using c0 by (simp add: mult.assoc)
also have "... = (b' * c) * inverse c" using eqc' by simp
also have "... = b'" using c0 by (simp add: mult.assoc)
finally show ?thesis .
qed
show "x = y" using x' y' b_eq c_eq by simp
qed
lemma KM_product_basis_card:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "card (product_basis B C) = card B * card C"
unfolding product_basis_image
by (simp add: card_image[OF KM_product_map_inj[OF B C]] card_cartesian_product
mult.commute)
lemma KM_product_basis_subset:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "product_basis B C ⊆ M"
proof
fix x assume "x ∈ product_basis B C"
then obtain z where zP: "z ∈ C × B" and xz: "x = product_map z"
unfolding product_basis_image by blast
obtain c b where z: "z = (c, b)" and cC: "c ∈ C" and bB: "b ∈ B"
using zP by (cases z) auto
have x: "x = b * c" using xz z by (simp add: product_map_def)
have cM: "c ∈ M" using LM_basis_subset[OF C] cC by blast
have bM: "b ∈ M"
using KL_basis_subset[OF B] bB LM.ext.mult_closed LM.base_subset by blast
show "x ∈ M" using x bM cM by (auto intro: LM.ext.mult_closed)
qed
lemma KM_product_basis_spanning:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "M ⊆ KM.vs.span (product_basis B C)"
proof
fix x assume xM: "x ∈ M"
have Cfin: "finite C" and CM: "C ⊆ M"
using C LM_basis_subset[OF C] by (auto simp: LM.vs.basis_def)
have Bfin: "finite B" and BL: "B ⊆ L"
using B KL_basis_subset[OF B] by (auto simp: KL.vs.basis_def)
obtain d where dC: "d ∈ C →⇩E L" and xd: "x = LM.vs.lincomb d C"
using LM.vs.basis_spanning[OF C] xM by (auto simp: LM.vs.spanning_def)
define inner_sum ::
"'a set ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ 'a"
where "inner_sum B e c = (∑b ∈ B. e c b * (b * c))" for B e c
define coefficient_sum ::
"'a set ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ 'a"
where "coefficient_sum B f c = (∑b ∈ B. f c b * b)" for B f c
define outer_sum :: "'a set ⇒ ('a ⇒ 'a) ⇒ 'a"
where "outer_sum C h = (∑c ∈ C. h c)" for C h
define scale_function :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a)"
where "scale_function d c = d c * c" for d c
define product_sum :: "('a × 'a) set ⇒ ('a × 'a ⇒ 'a) ⇒ 'a"
where "product_sum S p = (∑z ∈ S. p z)" for S p
define product_term ::
"('a ⇒ 'a ⇒ 'a) ⇒ 'a × 'a ⇒ 'a"
where "product_term e z = e (fst z) (snd z) * product_map z" for e z
define coeff :: "'a ⇒ 'a ⇒ 'a"
where "coeff = (λc. SOME f. f ∈ B →⇩E K ∧ d c = KL.vs.lincomb f B)"
define h :: "'a ⇒ 'a"
where "h = inner_sum B coeff"
define p :: "'a × 'a ⇒ 'a"
where "p = product_term coeff"
have coeff_spec_point:
"coeff c ∈ B →⇩E K ∧
d c = KL.vs.lincomb (coeff c) B"
if cC: "c ∈ C" for c
proof -
have dcL: "d c ∈ L" using dC cC by (auto simp: PiE_def)
have spans:
"∀v ∈ L. ∃f ∈ B →⇩E K.
v = KL.vs.lincomb f B"
using KL.vs.basis_spanning[OF B]
by (simp add: KL.vs.spanning_def)
have some_exists:
"∃f. f ∈ B →⇩E K ∧ d c = KL.vs.lincomb f B"
using spans dcL by blast
show ?thesis
unfolding coeff_def
using some_exists by (rule someI_ex)
qed
have coeff_spec:
"∀c ∈ C. coeff c ∈ B →⇩E K ∧
d c = KL.vs.lincomb (coeff c) B"
using coeff_spec_point by blast
have d_expands: "d c = coefficient_sum B coeff c"
if cC: "c ∈ C" for c
proof -
have coeff_c: "coeff c ∈ B →⇩E K"
using coeff_spec cC by blast
have coeffK: "⋀b. b ∈ B ⟹ coeff c b ∈ K"
using coeff_c by blast
have lc:
"KL.vs.lincomb (coeff c) B =
(∑b ∈ B. coeff c b * b)"
using KL.vs_lincomb_eq_sum[OF Bfin BL coeffK] .
show ?thesis
using coeff_spec cC lc by (simp add: coefficient_sum_def)
qed
have xsum: "x = (∑c ∈ C. d c * c)"
using xd LM.vs_lincomb_eq_sum[OF Cfin CM] dC
by (auto simp: PiE_def)
have xdouble: "x = outer_sum C h"
proof -
have x_outer: "x = outer_sum C (scale_function d)"
using xsum by (simp add: outer_sum_def scale_function_def)
have h_outer: "outer_sum C (scale_function d) = outer_sum C h"
unfolding outer_sum_def
by (rule sum.cong[OF refl])
(simp add: h_def inner_sum_def coefficient_sum_def
sum_distrib_right d_expands scale_function_def mult.assoc)
show ?thesis by (rule trans[OF x_outer h_outer])
qed
have pair_span:
"(∑z ∈ C × B. p z)
∈ KM.vs.span (product_basis B C)"
proof -
have pair_span':
"(∑z ∈ C × B.
coeff (fst z) (snd z) * product_map z)
∈ KM.vs.span (image product_map (C × B))"
proof (rule KM.sum_scale_in_span)
show "finite (C × B)" by (simp add: Bfin Cfin)
show "product_map z ∈ M" if z: "z ∈ C × B" for z
proof -
have zP: "product_map z ∈ product_basis B C"
using z by (simp add: product_basis_image)
show ?thesis
using KM_product_basis_subset[OF B C] zP by blast
qed
show "coeff (fst z) (snd z) ∈ K"
if z: "z ∈ C × B" for z
proof -
have cC: "fst z ∈ C" using z by (cases z) auto
have bB: "snd z ∈ B" using z by (cases z) auto
have coeff_c: "coeff (fst z) ∈ B →⇩E K"
using coeff_spec cC by blast
show ?thesis using coeff_c bB by (auto simp: PiE_def)
qed
qed
show ?thesis
using pair_span' by (simp add: p_def product_term_def product_basis_image)
qed
have pair_eq: "outer_sum C h = product_sum (C × B) p"
unfolding outer_sum_def product_sum_def h_def p_def inner_sum_def product_term_def
by (simp add: sum.cartesian_product product_map_def case_prod_unfold)
show "x ∈ KM.vs.span (product_basis B C)"
using xdouble pair_eq pair_span by (simp add: product_sum_def)
qed
lemma KM_product_basis_condition:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "∀f ∈ product_basis B C →⇩E K.
KM.vs.lincomb f (product_basis B C) = 0 ⟶
(∀v ∈ product_basis B C. f v = 0)"
proof (rule ballI, rule impI)
fix f assume fP: "f ∈ product_basis B C →⇩E K"
and fzero: "KM.vs.lincomb f (product_basis B C) = 0"
define outer_sum :: "'a set ⇒ ('a ⇒ 'a) ⇒ 'a"
where "outer_sum C h = (∑c ∈ C. h c)" for C h
define scale_function :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a)"
where "scale_function d c = d c * c" for d c
define pair_scale ::
"('a ⇒ 'a) ⇒ 'a × 'a ⇒ 'a"
where "pair_scale f z = f (product_map z) * product_map z" for f z
define fiber_function ::
"('a ⇒ 'a) ⇒ 'a ⇒ 'a ⇒ 'a"
where "fiber_function f c b = f (b * c)" for f c b
define fiber_sum ::
"('a ⇒ 'a) ⇒ 'a set ⇒ 'a ⇒ 'a"
where "fiber_sum f B c = (∑b ∈ B. f (b * c) * b)" for f B c
define product_sum :: "('a × 'a) set ⇒ ('a × 'a ⇒ 'a) ⇒ 'a"
where "product_sum S p = (∑z ∈ S. p z)" for S p
have Bfin: "finite B" and BL: "B ⊆ L"
using B KL_basis_subset[OF B] by (auto simp: KL.vs.basis_def)
have Cfin: "finite C" and CM: "C ⊆ M"
using C LM_basis_subset[OF C] by (auto simp: LM.vs.basis_def)
have Pfin: "finite (product_basis B C)" by (simp add: product_basis_image Bfin Cfin)
have PM: "product_basis B C ⊆ M" by (rule KM_product_basis_subset[OF B C])
have fK: "f v ∈ K" if v: "v ∈ product_basis B C" for v
using fP v by blast
have sumzero:
"outer_sum (product_basis B C) (scale_function f) = 0"
proof -
have fK': "⋀v. v ∈ product_basis B C ⟹ f v ∈ K"
using fP by blast
have lincomb_sum:
"KM.vs.lincomb f (product_basis B C) =
outer_sum (product_basis B C) (scale_function f)"
using KM.vs_lincomb_eq_sum[OF Pfin PM fK']
by (simp add: outer_sum_def scale_function_def)
show ?thesis using lincomb_sum fzero by simp
qed
have inj: "inj_on product_map (C × B)"
by (rule KM_product_map_inj[OF B C])
have pairzero: "product_sum (C × B) (pair_scale f) = 0"
proof -
have pair_sum_eq:
"product_sum (C × B) (pair_scale f) =
outer_sum (product_basis B C) (scale_function f)"
unfolding outer_sum_def scale_function_def product_sum_def pair_scale_def
product_basis_image
by (subst sum.reindex[OF inj]) (simp add: o_def)
show ?thesis using pair_sum_eq sumzero by simp
qed
define e :: "'a ⇒ 'a"
where "e = fiber_sum f B"
have subL: "Subfield L" by (rule KL.ext.Subfield_axioms)
have eL: "e c ∈ L" if cC: "c ∈ C" for c
unfolding e_def fiber_sum_def
proof (rule Subfield.sum_closed[OF subL])
fix b assume bB: "b ∈ B"
have bL: "b ∈ L" using BL bB by blast
have bcP: "b * c ∈ product_basis B C"
proof -
have pair: "(c, b) ∈ C × B" by (simp add: cC bB)
have img: "product_map (c, b) ∈ image product_map (C × B)"
by (rule imageI[OF pair])
have eq: "product_map (c, b) = b * c"
by (simp add: product_map_def)
show ?thesis unfolding product_basis_image using img eq by simp
qed
then have "f (b * c) ∈ K" by (rule fK)
then have fL: "f (b * c) ∈ L"
using KL.base_subset by blast
then show "f (b * c) * b ∈ L"
using bL by (rule Subfield.mult_closed[OF subL])
qed
have nested:
"(∑z ∈ C × B. pair_scale f z) =
(∑c ∈ C. ∑b ∈ B. pair_scale f (c, b))"
by (simp add: sum.cartesian_product)
have pair_terms:
"(∑c ∈ C. ∑b ∈ B. pair_scale f (c, b)) =
(∑c ∈ C. ∑b ∈ B. (f (b * c) * b) * c)"
by (simp add: pair_scale_def product_map_def mult.assoc)
have distribute:
"(∑c ∈ C. ∑b ∈ B. (f (b * c) * b) * c) =
(∑c ∈ C. (∑b ∈ B. f (b * c) * b) * c)"
by (simp add: sum_distrib_right)
have pair_outer_unfolded:
"(∑z ∈ C × B. pair_scale f z) =
(∑c ∈ C. (∑b ∈ B. f (b * c) * b) * c)"
by (rule trans[OF nested], rule trans[OF pair_terms distribute])
have pair_outer:
"product_sum (C × B) (pair_scale f) =
outer_sum C (scale_function e)"
using pair_outer_unfolded
by (simp only: product_sum_def outer_sum_def scale_function_def
e_def fiber_sum_def)
have esumzero: "outer_sum C (scale_function e) = 0"
using pairzero pair_outer by simp
have eC: "restrict e C ∈ C →⇩E L"
using eL by (auto simp: PiE_def)
have eL': "⋀v. v ∈ C ⟹ restrict e C v ∈ L"
using eL by (auto simp: PiE_def)
have elincomb: "LM.vs.lincomb (restrict e C) C = 0"
proof -
have lincomb_sum:
"LM.vs.lincomb (restrict e C) C =
outer_sum C (scale_function e)"
using LM.vs_lincomb_eq_sum[where c="restrict e C", OF Cfin CM eL']
by (simp add: outer_sum_def scale_function_def restrict_apply')
show ?thesis using lincomb_sum esumzero by simp
qed
have fzero_pair: "f (b * c) = 0" if bB: "b ∈ B" and cC: "c ∈ C" for b c
proof -
have e_restrict_zero: "restrict e C c = 0"
proof -
have ecoeffs: "LM.vs.mod.coeffs_on (restrict e C) C"
using eC by (auto intro!: LM.vs.mod.coeffs_onI)
have eind: "LM.vs.mod.lin_indep C"
by (rule iffD1[OF LM.vs.lin_indep_iff_mod_lin_indep[OF Cfin CM]
LM.vs.basis_lin_indep[OF C]])
have ezero': "LM.vs.mod.lincomb (restrict e C) C = 0"
by (rule elincomb)
show "restrict e C c = 0"
by (rule LM.vs.mod.lin_indepD[OF eind Cfin subset_refl ecoeffs ezero' cC])
qed
have ezero_c: "e c = 0"
using e_restrict_zero by (simp add: restrict_apply' cC)
define g :: "'a ⇒ 'a" where "g = fiber_function f c"
have gK: "g u ∈ K" if uB: "u ∈ B" for u
proof -
have pair: "(c, u) ∈ C × B" by (simp add: cC uB)
have img: "product_map (c, u) ∈ image product_map (C × B)"
by (rule imageI[OF pair])
have eq: "product_map (c, u) = u * c"
by (simp add: product_map_def)
have ucP: "u * c ∈ product_basis B C"
unfolding product_basis_image using img eq by simp
show "g u ∈ K"
unfolding g_def fiber_function_def
by (rule fK[OF ucP])
qed
have gK': "⋀u. u ∈ B ⟹ restrict g B u ∈ K"
using gK by (auto simp: restrict_apply')
have glincomb: "KL.vs.lincomb (restrict g B) B = 0"
proof -
have lincomb_outer:
"KL.vs.lincomb (restrict g B) B =
outer_sum B (scale_function g)"
using KL.vs_lincomb_eq_sum[where c="restrict g B", OF Bfin BL gK']
by (simp add: outer_sum_def scale_function_def restrict_apply')
have outer_e: "outer_sum B (scale_function g) = e c"
unfolding outer_sum_def scale_function_def g_def
e_def fiber_sum_def fiber_function_def
by simp
show "KL.vs.lincomb (restrict g B) B = 0"
using lincomb_outer outer_e ezero_c by simp
qed
have g_ind: "KL.vs.mod.lin_indep B"
by (rule iffD1[OF KL.vs.lin_indep_iff_mod_lin_indep[OF Bfin BL]
KL.vs.basis_lin_indep[OF B]])
have g_coeffs: "KL.vs.mod.coeffs_on (restrict g B) B"
using gK' by (auto intro!: KL.vs.mod.coeffs_onI)
have "restrict g B b = 0"
by (rule KL.vs.mod.lin_indepD[OF g_ind Bfin subset_refl g_coeffs glincomb bB])
then show ?thesis by (simp add: restrict_apply' bB g_def fiber_function_def)
qed
show "∀v∈product_basis B C. f v = 0"
proof
fix v assume vP: "v ∈ product_basis B C"
then obtain b c where bB: "b ∈ B" and cC: "c ∈ C" and v_eq: "v = b * c"
unfolding product_basis_def by blast
show "f v = 0" using fzero_pair[OF bB cC] v_eq by simp
qed
qed
lemma KM_product_basis_independent:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "KM.vs.lin_indep (product_basis B C)"
proof -
have Bfin: "finite B" and BL: "B ⊆ L"
using B KL_basis_subset[OF B] by (auto simp: KL.vs.basis_def)
have Cfin: "finite C" and CM: "C ⊆ M"
using C LM_basis_subset[OF C] by (auto simp: LM.vs.basis_def)
have Pfin: "finite (product_basis B C)" by (simp add: product_basis_image Bfin Cfin)
have PM: "product_basis B C ⊆ M" by (rule KM_product_basis_subset[OF B C])
show "KM.vs.lin_indep (product_basis B C)"
unfolding KM.vs.lin_indep_def
using Pfin PM KM_product_basis_condition[OF B C] by blast
qed
theorem KM_product_basis:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "KM.vs.basis (product_basis B C)"
proof (rule KM.vs.basisI)
have Bfin: "finite B" using B by (auto simp: KL.vs.basis_def)
have Cfin: "finite C" using C by (auto simp: LM.vs.basis_def)
have Pfin: "finite (product_basis B C)"
by (simp add: product_basis_image Bfin Cfin)
have PM: "product_basis B C ⊆ M"
by (rule KM_product_basis_subset[OF B C])
have mod_spanning: "KM.vs.mod.spanning (product_basis B C)"
proof (rule KM.vs.mod.spanningI[OF PM])
fix v assume vM: "v ∈ M"
show "v ∈ KM.vs.mod.span (product_basis B C)"
using KM_product_basis_spanning[OF B C] vM by blast
qed
show "KM.vs.spanning (product_basis B C)"
using KM.vs.spanning_iff_mod_spanning[OF Pfin PM] mod_spanning by blast
show "KM.vs.lin_indep (product_basis B C)"
by (rule KM_product_basis_independent[OF B C])
qed
sublocale KMF: finite_subfield_tower K M
proof -
obtain B where B: "KL.vs.basis B" using KL.finite_basis_exists by blast
obtain C where C: "LM.vs.basis C" using LM.finite_basis_exists by blast
have P: "KM.vs.basis (product_basis B C)" by (rule KM_product_basis[OF B C])
show "finite_subfield_tower K M"
proof (rule finite_subfield_tower.intro)
show "subfield_tower K M" by (rule subfield_tower_KM)
show "finite_subfield_tower_axioms K M"
by (rule finite_subfield_tower_axioms.intro) (rule exI[of _ "product_basis B C"], rule P)
qed
qed
theorem extension_degree_tower_law:
assumes B: "KL.vs.basis B" and C: "LM.vs.basis C"
shows "KMF.extension_degree = KL.extension_degree * LM.extension_degree"
proof -
have P: "KM.vs.basis (product_basis B C)" by (rule KM_product_basis[OF B C])
have cardP: "card (product_basis B C) = card B * card C"
by (rule KM_product_basis_card[OF B C])
have cardB: "card B = KL.extension_degree"
using KL.extension_degree_eq_card_basis[OF B] by simp
have cardC: "card C = LM.extension_degree"
using LM.extension_degree_eq_card_basis[OF C] by simp
have cardP': "card (product_basis B C) = KL.extension_degree * LM.extension_degree"
using cardP cardB cardC by simp
show ?thesis
using KMF.extension_degree_eq_card_basis[OF P] cardP' by simp
qed
theorem extension_degree_tower_law_exists:
"KMF.extension_degree = KL.extension_degree * LM.extension_degree"
proof -
obtain B where B: "KL.vs.basis B" using KL.finite_basis_exists by blast
obtain C where C: "LM.vs.basis C" using LM.finite_basis_exists by blast
show ?thesis by (rule extension_degree_tower_law[OF B C])
qed
end
end