Theory Galois_Finite_Correspondence

section ‹The fundamental theorem for finite Galois extensions›

theory Galois_Finite_Correspondence
  imports Artin_Degree Galois_Degree Finite_Extension_Tower Galois_Restriction
begin

text ‹Separability survives enlargement of the base field.  The new minimal polynomial divides
  the old one, and root-squarefreeness passes to divisors.›
theorem finite_separable_extension_base_change:
  fixes F E K :: "'a :: field set"
  assumes T: "finite_subfield_tower F K" and sep: "separable_extension K F"
    and sfE: "Subfield E" and FE: "F ⊆ E" and EK: "E ⊆ K"
  shows "separable_extension K E"
proof (rule separable_extensionI)
  interpret T: finite_subfield_tower F K by (rule T)
  fix x assume xK: "x ∈ K" and algE: "algebraic_over E x"
  have algF: "algebraic_over F x" by (rule T.finite_extension_algebraic[OF xK])
  have sepF: "rsquarefree (minpoly F x)"
    by (rule separable_extensionD[OF sep xK algF])
  have minE: "is_minpoly E x (minpoly E x)"
    by (rule Subfield.is_minpoly_minpoly[OF sfE algE])
  have "minpoly F x ∈ poly_over E"
    using T.base.minpoly_over[OF algF] poly_over_mono[OF FE] by blast
  then show "rsquarefree (minpoly E x)"
    using Subfield.minpoly_dvd T.base.minpoly_root algF minE rsquarefree_dvd sepF sfE
    by blast
qed

text ‹Normality also survives enlargement of the base inside a finite extension.  The minimal
  polynomial over the larger base divides the old minimal polynomial, so every new conjugate is
  already an old conjugate.›
theorem finite_normal_extension_base_change:
  fixes F E K :: "'a :: field set"
  assumes T: "finite_subfield_tower F K" and normal: "normal_extension K F"
    and sfE: "Subfield E" and FE: "F ⊆ E" and EK: "E ⊆ K"
  shows "normal_extension K E"
proof (rule normal_extensionI)
  interpret T: finite_subfield_tower F K by (rule T)
  fix p a
  assume pE: "p ∈ poly_over E" and irr: "irreducible_over E p"
    and aK: "a ∈ K" and pa: "poly p a = 0"
  have algF: "algebraic_over F a"
    by (rule T.finite_extension_algebraic[OF aK])
  have algE: "algebraic_over E a"
    by (rule algebraic_over_mono[OF algF FE])
  then have minE: "is_minpoly E a (minpoly E a)"
    by (rule Subfield.is_minpoly_minpoly[OF sfE])
  have minF_E: "minpoly F a ∈ poly_over E"
    using T.base.minpoly_over[OF algF] poly_over_mono[OF FE] by blast
  have dvd: "minpoly E a dvd minpoly F a"
    by (rule Subfield.minpoly_dvd[OF sfE minE minF_E T.base.minpoly_root[OF algF]])
  have "poly_root_set (minpoly F a) ⊆ K"
    using T.base.Subfield_axioms T.base.minpoly_over T.base.minpoly_root aK algF
      irreducible_over_minpoly normal normal_extensionD by blast
  then show "poly_root_set p ⊆ K"
    using Subfield.irreducible_over_root_is_minpoly_root dvd irr minE pE pa sfE
    by fastforce
qed


subsection ‹The finite correspondence›

context
  fixes F K :: "'a :: alg_closed_field set"
  assumes finite: "finite_subfield_tower F K"
    and normal: "normal_extension K F"
    and separable: "separable_extension K F"
begin

interpretation T: finite_subfield_tower F K by (rule finite)

interpretation GE: galois_extension K F
  by (rule galois_extension.intro[OF T.ext.Subfield_axioms T.base.Subfield_axioms
    T.base_subset])

text ‹Any two conjugates over the base are related by an automorphism of a finite Galois
  extension.  A primitive element presents the extension as the field generated by the roots of its
  minimal polynomial; multiplying that polynomial by the minimal polynomial 
  lets the generic transitivity theorem act on both roots without changing the generated field.›
