Theory Galois_Restriction

section ‹Generic restriction of field automorphisms›

theory Galois_Restriction
  imports Galois_Automorphism Solvable_Transfer Galois_Action 
begin


text ‹For a base subset ‹F ⊆ E ⊆ K›, where ‹E› and ‹K› are
  subfields, stability of the intermediate carrier under the base-field automorphisms makes
  restriction a homomorphism between the two corresponding automorphism groups.  This theory
  contains the reusable carrier-set bookkeeping; splitting-field and polynomial-extension
  arguments remain in the theories that consume it.›

definition galois_restriction ::
    "'a :: field set ⇒ 'a set ⇒ 'a set ⇒
     (('a ⇒ 'a) ⇒ ('a ⇒ 'a))"
  where "galois_restriction (K :: 'a set) E F = restrict (λσ. restrict σ E) (field_auto K F)"

lemma galois_restriction_apply [simp]:
  "σ ∈ field_auto K F ⟹
    galois_restriction K E F σ = restrict σ E"
  by (simp add: galois_restriction_def)

context
  fixes K E F :: "'a :: field set"
  assumes K: "Subfield K" and sfE: "Subfield E"
    and FE: "F ⊆ E" and EK: "E ⊆ K"
    and stable: "⋀σ. σ ∈ field_auto K F ⟹ σ ` E = E"
begin

lemma field_auto_bij: "σ ∈ field_auto K F ⟹ bij_betw σ E E"
  by (metis EK bij_betw_subset field_auto_mem_iff stable)

text ‹Restriction inherits the field laws and fixed-base condition, while stability supplies
  the required bijection of the intermediate carrier.›
lemma gal_res_mem:
  assumes s: "σ ∈ field_auto K F"
  shows "restrict σ E ∈ field_auto E F"
proof -
  have sE: "σ ` E = E" using s by (rule stable)
  have addh: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x + y) = σ x + σ y"
    and multh: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x * y) = σ x * σ y"
    and one: "σ 1 = 1" and fixF: "⋀x. x ∈ F ⟹ σ x = x"
    using s by (auto simp: field_auto_mem_iff)
  interpret E: Subfield E by (rule sfE)
  show ?thesis
    unfolding field_auto_mem_iff
  proof (intro conjI ballI)
    fix x y assume xy: "x ∈ E" "y ∈ E"
    have xyK: "x ∈ K" "y ∈ K" using xy EK by auto
    show "restrict σ E (x + y) = restrict σ E x + restrict σ E y"
      using xy xyK E.add_closed addh by simp
    show "restrict σ E (x * y) = restrict σ E x * restrict σ E y"
      using xy xyK E.mult_closed multh by simp
  qed (use field_auto_bij[OF s] sE fixF FE one in auto)
qed

text ‹Restriction turns composition in @{term K} into composition in @{term E}.›
lemma gal_res_compose:
  assumes s: "σ ∈ field_auto K F" and t: "τ ∈ field_auto K F"
  shows "restrict (compose K σ τ) E = compose E (restrict σ E) (restrict τ E)"
proof (rule ext)
  fix x
  show "restrict (compose K σ τ) E x = compose E (restrict σ E) (restrict τ E) x"
  proof (cases "x ∈ E")
    case True
    with EK have xK: "x ∈ K" by blast
    have txE: "τ x ∈ E"
    proof -
      have "τ x ∈ τ ` E" by (rule imageI[OF True])
      then show ?thesis using stable[OF t] by simp
    qed
    show ?thesis by (simp add: compose_def txE xK)
  qed (simp add: compose_def restrict_def)
qed

text ‹Restriction sends the identity of @{term K} to the identity of @{term E}.›
lemma gal_res_unit: "restrict (identity K) E = identity E"
  using EK by fastforce

theorem galois_restriction_hom:
  "group_homomorphism (restrict (λσ. restrict σ E) (field_auto K F))
      (field_auto K F) (compose K) (identity K)
      (field_auto E F) (compose E) (identity E)"
proof -
  have FK: "F ⊆ K" using FE EK by blast
  interpret GK: Group "field_auto K F" "compose K" "identity K"
    by (rule field_auto_group[OF K FK])
  interpret GE: Group "field_auto E F" "compose E" "identity E"
    by (rule field_auto_group[OF sfE FE])
  show ?thesis
  proof qed (use gal_res_mem gal_res_unit in ‹auto simp: gal_res_compose›)
