Theory Sym_Groups
theory Sym_Groups
imports
"HOL-Combinatorics.Cycles"
Solvable_Groups
begin
section ‹Symmetric Groups›
subsection ‹Definitions›
abbreviation inv' :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a)"
where "inv' f ≡ Hilbert_Choice.inv f"
definition sym_group :: "nat ⇒ (nat ⇒ nat) monoid"
where "sym_group n = ⦇ carrier = { p. p permutes {1..n} }, mult = (∘), one = id ⦈"
definition alt_group :: "nat ⇒ (nat ⇒ nat) monoid"
where "alt_group n = (sym_group n) ⦇ carrier := { p. p permutes {1..n} ∧ evenperm p } ⦈"
definition sign_img :: "int monoid"
where "sign_img = ⦇ carrier = { -1, 1 }, mult = (*), one = 1 ⦈"
subsection ‹Basic Properties›
lemma sym_group_carrier: "p ∈ carrier (sym_group n) ⟷ p permutes {1..n}"
unfolding sym_group_def by simp
lemma sym_group_mult: "mult (sym_group n) = (∘)"
unfolding sym_group_def by simp
lemma sym_group_one: "one (sym_group n) = id"
unfolding sym_group_def by simp
lemma sym_group_carrier': "p ∈ carrier (sym_group n) ⟹ permutation p"
unfolding sym_group_carrier permutation_permutes by auto
lemma alt_group_carrier: "p ∈ carrier (alt_group n) ⟷ p permutes {1..n} ∧ evenperm p"
unfolding alt_group_def by auto
lemma alt_group_mult: "mult (alt_group n) = (∘)"
unfolding alt_group_def using sym_group_mult by simp
lemma alt_group_one: "one (alt_group n) = id"
unfolding alt_group_def using sym_group_one by simp
lemma alt_group_carrier': "p ∈ carrier (alt_group n) ⟹ permutation p"
unfolding alt_group_carrier permutation_permutes by auto
lemma sym_group_is_group: "group (sym_group n)"
using permutes_inv permutes_inv_o(2)
by (auto intro!: groupI
simp add: sym_group_def permutes_compose
permutes_id comp_assoc, blast)
lemma sign_img_is_group: "group sign_img"
unfolding sign_img_def by (unfold_locales, auto simp add: Units_def)
lemma sym_group_inv_closed:
assumes "p ∈ carrier (sym_group n)" shows "inv' p ∈ carrier (sym_group n)"
using assms permutes_inv sym_group_def by auto
lemma alt_group_inv_closed:
assumes "p ∈ carrier (alt_group n)" shows "inv' p ∈ carrier (alt_group n)"
using evenperm_inv[OF alt_group_carrier'] permutes_inv assms alt_group_carrier by auto
lemma sym_group_inv_equality [simp]:
assumes "p ∈ carrier (sym_group n)" shows "inv⇘(sym_group n)⇙ p = inv' p"
proof -
have "inv' p ∘ p = id"
using assms permutes_inv_o(2) sym_group_def by auto
hence "(inv' p) ⊗⇘(sym_group n)⇙ p = one (sym_group n)"
by (simp add: sym_group_def)
thus ?thesis using group.inv_equality[OF sym_group_is_group]
by (simp add: assms sym_group_inv_closed)
qed
lemma sign_is_hom: "sign ∈ hom (sym_group n) sign_img"
unfolding hom_def sign_img_def sym_group_mult using sym_group_carrier'[of _ n]
by (auto simp add: sign_compose, meson sign_def)
lemma sign_group_hom: "group_hom (sym_group n) sign_img sign"
using group_hom.intro[OF sym_group_is_group sign_img_is_group] sign_is_hom
by (simp add: group_hom_axioms_def)
lemma sign_is_surj:
assumes "n ≥ 2" shows "sign ` (carrier (sym_group n)) = carrier sign_img"
proof -
have "swapidseq (Suc 0) (Fun.swap (1 :: nat) 2 id)"
using comp_Suc[OF id, of "1 :: nat" "2"] by auto
hence "sign (Fun.swap (1 :: nat) 2 id) = (-1 :: int)"
by (simp add: sign_swap_id)
moreover have "Fun.swap (1 :: nat) 2 id ∈ carrier (sym_group n)" and "id ∈ carrier (sym_group n)"
using assms permutes_swap_id[of "1 :: nat" "{1..n}" 2] permutes_id
unfolding sym_group_carrier by auto
ultimately have "carrier sign_img ⊆ sign ` (carrier (sym_group n))"
using sign_id mk_disjoint_insert unfolding sign_img_def by fastforce
moreover have "sign ` (carrier (sym_group n)) ⊆ carrier sign_img"
using sign_is_hom unfolding hom_def by auto
ultimately show ?thesis
by blast
qed
lemma alt_group_is_sign_kernel:
"carrier (alt_group n) = kernel (sym_group n) sign_img sign"
unfolding alt_group_def sym_group_def sign_img_def kernel_def sign_def by auto
lemma alt_group_is_subgroup: "subgroup (carrier (alt_group n)) (sym_group n)"
using group_hom.subgroup_kernel[OF sign_group_hom]
unfolding alt_group_is_sign_kernel by blast
lemma alt_group_is_group: "group (alt_group n)"
using group.subgroup_imp_group[OF sym_group_is_group alt_group_is_subgroup]
by (simp add: alt_group_def)
lemma sign_iso:
assumes "n ≥ 2" shows "(sym_group n) Mod (carrier (alt_group n)) ≅ sign_img"
using group_hom.FactGroup_iso[OF sign_group_hom sign_is_surj[OF assms]]
unfolding alt_group_is_sign_kernel .
lemma alt_group_inv_equality:
assumes "p ∈ carrier (alt_group n)" shows "inv⇘(alt_group n)⇙ p = inv' p"
proof -
have "inv' p ∘ p = id"
using assms permutes_inv_o(2) alt_group_def by auto
hence "(inv' p) ⊗⇘(alt_group n)⇙ p = one (alt_group n)"
by (simp add: alt_group_def sym_group_def)
thus ?thesis using group.inv_equality[OF alt_group_is_group]
by (simp add: assms alt_group_inv_closed)
qed
lemma sym_group_card_carrier: "card (carrier (sym_group n)) = fact n"
using card_permutations[of "{1..n}" n] unfolding sym_group_def by simp
lemma alt_group_card_carrier:
assumes "n ≥ 2" shows "2 * card (carrier (alt_group n)) = fact n"
proof -
have "card (rcosets⇘sym_group n⇙ (carrier (alt_group n))) = 2"
using iso_same_card[OF sign_iso[OF assms]] unfolding FactGroup_def sign_img_def by auto
thus ?thesis
using group.lagrange[OF sym_group_is_group alt_group_is_subgroup, of n]
unfolding order_def sym_group_card_carrier by simp
qed
subsection ‹Transposition Sequences›
text ‹In order to prove that the Alternating Group can be generated by 3-cycles, we need
a stronger decomposition of permutations as transposition sequences than the one
proposed at Permutations.thy. ›
inductive swapidseq_ext :: "'a set ⇒ nat ⇒ ('a ⇒ 'a) ⇒ bool"
where
empty: "swapidseq_ext {} 0 id"
| single: "⟦ swapidseq_ext S n p; a ∉ S ⟧ ⟹ swapidseq_ext (insert a S) n p"
| comp: "⟦ swapidseq_ext S n p; a ≠ b ⟧ ⟹
swapidseq_ext (insert a (insert b S)) (Suc n) ((transpose a b) ∘ p)"
lemma swapidseq_ext_finite:
assumes "swapidseq_ext S n p" shows "finite S"
using assms by (induction) (auto)
lemma swapidseq_ext_zero:
assumes "finite S" shows "swapidseq_ext S 0 id"
using assms empty by (induct set: "finite", fastforce, simp add: single)
lemma swapidseq_ext_imp_swapidseq:
‹swapidseq n p› if ‹swapidseq_ext S n p›
using that proof induction
case empty
then show ?case
by (simp add: fun_eq_iff)
next
case (single S n p a)
then show ?case by simp
next
case (comp S n p a b)
then have ‹swapidseq (Suc n) (transpose a b ∘ p)›
by (simp add: comp_Suc)
then show ?case by (simp add: comp_def)
qed
lemma swapidseq_ext_zero_imp_id:
assumes "swapidseq_ext S 0 p" shows "p = id"
proof -
have "⟦ swapidseq_ext S n p; n = 0 ⟧ ⟹ p = id" for n
by (induction rule: swapidseq_ext.induct, auto)
thus ?thesis
using assms by simp
qed
lemma swapidseq_ext_finite_expansion:
assumes "finite B" and "swapidseq_ext A n p" shows "swapidseq_ext (A ∪ B) n p"
using assms
proof (induct set: "finite", simp)
case (insert b B) show ?case
using insert single[OF insert(3), of b] by (metis Un_insert_right insert_absorb)
qed
lemma swapidseq_ext_backwards:
assumes "swapidseq_ext A (Suc n) p"
shows "∃a b A' p'. a ≠ b ∧ A = (insert a (insert b A')) ∧
swapidseq_ext A' n p' ∧ p = (transpose a b) ∘ p'"
proof -
{ fix A n k and p :: "'a ⇒ 'a"
assume "swapidseq_ext A n p" "n = Suc k"
hence "∃a b A' p'. a ≠ b ∧ A = (insert a (insert b A')) ∧
swapidseq_ext A' k p' ∧ p = (transpose a b) ∘ p'"
proof (induction, simp)
case single thus ?case
by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
next
case comp thus ?case
by blast
qed }
thus ?thesis
using assms by simp
qed
lemma swapidseq_ext_backwards':
assumes "swapidseq_ext A (Suc n) p"
shows "∃a b A' p'. a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ swapidseq_ext A n p' ∧ p = (transpose a b) ∘ p'"
using swapidseq_ext_backwards[OF assms] swapidseq_ext_finite_expansion
by (metis Un_insert_left assms insertI1 sup.idem sup_commute swapidseq_ext_finite)
lemma swapidseq_ext_endswap:
assumes "swapidseq_ext S n p" "a ≠ b"
shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p ∘ (transpose a b))"
using assms
proof (induction n arbitrary: S p a b)
case 0 hence "p = id"
using swapidseq_ext_zero_imp_id by blast
thus ?case
using 0 by (metis comp_id id_comp swapidseq_ext.comp)
next
case (Suc n)
then obtain c d S' and p' :: "'a ⇒ 'a"
where cd: "c ≠ d" and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
and p: "p = transpose c d ∘ p'"
using swapidseq_ext_backwards[OF Suc(2)] by blast
hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' ∘ (transpose a b))"
by (simp add: Suc.IH Suc.prems(2))
hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
(transpose c d ∘ p' ∘ (transpose a b))"
by (metis cd fun.map_comp swapidseq_ext.comp)
thus ?case
by (metis S(1) p insert_commute)
qed
lemma swapidseq_ext_extension:
assumes "swapidseq_ext A n p" and "swapidseq_ext B m q" and "A ∩ B = {}"
shows "swapidseq_ext (A ∪ B) (n + m) (p ∘ q)"
using assms(1,3)
proof (induction, simp add: assms(2))
case single show ?case
using swapidseq_ext.single[OF single(3)] single(2,4) by auto
next
case comp show ?case
using swapidseq_ext.comp[OF comp(3,2)] comp(4)
by (metis Un_insert_left add_Suc insert_disjoint(1) o_assoc)
qed
lemma swapidseq_ext_of_cycles:
assumes "cycle cs" shows "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
using assms
proof (induct cs rule: cycle_of_list.induct)
case (1 i j cs) show ?case
using comp[OF 1(1), of i j] 1(2) by (simp add: o_def)
next
case "2_1" show ?case
by (simp, metis eq_id_iff empty)
next
case ("2_2" v) show ?case
using single[OF empty, of v] by (simp, metis eq_id_iff)
qed
lemma cycle_decomp_imp_swapidseq_ext:
assumes "cycle_decomp S p" shows "∃n. swapidseq_ext S n p"
using assms
proof (induction)
case empty show ?case
using swapidseq_ext.empty by blast
next
case (comp I p cs)
then obtain m where m: "swapidseq_ext I m p" by blast
hence "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
using comp.hyps(2) swapidseq_ext_of_cycles by blast
thus ?case using swapidseq_ext_extension m
using comp.hyps(3) by blast
qed
lemma swapidseq_ext_of_permutation:
assumes "p permutes S" and "finite S" shows "∃n. swapidseq_ext S n p"
using cycle_decomp_imp_swapidseq_ext[OF cycle_decomposition[OF assms]] .
lemma split_swapidseq_ext:
assumes "k ≤ n" and "swapidseq_ext S n p"
obtains q r U V where "swapidseq_ext U (n - k) q" and "swapidseq_ext V k r" and "p = q ∘ r" and "U ∪ V = S"
proof -
from assms
have "∃q r U V. swapidseq_ext U (n - k) q ∧ swapidseq_ext V k r ∧ p = q ∘ r ∧ U ∪ V = S"
(is "∃q r U V. ?split k q r U V")
proof (induct k rule: inc_induct)
case base thus ?case
by (metis diff_self_eq_0 id_o sup_bot.left_neutral empty)
next
case (step m)
then obtain q r U V
where q: "swapidseq_ext U (n - Suc m) q" and r: "swapidseq_ext V (Suc m) r"
and p: "p = q ∘ r" and S: "U ∪ V = S"
by blast
obtain a b r' V'
where "a ≠ b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (transpose a b) ∘ r'"
using swapidseq_ext_backwards[OF r] by blast
have "swapidseq_ext (insert a (insert b U)) (n - m) (q ∘ (transpose a b))"
using swapidseq_ext_endswap[OF q ‹a ≠ b›] step(2) by (metis Suc_diff_Suc)
hence "?split m (q ∘ (transpose a b)) r' (insert a (insert b U)) V'"
using r' S unfolding p by fastforce
thus ?case by blast
qed
thus ?thesis
using that by blast
qed
subsection ‹Unsolvability of Symmetric Groups›
text ‹We show that symmetric groups (\<^term>‹sym_group n›) are unsolvable for \<^term>‹n ≥ 5›.›
abbreviation three_cycles :: "nat ⇒ (nat ⇒ nat) set"
where "three_cycles n ≡
{ cycle_of_list cs | cs. cycle cs ∧ length cs = 3 ∧ set cs ⊆ {1..n} }"
lemma stupid_lemma:
assumes "length cs = 3" shows "cs = [ (cs ! 0), (cs ! 1), (cs ! 2) ]"
using assms by (auto intro!: nth_equalityI)
(metis Suc_lessI less_2_cases not_less_eq nth_Cons_0
nth_Cons_Suc numeral_2_eq_2 numeral_3_eq_3)
lemma three_cycles_incl: "three_cycles n ⊆ carrier (alt_group n)"
proof
fix p assume "p ∈ three_cycles n"
then obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs ⊆ {1..n}"
by auto
obtain a b c where cs_def: "cs = [ a, b, c ]"
using stupid_lemma[OF cs(3)] by auto
have "swapidseq (Suc (Suc 0)) ((transpose a b) ∘ (Fun.swap b c id))"
using comp_Suc[OF comp_Suc[OF id], of b c a b] cs(2) unfolding cs_def by simp
hence "evenperm p"
using cs(1) unfolding cs_def by (simp add: evenperm_unique)
thus "p ∈ carrier (alt_group n)"
using permutes_subset[OF cycle_permutes cs(4)]
unfolding alt_group_carrier cs(1) by simp
qed
lemma alt_group_carrier_as_three_cycles:
"carrier (alt_group n) = generate (alt_group n) (three_cycles n)"
proof -
interpret A: group "alt_group n"
using alt_group_is_group by simp
show ?thesis
proof
show "generate (alt_group n) (three_cycles n) ⊆ carrier (alt_group n)"
using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
next
show "carrier (alt_group n) ⊆ generate (alt_group n) (three_cycles n)"
proof
{ fix q :: "nat ⇒ nat" and a b c
assume "a ≠ b" "b ≠ c" "{ a, b, c } ⊆ {1..n}"
have "cycle_of_list [a, b, c] ∈ generate (alt_group n) (three_cycles n)"
proof (cases)
assume "c = a"
hence "cycle_of_list [ a, b, c ] = id"
by (simp add: swap_commute)
thus "cycle_of_list [ a, b, c ] ∈ generate (alt_group n) (three_cycles n)"
using one[of "alt_group n"] unfolding alt_group_one by simp
next
assume "c ≠ a"
have "distinct [a, b, c]"
using ‹a ≠ b› and ‹b ≠ c› and ‹c ≠ a› by auto
with ‹{ a, b, c } ⊆ {1..n}›
show "cycle_of_list [ a, b, c ] ∈ generate (alt_group n) (three_cycles n)"
by (intro incl, fastforce)
qed } note aux_lemma1 = this
{ fix S :: "nat set" and q :: "nat ⇒ nat"
assume seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S ⊆ {1..n}"
have "q ∈ generate (alt_group n) (three_cycles n)"
proof -
obtain a b q' where ab: "a ≠ b" "a ∈ S" "b ∈ S"
and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) ∘ q'"
using swapidseq_ext_backwards'[OF seq] by auto
obtain c d where cd: "c ≠ d" "c ∈ S" "d ∈ S"
and q: "q = (transpose a b) ∘ (Fun.swap c d id)"
using swapidseq_ext_backwards'[OF q'(1)]
swapidseq_ext_zero_imp_id
unfolding q'(2)
by fastforce
consider (eq) "b = c" | (ineq) "b ≠ c" by auto
thus ?thesis
proof cases
case eq then have "q = cycle_of_list [ a, b, d ]"
unfolding q by simp
moreover have "{ a, b, d } ⊆ {1..n}"
using ab cd S by blast
ultimately show ?thesis
using aux_lemma1[OF ab(1)] cd(1) eq by simp
next
case ineq
hence "q = cycle_of_list [ a, b, c ] ∘ cycle_of_list [ b, c, d ]"
unfolding q by (simp add: swap_nilpotent o_assoc)
moreover have "{ a, b, c } ⊆ {1..n}" and "{ b, c, d } ⊆ {1..n}"
using ab cd S by blast+
ultimately show ?thesis
using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
unfolding alt_group_mult by simp
qed
qed } note aux_lemma2 = this
fix p assume "p ∈ carrier (alt_group n)" then have p: "p permutes {1..n}" "evenperm p"
unfolding alt_group_carrier by auto
obtain m where m: "swapidseq_ext {1..n} m p"
using swapidseq_ext_of_permutation[OF p(1)] by auto
have "even m"
using swapidseq_ext_imp_swapidseq[OF m] p(2) evenperm_unique by blast
then obtain k where k: "m = 2 * k"
by auto
show "p ∈ generate (alt_group n) (three_cycles n)"
using m unfolding k
proof (induct k arbitrary: p)
case 0 then have "p = id"
using swapidseq_ext_zero_imp_id by simp
show ?case
using generate.one[of "alt_group n" "three_cycles n"]
unfolding alt_group_one ‹p = id› .
next
case (Suc m)
have arith: "2 * (Suc m) - (Suc (Suc 0)) = 2 * m" and "Suc (Suc 0) ≤ 2 * Suc m"
by auto
then obtain q r U V
where q: "swapidseq_ext U (2 * m) q" and r: "swapidseq_ext V (Suc (Suc 0)) r"
and p: "p = q ∘ r" and UV: "U ∪ V = {1..n}"
using split_swapidseq_ext[OF _ Suc(2), of "Suc (Suc 0)"] unfolding arith by metis
have "swapidseq_ext {1..n} (2 * m) q"
using UV q swapidseq_ext_finite_expansion[OF swapidseq_ext_finite[OF r] q] by simp
thus ?case
using eng[OF Suc(1) aux_lemma2[OF r], of q] UV unfolding alt_group_mult p by blast
qed
qed
qed
qed
theorem derived_alt_group_const:
assumes "n ≥ 5" shows "derived (alt_group n) (carrier (alt_group n)) = carrier (alt_group n)"
proof
show "derived (alt_group n) (carrier (alt_group n)) ⊆ carrier (alt_group n)"
using group.derived_in_carrier[OF alt_group_is_group] by simp
next
{ fix p assume "p ∈ three_cycles n" have "p ∈ derived (alt_group n) (carrier (alt_group n))"
proof -
obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs ⊆ {1..n}"
using ‹p ∈ three_cycles n› by auto
then obtain a b c where cs_def: "cs = [ a, b, c ]"
using stupid_lemma[OF cs(3)] by blast
have "card (set cs) = 3"
using cs(2-3)
by (simp add: distinct_card)
have "set cs ≠ {1..n}"
using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
then obtain d where d: "d ∉ set cs" "d ∈ {1..n}"
using cs(4) by blast
hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
using cs(2-3) by auto
hence "set (d # cs) ≠ {1..n}"
using assms unfolding sym[OF distinct_card[OF ‹cycle (d # cs)›]]
by (metis Suc_n_not_le_n eval_nat_numeral(3))
then obtain e where e: "e ∉ set (d # cs)" "e ∈ {1..n}"
using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym)
define q where "q = (Fun.swap d e id) ∘ (Fun.swap b c id)"
hence "bij q"
by (simp add: bij_comp)
moreover have "q b = c" and "q c = b"
using d(1) e(1) unfolding q_def cs_def by simp+
moreover have "q a = a"
using d(1) e(1) cs(2) unfolding q_def cs_def by auto
ultimately have "q ∘ p ∘ (inv' q) = cycle_of_list [ a, c, b ]"
using conjugation_of_cycle[OF cs(2), of q]
unfolding sym[OF cs(1)] unfolding cs_def by simp
also have " ... = p ∘ p"
using cs(2) unfolding cs(1) cs_def
by (simp add: comp_swap swap_commute transpose_comp_triple)
finally have "q ∘ p ∘ (inv' q) = p ∘ p" .
moreover have "bij p"
unfolding cs(1) cs_def by (simp add: bij_comp)
ultimately have p: "q ∘ p ∘ (inv' q) ∘ (inv' p) = p"
by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)
have "swapidseq (Suc (Suc 0)) q"
using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2) unfolding q_def cs_def by auto
hence "evenperm q"
using even_Suc_Suc_iff evenperm_unique by blast
moreover have "q permutes { d, e, b, c }"
unfolding q_def by (simp add: permutes_compose permutes_swap_id)
hence "q permutes {1..n}"
using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
ultimately have "q ∈ carrier (alt_group n)"
unfolding alt_group_carrier by simp
moreover have "p ∈ carrier (alt_group n)"
using ‹p ∈ three_cycles n› three_cycles_incl by blast
ultimately have "p ∈ derived_set (alt_group n) (carrier (alt_group n))"
using p alt_group_inv_equality unfolding alt_group_mult
by (metis (no_types, lifting) UN_iff singletonI)
thus "p ∈ derived (alt_group n) (carrier (alt_group n))"
unfolding derived_def by (rule incl)
qed } note aux_lemma = this
interpret A: group "alt_group n"
using alt_group_is_group .
have "generate (alt_group n) (three_cycles n) ⊆ derived (alt_group n) (carrier (alt_group n))"
using A.generate_subgroup_incl[OF _ A.derived_is_subgroup] aux_lemma by (meson subsetI)
thus "carrier (alt_group n) ⊆ derived (alt_group n) (carrier (alt_group n))"
using alt_group_carrier_as_three_cycles by simp
qed
corollary alt_group_is_unsolvable:
assumes "n ≥ 5" shows "¬ solvable (alt_group n)"
proof (rule ccontr)
assume "¬ ¬ solvable (alt_group n)"
then obtain m where "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = { id }"
using group.solvable_iff_trivial_derived_seq[OF alt_group_is_group] unfolding alt_group_one by blast
moreover have "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = carrier (alt_group n)"
using derived_alt_group_const[OF assms] by (induct m) (auto)
ultimately have card_eq_1: "card (carrier (alt_group n)) = 1"
by simp
have ge_2: "n ≥ 2"
using assms by simp
moreover have "2 = fact n"
using alt_group_card_carrier[OF ge_2] unfolding card_eq_1
by (metis fact_2 mult.right_neutral of_nat_fact)
ultimately have "n = 2"
by (metis antisym_conv fact_ge_self)
thus False
using assms by simp
qed
corollary sym_group_is_unsolvable:
assumes "n ≥ 5" shows "¬ solvable (sym_group n)"
proof -
interpret Id: group_hom "alt_group n" "sym_group n" id
using group.canonical_inj_is_hom[OF sym_group_is_group alt_group_is_subgroup] alt_group_def by simp
show ?thesis
using Id.inj_hom_imp_solvable alt_group_is_unsolvable[OF assms] by auto
qed
end