theorem finite_galois_root_transfer:
  assumes aK: "a ∈ K" and mb: "poly (minpoly F a) b = 0"
  shows "∃σ∈field_auto K F. σ a = b"
proof -
  have alga: "algebraic_over F a"
    by (rule T.finite_extension_algebraic[OF aK])
  obtain theta where thetaK: "theta ∈ K" and prim: "primitive_element F K theta" and "algebraic_over F theta"
    by (meson T.finite_extension_algebraic finite separable finite_separable_extension_is_simple)
  have algtheta: "algebraic_over F theta"
    by (rule T.finite_extension_algebraic[OF thetaK])
  define q where "q ≡ minpoly F theta"
  define m where "m ≡ minpoly F a"
  define Phi where "Phi ≡ q * m"
  define R where "R ≡ {r. poly Phi r = 0}"
  obtain qF: "q ∈ poly_over F" and mF: "m ∈ poly_over F"
    by (simp add: T.base.minpoly_over alga algtheta m_def q_def)
  obtain q0: "q ≠ 0" and m0: "m ≠ 0"
    using T.base.minpoly_nonzero alga algtheta m_def q_def by presburger
  have PhiF: "Phi ∈ poly_over F"
    unfolding Phi_def by (rule T.base.poly_over_mult[OF qF mF])
  have Phi0: "Phi ≠ 0" unfolding Phi_def using q0 m0 by simp
  have finR: "finite R"
    unfolding R_def by (rule poly_roots_finite[OF Phi0])
  have qroots: "poly_root_set q ⊆ K"
    using T.base.Subfield_axioms T.base.minpoly_root algtheta irreducible_over_minpoly normal
      normal_extensionD qF q_def thetaK by blast
  have mroots: "poly_root_set m ⊆ K"
    using normal mF unfolding normal_extension_def m_def
    using GE.Fsub T.base.minpoly_root aK alga irreducible_over_minpoly by blast
  have RsubK: "R ⊆ K"
    using qroots mroots
    unfolding R_def Phi_def poly_root_set_def by (auto simp: poly_mult)
  have algR: "⋀r. r ∈ R ⟹ algebraic_over F r"
    by (rule T.finite_extension_algebraic) (use RsubK in blast)
  obtain thetaR: "theta ∈ R" and aR: "a ∈ R" and bR: "b ∈ R"
    unfolding R_def Phi_def q_def
    by (simp add: T.base.minpoly_root alga algtheta m_def mb)
  have Kgen: "K = generate_field (F ∪ R)"
  proof 
    show "K ⊆ generate_field (F ∪ R)"      
      using primitive_elementD[OF prim] T.base.eval_img_eq_generate_field[OF algtheta] 
      by (simp add: generate_field_mono thetaR)
    show "generate_field (F ∪ R) ⊆ K"
      using RsubK T.base_subset by (simp add: T.ext.Subfield_axioms generate_field_least) 
  qed
  have min_a: "is_minpoly F a (minpoly F a)"
    by (rule T.base.is_minpoly_minpoly[OF alga])
  obtain g where homg: "field_hom_on (generate_field (F ∪ R)) g"
    and gab: "g a = b" and fixg: "∀x∈F. g x = x"
    and imageg: "g ` generate_field (F ∪ R) = generate_field (F ∪ R)"
    using galois_transitive[OF T.base.Subfield_axioms finR algR]
      PhiF R_def alg_closed_imp_poly_has_root aR bR min_a mb
    by blast
  have aut: "restrict g K ∈ field_auto K F"
    using Kgen field_hom_on_imp_field_auto fixg homg imageg by blast
  have "restrict g K a = b" using aK gab by simp
  then show ?thesis using aut by blast
qed

text ‹Every intermediate field is recovered as the fixed field of its relative Galois group.
  The upper extension remains finite, normal and separable.  Its degree equals the order of the
  relative group; Artin's theorem computes the degree over that group's fixed field.  The tower law
  then makes the intervening degree one.›
