(* Title: HOL/Algebra/Solvable_Groups.thy Author: Paulo Emílio de Vilhena *) theory Solvable_Groups imports Generated_Groups begin section ‹Solvable Groups› subsection ‹Definitions› inductive solvable_seq :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ bool" for G where unity: "solvable_seq G { 𝟭⇘G⇙ }" | extension: "⟦ solvable_seq G K; K ⊲ (G ⦇ carrier := H ⦈); subgroup H G; comm_group ((G ⦇ carrier := H ⦈) Mod K) ⟧ ⟹ solvable_seq G H" definition solvable :: "('a, 'b) monoid_scheme ⇒ bool" where "solvable G ⟷ solvable_seq G (carrier G)" subsection ‹Solvable Groups and Derived Subgroups› text ‹We show that a group G is solvable iff the subgroup (derived G ^^ n) (carrier G) is trivial for a sufficiently large n. › lemma (in group) solvable_imp_subgroup: assumes "solvable_seq G H" shows "subgroup H G" using assms normal.axioms(1)[OF one_is_normal] by (induction) (auto) lemma (in group) augment_solvable_seq: assumes "subgroup H G" and "solvable_seq G (derived G H)" shows "solvable_seq G H" using extension[OF _ derived_subgroup_is_normal _ derived_quot_of_subgroup_is_comm_group] assms by simp theorem (in group) trivial_derived_seq_imp_solvable: assumes "subgroup H G" and "((derived G) ^^ n) H = { 𝟭 }" shows "solvable_seq G H" using assms proof (induct n arbitrary: H, simp add: unity[of G]) case (Suc n) thus ?case using augment_solvable_seq derived_is_subgroup[OF subgroup.subset] by (simp add: funpow_swap1) qed theorem (in group) solvable_imp_trivial_derived_seq: assumes "solvable_seq G H" shows "∃n. (derived G ^^ n) H = { 𝟭 }" using assms proof (induction) case unity have "(derived G ^^ 0) { 𝟭 } = { 𝟭 }" by simp thus ?case by blast next case (extension K H) obtain n where "(derived G ^^ n) K = { 𝟭 }" using solvable_imp_subgroup extension(1,5) by auto hence "(derived G ^^ (Suc n)) H ⊆ { 𝟭 }" using mono_exp_of_derived[OF derived_of_subgroup_minimal[OF extension(2-4)], of n] by (simp add: funpow_swap1) moreover have "{ 𝟭 } ⊆ (derived G ^^ (Suc n)) H" using subgroup.one_closed[OF exp_of_derived_is_subgroup[OF extension(3)], of "Suc n"] by auto ultimately show ?case by blast qed theorem (in group) solvable_iff_trivial_derived_seq: "solvable G ⟷ (∃n. (derived G ^^ n) (carrier G) = { 𝟭 })" using solvable_imp_trivial_derived_seq subgroup_self trivial_derived_seq_imp_solvable by (auto simp add: solvable_def) corollary (in group) solvable_subgroup: assumes "subgroup H G" and "solvable G" shows "solvable_seq G H" proof - obtain n where n: "(derived G ^^ n) (carrier G) = { 𝟭 }" using assms(2) solvable_imp_trivial_derived_seq by (auto simp add: solvable_def) show ?thesis proof (rule trivial_derived_seq_imp_solvable[OF assms(1), of n]) show "(derived G ^^ n) H = { 𝟭 }" using subgroup.one_closed[OF exp_of_derived_is_subgroup[OF assms(1)], of n] mono_exp_of_derived[OF subgroup.subset[OF assms(1)], of n] n by auto qed qed subsection ‹Short Exact Sequences› text ‹Even if we don't talk about short exact sequences explicitly, we show that given an injective homomorphism from a group H to a group G, if H isn't solvable the group G isn't neither. › theorem (in group_hom) solvable_img_imp_solvable: assumes "subgroup K G" and "inj_on h K" and "solvable_seq H (h ` K)" shows "solvable_seq G K" proof - obtain n where "(derived H ^^ n) (h ` K) = { 𝟭⇘H⇙ }" using solvable_imp_trivial_derived_seq assms(1,3) by auto hence "h ` ((derived G ^^ n) K) = { 𝟭⇘H⇙ }" unfolding exp_of_derived_img[OF subgroup.subset[OF assms(1)]] . moreover have "(derived G ^^ n) K ⊆ K" using G.mono_derived[of _ K] G.derived_incl[OF _ assms(1)] by (induct n) (auto) hence "inj_on h ((derived G ^^ n) K)" using inj_on_subset[OF assms(2)] by blast moreover have "{ 𝟭 } ⊆ (derived G ^^ n) K" using subgroup.one_closed[OF G.exp_of_derived_is_subgroup[OF assms(1)]] by blast ultimately show ?thesis using G.trivial_derived_seq_imp_solvable[OF assms(1), of n] by (metis (no_types, lifting) hom_one image_empty image_insert inj_on_image_eq_iff order_refl) qed corollary (in group_hom) inj_hom_imp_solvable: assumes "inj_on h (carrier G)" and "solvable H" shows "solvable G" using solvable_img_imp_solvable[OF _ assms(1)] G.subgroup_self solvable_subgroup[OF subgroup_img_is_subgroup assms(2)] unfolding solvable_def by simp theorem (in group_hom) solvable_imp_solvable_img: assumes "solvable_seq G K" shows "solvable_seq H (h ` K)" proof - obtain n where "(derived G ^^ n) K = { 𝟭 }" using G.solvable_imp_trivial_derived_seq[OF assms] by blast thus ?thesis using trivial_derived_seq_imp_solvable[OF subgroup_img_is_subgroup, of _ n] exp_of_derived_img[OF subgroup.subset, of _ n] G.solvable_imp_subgroup[OF assms] by auto qed corollary (in group_hom) surj_hom_imp_solvable: assumes "h ` carrier G = carrier H" and "solvable G" shows "solvable H" using assms solvable_imp_solvable_img[of "carrier G"] unfolding solvable_def by simp lemma solvable_seq_condition: assumes "group_hom G H f" "group_hom H K g" and "f ` I ⊆ J" and "kernel H K g ⊆ f ` I" and "subgroup J H" and "solvable_seq G I" "solvable_seq K (g ` J)" shows "solvable_seq H J" proof - interpret G: group G + H: group H + K: group K + J: subgroup J H + I: subgroup I G using assms(1-2,5) group.solvable_imp_subgroup[OF _ assms(6)] unfolding group_hom_def by auto obtain n m where n: "(derived G ^^ n) I = { 𝟭⇘G⇙ }" and m: "(derived K ^^ m) (g ` J) = { 𝟭⇘K⇙ }" using G.solvable_imp_trivial_derived_seq[OF assms(6)] K.solvable_imp_trivial_derived_seq[OF assms(7)] by auto have "(derived H ^^ m) J ⊆ f ` I" using m H.exp_of_derived_in_carrier[OF J.subset, of m] assms(4) by (auto simp add: group_hom.exp_of_derived_img[OF assms(2) J.subset] kernel_def) hence "(derived H ^^ n) ((derived H ^^ m) J) ⊆ f ` ((derived G ^^ n) I)" using n H.mono_exp_of_derived unfolding sym[OF group_hom.exp_of_derived_img[OF assms(1) I.subset, of n]] by simp hence "(derived H ^^ (n + m)) J ⊆ { 𝟭⇘H⇙ }" using group_hom.hom_one[OF assms(1)] unfolding n by (simp add: funpow_add) moreover have "{ 𝟭⇘H⇙ } ⊆ (derived H ^^ (n + m)) J" using subgroup.one_closed[OF H.exp_of_derived_is_subgroup[OF assms(5), of "n + m"]] by blast ultimately show ?thesis using H.trivial_derived_seq_imp_solvable[OF assms(5)] by simp qed lemma solvable_condition: assumes "group_hom G H f" "group_hom H K g" and "g ` (carrier H) = carrier K" and "kernel H K g ⊆ f ` (carrier G)" and "solvable G" "solvable K" shows "solvable H" using solvable_seq_condition[OF assms(1-2) _ assms(4) group.subgroup_self] assms(3,5-6) subgroup.subset[OF group_hom.img_is_subgroup[OF assms(1)]] group_hom.axioms(2)[OF assms(1)] by (simp add: solvable_def) end