Quelle Zassenhaus.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Zassenhaus.thy
    Author:     Martin Baillon
*)

section \<open>The Zassenhaus Lemma\<close>

theory Zassenhaus
  imports Coset Group_Action
begin

text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close>

subsection \<open>Lemmas about normalizer\<close>

lemma (in group) subgroup_in_normalizer:
  assumes "subgroup H G"
  shows "normal H (G\carrier:= (normalizer G H)\)"
proof(intro group.normal_invI)
  show "Group.group (G\carrier := normalizer G H\)"
    by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
  have K:"H \ (normalizer G H)" unfolding normalizer_def
  proof
    fix x assume xH: "x \ H"
    from xH have xG : "x \ carrier G" using subgroup.subset assms by auto
    have "x <# H = H"
      by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
         l_repr_independence one_closed subgroup.subset)
    moreover have "H #> inv x = H"
      by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
    ultimately have "x <# H #> (inv x) = H" by simp
    thus " x \ stabilizer G (\g. \H\{H. H \ carrier G}. g <# H #> inv g) H"
      using assms xG subgroup.subset unfolding stabilizer_def by auto
  qed
  thus "subgroup H (G\carrier:= (normalizer G H)\)"
    using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
  show  " \x h. x \ carrier (G\carrier := normalizer G H\) \ h \ H \
             x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
               \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
    proof-
    fix x h assume xnorm : "x \ carrier (G\carrier := normalizer G H\)" and hH : "h \ H"
    have xnormalizer:"x \ normalizer G H" using xnorm by simp
    moreover have hnormalizer:"h \ normalizer G H" using hH K by auto
    ultimately have "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h = x \ h" by simp
    moreover have " inv\<^bsub>G\carrier := normalizer G H\\<^esub> x = inv x"
      using xnormalizer
      by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent)
    ultimately  have xhxegal: "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h
                \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
                  = x \<otimes>h \<otimes> inv x"
      using  hnormalizer by simp
    have  "x \h \ inv x \ (x <# H #> inv x)"
      unfolding l_coset_def r_coset_def using hH  by auto
    moreover have "x <# H #> inv x = H"
      using xnormalizer assms subgroup.subset[OF assms]
      unfolding normalizer_def stabilizer_def by auto
    ultimately have "x \h \ inv x \ H" by simp
    thus  " x \\<^bsub>G\carrier := normalizer G H\\<^esub> h
               \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
      using xhxegal hH xnorm by simp
  qed
qed

lemma (in group) normal_imp_subgroup_normalizer:
  assumes "subgroup H G"
    and "N \ (G\carrier := H\)"
  shows "subgroup H (G\carrier := normalizer G N\)"
proof-
  have N_carrierG : "N \ carrier(G)"
    using assms normal_imp_subgroup subgroup.subset
    using incl_subgroup by blast
  {have "H \ normalizer G N" unfolding normalizer_def stabilizer_def
    proof
      fix x assume xH : "x \ H"
      hence xcarrierG : "x \ carrier(G)" using assms subgroup.subset by auto
      have " N #> x = x <# N" using assms xH
        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
      hence "x <# N #> inv x =(N #> x) #> inv x"
        by simp
      also have "... = N #> \"
        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp
      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
      thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) N = N}"
        using xcarrierG by (simp add : N_carrierG)
    qed}
  thus "subgroup H (G\carrier := normalizer G N\)"
    using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
      assms normal_imp_subgroup subgroup.subset
    by (metis  group.incl_subgroup is_group)
qed

subsection \<open>Second Isomorphism Theorem\<close>

lemma (in group) mult_norm_subgroup:
  assumes "normal N G"
    and "subgroup H G"
  shows "subgroup (N<#>H) G" unfolding subgroup_def
