Theory Abel_Ruffini

section ‹The Symmetric Group on the Roots and Non-Solvability›

theory Abel_Ruffini
  imports Galois_Action Action_To_Sn
begin

text ‹A subgroup of Sn p containing some p-cycle (conjugate to ncycle p) and some
  transposition is the whole group.›
lemma subgroup_with_cycle_transpose_eq_Sn:
  fixes p :: nat and q :: "nat ⇒ nat" and i j :: nat
  assumes p: "prime p" and H: "Subgroup H (Sn p) (∘) id"
    and q: "q ∈ Sn p"
    and c_in: "q ∘ ncycle p ∘ inv q ∈ H"
    and t_in: "Transposition.transpose i j ∈ H"
    and i: "i < p" and jj: "j < p" and ij: "i ≠ j"
  shows "H = Sn p"
proof -
  interpret G: Group "Sn p" "(∘)" id by (rule Group_Sn)
  interpret H: Subgroup H "Sn p" "(∘)" id by (rule H)
  have bq: "bij q" using q by (simp add: Sn_def permutes_bij)
  ― ‹Write the transposition as the same-conjugator form.›
  define a where "a = inv q i"
  define b where "b = inv q j"
  have qa: "q a = i" unfolding a_def using bq by (simp add: surj_f_inv_f bij_is_surj)
  have qb: "q b = j" unfolding b_def using bq by (simp add: surj_f_inv_f bij_is_surj)
  have qperm: "q permutes {0..<p}" using q by (simp add: Sn_iff)
  have ap: "a < p"
    using a_def i permutes_nat_inv_less qperm by presburger
  have bp: "b < p"
    using b_def jj permutes_nat_less permutes_nat_inv_less qperm by blast
  have ab: "a ≠ b" using ij qa qb by auto
  have t_eq: "Transposition.transpose i j = q ∘ Transposition.transpose a b ∘ inv q"
    using bq qa qb by (simp add: transpose_conjug)
  ― ‹Both generators lie in H, so the generated subgroup (= Sn p) is contained in H.›
  have gens_sub: "{q ∘ ncycle p ∘ inv q, q ∘ Transposition.transpose a b ∘ inv q} ⊆ H"
    using c_in t_in t_eq by auto
  have "Sn p = G.generate {q ∘ ncycle p ∘ inv q, q ∘ Transposition.transpose a b ∘ inv q}"
    using Sn_generated_conj_cycle_transpose[OF p q ap bp ab] by simp
  also have "… ⊆ H"
    using G.generate_mono G.generate_subgroup_eq H gens_sub by blast
  finally show ?thesis by blast
qed


text ‹The abstract group-theoretic heart of Abel--Ruffini: a finite group acting faithfully
  and transitively on a set of prime cardinality @{term "p ≥ 5"}, whose image in @{term "Sn p"}
  contains a transposition, is not solvable, because that image is then all of @{term "Sn p"},
  which is not solvable.›
theorem (in Group_Action) not_solvable_of_transitive_with_transposition:
  fixes e :: "nat ⇒ 'b" and p :: nat
  assumes ebij: "bij_betw e {0..<p} S"
    and p: "prime p" and p5: "5 ≤ p" and finG: "finite G"
    and faith: faithful
    and trans: "∃s∈S. orbit s = S"
    and transp: "∃i j. i < p ∧ j < p ∧ i ≠ j
                   ∧ Transposition.transpose i j ∈ (λg. pull p e (φ g)) ` G"
  shows "¬ Group.solvable G (⋅) 𝟭"
proof
  assume solv: "Group.solvable G (⋅) 𝟭"
  define Ψ where "Ψ = restrict (λg. pull p e (φ g)) G"
  define I where "I = (λg. pull p e (φ g)) ` G"
  ― ‹The transported action is an isomorphism of G onto the subgroup I of Sn p.›
  have iso: "group_isomorphism Ψ G (⋅) 𝟭 I (∘) id"
    unfolding Ψ_def I_def by (rule action_embeds_Sn[OF ebij faith])
  interpret Iso: group_isomorphism Ψ G "(⋅)" 𝟭 I "(∘)" id by (rule iso)
  interpret Hom: group_homomorphism Ψ G "(⋅)" 𝟭 "Sn p" "(∘)" id
    unfolding Ψ_def by (rule action_pull_hom[OF ebij])
  interpret G5: Group "Sn p" "(∘)" id by (rule Group_Sn)
  have finS: "finite S" using ebij bij_betw_finite by blast
  have cardS: "card S = p" using ebij bij_betw_same_card by (metis card_atLeastLessThan diff_zero)
  ― ‹p divides card G, by orbit-stabilizer with a full orbit.›
  obtain s0 where s0: "s0 ∈ S" and orb: "orbit s0 = S" using trans by blast
  have "card G = card (orbit s0) * card (stabilizer s0)"
    using s0 finG by (rule orbit_stabilizer_card)
  then have pdvd: "p dvd card G" using orb cardS by (metis dvd_triv_left)
  ― ‹Cauchy: an order-p element of G.›
  obtain g0 where g0: "g0 ∈ G" and g0ord: "grp.element_order g0 = p"
    using grp.Cauchy[OF p finG pdvd] by blast
  ― ‹Its image has the same order @{term p}, computed via the isomorphism (using the raw
    @{const Monoid.element_order} bridge so the orders match by name), and so is a p-cycle.›
  have psg0_in: "Ψ g0 ∈ I" unfolding I_def Ψ_def using g0 by auto
  have I_sub_Sn: "I ⊆ Sn p"
    using hom_closed ebij by (simp add: I_def image_subset_iff pull_in_Sn)
  have finI: "finite I" using I_sub_Sn finite_Sn finite_subset by blast
  have psg0_Sn: "Ψ g0 ∈ Sn p" using psg0_in I_sub_Sn by blast
  have img_ord: "Monoid.element_order (∘) id (Ψ g0) = p"
    using Iso.element_order_preserved'[OF finG finI g0] g0ord by simp
  obtain q where q: "q ∈ Sn p" and cyc: "Ψ g0 = q ∘ ncycle p ∘ inv q"
    using order_p_elt_conj_ncycle_order[OF p psg0_Sn img_ord] by blast
  ― ‹I is a subgroup of Sn p containing this p-cycle and (by hypothesis) a transposition.›
  have I_sub: "Subgroup I (Sn p) (∘) id"
    using Hom.image.Subgroup_axioms unfolding Ψ_def I_def by simp
  obtain i j where ij: "i < p" "j < p" "i ≠ j" and t_in: "Transposition.transpose i j ∈ I"
    using transp I_def by blast
  have c_in: "q ∘ ncycle p ∘ inv q ∈ I" using psg0_in cyc by simp
  have "I = Sn p"
    using subgroup_with_cycle_transpose_eq_Sn[OF p I_sub q c_in t_in ij] .
  ― ‹So G is isomorphic onto Sn p, which would make Sn p solvable --- contradiction.›
  then have "Group.solvable (Sn p) (∘) id"
    using Iso.solvable_image_epi[OF solv] by simp
  with Sn_not_solvable p5 show False by blast
qed

end