Theory HOL-Algebra.Solvable_Groups

(*  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