Theory Galois_Transitivity
section ‹Transitivity of the Galois Action on the Roots›
theory Galois_Transitivity
imports Iso_Extension_Tower
begin
text ‹
The capstone of the iso-extension development: for a polynomial @{term Phi} over a base
subfield @{term F} whose root set @{term R} is finite and consists of elements algebraic
over @{term F}, any two roots related by the minimal polynomial of one of them are connected
by an @{term F}-fixing automorphism of the splitting field @{term "K = generate_field (F ∪ R)"}.
This is ∗‹transitivity› of the Galois action on the roots, the key input to identifying the
Galois group of an irreducible quintic with @{text "S⇩5"}.
The construction has three parts: a base isomorphism ‹F(a) ≅ F(b)› sending @{term a} to
@{term b} (the single-step @{thm [source] field_hom_on.iso_extension}); its extension across
the remaining roots (@{thm [source] field_hom_on_extend_finite}); and the observation that the
resulting embedding permutes the finite root set and therefore maps the splitting field onto
itself (@{thm [source] field_hom_on.image_generate_field_eq}), i.e.\ is an automorphism.
›
text ‹The identity is a homomorphism of any subfield --- the starting point of the tower.›
lemma field_hom_on_id:
assumes "Subfield K" shows "field_hom_on K (λx. x)"
proof -
interpret Subfield K by fact
show ?thesis by unfold_locales auto
qed
text ‹An endomorphism fixing @{term F} pointwise leaves every polynomial over @{term F}
unchanged under @{term map_poly}.›
lemma map_poly_fix:
fixes f :: "'a :: field ⇒ 'a"
assumes hom: "field_hom_on K f" and sfF: "Subfield F"
and p: "p ∈ poly_over F" and fixF: "⋀x. x ∈ F ⟹ f x = x"
shows "map_poly f p = p"
proof (rule poly_eqI)
fix n
have cF: "coeff p n ∈ F" using p by (rule Subfield.poly_over_coeff[OF sfF])
have "coeff (map_poly f p) n = f (coeff p n)"
by (rule field_hom_on.coeff_map_poly_f[OF hom])
also have "… = coeff p n" using cF by (rule fixF)
finally show "coeff (map_poly f p) n = coeff p n" .
qed
text ‹Hence such an endomorphism sends a root of @{term Phi} to a root of @{term Phi}.›
lemma hom_preserves_roots:
fixes f :: "'a :: field ⇒ 'a"
assumes hom: "field_hom_on K f" and sfF: "Subfield F" and FK: "F ⊆ K"
and fixF: "⋀x. x ∈ F ⟹ f x = x"
and Phi: "Phi ∈ poly_over F" and r: "r ∈ K" and root: "poly Phi r = 0"
shows "poly Phi (f r) = 0"
proof -
have PhiK: "Phi ∈ poly_over K"
using Phi poly_over_mono[OF FK] by blast
have "poly Phi (f r) = poly (map_poly f Phi) (f r)"
using map_poly_fix[OF hom sfF Phi fixF] by simp
also have "… = f (poly Phi r)"
by (rule field_hom_on.poly_map_poly_hom[OF hom PhiK r])
also have "… = 0" using root field_hom_on.hom_0[OF hom] by simp
finally show ?thesis .
qed
theorem galois_transitive:
fixes F :: "'a :: field set"
assumes sfF: "Subfield F"
and finR: "finite R"
and algR: "⋀r. r ∈ R ⟹ algebraic_over F r"
and Phi: "Phi ∈ poly_over F"
and rootsR: "R = {r. poly Phi r = 0}"
and closed: "⋀q :: 'a poly. 0 < degree q ⟹ ∃b. poly q b = 0"
and a: "a ∈ R" and b: "b ∈ R"
and m: "is_minpoly F a m" and mb: "poly m b = 0"
defines "K ≡ generate_field (F ∪ R)"
shows "∃σ. field_hom_on K σ ∧ σ a = b ∧ (∀x∈F. σ x = x) ∧ σ ` K = K"
proof -
interpret F: field_hom_on F "λx. x" by (rule field_hom_on_id[OF sfF])
have alga: "algebraic_over F a" using a by (rule algR)
have mapm: "map_poly (λx. x) m = m" by (intro poly_eqI) (simp add: coeff_map_poly)
have rootb: "poly (map_poly (λx. x) m) b = 0" unfolding mapm by (rule mb)
obtain g0 where g0: "field_hom_on (eval_img F a) g0" "g0 a = b" "∀x∈F. g0 x = x"
using F.iso_extension[OF alga m rootb] by blast
define E where "E = eval_img F a"
have sfE: "Subfield E" unfolding E_def by (rule Subfield.subfield_eval_img[OF sfF alga])
have FsubE: "F ⊆ E" unfolding E_def using Subfield.eval_img_base[OF sfF] by auto
have algRE: "⋀r. r ∈ R - {a} ⟹ algebraic_over E r"
using algR FsubE by (auto intro: algebraic_over_mono)
have finRa: "finite (R - {a})" using finR by simp
obtain g where g: "field_hom_on (generate_field (E ∪ (R - {a}))) g" "∀x∈E. g x = g0 x"
using field_hom_on_extend_finite[OF closed finRa g0(1)[folded E_def] algRE] by blast
have Edef: "E = generate_field (F ∪ {a})"
unfolding E_def by (rule Subfield.eval_img_eq_generate_field[OF sfF alga])
have domK: "generate_field (E ∪ (R - {a})) = K"
proof -
have "generate_field (E ∪ (R - {a})) = generate_field (generate_field (F ∪ {a}) ∪ (R - {a}))"
by (simp add: Edef)
also have "… = generate_field ((F ∪ {a}) ∪ (R - {a}))"
by (rule generate_field_Un_collapse1)
also have "(F ∪ {a}) ∪ (R - {a}) = F ∪ R" using a by auto
finally show ?thesis by (simp add: K_def)
qed
have homg: "field_hom_on K g" using g(1) domK by simp
interpret G: field_hom_on K g by (rule homg)
have gfixF: "⋀x. x ∈ F ⟹ g x = x"
using g(2) g0(3) FsubE by auto
have gab: "g a = b"
proof -
have "a ∈ E" unfolding E_def using Subfield.eval_img_self[OF sfF] by auto
then have "g a = g0 a" using g(2) by simp
then show ?thesis using g0(2) by simp
qed
have RsubK: "R ⊆ K"
unfolding K_def using subset_generate_field by blast
have FsubK: "F ⊆ K"
unfolding K_def using subset_generate_field by blast
have gR_sub: "g ` R ⊆ R"
proof
fix y assume "y ∈ g ` R"
then obtain r where r: "r ∈ R" "y = g r" by blast
have rK: "r ∈ K" using r(1) RsubK by blast
have "poly Phi r = 0" using r(1) unfolding rootsR by blast
then have "poly Phi (g r) = 0"
using hom_preserves_roots[OF homg sfF FsubK gfixF Phi rK] by blast
then have "g r ∈ R" unfolding rootsR by blast
then show "y ∈ R" using r(2) by simp
qed
have gR_eq: "g ` R = R"
proof -
have "inj_on g R" using G.inj_on RsubK by (rule inj_on_subset)
then show ?thesis using gR_sub finR by (simp add: endo_inj_surj)
qed
have gF_eq: "g ` F = F"
proof
show "g ` F ⊆ F" using gfixF by auto
show "F ⊆ g ` F" using gfixF by force
qed
have FRsubK: "F ∪ R ⊆ K" using FsubK RsubK by blast
have "g ` K = g ` generate_field (F ∪ R)" by (simp add: K_def)
also have "… = generate_field (g ` (F ∪ R))"
by (rule G.image_generate_field_eq[OF FRsubK])
also have "g ` (F ∪ R) = F ∪ R" using gF_eq gR_eq by (simp add: image_Un)
also have "generate_field (F ∪ R) = K" by (simp add: K_def)
finally have gK: "g ` K = K" .
show ?thesis using homg gab gfixF gK by blast
qed
text ‹For an ∗‹irreducible› polynomial the minimal-polynomial hypothesis is automatic, so the
Galois action is transitive on its roots: any two roots are related by an @{term F}-fixing
automorphism of the splitting field.›
corollary galois_transitive_irreducible:
fixes F :: "'a :: field set"
assumes sfF: "Subfield F"
and finR: "finite R"
and algR: "⋀r. r ∈ R ⟹ algebraic_over F r"
and Phi: "Phi ∈ poly_over F"
and irr: "irreducible_over F Phi"
and rootsR: "R = {r. poly Phi r = 0}"
and closed: "⋀q :: 'a poly. 0 < degree q ⟹ ∃b. poly q b = 0"
and a: "a ∈ R" and b: "b ∈ R"
defines "K ≡ generate_field (F ∪ R)"
shows "∃σ. field_hom_on K σ ∧ σ a = b ∧ (∀x∈F. σ x = x) ∧ σ ` K = K"
proof -
have alga: "algebraic_over F a" using a by (rule algR)
obtain m where m: "is_minpoly F a m" using Subfield.minpoly_exists[OF sfF alga] by blast
have pa: "poly Phi a = 0" using a unfolding rootsR by blast
have pb: "poly Phi b = 0" using b unfolding rootsR by blast
have mb: "poly m b = 0"
by (rule Subfield.irreducible_over_root_is_minpoly_root[OF sfF irr Phi m pa pb])
show ?thesis
unfolding K_def
by (rule galois_transitive[OF sfF finR algR Phi rootsR closed a b m mb])
qed
subsection ‹Rational Subfields and Irreducibility over the Rationals›
text ‹A complex polynomial all of whose coefficients are rational is the ‹of_rat›-image of a
rational polynomial.›
lemma poly_over_Rats_imp_map_of_rat:
assumes "p ∈ poly_over (ℚ :: complex set)"
shows "∃r :: rat poly. p = map_poly of_rat r"
using assms by (meson Rats_0 poly_over_iff_aux ratpolyE)
lemma map_poly_of_rat_mult:
"map_poly of_rat (a * b) = (map_poly of_rat a :: complex poly) * map_poly of_rat b"
by (intro poly_eqI) (simp add: coeff_map_poly of_rat_mult of_rat_sum coeff_mult)
lemma map_poly_of_rat_inj: "inj (map_poly of_rat :: rat poly ⇒ complex poly)"
by (intro injI poly_eqI) (metis coeff_map_poly of_rat_0 of_rat_eq_iff)
lemma degree_map_poly_of_rat:
"degree (map_poly of_rat r :: complex poly) = degree r"
by (simp add: degree_map_poly)
text ‹Irreducibility of a rational polynomial transfers to irreducibility ∗‹over @{term ℚ}›
of its complex image: a factorisation over @{term ℚ} pulls back along the injective ring
homomorphism @{term "map_poly of_rat"} to a factorisation of the rational polynomial.›
lemma irreducible_imp_irreducible_over_Rats:
fixes r :: "rat poly"
assumes irr: "irreducible r" and deg: "degree r > 0"
shows "irreducible_over (ℚ :: complex set) (map_poly of_rat r)"
unfolding irreducible_over_def
proof (intro conjI allI impI)
show "map_poly of_rat r ≠ (0 :: complex poly)"
by (metis deg degree_0 degree_map_poly_of_rat not_less_zero)
show "0 < degree (map_poly of_rat r :: complex poly)"
using deg by (simp add: degree_map_poly_of_rat)
next
fix b c :: "complex poly"
assume bover: "b ∈ poly_over ℚ" and cover: "c ∈ poly_over ℚ"
and eq: "map_poly of_rat r = b * c"
obtain b' where b': "b = map_poly of_rat b'" using bover poly_over_Rats_imp_map_of_rat by blast
obtain c' where c': "c = map_poly of_rat c'" using cover poly_over_Rats_imp_map_of_rat by blast
have "(map_poly of_rat r :: complex poly) = map_poly of_rat (b' * c')"
by (simp add: b' c' eq map_poly_of_rat_mult)
then have rbc: "r = b' * c'" using map_poly_of_rat_inj by (simp add: inj_eq)
show "degree b = 0 ∨ degree c = 0"
using irreducibleD[OF irr rbc] b' c' degree_map_poly_of_rat poly_dvd_1 by auto
qed
end