Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
ml_print_depth.ML
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
[ Verzeichnis aufwärts0.64unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
|