qed

theorem galois_restriction_epimorphism:
  assumes onto: "galois_restriction K E F ` field_auto K F = field_auto E F"
  shows "group_epimorphism (galois_restriction K E F)
      (field_auto K F) (compose K) (identity K)
      (field_auto E F) (compose E) (identity E)"
proof -
  have hom: "group_homomorphism (galois_restriction K E F)
      (field_auto K F) (compose K) (identity K)
      (field_auto E F) (compose E) (identity E)"
    by (unfold galois_restriction_def; rule galois_restriction_hom)
  interpret H: group_homomorphism "galois_restriction K E F"
      "field_auto K F" "compose K" "identity K"
      "field_auto E F" "compose E" "identity E"
    by (rule hom)
  interpret S: surjective_map "galois_restriction K E F"
      "field_auto K F" "field_auto E F"
    by unfold_locales (rule onto)
  show ?thesis
  proof (rule group_epimorphism.intro)
    show "group_homomorphism (galois_restriction K E F)
        (field_auto K F) (compose K) (identity K)
        (field_auto E F) (compose E) (identity E)"
      by (rule hom)
    show "Monoid_epimorphism (galois_restriction K E F)
        (field_auto K F) (compose K) (identity K)
        (field_auto E F) (compose E) (identity E)"
      by (rule Monoid_epimorphism.intro[OF H.Monoid_homomorphism_axioms S.surjective_map_axioms])
  qed
qed

theorem galois_restriction_Ker:
  "group_homomorphism.Ker (restrict (λσ. restrict σ E) (field_auto K F))
      (field_auto K F) (identity E) = field_auto K E"