proof-
  have  A :"N <#> H \ carrier G"
    using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)

  have B :"\ x y. \x \ (N <#> H); y \ (N <#> H)\ \ (x \ y) \ (N<#>H)"
  proof-
    fix x y assume B1a: "x \ (N <#> H)" and B1b: "y \ (N <#> H)"
    obtain n1 h1 where B2:"n1 \ N \ h1 \ H \ n1\h1 = x"
      using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD)
    obtain n2 h2 where B3:"n2 \ N \ h2 \ H \ n2\h2 = y"
      using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
    have "N #> h1 = h1 <# N"
      using normalI B2 assms normal.coset_eq subgroup.subset by blast
    hence "h1\n2 \ N #> h1"
      using B2 B3 assms l_coset_def by fastforce
    from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2"
      using singletonD by (metis (no_types, lifting) UN_E r_coset_def)
    have "\a. a \ N \ a \ carrier G" "\a. a \ H \ a \ carrier G"
      by (meson assms normal_def subgroup.mem_carrier)+
    then have "x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3
      by (metis (no_types) B2 B3 \<open>\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G\<close> m_assoc m_closed y2_def y2_prop)
    moreover have B4 :"n1 \ y2 \N"
      using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def)
    moreover have "h1 \ h2 \H" using B2 B3 assms by (simp add: subgroup.m_closed)
    hence "(n1 \ y2) \ (h1 \ h2) \(N<#>H) "
      using B4  unfolding set_mult_def by auto
    hence "n1 \ y2 \ h1 \ h2 \(N<#>H)"
      using m_assoc B2 B3 assms  normal_imp_subgroup by (metis B4 subgroup.mem_carrier)
    ultimately show  "x \ y \ N <#> H" by auto
  qed
  have C :"\ x. x\(N<#>H) \ (inv x)\(N<#>H)"

  proof-
    fix x assume C1 : "x \ (N<#>H)"
    obtain n h where C2:"n \ N \ h \ H \ n\h = x"
      using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD)
    have C3 :"inv(n\h) = inv(h)\inv(n)"
      by (meson C2  assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier)
    hence "... \h \ N"
      using assms C2
      by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier)
    hence  C4:"(inv h \ inv n \ h) \ inv h \ (N<#>H)"
      using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
    have "inv h \ inv n \ h \ inv h = inv h \ inv n"
      using  subgroup.subset[OF assms(2)]
      by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
    thus "inv(x)\N<#>H" using C4 C2 C3 by simp
  qed

  have D : "\ \ N <#> H"
  proof-
    have D1 : "\ \ N"
      using assms by (simp add: normal_def subgroup.one_closed)
     have D2 :"\ \ H"
      using assms by (simp add: subgroup.one_closed)
    thus "\ \ (N <#> H)"
      using set_mult_def D1 assms by fastforce
  qed
  thus "(N <#> H \ carrier G \ (\x y. x \ N <#> H \ y \ N <#> H \ x \ y \ N <#> H)) \
    \<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast
qed

lemma (in group) mult_norm_sub_in_sub:
  assumes "normal N (G\carrier:=K\)"
  assumes "subgroup H (G\carrier:=K\)"
  assumes "subgroup K G"
  shows  "subgroup (N<#>H) (G\carrier:=K\)"
proof-
  have Hyp:"subgroup (N <#>\<^bsub>G\carrier := K\\<^esub> H) (G\carrier := K\)"
    using group.mult_norm_subgroup[where ?G = "G\carrier := K\"] assms subgroup_imp_group by auto
  have "H \ carrier(G\carrier := K\)" using assms subgroup.subset by blast
  also have "... \ K" by simp
  finally have Incl1:"H \ K" by simp
  have "N \ carrier(G\carrier := K\)" using assms normal_imp_subgroup subgroup.subset by blast
  also have "... \ K" by simp
  finally have Incl2:"N \ K" by simp
  have "(N <#>\<^bsub>G\carrier := K\\<^esub> H) = (N <#> H)"
    using set_mult_consistent by simp
  thus "subgroup (N<#>H) (G\carrier:=K\)" using Hyp by auto
qed

lemma (in group) subgroup_of_normal_set_mult:
  assumes "normal N G"
and "subgroup H G"
shows "subgroup H (G\carrier := N <#> H\)"
proof-
  have "\ \ N" using normal_imp_subgroup assms(1) subgroup_def by blast
  hence "\ <# H \ N <#> H" unfolding set_mult_def l_coset_def by blast
  hence H_incl : "H \ N <#> H"
    by (metis assms(2) lcos_mult_one subgroup_def)
  show "subgroup H (G\carrier := N <#> H\)"
  using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] .
qed

