Theory Normal_Closure
section ‹Stability of root-generated intermediate fields›
theory Normal_Closure
imports Galois_Restriction Radical_Extension
begin
text ‹The @{const solvable_tower} predicate of ‹Galois_Solvable_Tower›
requires each intermediate field to be
∗‹stable› under the ambient Galois group. The reusable fact that supplies this is: a field
@{term "generate_field (F ∪ X)"} generated over @{term F} by the ∗‹full› root set @{term X} of an
@{term F}-polynomial is stable under every @{term F}-automorphism of any ambient field @{term K}
containing it.›
subsection ‹An automorphism fixes the base field setwise›
text ‹An @{term F}-automorphism of @{term K} maps @{term F} onto @{term F}: it fixes @{term F}
pointwise, and every element of @{term F} is the image of itself.›
lemma field_auto_image_base:
assumes s: "σ ∈ field_auto K F"
shows "σ ` F = F"
proof -
have base_fix: "∀x. x ∈ F ⟶ σ x = x"
using s by (auto simp: field_auto_mem_iff)
have image_subset: "σ ` F ⊆ F"
proof (rule subsetI)
fix y
assume y_image: "y ∈ σ ` F"
obtain x where xF: "x ∈ F" and y_eq: "σ x = y"
using y_image by blast
have sigma_fix: "σ x = x" using base_fix xF by blast
then show "y ∈ F" using xF y_eq by simp
qed
have subset_image: "F ⊆ σ ` F"
proof (rule subsetI)
fix x
assume xF: "x ∈ F"
have "σ x ∈ σ ` F" using xF by (rule imageI)
then show "x ∈ σ ` F" using base_fix xF by simp
qed
show ?thesis by (rule subset_antisym[OF image_subset subset_image])
qed
subsection ‹Root-generated fields are stable›
text ‹∗‹The stability lemma.› Let @{term X} be the full set of roots (in the ambient @{term K}) of an
@{term F}-polynomial @{term Phi}, and let @{term "E = generate_field (F ∪ X)"} be the field it
generates over @{term F}. Then @{term E} is stable under every @{term F}-automorphism of @{term K}.›
theorem root_generated_stable:
fixes K F :: "complex set" and Phi :: "complex poly"
assumes K: "Subfield K" and sfF: "Subfield F" and FK: "F ⊆ K"
and Phi: "Phi ∈ poly_over F"
and Xdef: "X = {r. poly Phi r = 0}" and XK: "X ⊆ K" and finX: "finite X"
and s: "σ ∈ field_auto K F"
shows "σ ` generate_field (F ∪ X) = generate_field (F ∪ X)"
proof -
have hom: "field_hom_on K σ" using K s by (rule field_auto_imp_field_hom_on)
have sX: "σ ` X = X"
using field_auto_bij_on_root[OF K sfF FK Phi Xdef XK finX s] by (rule bij_betw_imp_surj_on)
have sF: "σ ` F = F" by (rule field_auto_image_base[OF s])
have sUn: "σ ` (F ∪ X) = F ∪ X"
using sF sX by (simp add: image_Un)
have "F ∪ X ⊆ K" using FK XK by simp
then show ?thesis
using field_hom_on.image_generate_field_eq[OF hom] sUn by presburger
qed
subsection ‹A field homomorphism carries radical steps to radical steps›
text ‹A conjugate of a radical is a radical›
lemma radical_step_image:
fixes f :: "complex ⇒ complex"
assumes hom: "field_hom_on K f" and sfF: "Subfield F" and FK: "F ⊆ K"
and fixF: "⋀x. x ∈ F ⟹ f x = x"
and step: "radical_step F G" and GK: "G ⊆ K"
shows "radical_step F (f ` G)"
proof -
obtain a n where n: "n > 0" and anF: "a ^ n ∈ F" and Gdef: "G = generate_field (F ∪ {a})"
using step by (auto simp: radical_step_def)
have aK: "a ∈ K" using Gdef GK subset_generate_field by fastforce
have fanF: "(f a) ^ n ∈ F"
using aK field_hom_on.hom_power[OF hom] anF fixF by fastforce
have "f ` G = generate_field (F ∪ {f a})"
using fixF FK aK field_hom_on.image_generate_field_eq[OF hom] by (simp add: Gdef image_Un)
then show ?thesis unfolding radical_step_def using n fanF by blast
qed
text ‹∗‹General form› (no fixing hypothesis): a field homomorphism carries a radical step
‹F ↝ G› to the radical step ‹f ` F ↝ f ` G›. This is the form that iterates
along a tower, where after the first step the base is no longer fixed pointwise.›
lemma radical_step_image_gen:
fixes f :: "complex ⇒ complex"
assumes hom: "field_hom_on K f" and FK: "F ⊆ K"
and step: "radical_step F G" and GK: "G ⊆ K"
shows "radical_step (f ` F) (f ` G)"
proof -
obtain a n where n: "n > 0" and anF: "a ^ n ∈ F" and Gdef: "G = generate_field (F ∪ {a})"
using step by (auto simp: radical_step_def)
have aK: "a ∈ K" using Gdef GK subset_generate_field by fastforce
have fanF: "(f a) ^ n ∈ f ` F"
using aK field_hom_on.hom_power[OF hom] by (metis anF imageI)
have "f ` G = f ` generate_field (F ∪ {a})" by (simp add: Gdef)
also have "… = generate_field (f ` F ∪ {f a})"
using field_hom_on.image_generate_field_eq[OF hom] FK aK by (simp add: image_Un)
finally show ?thesis unfolding radical_step_def using n fanF by blast
qed
subsection ‹A field homomorphism carries radical towers to radical towers›
text ‹Each field of a radical tower is a subfield (each is generated over the previous), and the tower
is increasing. In particular every field is contained in any subfield @{term K} that contains the
∗‹top› field --- but for the tower-image induction we only need that consecutive fields nest, which we
package as: every field of the tower is a subfield of the last. We instead carry an explicit ambient
@{term K} with @{term "tower_top F Fs ⊆ K"}.›
lemma radical_step_field:
assumes "radical_step F G" shows "Subfield G ∧ F ⊆ G"
using assms radical_step_def by auto
lemma radical_tower_subset_ambient:
"Subfield K ⟹ Subfield F ⟹ radical_tower F Fs ⟹ tower_top F Fs ⊆ K
⟹ F ⊆ K ∧ (∀G ∈ set Fs. G ⊆ K)"
proof (induction Fs arbitrary: F)
case Nil
then show ?case by simp
next
case (Cons G Gs)
have "radical_step F G" and tower': "radical_tower G Gs" using Cons.prems(3) by auto
then have sfG: "Subfield G" and FG: "F ⊆ G"
using radical_step_field by auto
have topGs: "tower_top G Gs ⊆ K" using Cons.prems(4) by simp
with Cons show ?case
by (metis FG order_trans set_ConsD sfG tower')
qed
text ‹∗‹A conjugate of a radical tower is a radical tower.› Applying a field homomorphism @{term f} to
every field of a radical tower over @{term F} yields a radical tower over @{term "f ` F"}: each step
maps to a step by @{thm [source] radical_step_image_gen}.›
theorem radical_tower_image:
fixes f :: "complex ⇒ complex"
assumes K: "Subfield K" and hom: "field_hom_on K f"
shows "Subfield F ⟹ radical_tower F Fs ⟹ tower_top F Fs ⊆ K
⟹ radical_tower (f ` F) (List.map ((`) f) Fs)"
proof (induction Fs arbitrary: F)
case Nil
then show ?case by simp
next
case (Cons G Gs)
have step: "radical_step F G" and tower': "radical_tower G Gs" using Cons.prems(2) by auto
have sfG: "Subfield G"
using Cons.prems(1) local.step radical_step_field by blast
have FK: "F ⊆ K" and GK: "G ⊆ K"
using radical_tower_subset_ambient[OF K] Cons.prems sfG tower' tower_top_Cons
by blast+
show ?case
using Cons.prems radical_step_image_gen[OF hom FK step GK] Cons.IH[OF sfG tower'] by simp
qed
subsection ‹The top of a radical tower is a subfield containing the base›
lemma subfield_tower_top:
"Subfield F ⟹ radical_tower F Fs ⟹ Subfield (tower_top F Fs) ∧ F ⊆ tower_top F Fs"
by (induction Fs arbitrary: F) (use radical_step_field in force)+
subsection ‹Splicing a list of towers over a common base into one radical tower›
text ‹∗‹Base change of a tower onto a subfield containing the base.› If @{term F} is a subfield of the
subfield @{term B}, a radical tower over @{term F} base-changes to a radical tower over @{term B}
(not merely over @{term "generate_field (B ∪ F)"}): since @{term B} is a subfield containing
@{term F}, @{term "generate_field (B ∪ F) = B"}.›
lemma radical_tower_basechange_subfield:
assumes B: "Subfield B" and FB: "F ⊆ B" and tower: "radical_tower F Fs"
shows "radical_tower B (List.map (λH. generate_field (B ∪ H)) Fs)"
using B radical_tower_basechange[OF tower, of B]
by (simp add: FB Un_absorb2 Subfield.generate_field_self)
text ‹Validity of a family of towers each based at @{term F}.›
fun all_towers_over :: "'a :: field set ⇒ 'a set list list ⇒ bool" where
"all_towers_over F [] ⟷ True"
| "all_towers_over F (Ts # Tss) ⟷ radical_tower F Ts ∧ all_towers_over F Tss"
text ‹∗‹Splice› a family of towers (all based at @{term F}) into one list, base-changing each successive
tower onto the running top @{term B}. The accumulator @{term B} is the subfield reached so far.›
fun spliced :: "'a :: field set ⇒ 'a set list list ⇒ 'a set list" where
"spliced B [] = []"
| "spliced B (Ts # Tss) =
(let Ts' = List.map (λH. generate_field (B ∪ H)) Ts
in Ts' @ spliced (tower_top B Ts') Tss)"
text ‹Splicing a family of towers-over-@{term F} onto a subfield @{term B} containing @{term F} yields a
radical tower over @{term B}.›
lemma radical_tower_spliced:
"Subfield B ⟹ Subfield F ⟹ F ⊆ B ⟹ all_towers_over F Tss
⟹ radical_tower B (spliced B Tss)"
proof (induction Tss arbitrary: B)
case Nil
then show ?case by simp
next
case (Cons Ts Tss)
define Ts' where "Ts' = List.map (λH. generate_field (B ∪ H)) Ts"
have rtTs': "radical_tower B Ts'"
unfolding Ts'_def
using Cons.prems radical_tower_basechange_subfield by auto
define B' where "B' = tower_top B Ts'"
have FB': "F ⊆ B'"
using B'_def Cons.prems(1,3) rtTs' subfield_tower_top by blast
have "radical_tower B' (spliced B' Tss)"
using B'_def Cons.IH Cons.prems FB' rtTs' subfield_tower_top by force
then have "radical_tower B (Ts' @ spliced B' Tss)"
using rtTs' by (simp add: B'_def radical_tower_append)
then show ?case by (simp add: Ts'_def B'_def Let_def)
qed
subsection ‹A radical tower is increasing; every field lies in the top›
text ‹Each field of a radical tower over @{term F} is contained in the top field: the tower is
increasing (each step is a field extension, @{thm [source] radical_step_field}), so @{term F} and
every listed field embed into @{term "tower_top F Fs"}.›
lemma field_subset_tower_top:
"Subfield F ⟹ radical_tower F Fs ⟹ F ⊆ tower_top F Fs ∧ (∀H ∈ set Fs. H ⊆ tower_top F Fs)"
proof (induction Fs arbitrary: F)
case Nil
then show ?case by simp
next
case (Cons G Gs)
then show ?case
by (meson equalityE radical_tower_subset_ambient subfield_tower_top)
qed
end