Theory Galois_Action

section ‹The Galois Group Acts on the Roots›

theory Galois_Action
  imports Galois_Transitivity Symmetric_Generation Sym_Not_Solvable
begin

text ‹A field automorphism (an element of @{const field_auto}) is, in particular, a
  field homomorphism on its subfield domain.›
lemma field_auto_imp_field_hom_on:
  assumes K: "Subfield K" and s: "σ ∈ field_auto K F"
  shows "field_hom_on K σ"
  using K s by (rule field_auto_as_hom)

text ‹An automorphism fixing @{term F} maps a root in @{term K} of an @{term F}-polynomial to a
  root: it permutes the root set.›
lemma field_auto_maps_root:
  assumes K: "Subfield K" and sfF: "Subfield F" and FK: "F ⊆ K"
    and s: "σ ∈ field_auto K F" and Phi: "Phi ∈ poly_over F"
    and r: "r ∈ K" and root: "poly Phi r = 0"
  shows "poly Phi (σ r) = 0"
  using hom_preserves_roots[OF field_auto_imp_field_hom_on sfF FK _ Phi r root]
  using K field_auto_mem_iff s by blast

text ‹The Galois group acts on the root set by restriction.  We package this as a
  @{locale Group_Action} of @{term "field_auto K F"} on the finite root set @{term X}.›

context
  fixes K F :: "'a :: field set" and Phi :: "'a poly" and X :: "'a set"
  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"
begin

lemma field_auto_image_root_subset:
  assumes s: "σ ∈ field_auto K F"
  shows "σ ` X ⊆ X"
  using FK K Phi XK Xdef field_auto_maps_root s sfF by blast

lemma field_auto_bij_on_root:
  assumes s: "σ ∈ field_auto K F"
  shows "bij_betw σ X X"
  unfolding bij_betw_def
proof 
  show "inj_on σ X" using XK
    by (meson bij_betw_imp_inj_on field_auto_mem_iff inj_on_subset s)
  show "σ ` X = X"
    by (meson ‹inj_on σ X› endo_inj_surj field_auto_image_root_subset finX s)
qed

lemma ga_sym:
  assumes s: "σ ∈ field_auto K F"
  shows "restrict σ X ∈ transformations.Sym X"
  by (simp add: bij_betw_imp_funcset field_auto_bij_on_root s transformations.Units_bij_betwD)

lemma ga_compose:
  assumes s: "σ ∈ field_auto K F" and t: "τ ∈ field_auto K F"
  shows "restrict (compose K σ τ) X = compose X (restrict σ X) (restrict τ X)"
  using assms XK field_auto_image_root_subset by (fastforce simp: compose_def)

lemma ga_unit: "restrict (identity K) X = identity X"
  using XK by force

lemma galois_group_action:
  "Group_Action (field_auto K F) (compose K) (identity K) (λσ. restrict σ X) X"
proof -
  interpret G: Group "field_auto K F" "compose K" "identity K"
    by (rule field_auto_group[OF K FK])
  interpret T: transformations X .
  show ?thesis
  proof
    fix σ assume s: "σ ∈ field_auto K F"
    show "restrict σ X ∈ transformations.Sym X"
      by (rule ga_sym[OF s])
  next
    fix σ τ
    assume s: "σ ∈ field_auto K F" and t: "τ ∈ field_auto K F"
    show "restrict (compose K σ τ) X =
        compose X (restrict σ X) (restrict τ X)"
      by (rule ga_compose[OF s t])
  next
    show "restrict (identity K) X = identity X"
      by (rule ga_unit)
  qed
qed

text ‹When the ambient field is generated by the base and the root set, the root action is
  faithful: an automorphism fixing every root fixes the generators and is therefore the identity.›
lemma galois_action_faithful:
  assumes Kgen: "K = generate_field (F ∪ X)"
  shows "∀σ ∈ field_auto K F.
      (∀x∈X. restrict σ X x = x) ⟶ σ = identity K"
