Theory Radical_Extension

section ‹Radical extensions and solvability by radicals›

theory Radical_Extension
  imports Simple_Extension
begin

text ‹This theory begins the ∗‹forward› Abel--Ruffini direction (phase R1: the definitions).  It
  fixes the notion of ∗‹solvability by radicals› over a base field, on the same generic
  @{typ "'a :: field"}/@{const generate_field} foundation used for the quintic.  Later phases will
  connect it to solvability of the Galois group (via the Galois correspondence, cyclotomic and
  Kummer theory).  Here we only make the target statement expressible.›

subsection ‹Radical steps and towers›

text ‹A single ∗‹radical step› from @{term F} to @{term F'} adjoins an element @{term a} some power
  of which already lies in @{term F}: @{term "F' = generate_field (F ∪ {a})"} with
  @{term "a ^ n ∈ F"} for some @{term "n > 0"}.›
definition radical_step :: "'a :: field set ⇒ 'a set ⇒ bool"
  where "radical_step F F' ≡ (∃a n. n > 0 ∧ a ^ n ∈ F ∧ F' = generate_field (F ∪ {a}))"

text ‹A ∗‹radical tower› is a list of fields, each obtained from the previous by a radical step.
  @{term "radical_tower F Fs"} says the tower starting at @{term F} and following @{term Fs} is
  valid (each consecutive pair is a radical step).›
fun radical_tower :: "'a :: field set ⇒ 'a set list ⇒ bool" where
  "radical_tower F [] ⟷ True"
| "radical_tower F (G # Gs) ⟷ radical_step F G ∧ radical_tower G Gs"

text ‹The top field of a tower (the last field, or the base if the tower is empty).›
definition tower_top :: "'a :: field set ⇒ 'a set list ⇒ 'a set"
  where "tower_top F Fs = last (F # Fs)"

lemma tower_top_Nil [simp]: "tower_top F [] = F"
  by (simp add: tower_top_def)

lemma tower_top_Cons [simp]: "tower_top F (G # Gs) = tower_top G Gs"
  by (simp add: tower_top_def)

subsection ‹Solvability by radicals›

text ‹A set @{term S} (typically the roots of a polynomial, together with the base field) is
  ∗‹solvable by radicals› over @{term F} when there is a radical tower over @{term F} whose top field
  contains @{term S}.›
definition solvable_by_radicals :: "'a :: field set ⇒ 'a set ⇒ bool"
  where "solvable_by_radicals F S ⟷ (∃Fs. radical_tower F Fs ∧ S ⊆ tower_top F Fs)"

text ‹The base field itself is trivially solvable by radicals (the empty tower).›
lemma solvable_by_radicals_base:
  assumes "S ⊆ F" shows "solvable_by_radicals F S"
  unfolding solvable_by_radicals_def  
  using assms by (auto intro!: exI[of _ "[]"])

text ‹A single radical step gives a one-element tower.›
lemma solvable_by_radicals_step:
  assumes "n > 0" and "a ^ n ∈ F" and "S ⊆ generate_field (F ∪ {a})"
  shows "solvable_by_radicals F S"
  unfolding solvable_by_radicals_def
proof (intro exI[of _ "[generate_field (F ∪ {a})]"] conjI)
  show "radical_tower F [generate_field (F ∪ {a})]"
    using assms by (auto simp: radical_step_def)
  show "S ⊆ tower_top F [generate_field (F ∪ {a})]" using assms(3) by simp
qed

subsection ‹Concatenation of radical towers›

text ‹The top of a concatenated tower is the top of the second part (or of the first, if the second is
  empty).›
lemma tower_top_append:
  "tower_top F (Fs @ Gs) = tower_top (tower_top F Fs) Gs"
  by (simp add: tower_top_def last_append)

text ‹∗‹Radical towers concatenate.›  A radical tower over @{term F} followed by a radical tower over its
  top field @{term "tower_top F Fs"} yields a radical tower over @{term F} along the appended list.
  This is the splicing primitive used to build a compositum of radical extensions into a single tower.›
lemma radical_tower_append:
  "radical_tower F Fs ⟹ radical_tower (tower_top F Fs) Gs ⟹ radical_tower F (Fs @ Gs)"
  by (induction Fs arbitrary: F) auto

text ‹∗‹Iterated concatenation.›  Given a list of towers, each valid over the top reached so far, their
  concatenation is a single radical tower.  We phrase validity of a list of towers recursively.›
fun radical_tower_list :: "'a :: field set ⇒ 'a set list list ⇒ bool" where
  "radical_tower_list F [] ⟷ True"
| "radical_tower_list F (Ts # Tss) ⟷
     radical_tower F Ts ∧ radical_tower_list (tower_top F Ts) Tss"

lemma radical_tower_concat:
  "radical_tower_list F Tss ⟹ radical_tower F (concat Tss)"
  by (induction Tss arbitrary: F) (auto simp: radical_tower_append)

lemma tower_top_concat:
  "radical_tower_list F Tss ⟹ tower_top F (concat Tss) = foldl tower_top F Tss"
  by (induction Tss arbitrary: F) (auto simp: tower_top_append)

subsection ‹Base change: lifting a radical tower to a larger base›

text ‹Adjoining a fixed set @{term E} to every field of a radical tower over @{term F} yields a radical
  tower over @{term "generate_field (E ∪ F)"}: each step ‹H ↝ generate_field (H ∪ {a})› becomes
  ‹generate_field (E ∪ H) ↝ generate_field (E ∪ generate_field (H ∪ {a}))›, which by the collapse
  lemmas is @{term "generate_field (generate_field (E ∪ H) ∪ {a})"} with the same radical @{term a}
  (its power ‹a⇧n ∈ H ⊆ generate_field (E ∪ H)›).  This is what lets conjugate towers, each
  based at @{term F}, be spliced onto a growing compositum.›
lemma radical_step_basechange:
  assumes "radical_step F G"
  shows "radical_step (generate_field (E ∪ F)) (generate_field (E ∪ G))"
proof -
  obtain a n where n: "n > 0" and anF: "a ^ n ∈ F" and Gdef: "G = generate_field (F ∪ {a})"
    using assms by (auto simp: radical_step_def)
  have "a ^ n ∈ generate_field (E ∪ F)" using anF subset_generate_field by blast
  moreover have "generate_field (E ∪ G) = generate_field (generate_field (E ∪ F) ∪ {a})"
    by (metis Gdef Un_commute generate_field_Un_collapse2 sup.assoc)
  ultimately show ?thesis unfolding radical_step_def using n by blast
qed

text ‹Hence base change of a whole radical tower: mapping each field @{term H} to
  @{term "generate_field (E ∪ H)"} sends a radical tower over @{term F} to a radical tower over
  @{term "generate_field (E ∪ F)"}.›
lemma radical_tower_basechange:
  "radical_tower F Fs ⟹ radical_tower (generate_field (E ∪ F)) (map (λH. generate_field (E ∪ H)) Fs)"
  by (induction Fs arbitrary: F) (auto simp: radical_step_basechange)

end