Quelle Solvable_Groups.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Solvable_Groups.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Solvable_Groups
  imports Generated_Groups

begin

section \<open>Solvable Groups\<close>

subsection \<open>Definitions\<close>

inductive solvable_seq :: "('a, 'b) monoid_scheme \ 'a set \ bool"
  for G where
    unity: "solvable_seq G { \\<^bsub>G\<^esub> }"
  | extension: "\ solvable_seq G K; K \ (G \ carrier := H \); subgroup H G;
                  comm_group ((G \<lparr> carrier := H \<rparr>) Mod K) \<rbrakk> \<Longrightarrow> solvable_seq G H"

definition solvable :: "('a, 'b) monoid_scheme \ bool"
  where "solvable G \ solvable_seq G (carrier G)"

subsection \<open>Solvable Groups and Derived Subgroups\<close>

text \<open>We show that a group G is solvable iff the subgroup (derived G ^^ n) (carrier G)
      is trivial for a sufficiently large n. \<close>

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 \<open>Short Exact Sequences\<close>

text \<open>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) = { \\<^bsub>H\<^esub> }"
    using solvable_imp_trivial_derived_seq assms(1,3) by auto
  hence "h ` ((derived G ^^ n) K) = { \\<^bsub>H\<^esub> }"
    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 = { \\<^bsub>G\<^esub> }" and m: "(derived K ^^ m) (g ` J) = { \\<^bsub>K\<^esub> }"
    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 \ { \\<^bsub>H\<^esub> }"
    using group_hom.hom_one[OF assms(1)] unfolding n by (simp add: funpow_add)
  moreover have "{ \\<^bsub>H\<^esub> } \ (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

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.