(* Title: HOL/Algebra/Sym_Groups.thy
Author: Paulo EmÃlio de Vilhena
*)
theory Sym_Groups
imports Cycles Group Coset Generated_Groups Solvable_Groups
begin
abbreviation inv' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
where "inv' f \<equiv> Hilbert_Choice.inv f"
definition sym_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid"
where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>"
definition sign_img :: "int monoid"
where "sign_img = \<lparr> carrier = { -1, 1 }, mult = ( * ), one = 1 \<rparr>"
lemma sym_group_is_group: "group (sym_group n)"
apply (rule groupI)
apply (simp_all add: sym_group_def permutes_compose permutes_id comp_assoc)
using permutes_inv permutes_inv_o(2) by blast
lemma sym_group_inv_closed:
assumes "p \<in> carrier (sym_group n)"
shows "inv' p \<in> carrier (sym_group n)"
using assms permutes_inv sym_group_def by auto
lemma sym_group_inv_equality:
assumes "p \<in> carrier (sym_group n)"
shows "inv\<^bsub>(sym_group n)\<^esub> p = inv' p"
proof -
have "inv' p \<circ> p = id"
using assms permutes_inv_o(2) sym_group_def by auto
hence "(inv' p) \<otimes>\<^bsub>(sym_group n)\<^esub> 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:
"group_hom (sym_group n) sign_img sign"
unfolding group_hom_def
proof (auto)
show "group (sym_group n)"
by (simp add: sym_group_is_group)
next
show "group sign_img"
unfolding sign_img_def group_def monoid_def group_axioms_def Units_def by auto
next
show "group_hom_axioms (sym_group n) sign_img sign"
unfolding sign_img_def group_hom_axioms_def sym_group_def hom_def
proof auto
show "\<And>x. sign x \<noteq> - 1 \<Longrightarrow> x permutes {Suc 0..n} \<Longrightarrow> sign x = 1"
by (meson sign_def)
show "\<And>x y. \<lbrakk> x permutes {Suc 0..n}; y permutes {Suc 0..n} \<rbrakk> \<Longrightarrow>
sign (x \<circ> y) = sign x * sign y"
using sign_compose permutation_permutes by blast
qed
qed
definition alt_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid"
where "alt_group n = (sym_group n) \<lparr> carrier := { p. p permutes {1..n} \<and> evenperm p } \<rparr>"
lemma alt_group_is_kernel_from_sign:
"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_group:
"group (alt_group n)"
proof -
have "subgroup (kernel (sym_group n) sign_img sign) (sym_group n)"
using group_hom.subgroup_kernel sign_is_hom by blast
thus ?thesis
using alt_group_def alt_group_is_kernel_from_sign group.subgroup_imp_group
sym_group_is_group by fastforce
qed
lemma alt_group_inv_closed:
assumes "p \<in> carrier (alt_group n)"
shows "inv' p \<in> carrier (alt_group n)"
using assms permutes_inv alt_group_def
using evenperm_inv permutation_permutes by fastforce
lemma alt_group_inv_equality:
assumes "p \<in> carrier (alt_group n)"
shows "inv\<^bsub>(alt_group n)\<^esub> p = inv' p"
proof -
have "inv' p \<circ> p = id"
using assms permutes_inv_o(2) alt_group_def by auto
hence "(inv' p) \<otimes>\<^bsub>(alt_group n)\<^esub> 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
subsection \<open>Transposition Sequences\<close>
text \<open>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 found at Permutations.thy\<close>
inductive swapidseq_ext :: "'a set \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
empty: "swapidseq_ext {} 0 id" |
single: "\<lbrakk> swapidseq_ext S n p; a \<notin> S \<rbrakk> \<Longrightarrow> swapidseq_ext (insert a S) n p" |
comp: "\<lbrakk> swapidseq_ext S n p; a \<noteq> b \<rbrakk> \<Longrightarrow>
swapidseq_ext (insert a (insert b S)) (Suc n) ((Fun.swap a b id) \<circ> p)"
lemma swapidseq_ext_finite:
assumes "swapidseq_ext S n p"
shows "finite S" using assms
apply (induction) by auto
lemma swapidseq_ext_zero_imp_id:
assumes "swapidseq_ext S 0 p"
shows "p = id"
proof -
{ fix S n and p :: "'a \<Rightarrow> 'a" assume "swapidseq_ext S n p" "n = 0"
hence "p = id"
apply (induction) by auto }
thus ?thesis using assms by auto
qed
lemma swapidseq_ext_zero:
assumes "finite S"
shows "swapidseq_ext S 0 id" using assms
proof (induct set: "finite")
case empty thus ?case using swapidseq_ext.empty .
next
case insert show ?case using swapidseq_ext.single[OF insert(3) insert(2)] .
qed
lemma swapidseq_ext_finite_expansion:
assumes "finite B" "swapidseq_ext A n p"
shows "swapidseq_ext (A \<union> B) n p" using assms
proof (induct set: "finite")
case empty thus ?case by simp
next
case insert show ?case
by (metis Un_insert_right insert.hyps(3) insert.prems insert_absorb single)
qed
lemma swapidseq_ext_backwards:
assumes "swapidseq_ext A (Suc n) p"
shows "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
swapidseq_ext A' n p' \<and> p = (Fun.swap a b id) \<circ> p'"
proof -
{ fix A n k and p :: "'a \<Rightarrow> 'a" assume "swapidseq_ext A n p" "n = Suc k"
hence "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
swapidseq_ext A' k p' \<and> p = (Fun.swap a b id) \<circ> p'"
proof (induction)
case empty thus ?case by simp
next
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_endswap:
assumes "swapidseq_ext S n p" "a \<noteq> b"
shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p \<circ> (Fun.swap a b id))" 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 \<Rightarrow> 'a"
where cd: "c \<noteq> d"
and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
and p: "p = (Fun.swap c d id) \<circ> p'"
using swapidseq_ext_backwards[OF Suc(2)] by blast
hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' \<circ> (Fun.swap a b id))"
by (simp add: Suc.IH Suc.prems(2))
hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
((Fun.swap c d id) \<circ> p' \<circ> (Fun.swap a b id))"
by (metis cd fun.map_comp swapidseq_ext.comp)
then show ?case by (metis S(1) p insert_commute)
qed
lemma swapidseq_ext_imp_swapiseq:
assumes "swapidseq_ext S n p"
shows "swapidseq n p" using assms
proof (induction)
case empty thus ?case by simp
case single show ?case using single(3) .
next
case comp thus ?case by (meson comp_Suc)
qed
lemma swapidseq_ext_extension:
assumes "swapidseq_ext A n p" "swapidseq_ext B m q" "A \<inter> B = {}"
shows "swapidseq_ext (A \<union> B) (n + m) (p \<circ> q)"
proof -
{ fix m and q :: "'a \<Rightarrow> 'a" and A B :: "'a set" assume "finite A" "swapidseq_ext B m q"
hence "swapidseq_ext (A \<union> B) m q"
proof (induct set: "finite")
case empty thus ?case by simp
next
case (insert a A') thus ?case
using swapidseq_ext.single[of "A' \<union> B" m q a]
by (metis Un_insert_left insert_absorb)
qed } note aux_lemma = this
from assms show ?thesis
proof (induct n arbitrary: p A)
case 0 thus ?case
using swapidseq_ext_zero_imp_id[OF 0(1)] aux_lemma[of A B m q] by (simp add: swapidseq_ext_finite)
next
case (Suc n)
obtain a b A' and p' :: "'a \<Rightarrow> 'a"
where A': "a \<noteq> b" "A = (insert a (insert b A'))"
and p': "swapidseq_ext A' n p'"
and p: "p = (Fun.swap a b id) \<circ> p'"
using swapidseq_ext_backwards[OF Suc(2)] by blast
hence "swapidseq_ext (A' \<union> B) (n + m) (p' \<circ> q)"
using Suc.hyps Suc.prems(3) assms(2) by fastforce
thus ?case using swapidseq_ext.comp[of "A' \<union> B" "n + m" "p' \<circ> q" a b]
by (metis Un_insert_left p A' add_Suc rewriteR_comp_comp)
qed
qed
lemma swapidseq_ext_of_cycles:
assumes "cycle cs"
shows "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)" using assms
proof (induction cs rule: cycle_of_list.induct)
case (1 i j cs) show ?case
proof (cases)
assume "cs = []" thus ?case
using swapidseq_ext.comp[OF swapidseq_ext.empty, of i j] "1.prems" by auto
next
assume "cs \<noteq> []" hence "length (j # cs) \<ge> 2"
using not_less_eq_eq by fastforce
hence IH: "swapidseq_ext (set (j # cs)) (length (j # cs) - 1) (cycle_of_list (j # cs))"
using "1.IH" "1.prems" by auto
thus ?case using swapidseq_ext.comp[OF IH, of i j]
by (metis "1.prems" cycle_of_list.simps(1) diff_Suc_1 distinct.simps(2)
distinct_length_2_or_more insert_absorb length_Cons list.simps(15))
qed
next
case "2_1" thus ?case using swapidseq_ext.empty
by (metis cycle_of_list.simps(2) diff_0_eq_0 empty_set list.size(3))
next
case ("2_2" v) thus ?case using swapidseq_ext.single[OF swapidseq_ext.empty, of v]
by (metis cycle_of_list.simps(3) diff_Suc_1 distinct.simps(2)
empty_set length_Cons list.simps(15) list.size(3))
qed
lemma cycle_decomp_imp_swapidseq_ext:
assumes "cycle_decomp S p"
shows "\<exists>n. swapidseq_ext S n p" using assms
proof (induction)
case empty
then 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_permutations:
assumes "p permutes S" "finite S"
shows "\<exists>n. swapidseq_ext S n p"
using assms cycle_decomp_imp_swapidseq_ext cycle_decomposition by blast
lemma split_swapidseq:
assumes "k \<le> n" "swapidseq n p"
shows "\<exists>q r. swapidseq k q \<and> swapidseq (n - k) r \<and> p = q \<circ> r"
proof -
{ fix n :: "nat" and p :: "'a \<Rightarrow> 'a" assume "swapidseq (Suc n) p"
hence "\<exists>a b q. a \<noteq> b \<and> swapidseq n q \<and> p = (Fun.swap a b id) \<circ> q"
proof (cases)
case comp_Suc thus ?thesis by auto
qed } note aux_lemma = this
from assms show ?thesis
proof (induction k)
case 0 thus ?case by simp
next
case (Suc k)
then obtain r q where 1: "swapidseq k q" "swapidseq (n - k) r" "p = q \<circ> r"
using Suc_leD by blast
then obtain a b r' where 2: "a \<noteq> b" "swapidseq (n - (Suc k)) r'" "r = (Fun.swap a b id) \<circ> r'"
using aux_lemma[of "n - (Suc k)" r] by (metis Suc.prems(1) Suc_diff_le diff_Suc_Suc)
have "swapidseq (Suc k) (q \<circ> (Fun.swap a b id))" using 1 2 by (simp add: swapidseq_endswap)
moreover have "p = (q \<circ> (Fun.swap a b id)) \<circ> r'"
using 1 2 fun.map_comp by blast
ultimately show ?case using 2 by blast
qed
qed
lemma split_swapidseq_ext:
assumes "k \<le> n" "swapidseq_ext S n p"
shows "\<exists>q r S1 S2. swapidseq_ext S1 k q \<and> swapidseq_ext S2 (n - k) r \<and> p = q \<circ> r \<and> S1 \<union> S2 = S"
using assms
proof (induction k)
case 0 have "finite S"
using "0.prems"(2) swapidseq_ext_finite by auto
have "swapidseq_ext {} 0 id \<and> swapidseq_ext S (n - 0) p \<and> p = id \<circ> p"
using swapidseq_ext.empty by (simp add: assms(2))
thus ?case by blast
next
case (Suc k)
then obtain q r S1 S2 where "swapidseq_ext S1 k q" "swapidseq_ext S2 (n - k) r" "p = q \<circ> r" "S1 \<union> S2 = S"
using Suc_leD by blast
then obtain a b S2' and r' :: "'a \<Rightarrow> 'a"
where S2': "a \<noteq> b" "S2 = (insert a (insert b S2'))"
and r': "swapidseq_ext S2' (n - (Suc k)) r'"
and r: "r = (Fun.swap a b id) \<circ> r'"
by (metis Suc.prems(1) Suc_diff_le diff_Suc_Suc swapidseq_ext_backwards)
have "swapidseq_ext (insert a (insert b S1)) (Suc k) (q \<circ> (Fun.swap a b id))"
by (simp add: S2'(1) \<open>swapidseq_ext S1 k q\<close> swapidseq_ext_endswap)
moreover have "p = (q \<circ> (Fun.swap a b id)) \<circ> r'"
by (simp add: \<open>p = q \<circ> r\<close> fun.map_comp r)
moreover have "(insert a (insert b S1)) \<union> S2' = S"
using S2'(2) \<open>S1 \<union> S2 = S\<close> by auto
ultimately show ?case using r r' by blast
qed
definition three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
where "three_cycles n \<equiv>
{ cycle_of_list cs | cs. cycle cs \<and> length cs = 3 \<and> set cs \<subseteq> {1..n} }"
lemma stupid_lemma:
assumes "length cs = 3"
shows "cs = [(cs ! 0), (cs ! 1), (cs ! 2)]"
proof (intro nth_equalityI)
show "length cs = length [(cs ! 0), (cs ! 1), (cs ! 2)]"
using assms by simp
show "\<forall> ia < length cs. cs ! ia = [(cs ! 0), (cs ! 1), (cs ! 2)] ! ia"
by (metis Suc_1 Suc_eq_plus1 add.left_neutral assms less_antisym
less_one nth_Cons' nth_Cons_Suc numeral_3_eq_3)
qed
lemma alt_group_as_three_cycles:
"carrier (alt_group n) = generate (alt_group n) (three_cycles n)"
proof
show "generate (alt_group n) (three_cycles n) \<subseteq> carrier (alt_group n)"
proof
{ fix p assume "p \<in> three_cycles n"
have "p \<in> carrier (alt_group n)"
proof -
from \<open>p \<in> three_cycles n\<close>
obtain cs where p: "p = cycle_of_list cs"
and cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
using three_cycles_def by blast
hence "p = (Fun.swap (cs ! 0) (cs ! 1) id) \<circ> (Fun.swap (cs ! 1) (cs ! 2) id)"
using stupid_lemma[OF cs(2)] p
by (metis comp_id cycle_of_list.simps(1) cycle_of_list.simps(3))
hence "evenperm p"
by (metis cs(1) distinct_length_2_or_more evenperm_comp
evenperm_swap permutation_swap_id stupid_lemma[OF cs(2)])
moreover have "permutation p" using p cs(1) cycle_permutes by simp
hence "p permutes {1..n}"
using id_outside_supp[OF cs(1)] p cs permutation_permutes unfolding permutes_def
using permutation_permutes permutes_def subsetCE by metis
ultimately show ?thesis by (simp add: alt_group_def)
qed } note aux_lemma = this
fix p assume "p \<in> generate (alt_group n) (three_cycles n)"
thus "p \<in> carrier (alt_group n)"
proof (induction)
case one thus ?case by (simp add: alt_group_is_group group.is_monoid)
case incl thus ?case using aux_lemma unfolding alt_group_def by auto
case inv thus ?case using aux_lemma by (simp add: alt_group_is_group) next
case eng thus ?case by (simp add: alt_group_is_group group.is_monoid monoid.m_closed)
qed
qed
next
show "carrier (alt_group n) \<subseteq> generate (alt_group n) (three_cycles n)"
proof
fix p assume p: "p \<in> carrier (alt_group n)"
show "p \<in> generate (alt_group n) (three_cycles n)"
proof -
{ fix q :: "nat \<Rightarrow> nat" and a b c
assume A: "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}" "q = cycle_of_list [a, b, c]"
have "q \<in> generate (alt_group n) (three_cycles n)"
proof (cases)
assume "c = a" hence "q = id" by (simp add: A(4) swap_commute)
thus "q \<in> generate (alt_group n) (three_cycles n)"
using generate.one[of "alt_group n"] by (simp add: alt_group_def sym_group_def)
next
assume "c \<noteq> a"
have "q \<in> (three_cycles n)"
unfolding three_cycles_def mem_Collect_eq
proof (intro exI conjI)
show "cycle [a,b,c]"
using A \<open>c \<noteq> a\<close> by auto
qed (use A in auto)
thus "q \<in> generate (alt_group n) (three_cycles n)"
by (simp add: generate.incl)
qed } note gen3 = this
{ fix S :: "nat set" and q :: "nat \<Rightarrow> nat" assume A: "swapidseq_ext S 2 q" "S \<subseteq> {1..n}"
have "q \<in> generate (alt_group n) (three_cycles n)"
proof -
obtain a b S' q' where ab: "a \<noteq> b" "S = (insert a (insert b S'))"
and q': "swapidseq_ext S' 1 q'" "q = (Fun.swap a b id) \<circ> q'"
using swapidseq_ext_backwards[of S 1 q] A(1) Suc_1 by metis
then obtain c d S'' where cd: "c \<noteq> d" "S' = (insert c (insert d S''))"
and q: "q = (Fun.swap a b id) \<circ> (Fun.swap c d id)"
using swapidseq_ext_backwards[of S' 0 q']
by (metis One_nat_def comp_id swapidseq_ext_zero_imp_id)
hence incl: "{ a, b, c, d } \<subseteq> {1..n}" using A(2) ab(2) by blast
thus ?thesis
proof (cases)
assume Eq: "b = c" hence "q = cycle_of_list [a, b, d]" by (simp add: q)
thus ?thesis using gen3 ab cd Eq incl by simp
next
assume In: "b \<noteq> c"
have "q = (cycle_of_list [a, b, c]) \<circ> (cycle_of_list [b, c, d])"
by (metis (no_types, lifting) comp_id cycle_of_list.simps(1)
cycle_of_list.simps(3) fun.map_comp q swap_id_idempotent)
moreover have "... = cycle_of_list [a, b, c] \<otimes>\<^bsub>alt_group n\<^esub> cycle_of_list [b, c, d]"
by (simp add: alt_group_def sym_group_def)
ultimately show ?thesis
by (metis (no_types) In generate.eng[where ?h1.0 = "cycle_of_list [a, b, c]"
and ?h2.0 = "cycle_of_list [b, c, d]"]
gen3[of a b c] gen3[of b c d] \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> insert_subset incl)
qed
qed } note gen3swap = this
have "p permutes {1..n}"
using p permutation_permutes unfolding alt_group_def by auto
then obtain l where "swapidseq_ext {1..n} l p" "swapidseq l p"
using swapidseq_ext_of_permutations swapidseq_ext_imp_swapiseq by blast
have "evenperm p" using p by (simp add: alt_group_def)
hence "even l" using \<open>swapidseq l p\<close> evenperm_unique by blast
then obtain k where "swapidseq_ext {1..n} (2 * k) p"
using dvd_def by (metis \<open>swapidseq_ext {1..n} l p\<close>)
thus "p \<in> generate (alt_group n) (three_cycles n)"
proof (induct k arbitrary: p)
case 0
hence "p = id" by (simp add: swapidseq_ext_zero_imp_id)
moreover have "id \<in> generate (alt_group n) (three_cycles n)"
using generate.one[of "alt_group n"] by (simp add: alt_group_def sym_group_def)
ultimately show ?case by blast
next
case (Suc k)
then obtain S1 S2 q r
where split: "swapidseq_ext S1 2 q" "swapidseq_ext S2 (2 * k) r" "p = q \<circ> r" "S1 \<union> S2 = {1..n}"
using split_swapidseq_ext[of 2 "2 * Suc k" "{1..n}" p] by auto
hence "r \<in> generate (alt_group n) (three_cycles n)"
using Suc.hyps swapidseq_ext_finite_expansion[of "{1..n}" S2 "2 * k" r]
by (metis (no_types, lifting) Suc.prems Un_commute sup.right_idem swapidseq_ext_finite)
moreover have "q \<in> generate (alt_group n) (three_cycles n)"
using gen3swap[OF split(1)] \<open>S1 \<union> S2 = {1..n}\<close> by auto
ultimately show ?case
using split generate.eng[of q "alt_group n" "three_cycles n" r]
by (metis (full_types) alt_group_def monoid.simps(1) partial_object.simps(3) sym_group_def)
qed
qed
qed
qed
lemma elts_from_card:
assumes "card S \<ge> n"
obtains f where "inj_on f {1..n}" "f ` {1..n} \<subseteq> S"
proof -
have "\<exists>f. inj_on f {1..n} \<and> f ` {1..n} \<subseteq> S" using assms
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
then obtain f where f: "inj_on f {1..n}" "f ` {1..n} \<subseteq> S"
using Suc_leD by blast
hence "card (f ` {1..n}) = n" by (simp add: card_image)
then obtain y where y: "y \<in> S - (f ` {1..n})"
by (metis Diff_eq_empty_iff Suc.prems \<open>f ` {1..n} \<subseteq> S\<close> not_less_eq_eq order_refl some_in_eq subset_antisym)
define f' where f': "f' = (\<lambda>x. (if x \<in> {1..n} then f x else y))"
hence "\<And>i j. \<lbrakk> i \<in> {1..Suc n}; j \<in> {1..Suc n} \<rbrakk> \<Longrightarrow> f' i = f' j \<Longrightarrow> i = j"
by (metis (no_types, lifting) DiffD2 f(1) y atLeastAtMostSuc_conv atLeastatMost_empty_iff2
card_0_eq card_atLeastAtMost diff_Suc_1 finite_atLeastAtMost image_eqI inj_onD insertE nat.simps(3))
moreover have "f' ` {1..n} \<subseteq> S \<and> f' (Suc n) \<in> S"
using f f' y by (simp add: image_subset_iff)
hence "f' ` {1..Suc n} \<subseteq> S" using f' by auto
ultimately show ?case unfolding inj_on_def by blast
qed
thus ?thesis using that by auto
qed
theorem derived_alt_group_is_cons:
assumes "n \<ge> 5"
shows "derived (alt_group n) (carrier (alt_group n)) = carrier (alt_group n)"
proof
show "derived (alt_group n) (carrier (alt_group n)) \<subseteq> carrier (alt_group n)"
by (simp add: alt_group_is_group group.derived_incl group.subgroup_self)
next
show "carrier (alt_group n) \<subseteq> derived (alt_group n) (carrier (alt_group n))"
proof -
have derived_set_in_carrier:
"derived_set (alt_group n) (carrier (alt_group n)) \<subseteq> carrier (alt_group n)"
proof
fix p assume "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
then obtain q r
where q: "q \<in> carrier (alt_group n)"
and r: "r \<in> carrier (alt_group n)"
and "p = q \<otimes>\<^bsub>(alt_group n)\<^esub> r \<otimes>\<^bsub>(alt_group n)\<^esub> (inv' q) \<otimes>\<^bsub>(alt_group n)\<^esub> (inv' r)"
using alt_group_inv_equality by auto
hence p: "p = q \<circ> r \<circ> (inv' q) \<circ> (inv' r)"
by (simp add: alt_group_def sym_group_def)
have "q permutes {1..n}" using q by (simp add: alt_group_def)
moreover have r_perm: "r permutes {1..n}" using r by (simp add: alt_group_def)
ultimately have "p permutes {1..n} \<and> evenperm p" using p
apply (simp add: permutes_compose permutes_inv)
by (metis evenperm_comp evenperm_inv finite_atLeastAtMost
permutation_compose permutation_inverse permutation_permutes)
thus "p \<in> carrier (alt_group n)" by (simp add: alt_group_def)
qed
have "three_cycles n \<subseteq> derived_set (alt_group n) (carrier (alt_group n))"
proof
fix p :: "nat \<Rightarrow> nat" assume "p \<in> three_cycles n"
then obtain cs
where cs: "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}" and p: "p = cycle_of_list cs"
unfolding three_cycles_def by blast
then obtain i j k where i: "i = cs ! 0" and j: "j = cs ! 1" and k: "k = cs ! 2"
and ijk: "cs = [i, j, k]" using stupid_lemma[OF cs(2)] by blast
have "p ^^ 2 = cycle_of_list [i, k, j]"
proof
fix l show "(p ^^ 2) l = cycle_of_list [i, k, j] l"
proof (cases)
assume "l \<notin> {i, j, k}"
hence "l \<notin> set cs \<and> l \<notin> set [i, k, j]" using ijk by auto
thus ?thesis
using id_outside_supp[of cs l] id_outside_supp[of "[i, j, k]" l] p o_apply
by (simp add: ijk numeral_2_eq_2)
next
assume "\<not> l \<notin> {i, j, k}" hence "l \<in> {i, j, k}" by simp
have "map ((cycle_of_list cs) ^^ 2) cs = rotate 2 cs"
using cyclic_rotation[of cs 2] cs by simp
also have " ... = rotate1 (rotate1 [i, j , k])"
by (metis One_nat_def Suc_1 funpow_0 ijk rotate_Suc rotate_def)
also have " ... = [k, i, j]" by simp
finally have "map ((cycle_of_list cs) ^^ 2) cs = [k, i, j]" .
hence "map (p ^^ 2) [i, j, k] = [k, i, j]" using p ijk by simp
moreover have "map (cycle_of_list [i, k, j]) [i, j, k] = [k, i, j]"
using cs(1) ijk by auto
ultimately show ?thesis using \<open>l \<in> {i, j, k}\<close> by auto
qed
qed
hence p2: "p ^^ 2 = (Fun.swap j k id) \<circ> (cycle_of_list [i, j, k]) \<circ> (inv' (Fun.swap j k id))"
using conjugation_of_cycle[of "[i, j, k]" "Fun.swap j k id"] cs(1) ijk by auto
have "card ({1..n} - {i, j, k}) \<ge> card {1..n} - card {i, j, k}"
by (meson diff_card_le_card_Diff finite.emptyI finite.insertI)
hence card_ge_two: "card ({1..n} - {i, j, k}) \<ge> 2"
using assms cs ijk by simp
then obtain f :: "nat \<Rightarrow> nat" where f: "inj_on f {1..2}" "f ` {1..2} \<subseteq> {1..n} - {i, j, k}"
using elts_from_card[OF card_ge_two] by blast
then obtain g h where gh: "g = f 1" "h = f 2" "g \<noteq> h"
by (metis Suc_1 atLeastAtMost_iff diff_Suc_1 diff_Suc_Suc inj_onD nat.simps(3) one_le_numeral order_refl)
hence g: "g \<in> {1..n} - {i, j, k}" and h: "h \<in> {1..n} - {i, j, k}" using f(2) gh(2) by force+
hence gh_simps: "g \<noteq> h \<and> g \<in> {1..n} \<and> h \<in> {1..n} \<and> g \<notin> {i, j, k} \<and> h \<notin> {i, j, k}"
using g gh(3) by blast
moreover have ijjk: "Fun.swap i j id = Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id)"
and jkij: "Fun.swap j k id \<circ> (Fun.swap i j id \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id) = Fun.swap g h (Fun.swap g h (Fun.swap i j (Fun.swap j k id)))"
by (simp_all add: comp_swap inv_swap_id)
moreover have "Fun.swap g h (Fun.swap i j id) = Fun.swap i j (Fun.swap g h id)"
by (metis (no_types) comp_id comp_swap gh_simps insert_iff swap_id_independent)
moreover have "Fun.swap i j (Fun.swap g h (Fun.swap j k id \<circ> id)) = Fun.swap g h (Fun.swap i j (Fun.swap j k id))"
by (metis (no_types) calculation(4) comp_id comp_swap)
moreover have "inj (Fun.swap j k id)" "bij (Fun.swap g h id)" "bij (Fun.swap j k id)"
by auto
moreover have "Fun.swap j k id \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id) = Fun.swap g h id"
by (metis (no_types) bij_betw_id bij_swap_iff comp_id comp_swap gh_simps insert_iff inv_swap_id o_inv_distrib swap_id_independent swap_nilpotent)
moreover have "Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id)) \<circ> inv' (Fun.swap j k id) = Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id)"
by (simp add: comp_swap inv_swap_id)
moreover have "Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id = Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id))"
by (simp add: comp_swap inv_swap_id)
moreover have "Fun.swap g h id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id) = Fun.swap j k id \<circ> (Fun.swap j k id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id)) \<circ> inv' (Fun.swap j k id)"
by (metis calculation(10) calculation(4) calculation(9) comp_assoc comp_id comp_swap swap_nilpotent)
ultimately have "Fun.swap i j (Fun.swap j k id) = Fun.swap j k id \<circ> Fun.swap g h id \<circ> (Fun.swap j k id \<circ> Fun.swap i j (Fun.swap j k id) \<circ> Fun.swap j k id) \<circ> inv' (Fun.swap j k id \<circ> Fun.swap g h id)"
by (simp add: comp_assoc)
then have final_step:
"p ^^ 2 = ((Fun.swap j k id) \<circ> (Fun.swap g h id)) \<circ>
(cycle_of_list [i, j, k]) \<circ>
(inv' ((Fun.swap j k id) \<circ> (Fun.swap g h id)))"
using ijjk jkij by (auto simp: p2)
define q where "q \<equiv> (Fun.swap j k id) \<circ> (Fun.swap g h id)"
hence "(p \<circ> p) = q \<circ> p \<circ> (inv' q)"
by (metis final_step One_nat_def Suc_1 comp_id funpow.simps(2) funpow_simps_right(1) ijk p)
hence "(p \<circ> p) \<circ> (inv' p) = q \<circ> p \<circ> (inv' q) \<circ> (inv' p)" by simp
hence 1: "p = q \<circ> p \<circ> (inv' q) \<circ> (inv' p)"
using p cycle_permutes[OF cs(1)] o_assoc[of p p "inv' p"]
by (simp add: permutation_inverse_works(2))
have "(Fun.swap j k id) \<circ> (Fun.swap g h id) permutes {1..n}"
by (metis cs(3) gh_simps ijk insert_subset list.simps(15) permutes_compose permutes_swap_id)
moreover have "evenperm ((Fun.swap j k id) \<circ> (Fun.swap g h id))"
by (metis cs(1) distinct_length_2_or_more evenperm_comp evenperm_swap gh(3) ijk permutation_swap_id)
ultimately have 2: "q \<in> carrier (alt_group n)"
by (simp add: alt_group_def q_def)
have 3: "p \<in> carrier (alt_group n)"
using alt_group_as_three_cycles generate.incl[OF \<open>p \<in> three_cycles n\<close>] by simp
from 1 2 3 show "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
using alt_group_is_group[of n] alt_group_inv_equality[OF 2] alt_group_inv_equality[OF 3]
unfolding alt_group_def sym_group_def by fastforce
qed
hence "generate (alt_group n) (three_cycles n) \<subseteq> derived (alt_group n) (carrier (alt_group n))"
unfolding derived_def
using group.mono_generate[OF alt_group_is_group[of n]] derived_set_in_carrier by simp
thus ?thesis using alt_group_as_three_cycles by blast
qed
qed
corollary alt_group_not_solvable:
assumes "n \<ge> 5"
shows "\<not> solvable (alt_group n)"
proof (rule ccontr)
assume "\<not> \<not> solvable (alt_group n)" hence "solvable (alt_group n)" by simp
then obtain k
where trivial_seq: "(derived (alt_group n) ^^ k) (carrier (alt_group n)) = { \<one>\<^bsub>alt_group n\<^esub> }"
using group.solvable_iff_trivial_derived_seq[OF alt_group_is_group[of n]] by blast
have "(derived (alt_group n) ^^ k) (carrier (alt_group n)) = (carrier (alt_group n))"
apply (induction k) using derived_alt_group_is_cons[OF assms] by auto
hence "carrier (alt_group n) = { \<one>\<^bsub>alt_group n\<^esub> }"
using trivial_seq by auto
hence singleton: "carrier (alt_group n) = { id }"
by (simp add: alt_group_def sym_group_def)
have "set [1 :: nat, 2, 3] \<subseteq> {1..n}" using assms by auto
moreover have "cycle [1 :: nat, 2, 3]" by simp
moreover have "length [1 :: nat, 2, 3] = 3" by simp
ultimately have "cycle_of_list [1 :: nat, 2, 3] \<in> three_cycles n"
unfolding three_cycles_def by blast
hence "cycle_of_list [1 :: nat, 2, 3] \<in> carrier (alt_group n)"
using alt_group_as_three_cycles by (simp add: generate.incl)
moreover have "map (cycle_of_list [1 :: nat, 2, 3]) [1 :: nat, 2, 3] = [2 :: nat, 3, 1]"
using cyclic_rotation[OF \<open>cycle [1 :: nat, 2, 3]\<close>, of 1] by simp
hence "cycle_of_list [1 :: nat, 2, 3] \<noteq> id"
by (metis list.map_id list.sel(1) numeral_One numeral_eq_iff semiring_norm(85))
ultimately show False using singleton by blast
qed
corollary sym_group_not_solvable:
assumes "n \<ge> 5"
shows "\<not> solvable (sym_group n)"
proof -
have "subgroup (kernel (sym_group n) sign_img sign) (sym_group n)"
using group_hom.subgroup_kernel sign_is_hom by blast
hence "subgroup (carrier (alt_group n)) (sym_group n)"
using alt_group_is_kernel_from_sign[of n] by simp
hence "group_hom (alt_group n) (sym_group n) id"
using group.canonical_inj_is_hom[OF sym_group_is_group[of n]] by (simp add: alt_group_def)
thus ?thesis
using group_hom.not_solvable[of "alt_group n" "sym_group n" id]
alt_group_not_solvable[OF assms] inj_on_id by blast
qed
end