proof -
  interpret H: group_homomorphism "restrict (λσ. restrict σ E) (field_auto K F)"
      "field_auto K F" "compose K" "identity K" "field_auto E F" "compose E" "identity E"
    by (rule galois_restriction_hom)
  show ?thesis
  proof (rule set_eqI, rule iffI)
    fix σ assume mem: "σ ∈ H.Ker"
    then have sF: "σ ∈ field_auto K F" by (rule H.Ker_closed)
    have "restrict (λσ. restrict σ E) (field_auto K F) σ = identity E"
      using mem by (rule H.Ker_image)
    then have "restrict σ E = identity E" using sF by simp
    then show "σ ∈ field_auto K E"
      using sF unfolding field_auto_mem_iff by (metis restrict_apply')
  next
    fix σ assume sE: "σ ∈ field_auto K E"
    have fixE: "⋀x. x ∈ E ⟹ σ x = x"
      using sE by (auto simp: field_auto_mem_iff)
    have sF: "σ ∈ field_auto K F"
      using sE FE by (auto simp: field_auto_mem_iff)
    then show "σ ∈ H.Ker"
      by (metis (no_types, lifting) H.Ker_memI fixE restrict_apply' restrict_ext)
  qed
qed

text ‹The standard first-isomorphism theorem applies to this generic restriction map.›
interpretation restriction_core: group_homomorphism
    "galois_restriction K E F"
    "field_auto K F" "compose K" "identity K"
    "field_auto E F" "compose E" "identity E"
proof -
  show "group_homomorphism (galois_restriction K E F)
      (field_auto K F) (compose K) (identity K)
      (field_auto E F) (compose E) (identity E)"
    by (unfold galois_restriction_def; rule galois_restriction_hom)
qed

theorem galois_restriction_factor_isomorphism:
  "(restriction_core.kernel.Factor_Group,
     restriction_core.kernel.quotient_composition,
     restriction_core.kernel.Class (identity K)) ≅⇩G
    (galois_restriction K E F ` field_auto K F, compose E, identity E)"
  by (rule restriction_core.first_isomorphism)

subsection ‹The inductive step: solvability climbs the tower›

text ‹With @{term E} stable, solvability of the relative kernel and the intermediate-field
  automorphism group implies solvability of the full automorphism group.  The restriction map is
  corestricted to its image; the group quotient is handled by the standard first-isomorphism
  machinery.›
theorem galois_solvable_tower_step:
  assumes solvKE: "Group.solvable (field_auto K E) (compose K) (identity K)"
    and solvEF: "Group.solvable (field_auto E F) (compose E) (identity E)"
  shows "Group.solvable (field_auto K F) (compose K) (identity K)"
proof -
  define η where "η = galois_restriction K E F"
  interpret H: group_homomorphism η
      "field_auto K F" "compose K" "identity K" "field_auto E F" "compose E" "identity E"
    unfolding η_def galois_restriction_def by (rule galois_restriction_hom)
  interpret I: group_epimorphism η
      "field_auto K F" "compose K" "identity K" "η ` field_auto K F" "compose E" "identity E"
    by unfold_locales (auto simp: H.commutes_with_composition)
  have Ker_eq: "I.Ker = field_auto K E"
    using galois_restriction_Ker
    unfolding η_def galois_restriction_def I.Ker_def H.Ker_def by simp
  have solvKer: "Group.solvable I.Ker (compose K) (identity K)"
    using Ker_eq solvKE by simp
  have solvImage: "Group.solvable (η ` field_auto K F) (compose E) (identity E)"
  proof (rule Group.solvable_subgroup)
    show "Group (field_auto E F) (compose E) (identity E)"
      by (rule field_auto_group[OF sfE FE])
    show "Subgroup (η ` field_auto K F) (field_auto E F)
        (compose E) (identity E)"
      by (rule H.image.Subgroup_axioms)
    show "Group.solvable (field_auto E F) (compose E) (identity E)"
      by (rule solvEF)
  qed
  show ?thesis
    using I.solvable_extension solvImage solvKer
    by blast
qed

end

subsection ‹Complex splitting-field extension of generic restriction›

text ‹Surjectivity of restriction for a generated root field.  Let ‹F ⊆ E ⊆ K› with
  @{term K} generated by @{term E} and the roots of an @{term F}-polynomial.  The finite
  homomorphism-extension theorem supplies an extension of every @{term F}-automorphism of @{term E}.
›
theorem galois_restriction_surjective:
  fixes K E F :: "'a :: field set" and Phi :: "'a poly"
  assumes sfE: "Subfield E" and sfF: "Subfield F" and FE: "F ⊆ E"
    and Phi: "Phi ∈ poly_over F"
    and Kdef: "K = generate_field (E ∪ {r. poly Phi r = 0})"
    and finR: "finite {r. poly Phi r = 0}"
    and algR: "⋀r. poly Phi r = 0 ⟹ algebraic_over E r"
    and closed: "⋀q :: 'a poly. 0 < degree q ⟹ ∃b. poly q b = 0"
    and t: "τ ∈ field_auto E F"
  shows "∃σ ∈ field_auto K F. ∀x ∈ E. σ x = τ x"
proof -
  define R where "R = {r. poly Phi r = 0}"
  have EK: "E ⊆ K" using Kdef by (auto simp: subset_generate_field)
  have sfK: "Subfield K" unfolding Kdef by (rule subfield_generate_field)
  have FK: "F ⊆ K" using FE EK by simp
  have homt: "field_hom_on E τ" using sfE t by (rule field_auto_imp_field_hom_on)
  have fixFt: "⋀x. x ∈ F ⟹ τ x = x" using t by (auto simp: field_auto_mem_iff)
  ― ‹Extend @{term τ} over the finite root set to a homomorphism @{term g} on @{term K}.›
  have algRE: "⋀r. r ∈ R ⟹ algebraic_over E r" using algR by (simp add: R_def)
  obtain g where homg: "field_hom_on (generate_field (E ∪ R)) g"
    and gE: "⋀x. x ∈ E ⟹ g x = τ x"
    using field_hom_on_extend_finite[OF closed finR[folded R_def] homt algRE] by blast
  have homgK: "field_hom_on K g" using homg by (simp add: Kdef R_def)
  have fixFg: "⋀x. x ∈ F ⟹ g x = x" using gE fixFt FE by auto
  have RK: "R ⊆ K" using EK unfolding Kdef R_def using subset_generate_field by blast
  have gR_sub: "g ` R ⊆ R"
    using hom_preserves_roots[OF homgK sfF FK fixFg Phi] RK
    by (auto simp: R_def)
  have injK: "inj_on g K" by (rule field_hom_on.inj_on[OF homgK])
  have gR: "g ` R = R"
    by (metis RK R_def endo_inj_surj finR gR_sub injK inj_on_subset)
  have gE_onto: "g ` E = E"
    by (metis bij_betw_imp_surj_on field_auto_mem_iff gE image_cong t)
  have gUn: "g ` (E ∪ R) = E ∪ R" using gE_onto gR by (simp add: image_Un)
  have gK: "g ` K = K"
    by (metis EK Kdef RK R_def field_hom_on.image_generate_field_eq gUn homgK sup.boundedI)
  have aut: "restrict g K ∈ field_auto K F"
    by (rule field_hom_on_imp_field_auto[OF homgK gK fixFg FK])
  then show ?thesis using aut
    by (metis EK gE in_mono restrict_def)
qed

subsection ‹A normal solvable tower has a solvable Galois group›

text ‹Given a fixed complex splitting field @{term K} and a chain
  of intermediate fields ‹F = F⇩0 ⊆ F⇩1 ⊆ … ⊆ F⇩n = K› in which each ‹F⇩i› is ∗‹stable› under
  @{term "field_auto K F"} and each step's relative Galois group ‹field_auto F⇩i⇩+⇩1 F⇩i› is
  solvable, the whole Galois group @{term "field_auto K F"} is solvable.  This chains the inductive
  step @{thm [source] galois_solvable_tower_step} down the tower, the base case being the trivial
  group @{term "field_auto K K"}.›

subsubsection ‹The trivial Galois group›

text ‹An automorphism of @{term K} fixing all of @{term K} is the identity, so @{term "field_auto K K"}
  is trivial.›
lemma field_auto_self_trivial:
  fixes K :: "complex set"
  assumes K: "Subfield K"
  shows "field_auto K K = {identity K}"
proof -
  have cK: "complex_subfield K" using K by (simp add: complex_subfield_iff_subfield)
  have "σ ∈ {identity K}" if "σ ∈ field_auto K K" for σ
    by (metis that PiE_restrict field_auto_mem_iff insertI1 restrict_ext)
  then show ?thesis
    using cK identity_field_auto by auto
qed

lemma solvable_field_auto_self:
  fixes K :: "complex set"
  assumes K: "Subfield K"
  shows "Group.solvable (field_auto K K) (compose K) (identity K)"
proof -
  have cK: "complex_subfield K" using K by (simp add: complex_subfield_iff_subfield)
  interpret G: Group "field_auto K K" "compose K" "identity K"
    by (rule Galois_group_Group[OF cK subset_refl])
  show ?thesis unfolding G.solvable_def
    using G.derivedSeries.simps(1) assms field_auto_self_trivial by blast
qed

subsubsection ‹Normal solvable towers›

text ‹@{term "solvable_tower K F Fs"}: the chain starting at @{term F} and following @{term Fs}, with
  fixed top @{term K}, in which every field is a subfield of @{term K}, every intermediate field is
  stable under @{term "field_auto K F"}, and every step has a solvable relative Galois group.  (The
  empty tower requires @{term "F = K"}.)›
fun solvable_tower :: "complex set ⇒ complex set ⇒ complex set list ⇒ bool" where
  "solvable_tower K F [] ⟷ F = K"
| "solvable_tower K F (G # Gs) ⟷
     Subfield F ∧ Subfield G ∧ F ⊆ G ∧ G ⊆ K ∧
     (∀σ ∈ field_auto K F. σ ` G = G) ∧
     Group.solvable (field_auto G F) (compose G) (identity G) ∧
     solvable_tower K G Gs"

subsubsection ‹The assembly›

text ‹∗‹A normal solvable tower has a solvable Galois group.›  By induction down the tower: the top
  @{term K} has the trivial (hence solvable) group @{term "field_auto K K"}; each step combines the
  solvable relative group @{term "field_auto G F"} with the solvable @{term "field_auto K G"} (from
  the induction hypothesis) via @{thm [source] galois_solvable_tower_step}, using stability of
  @{term G} under @{term "field_auto K F"}.›
theorem solvable_tower_imp_solvable:
  assumes K: "Subfield K"
  shows "solvable_tower K F Fs ⟹ Subfield F
           ⟹ Group.solvable (field_auto K F) (compose K) (identity K)"
proof (induction Fs arbitrary: F)
  case Nil then show ?case
    by (metis solvable_field_auto_self solvable_tower.simps(1))
next
  case Cons
  then show ?case
    by (metis assms galois_solvable_tower_step solvable_tower.simps(2))
qed

end