Theory Solvable_Groups
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