lemma (in group) normal_in_normal_set_mult:
  assumes "normal N G"
and "subgroup H G"
shows "normal N (G\carrier := N <#> H\)"
proof-
  have "\ \ H" using assms(2) subgroup_def by blast
  hence "N #> \ \ N <#> H" unfolding set_mult_def r_coset_def by blast
  hence N_incl : "N \ N <#> H"
    by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def)
  thus "normal N (G\carrier := N <#> H\)"
    using normal_Int_subgroup[OF mult_norm_subgroup[OF assms] assms(1)]
    by (simp add : inf_absorb1)
qed

proposition (in group) weak_snd_iso_thme:
  assumes "subgroup H G"
    and "N\G"
  shows "(G\carrier := N<#>H\ Mod N \ G\carrier:=H\ Mod (N\H))"
proof-
  define f where "f = (#>) N"
  have GroupNH : "Group.group (G\carrier := N<#>H\)"
    using subgroup_imp_group assms mult_norm_subgroup by simp
  have  HcarrierNH :"H \ carrier(G\carrier := N<#>H\)"
    using assms subgroup_of_normal_set_mult subgroup.subset by blast
  hence HNH :"H \ N<#>H" by simp
  have op_hom : "f \ hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N)" unfolding hom_def
  proof
    have "\x . x \ carrier (G\carrier :=H\) \
       (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in>  carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)"
    proof-
      fix x assume  "x \ carrier (G\carrier :=H\)"
      hence xH : "x \ H" by simp
      hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ rcosets\<^bsub>G\carrier := N <#> H\\<^esub> N"
        using HcarrierNH RCOSETS_def[where ?G = "G\carrier := N <#> H\"] by blast
      thus "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ carrier (G\carrier := N <#> H\ Mod N)"
        unfolding FactGroup_def by simp
    qed
    hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N \ carrier (G\carrier :=H\) \
            carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" by auto
    hence "f \ carrier (G\carrier :=H\) \ carrier (G\carrier := N <#> H\ Mod N)"
      unfolding r_coset_def f_def  by simp
    moreover have "\x y. x\carrier (G\carrier := H\) \ y\carrier (G\carrier := H\) \
                  f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)"
    proof-
      fix x y assume "x\carrier (G\carrier := H\)" "y\carrier (G\carrier := H\)"
      hence xHyH :"x \ H" "y \ H" by auto
      have Nxeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> x = N #>x" unfolding r_coset_def by simp
      have Nyeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> y = N #>y" unfolding r_coset_def by simp

      have "x \\<^bsub>G\carrier := H\\<^esub> y =x \\<^bsub>G\carrier := N<#>H\\<^esub> y" by simp
      hence "N #>\<^bsub>G\carrier := N<#>H\\<^esub> x \\<^bsub>G\carrier := H\\<^esub> y
             = N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp
      also have "... = (N #>\<^bsub>G\carrier := N<#>H\\<^esub> x) <#>\<^bsub>G\carrier := N<#>H\\<^esub>
                       (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y)"
        using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y]
             xHyH assms HcarrierNH by auto
      finally show "f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y)"
        unfolding  FactGroup_def r_coset_def f_def  using Nxeq Nyeq  by auto
    qed
    hence "(\x\carrier (G\carrier := H\). \y\carrier (G\carrier := H\).
           f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))" by blast
    ultimately show  " f \ carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N) \
    (\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>).
     f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) =  f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))"
      by auto
  qed
  hence homomorphism : "group_hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N) f"
    unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)]
             normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto
  moreover have im_f :  "(f ` carrier(G\carrier:=H\)) = carrier(G\carrier := N <#> H\ Mod N)"
  proof
    show  "f ` carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N)"
      using op_hom unfolding hom_def using funcset_image by blast
  next
    show "carrier (G\carrier := N <#> H\ Mod N) \ f ` carrier (G\carrier := H\)"
    proof
      fix x assume p : " x \ carrier (G\carrier := N <#> H\ Mod N)"
      hence "x \ \{y. \x\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> x}}"
        unfolding FactGroup_def RCOSETS_def by auto
      hence hyp :"\y. \h\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> h} \ x \ y"
        using Union_iff by blast
      from hyp obtain nh where nhNH:"nh \carrier (G\carrier := N <#> H\)"
                          and "x \ {N #>\<^bsub>G\carrier := N <#> H\\<^esub> nh}"
        by blast
      hence K: "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N nh" by simp
      have "nh \ N <#> H" using nhNH by simp
      from this obtain n h where nN : "n \ N" and hH : " h \ H" and nhnh: "n \ h = nh"
        unfolding set_mult_def by blast
      have  "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N (n \ h)" using K nhnh by simp
      hence  "x = (#>) N (n \ h)" using K nhnh unfolding r_coset_def by auto
      also have "... = (N #> n) #>h"
        using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
        by (metis subgroup.mem_carrier)
      finally have "x = (#>) N h"
        using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
      thus "x \ f ` carrier (G\carrier := H\)" using hH unfolding f_def by simp
    qed
  qed
  moreover have ker_f :"kernel (G\carrier := H\) (G\carrier := N<#>H\ Mod N) f = N\H"
    unfolding kernel_def f_def
    proof-
      have "{x \ carrier (G\carrier := H\). N #> x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} =
            {x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = N}" unfolding FactGroup_def by simp
      also have "... = {x \ carrier (G\carrier := H\). x \ N}"
        using coset_join1
        by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group
          normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group)
      also have "... =N \ (carrier(G\carrier := H\))" by auto
      finally show "{x \ carrier (G\carrier := H\). N#>x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} = N \ H"
        by simp
    qed
    ultimately have "(G\carrier := H\ Mod N \ H) \ (G\carrier := N <#> H\ Mod N)"
      using group_hom.FactGroup_iso[OF homomorphism im_f] by auto
    hence "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H"
      by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_Int_subgroup)
    thus "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H" by auto