theorem finite_galois_fixed_field:
  assumes E: "E ∈ inter_fields K F"
  shows "fixed_field K (field_auto K E) = E"
proof -
  have sfE: "Subfield E" and FE: "F ⊆ E" and EK: "E ⊆ K"
    using E by (auto simp: inter_fields_iff)
  have TFE_raw: "finite_subfield_tower F E"
    by (rule finite_subfield_tower_intermediate_left[OF finite sfE FE EK])
  then interpret TFE: finite_subfield_tower F E .
  have TEK_raw: "finite_subfield_tower E K"
    by (rule finite_subfield_tower_intermediate_right[OF finite sfE FE EK])
  then interpret TEK: finite_subfield_tower E K .
  have normalEK: "normal_extension K E"
    by (rule finite_normal_extension_base_change[OF finite normal sfE FE EK])
  have sepEK: "separable_extension K E"
    by (rule finite_separable_extension_base_change[OF finite separable sfE FE EK])

  have Hsub_raw: "Subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
    by (rule field_auto_subgroup_of_Galois_group[OF T.ext.Subfield_axioms T.base_subset E])
  have Hsub: "field_auto K E ∈ galois_subgroups K F"
    using Hsub_raw by (simp add: galois_subgroups_iff)
  have Hle: "field_auto K E ⊆ field_auto K F"
    using Hsub by (rule galois_subgroups_subset)
  have finG: "finite (field_auto K F)"
    by (rule finite_normal_separable_field_auto[OF finite normal separable])
  have finH: "finite (field_auto K E)"
    by (rule finite_subset[OF Hle finG])
  have cardH: "card (field_auto K E) = TEK.extension_degree"
    by (rule finite_normal_separable_galois_degree[OF TEK_raw normalEK sepEK])

  have towerFix: "subfield_tower (fixed_field K (field_auto K E)) K"
    by (rule fixed_field_tower[OF T.ext.Subfield_axioms Hle])
  then interpret FixK: subfield_tower "fixed_field K (field_auto K E)" K .
  obtain B where basis: "FixK.vs.basis B"
    and cardB: "card B = card (field_auto K E)"
    using artin_fixed_field_degree_data[where K=K and F=F and H="field_auto K E",
      OF T.ext.Subfield_axioms T.base.Subfield_axioms T.base_subset Hsub finH]
    by blast
  interpret TFixK: finite_subfield_tower "fixed_field K (field_auto K E)" K
    by (fast intro!: towerFix finite_subfield_tower.intro finite_subfield_tower_axioms.intro basis)
  have degreeFix: "TFixK.extension_degree = card (field_auto K E)"
    using TFixK.extension_degree_eq_card_basis[OF basis] cardB by simp

  have EFix: "E ⊆ fixed_field K (field_auto K E)"
    by (rule GE.le_fixed_field_galois_group[OF E])
  have sfFix: "Subfield (fixed_field K (field_auto K E))"
    by (rule fixed_field_subfield[OF T.ext.Subfield_axioms Hle])
  have TEFix_raw: "finite_subfield_tower E (fixed_field K (field_auto K E))"
    by (rule finite_subfield_tower_intermediate_left[OF TEK_raw sfFix EFix fixed_field_subset])
  then interpret TEFix: finite_subfield_tower E "fixed_field K (field_auto K E)" .
  interpret C: finite_subfield_tower_chain E "fixed_field K (field_auto K E)" K
    by (simp add: TEFix_raw TFixK.finite_subfield_tower_axioms finite_subfield_tower_chain_def)
  have cancel_eq: "TFixK.extension_degree * 1 = TFixK.extension_degree * TEFix.extension_degree"
    using  C.extension_degree_tower_law_exists cardH degreeFix by (simp add: mult.commute)
  have degree_one: "TEFix.extension_degree = 1"
    using cancel_eq TFixK.extension_degree_pos nat_mult_eq_cancel1 by simp

  have sepEFix: "separable_extension (fixed_field K (field_auto K E)) E"
    using sepEK by (meson fixed_field_memD separable_extension_def)
  obtain theta where prim: "primitive_element E (fixed_field K (field_auto K E)) theta"
                and algTheta: "algebraic_over E theta"
    using TEFix.finite_extension_algebraic TEFix_raw finite_separable_extension_is_simple sepEFix
    by blast
  have ext_one: "ext_degree E theta = 1"
    using TEFix.primitive_element_degree[OF prim] degree_one by simp
  have thetaE: "theta ∈ E"
    using ext_one Subfield.ext_degree_eq_1_iff[OF sfE algTheta] by blast
  have "eval_img E theta = generate_field (E ∪ {theta})"
    by (rule Subfield.eval_img_eq_generate_field[OF sfE algTheta])
  also have "... = E"
    by (simp add: TFE.ext.generate_field_self insert_absorb thetaE)
  finally have "eval_img E theta = E" .
  then show ?thesis using primitive_elementD[OF prim] by simp