proof (intro ballI impI)
  fix σ
  assume s: "σ ∈ field_auto K F"
    and triv: "∀x∈X. restrict σ X x = x"
  have fixX: "⋀x. x ∈ X ⟹ σ x = x"
    using triv by (simp add: restrict_apply')
  have allfix: "∀x ∈ K. σ x = x"
    ― ‹The theory prefix is needed: ‹Complex_Field_Extension› declares a
      \<^typ>‹complex›-specific theorem of the same name, which shadows the generic one here.›
    using Galois_Automorphism.field_auto_faithful[OF Kgen s fixX] by force
  have sext: "σ ∈ K →⇩E K"
    using s by (simp only: field_auto_mem_iff)
  with allfix show "σ = identity K"
    by (metis PiE_restrict restrict_ext)
qed

lemma finite_galois_group:
  assumes Kgen: "K = generate_field (F ∪ X)"
  shows "finite (field_auto K F)"
proof -
  interpret GA: Group_Action "field_auto K F" "compose K" "identity K" "λσ. restrict σ X" X
    by (rule galois_group_action)
  ― ‹The action on the roots is faithful.›
  have faith: "GA.faithful"
    unfolding GA.faithful_def
    by (rule galois_action_faithful[OF Kgen])
    ― ‹Faithfulness gives an injection into the finite symmetric group on @{term X}.›
  have inj0: "inj_on (restrict (λσ. restrict σ X) (field_auto K F)) (field_auto K F)"
    using faith by (rule GA.faithful_inj)
  have inj: "inj_on (λσ. restrict σ X) (field_auto K F)"
    using inj0 inj_on_restrict_eq by blast
  have finSym: "finite (transformations.Sym X)"
    by (metis GA.mem_UnitsD finX finite_PiE finite_subset subsetI)
  show ?thesis using inj GA.hom_closed finSym inj_on_finite by blast
qed

end

text ‹Compatibility wrapper for the historical complex-only spelling.  The generic theorem uses
  @{const generate_field}; @{const gen_subfield} is the same construction on @{typ complex} and
  remains available to existing clients.›
lemma finite_field_auto:
  fixes K F :: "complex set" and Phi :: "complex poly" and X :: "complex set"
  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 Kgen: "K = gen_subfield (F ∪ X)"
  shows "finite (field_auto K F)"
proof -
  have Kgen': "K = generate_field (F ∪ X)"
    using Kgen by (simp add: gen_subfield_eq_generate_field)
  show ?thesis
    by (rule finite_galois_group[OF K sfF FK Phi Xdef XK finX Kgen'])
qed

text ‹Transitivity of the Galois action on the roots of an irreducible polynomial: any root
  is carried to any other by some @{term F}-automorphism (via @{thm [source]
  galois_transitive_irreducible} and the bridge @{thm [source] field_hom_on_imp_field_auto}).›
lemma galois_action_transitive:
  fixes F :: "'a :: field set" and Phi :: "'a poly" and X :: "'a set"
  assumes sfF: "Subfield F"
    and finX: "finite X"
    and Phi: "Phi ∈ poly_over F"
    and irr: "irreducible_over F Phi"
    and Xdef: "X = {r. poly Phi r = 0}"
    and closed: "⋀q :: 'a poly. 0 < degree q ⟹ ∃b. poly q b = 0"
    and a: "a ∈ X" and b: "b ∈ X"
  defines "K ≡ generate_field (F ∪ X)"
  shows "∃σ∈field_auto K F. restrict σ X a = b"
proof -
  have phinz: "Phi ≠ 0" using irr by (simp add: irreducible_over_def)
  have algX: "algebraic_over F r" if "r ∈ X" for r
    using that Phi phinz Xdef unfolding algebraic_over_def by auto
  have XK: "X ⊆ K" unfolding K_def using subset_generate_field by blast
  have aK: "a ∈ K" using a XK by blast
  obtain σ where hom: "field_hom_on K σ" and sab: "σ a = b"
    and fixF: "∀x∈F. σ x = x" and onto: "σ ` K = K"
    using galois_transitive_irreducible[OF sfF finX algX Phi irr Xdef closed a b]
    unfolding K_def by blast
  have FK: "F ⊆ K" unfolding K_def using subset_generate_field by blast
  have aut: "restrict σ K ∈ field_auto K F"
    using field_hom_on_imp_field_auto[OF hom onto _ FK] fixF by blast
  have "restrict (restrict σ K) X a = b"
    using aK a sab XK by simp
  then show ?thesis using aut by blast
qed

end