qed

theorem (in group) snd_iso_thme:
  assumes "subgroup H G"
    and "subgroup N G"
    and "subgroup H (G\carrier:= (normalizer G N)\)"
  shows "(G\carrier:= N<#>H\ Mod N) \ (G\carrier:= H\ Mod (H\N))"
proof-
  have "G\carrier := normalizer G N, carrier := H\
       = G\<lparr>carrier := H\<rparr>"  by simp
  hence "G\carrier := normalizer G N, carrier := H\ Mod N \ H =
         G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
  moreover have "G\carrier := normalizer G N,
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> =
                G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr>" by simp
  hence "G\carrier := normalizer G N,
          carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N =
          G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N" by auto
  hence "G\carrier := normalizer G N,
          carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
          (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
         G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
    using subgroup.subset[OF assms(3)]
          subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
    by simp
  ultimately have "G\carrier := normalizer G N,
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
                  G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
                 (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto
  moreover have "G\carrier := normalizer G N,
                    carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
                  G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
    using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
          subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
    by simp
  moreover have "H\N = N\H" using assms by auto
  ultimately show "(G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod H \ N" by auto
qed

corollary (in group) snd_iso_thme_recip :
  assumes "subgroup H G"
    and "subgroup N G"
    and "subgroup H (G\carrier:= (normalizer G N)\)"
  shows "(G\carrier:= H<#>N\ Mod N) \ (G\carrier:= H\ Mod (H\N))"
  by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
      normalizer_imp_subgroup snd_iso_thme)

subsection\<open>The Zassenhaus Lemma\<close>

lemma (in group) distinc:
  assumes "subgroup H G"
    and "H1\G\carrier := H\"
    and  "subgroup K G"
    and "K1\G\carrier:=K\"
  shows "subgroup (H\K) (G\carrier:=(normalizer G (H1<#>(H\K1))) \)"
proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
  show "subgroup (normalizer G (H1 <#> H \ K1)) G"
    using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
    by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
next
  show "H \ K \ normalizer G (H1 <#> H \ K1)" unfolding normalizer_def stabilizer_def
  proof
    fix x assume xHK : "x \ H \ K"
    hence xG : "{x} \ carrier G" "{inv x} \ carrier G"
      using subgroup.subset assms inv_closed xHK by auto
    have allG : "H \ carrier G" "K \ carrier G" "H1 \ carrier G" "K1 \ carrier G"
      using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
    have HK1: "H \ K1 \ carrier G"
      by (simp add: allG(1) le_infI1)
    have HK1_normal: "H\K1 \ (G\carrier := H \ K\)" using normal_inter[OF assms(3)assms(1)assms(4)]
      by (simp add : inf_commute)
    have "H \ K \ normalizer G (H \ K1)"
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
            assms(1)assms(3)]HK1_normal]] by auto
    hence "x <# (H \ K1) #> inv x = (H \ K1)"
      using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
                                                            normal_imp_subgroup[OF assms(4)]]]]
      unfolding normalizer_def stabilizer_def by auto
    moreover have "H \ normalizer G H1"
      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
    hence "x <# H1 #> inv x = H1"
      using xHK subgroup.subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
      unfolding normalizer_def stabilizer_def by auto
    ultimately have "H1 <#> H \ K1 = (x <# H1 #> inv x) <#> (x <# H \ K1 #> inv x)" by auto
    also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \ K1 <#> {inv x})"
      by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult)
    also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \ K1 <#> {inv x})"
      using HK1 allG(3) set_mult_assoc setmult_subset_G xG(1) by auto
    also have "... = ({x} <#> H1 <#> {\}) <#> (H \ K1 <#> {inv x})"
      using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G)
    also have "... =({x} <#> H1) <#> (H \ K1 <#> {inv x})"
      using coset_mult_one r_coset_eq_set_mult[of G H1 \<one>] set_mult_assoc[OF xG(1) allG(3)] allG
      by auto
    also have "... = {x} <#> (H1 <#> H \ K1) <#> {inv x}"
      using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2)
    finally have "H1 <#> H \ K1 = x <# (H1 <#> H \ K1) #> inv x"
      using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
    thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H1 <#> H \ K1)
                                                                       = H1 <#> H \<inter> K1}"
      using xG allG setmult_subset_G[OF allG(3), where ?K = "H\K1"] xHK
      by auto
  qed