qed

text ‹Conversely, a subgroup of the finite Galois group is recovered from its fixed field by
  Artin's theorem.›
theorem finite_galois_fixed_group:
  assumes H: "H ∈ galois_subgroups K F"
  shows "field_auto K (fixed_field K H) = H"
proof -
  have finG: "finite (field_auto K F)"
    by (rule finite_normal_separable_field_auto[OF finite normal separable])
  have finH: "finite H"
    using assms finG by (metis finite_subset galois_subgroups_subset) 
  show ?thesis
    by (rule artin_theorem[OF T.ext.Subfield_axioms T.base.Subfield_axioms
      T.base_subset H finH])
qed

text ‹The two antitone maps are therefore mutually inverse bijections.›
theorem finite_galois_field_group_bij:
  "bij_betw (field_auto K) (inter_fields K F) (galois_subgroups K F)"
proof (rule bij_betw_byWitness[where f'="fixed_field K"])
  show "∀E∈inter_fields K F. fixed_field K (field_auto K E) = E"
    using finite_galois_fixed_field by blast
  show "∀H∈galois_subgroups K F. field_auto K (fixed_field K H) = H"
    using finite_galois_fixed_group by blast
  show "field_auto K ` inter_fields K F ⊆ galois_subgroups K F"
    using field_auto_subgroup_of_Galois_group[OF T.ext.Subfield_axioms T.base_subset]
    by (auto simp: galois_subgroups_iff)
  show "fixed_field K ` galois_subgroups K F ⊆ inter_fields K F"
    using GE.fixed_field_in_inter_fields by blast
qed

theorem finite_galois_group_field_bij:
  "bij_betw (fixed_field K) (galois_subgroups K F) (inter_fields K F)"
proof (rule bij_betw_byWitness[where f'="field_auto K"])
  show "∀H∈galois_subgroups K F. field_auto K (fixed_field K H) = H"
    using finite_galois_fixed_group by blast
  show "∀E∈inter_fields K F. fixed_field K (field_auto K E) = E"
    using finite_galois_fixed_field by blast
  show "fixed_field K ` galois_subgroups K F ⊆ inter_fields K F"
using finite_galois_fixed_group
    using GE.fixed_field_in_inter_fields by blast
  show "field_auto K ` inter_fields K F ⊆ galois_subgroups K F"
    using field_auto_subgroup_of_Galois_group[OF T.ext.Subfield_axioms T.base_subset]
    by (auto simp: galois_subgroups_iff)
qed

theorem finite_galois_correspondence:
  "bij_betw (field_auto K) (inter_fields K F) (galois_subgroups K F) ∧
   bij_betw (fixed_field K) (galois_subgroups K F) (inter_fields K F)"
  using finite_galois_field_group_bij finite_galois_group_field_bij by blast


subsection ‹Degree and index formulas›

context
  fixes E :: "'a set"
  assumes intermediate: "E ∈ inter_fields K F"
begin

lemma intermediate_data:
  "Subfield E ∧ F ⊆ E ∧ E ⊆ K"
  using intermediate by (simp add: inter_fields_iff)

lemma TFE_raw: "finite_subfield_tower F E"
  using intermediate_data
  by (blast intro: finite_subfield_tower_intermediate_left[OF finite])

lemma TEK_raw: "finite_subfield_tower E K"
  using intermediate_data
  by (blast intro: finite_subfield_tower_intermediate_right[OF finite])

interpretation TFE: finite_subfield_tower F E by (rule TFE_raw)
interpretation TEK: finite_subfield_tower E K by (rule TEK_raw)

lemma normalEK: "normal_extension K E"
  using intermediate_data
  by (blast intro: finite_normal_extension_base_change[OF finite normal])

lemma separableEK: "separable_extension K E"
  using intermediate_data
  by (blast intro: finite_separable_extension_base_change[OF finite separable])

lemma relative_subgroup:
  "Subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
  by (rule field_auto_subgroup_of_Galois_group[OF T.ext.Subfield_axioms T.base_subset
    intermediate])

interpretation S: subgroup_of_group "field_auto K E" "field_auto K F"
    "compose K" "identity K"
  by (simp add: T.base_subset T.ext.Subfield_axioms field_auto_group relative_subgroup
      subgroup_of_group.intro)

text ‹The relative Galois group has order equal to the degree of the upper extension.›
theorem finite_galois_relative_group_order:
  "card (field_auto K E) = TEK.extension_degree"
  by (rule finite_normal_separable_galois_degree[OF TEK_raw normalEK separableEK])

text ‹Its index in the full Galois group is the degree of the lower extension.›
theorem finite_galois_relative_group_index:
  "S.index = TFE.extension_degree"
proof -
  have finG: "finite (field_auto K F)"
    by (rule finite_normal_separable_field_auto[OF finite normal separable])
  have global_order: "card (field_auto K F) = T.extension_degree"
    by (rule finite_normal_separable_galois_degree[OF finite normal separable])
  interpret C: finite_subfield_tower_chain F E K
    by (rule finite_subfield_tower_chain.intro[OF TFE_raw TEK_raw])
  have cancel_eq: "TEK.extension_degree * TFE.extension_degree = TEK.extension_degree * S.index"
    using C.extension_degree_tower_law_exists S.lagrange finG finite_galois_relative_group_order
      global_order by force
  show ?thesis
    using cancel_eq TEK.extension_degree_pos nat_mult_eq_cancel1 by simp
qed

theorem finite_galois_relative_degree_index:
  "card (field_auto K E) = TEK.extension_degree ∧
   S.index = TFE.extension_degree"
  using finite_galois_relative_group_order finite_galois_relative_group_index by blast


subsection ‹Normal intermediate fields›

text ‹An intermediate field is normal over the base exactly when every automorphism of the
  ambient finite Galois extension preserves it setwise. Some duplication with a later proof.›
theorem finite_galois_normal_iff_stable:
  "normal_extension E F ⟷
    (∀σ∈field_auto K F. σ ` E = E)"
proof (intro iffI strip)
  assume normalE: "normal_extension E F"
  have image_subset: "σ ` E ⊆ E" if sigma: "σ ∈ field_auto K F" for σ
  proof
    fix y assume "y ∈ σ ` E"
    then obtain x where xE: "x ∈ E" and y: "y = σ x" by blast
    have xK: "x ∈ K" using intermediate_data xE by blast
    have algx: "algebraic_over F x"
      by (rule TFE.finite_extension_algebraic[OF xE])
    have rootsE: "poly_root_set (minpoly F x) ⊆ E"
      using GE.Fsub T.base.minpoly_over T.base.minpoly_root algx irreducible_over_minpoly normalE
        normal_extensionD xE by blast
    have hom: "field_hom_on K σ"
      by (rule field_auto_as_hom[OF T.ext.Subfield_axioms sigma])
    have fixF: "⋀z. z ∈ F ⟹ σ z = z"
      using sigma by (auto simp: field_auto_mem_iff)
    have image_root: "poly (minpoly F x) (σ x) = 0"
      using GE.Fsub T.base.minpoly_over T.base.minpoly_root T.base_subset algx fixF hom xK
      by (meson hom_preserves_roots)
    have "σ x ∈ poly_root_set (minpoly F x)"
      using image_root unfolding poly_root_set_def by simp
    then show "y ∈ E" using rootsE y by blast
  qed
  show "σ ` E = E" if sigma: "σ ∈ field_auto K F" for σ
  proof -
    define tau where "tau ≡ restrict (inv_into K σ) K"
    have tauG: "tau ∈ field_auto K F"
      by (simp add: T.base_subset T.ext.Subfield_axioms field_auto_inverse sigma tau_def)
    show "σ ` E = E"
    proof (intro antisym subsetI)
      fix y assume yE: "y ∈ E"
      have yK: "y ∈ K" using intermediate_data yE by blast
      have "y ∈ σ ` K"
        using sigma yK by (metis bij_betw_imp_surj_on field_auto_mem_iff)
      then have sigma_tau: "σ (tau y) = y"
        unfolding tau_def using yK by (simp add: f_inv_into_f)
      then show "y ∈ σ ` E" 
        unfolding image_iff by (metis image_subset tauG yE image_subset_iff)
    qed (use image_subset sigma in auto)
  qed
next
  assume stable: "∀σ∈field_auto K F. σ ` E = E"
  show "normal_extension E F"
  proof (rule normal_extensionI)
    fix p a
    assume pF: "p ∈ poly_over F" and irr: "irreducible_over F p"
      and aE: "a ∈ E" and pa: "poly p a = 0"
    have aK: "a ∈ K" using intermediate_data aE by blast
    show "poly_root_set p ⊆ E"
    proof
      fix b assume bR: "b ∈ poly_root_set p"
      have min_a: "is_minpoly F a (minpoly F a)"
        using T.base.is_minpoly_minpoly T.finite_extension_algebraic aK by blast
      have min_b: "poly (minpoly F a) b = 0"
        using T.base.irreducible_over_root_is_minpoly_root bR irr min_a pF pa by auto
      then show "b ∈ E"
        using aE stable finite_galois_root_transfer[OF aK min_b] by fastforce
    qed
  qed
qed


text ‹Setwise stability is also exactly normality of the corresponding subgroup.
     A lot of duplication with the similar theorem below.›
theorem finite_galois_normal_subgroup_iff_stable:
  "normal_subgroup (field_auto K E) (field_auto K F) (compose K) (identity K) ⟷
    (∀σ∈field_auto K F. σ ` E = E)"
proof (intro iffI strip)
  assume normalH:
    "normal_subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
  interpret N: normal_subgroup "field_auto K E" "field_auto K F"
    "compose K" "identity K" by (rule normalH)
  have fixedE: "fixed_field K (field_auto K E) = E"
    by (rule finite_galois_fixed_field[OF intermediate])
  have image_subset: "σ ` E ⊆ E" if sigma: "σ ∈ field_auto K F" for σ
  proof
    fix y assume "y ∈ σ ` E"
    then obtain x where xE: "x ∈ E" and y: "y = σ x" by blast
    have xFix: "x ∈ fixed_field K (field_auto K E)" using xE fixedE by simp
    have xK: "x ∈ K" using fixed_field_memD[OF xFix] by blast
    have sigxK: "σ x ∈ K"
      using sigma xK by (auto simp: field_auto_mem_iff PiE_iff)
    have sigxFix: "σ x ∈ fixed_field K (field_auto K E)"
    proof (rule fixed_field_memI[OF sigxK])
      fix h assume hH: "h ∈ field_auto K E"
      have cosets:
          "coset_notation.Left_Coset (compose K) σ (field_auto K E) =
           coset_notation.Right_Coset (compose K) (field_auto K E) σ"
        by (rule N.Left_equals_Right_coset[OF sigma])
      have "compose K h σ ∈ coset_notation.Right_Coset (compose K) (field_auto K E) σ"
        using hH by blast
      then obtain k where kH: "k ∈ field_auto K E" and commute: "compose K σ k = compose K h σ"
        unfolding coset_notation.Left_Coset_def
        using S.Left_Coset_memE cosets by metis
      then show "h (σ x) = σ x"
        by (metis fixedE xE compose_eq fixed_field_memD) 
    qed
    show "y ∈ E" using sigxFix fixedE y by simp
  qed
  show "σ ` E = E" if sigma: "σ ∈ field_auto K F" for σ
  proof -
    define tau where "tau ≡ restrict (inv_into K σ) K"
    have tauG: "tau ∈ field_auto K F"
      by (simp add: T.base_subset T.ext.Subfield_axioms field_auto_inverse sigma tau_def)
    show "σ ` E = E"
    proof 
      show "E ⊆ σ ` E"
      proof
        fix y assume yE: "y ∈ E"
        have yK: "y ∈ K" using intermediate_data yE by blast
        have "y ∈ σ ` K"
          using sigma yK by (metis bij_betw_imp_surj_on field_auto_mem_iff)
        then have sigma_tau: "σ (tau y) = y"
          unfolding tau_def using yK by (simp add: f_inv_into_f)
        then show "y ∈ σ ` E" 
          unfolding image_iff by (metis image_subset tauG yE image_subset_iff)
      qed
      show "σ ` E ⊆ E"
        by (simp add: image_subset sigma)
    qed
  qed
next
  assume stable: "∀σ∈field_auto K F. σ ` E = E"
  interpret R: group_homomorphism "galois_restriction K E F"
                "field_auto K F" "compose K" "identity K"
                "field_auto E F" "compose E" "identity E"
    by (simp add: T.ext.Subfield_axioms galois_restriction_def galois_restriction_hom intermediate_data
        stable)
  have ker: "R.Ker = field_auto K E"
    unfolding galois_restriction_def
    by (simp add: T.ext.Subfield_axioms galois_restriction_Ker intermediate_data stable)
  then show "normal_subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
    using R.kernel.normal_subgroup_axioms by presburger
qed

text ‹This is the normal-field/normal-subgroup clause of the fundamental theorem.›
theorem finite_galois_normal_iff_normal_subgroup:
  "normal_extension E F ⟷
   normal_subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
  using finite_galois_normal_iff_stable finite_galois_normal_subgroup_iff_stable by blast


subsection ‹Restriction and the quotient theorem›

text ‹Restriction onto a stable intermediate field is surjective.  A primitive element for
  the full extension supplies a finite root-generated presentation over the intermediate field, so
  the generic homomorphism-extension theorem applies.›
theorem finite_galois_restriction_image:
  assumes stable: "⋀σ. σ ∈ field_auto K F ⟹ σ ` E = E"
  shows "galois_restriction K E F ` field_auto K F = field_auto E F"
proof -
  have sfE: "Subfield E" and FE: "F ⊆ E" and EK: "E ⊆ K"
    using intermediate_data by blast+
  obtain theta where thetaK: "theta ∈ K" and prim: "primitive_element F K theta"
    using finite_separable_extension_is_simple[OF finite separable] by blast
  have algtheta: "algebraic_over F theta"
    by (rule T.finite_extension_algebraic[OF thetaK])
  define p where "p ≡ minpoly F theta"
  define R where "R ≡ {r. poly p r = 0}"
  obtain pF: "p ∈ poly_over F" and p0: "p ≠ 0"
    using T.base.minpoly_nonzero T.base.minpoly_over algtheta p_def by presburger
  have p0: "p ≠ 0"
    unfolding p_def by (rule T.base.minpoly_nonzero[OF algtheta])
  have rootsK: "R ⊆ K"
    using irreducible_over_minpoly normal_extensionD [OF normal pF]
    using R_def T.base.Subfield_axioms T.base.minpoly_root algtheta p_def thetaK by fastforce
  have thetaR: "theta ∈ R"
    unfolding R_def p_def using T.base.minpoly_root[OF algtheta] by simp
  have Kgen: "K = generate_field (E ∪ R)"
  proof (rule subset_antisym)
    have "K = generate_field (F ∪ {theta})"
      using T.base.eval_img_eq_generate_field algtheta prim primitive_elementD by blast
    also have "... ⊆ generate_field (E ∪ R)"
      by (rule generate_field_mono) (use FE thetaR in auto)
    finally show "K ⊆ generate_field (E ∪ R)" .
    show "generate_field (E ∪ R) ⊆ K"
      by (simp add: T.ext.Subfield_axioms generate_field_least local.EK rootsK)
  qed
  have algR: "⋀r. poly p r = 0 ⟹ algebraic_over E r"
    using R_def TEK.finite_extension_algebraic rootsK by blast
  have Kgen': "K = generate_field (E ∪ {r. poly p r = 0})"
    using Kgen unfolding R_def .
  have finR': "finite {r. poly p r = 0}"
    by (simp add: p0 poly_roots_finite)
  have image_subset: "galois_restriction K E F ` field_auto K F ⊆ field_auto E F"
    using T.ext.Subfield_axioms gal_res_mem intermediate_data stable by auto
  show ?thesis
  proof
    show "field_auto E F ⊆ galois_restriction K E F ` field_auto K F"
    proof
      fix tau assume tau: "tau ∈ field_auto E F"
      obtain sigma where sigma: "sigma ∈ field_auto K F"
        and agree: "∀x∈E. sigma x = tau x"
        using galois_restriction_surjective[OF sfE T.base.Subfield_axioms FE pF
            Kgen' finR' algR alg_closed_imp_poly_has_root tau]
        by blast
      have restrict_eq': "restrict sigma E = restrict tau E"
        by (rule restrict_ext) (use agree in simp)
      have tauPiE: "tau ∈ E →⇩E E"
        using tau by (simp only: field_auto_mem_iff)
      have restrict_tau: "restrict tau E = tau" by (rule PiE_restrict[OF tauPiE])
      show "tau ∈ galois_restriction K E F ` field_auto K F"
        using sigma sigma restrict_eq' restrict_tau by auto
    qed
  qed (use image_subset in blast)
qed

context
  assumes normal_intermediate: "normal_extension E F"
begin

lemma stable_intermediate:
  "⋀σ. σ ∈ field_auto K F ⟹ σ ` E = E"
  using iffD1[OF finite_galois_normal_iff_stable normal_intermediate] by blast

lemma restriction_image:
  "galois_restriction K E F ` field_auto K F = field_auto E F"
  by (rule finite_galois_restriction_image[OF stable_intermediate])

interpretation restriction: group_epimorphism "galois_restriction K E F"
    "field_auto K F" "compose K" "identity K"
    "field_auto E F" "compose E" "identity E"
  using galois_restriction_epimorphism[OF T.ext.Subfield_axioms]
  using intermediate_data restriction_image stable_intermediate by blast

theorem finite_galois_restriction_kernel: "restriction.Ker = field_auto K E"
  using intermediate_data
  unfolding galois_restriction_def
  by (simp add: T.ext.Subfield_axioms galois_restriction_Ker stable_intermediate)

text ‹The first isomorphism theorem gives
  @{text "Gal(K/F) / Gal(K/E) ≅ Gal(E/F)"}; the preceding kernel theorem identifies the
  factor-group kernel with the relative Galois group literally.›
theorem finite_galois_quotient_isomorphism:
  "(restriction.kernel.Factor_Group, restriction.kernel.quotient_composition, restriction.kernel.Class (identity K))
   ≅⇩G
   (field_auto E F, compose E, identity E)"
  using restriction.first_isomorphism restriction_image by argo

end

end

end

end