qed

lemma (in group) preliminary1:
  assumes "subgroup H G"
    and "H1\G\carrier := H\"
    and  "subgroup K G"
    and "K1\G\carrier:=K\"
  shows " (H\K) \ (H1<#>(H\K1)) = (H1\K)<#>(H\K1)"
proof
  have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G"
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
  show "H \ K \ (H1 <#> H \ K1) \ H1 \ K <#> H \ K1"
  proof
    fix x assume x_def : "x \ (H \ K) \ (H1 <#> (H \ K1))"
    from x_def have x_incl : "x \ H" "x \ K" "x \ (H1 <#> (H \ K1))" by auto
    then obtain h1 hk1 where h1hk1_def : "h1 \ H1" "hk1 \ H \ K1" "h1 \ hk1 = x"
      using assms unfolding set_mult_def by blast
    hence "hk1 \ H \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
    hence "inv hk1 \ H \ K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
    moreover have "h1 \ hk1 \ H \ K" using x_incl h1hk1_def by auto
    ultimately have "h1 \ hk1 \ inv hk1 \ H \ K"
      using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
    hence "h1 \ H \ K" using h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
      by (metis Int_iff contra_subsetD inv_solve_right m_closed)
    hence "h1 \ H1 \ H \ K" using h1hk1_def by auto
    hence "h1 \ H1 \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
    hence "h1 \ hk1 \ (H1\K)<#>(H\K1)"
      using h1hk1_def unfolding set_mult_def by auto
    thus " x \ (H1\K)<#>(H\K1)" using h1hk1_def x_def by auto
  qed
  show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)"
  proof-
    have "H1 \ K \ H \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
    moreover have "H \ K1 \ H \ K"
      using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
    ultimately have "H1 \ K <#> H \ K1 \ H \ K" unfolding set_mult_def
      using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
    moreover have "H1 \ K \ H1" by auto
    hence "H1 \ K <#> H \ K1 \ (H1 <#> H \ K1)" unfolding set_mult_def by auto
    ultimately show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)" by auto
  qed
qed

lemma (in group) preliminary2:
  assumes "subgroup H G"
    and "H1\G\carrier := H\"
    and  "subgroup K G"
    and "K1\G\carrier:=K\"
  shows "(H1<#>(H\K1)) \ G\carrier:=(H1<#>(H\K))\"
proof-
  have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G"
    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
  have subH1:"subgroup (H1 <#> H \ K) (G\carrier := H\)"
    using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
          assms(1)]] assms by auto
  have "Group.group (G\carrier:=(H1<#>(H\K))\)"
    using  subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]].
  moreover have subH2 : "subgroup (H1 <#> H \ K1) (G\carrier := H\)"
    using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
  hence "(H\K1) \ (H\K)"
    using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
    by (metis inf.mono  partial_object.simps(1) partial_object.update_convs(1) subset_refl)
  hence incl:"(H1<#>(H\K1)) \ H1<#>(H\K)" using assms subgroup.subset normal_imp_subgroup
    unfolding set_mult_def by blast
  hence "subgroup (H1 <#> H \ K1) (G\carrier := (H1<#>(H\K))\)"
    using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
          subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
  moreover have " (\ x. x\carrier (G\carrier := H1 <#> H \ K\) \
        H1 <#> H\<inter>K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> x = x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1))"
  proof-
    fix x assume  "x \carrier (G\carrier := H1 <#> H \ K\)"
    hence x_def : "x \ H1 <#> H \ K" by simp
    from this obtain h1 hk where h1hk_def :"h1 \ H1" "hk \ H \ K" "h1 \ hk = x"
      unfolding set_mult_def by blast
    have HK1: "H \ K1 \ carrier G"
      by (simp add: all_inclG(1) le_infI1)
    have xH : "x \ H" using subgroup.subset[OF subH1] using x_def by auto
    hence allG : "h1 \ carrier G" "hk \ carrier G" "x \ carrier G"
      using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
    hence "x <#\<^bsub>G\carrier := H1 <#> H\K\\<^esub> (H1 <#> H\K1) =h1 \ hk <# (H1 <#> H\K1)"
      using subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    also have "... = h1 <# (hk <# (H1 <#> H\K1))"
      using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
      by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
    also have "... = h1 <# (hk <# H1 <#> H\K1)"
      using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
    also have "... = h1 <# (hk <# H1 #> \ <#> H\K1 #> \)"
      using coset_mult_one allG all_inclG l_coset_subset_G
      by (simp add: inf.coboundedI2 setmult_subset_G)
    also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\K1 #> inv hk #> hk)"
      using all_inclG allG coset_mult_assoc l_coset_subset_G
      by (simp add: inf.coboundedI1 setmult_subset_G)
    finally have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1)
                  = h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)"
      using rcos_assoc_lcos allG all_inclG HK1
      by (simp add: l_coset_subset_G r_coset_subset_G setmult_rcos_assoc)
    moreover have "H \ normalizer G H1"
      using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
    hence "\g. g \ H \ g \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) H1 = H1}"
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
    hence "\g. g \ H \ g <# H1 #> inv g = H1" using all_inclG by simp
    hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
    moreover have "H\K \ normalizer G (H\K1)"
      using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
            subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
    hence "\g. g\H\K \ g\{g\carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H\K1) = H\K1}"
      using all_inclG assms unfolding normalizer_def stabilizer_def by auto
    hence "\g. g \ H\K \ g <# (H\K1) #> inv g = H\K1"
      using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
            assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
    hence "(hk <# H\K1 #> inv hk) = H\K1" using h1hk_def by simp
    ultimately have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = h1 <#(H1 <#> (H \ K1)#> hk)"
      by auto
    also have "... = h1 <# H1 <#> ((H \ K1)#> hk)"
      using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \ K1)#> hk"] allG all_inclG
      by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc)
    also have "... = H1 <#> ((H \ K1)#> hk)"
      using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def
      by auto
    finally have eq1 : "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = H1 <#> (H \ K1) #> hk"
      by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
    have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = H1 <#> H \ K1 #> (h1 \ hk)"
      using subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    also have "... = H1 <#> H \ K1 #> h1 #> hk"
      using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
    also have"... = H \ K1 <#> H1 #> h1 #> hk"
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
    also have "... = H \ K1 <#> H1 #> hk"
      using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup]
            h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc)
    finally  have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x =H1 <#> H \ K1 #> hk"
      using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF
           assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp
    thus " H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x =
             x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp
  qed
  ultimately show "H1 <#> H \ K1 \ G\carrier := H1 <#> H \ K\"
    unfolding normal_def normal_axioms_def by auto
qed

proposition (in group)  Zassenhaus_1:
  assumes "subgroup H G"
    and "H1\G\carrier := H\"
    and  "subgroup K G"
    and "K1\G\carrier:=K\"
  shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>H\K1)) \ (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))"
proof-
  define N  and N1 where "N = (H\K)" and "N1 =H1<#>(H\K1)"
  have normal_N_N1 : "subgroup N (G\carrier:=(normalizer G N1)\)"
    by (simp add: N1_def N_def assms distinc normal_imp_subgroup)
  have Hp:"(G\carrier:= N<#>N1\ Mod N1) \ (G\carrier:= N\ Mod (N\N1))"
  by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub
        normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair)
  have H_simp: "N<#>N1 = H1<#> (H\K)"
  proof-
    have H1_incl_G : "H1 \ carrier G"
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
    have K1_incl_G :"K1 \ carrier G"
      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
    have "N<#>N1= (H\K)<#> (H1<#>(H\K1))" by (auto simp add: N_def N1_def)
    also have "... = ((H\K)<#>H1) <#>(H\K1)"
      using set_mult_assoc[where ?M = "H\K"] K1_incl_G H1_incl_G assms
      by (simp add: inf.coboundedI2 subgroup.subset)
    also have "... = (H1<#>(H\K))<#>(H\K1)"
      using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
    also have "... = H1 <#> ((H\K)<#>(H\K1))"
      using set_mult_assoc K1_incl_G H1_incl_G assms
      by (simp add: inf.coboundedI2 subgroup.subset)
    also have " ((H\K)<#>(H\K1)) = (H\K)"
    proof (intro set_mult_subgroup_idem[where ?H = "H\K" and ?N="H\K1",
             OF subgroups_Inter_pair[OF assms(1) assms(3)]])
      show "subgroup (H \ K1) (G\carrier := H \ K\)"
        using subgroup_incl[where ?I = "H\K1" and ?J = "H\K",OF subgroups_Inter_pair[OF assms(1)
              incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms
              normal_imp_subgroup by (metis inf_commute normal_inter)
    qed
    hence " H1 <#> ((H\K)<#>(H\K1)) = H1 <#> ((H\K))"
      by simp
    thus "N <#> N1 = H1 <#> H \ K"
      by (simp add: calculation)
  qed

  have "N\N1 = (H1\K)<#>(H\K1)"
    using preliminary1 assms N_def N1_def by simp
  thus  "(G\carrier:= H1 <#> (H\K)\ Mod N1) \ (G\carrier:= N\ Mod ((H1\K)<#>(H\K1)))"
    using H_simp Hp by auto
qed

theorem (in group) Zassenhaus:
  assumes "subgroup H G"
    and "H1\G\carrier := H\"
    and  "subgroup K G"
    and "K1\G\carrier:=K\"
  shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) \
         (G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))"
proof-
  define Gmod1 Gmod2 Gmod3 Gmod4
    where "Gmod1 = (G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) "
      and "Gmod2 = (G\carrier:= K1 <#> (K\H)\ Mod (K1<#>(K\H1)))"
      and "Gmod3 = (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))"
      and "Gmod4 = (G\carrier:= (K\H)\ Mod ((K1\H)<#>(K\H1)))"
  have Hyp :  "Gmod1 \ Gmod3" "Gmod2 \ Gmod4"
    using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto
  have Hp : "Gmod3 = G\carrier:= (K\H)\ Mod ((K\H1)<#>(K1\H))"
    by (simp add: Gmod3_def inf_commute)
  have "(K\H1)<#>(K1\H) = (K1\H)<#>(K\H1)"
  proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]])
    show "K1 \ H \ G\carrier := H \ K\"
      using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute)
   next
    show "subgroup (K \ H1) (G\carrier := H \ K\)"
      using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter)
  qed
  hence  "Gmod3 = Gmod4" using Hp Gmod4_def by simp
  hence "Gmod1 \ Gmod2"
    by (metis assms group.iso_sym iso_trans Hyp normal.factorgroup_is_group Gmod2_def preliminary2)
  thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute)
qed

end

quality99%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.