src/HOL/Algebra/Zassenhaus.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68466 3d8241f4198b child 68555 22d51874f37d permissions -rw-r--r--
More on Algebra by Paulo and Martin
 lp15@68466 ` 1` ```(* Title: HOL/Algebra/Zassenhaus.thy ``` lp15@68466 ` 2` ``` Author: Martin Baillon ``` lp15@68466 ` 3` ```*) ``` lp15@68466 ` 4` lp15@68466 ` 5` ```section \The Zassenhaus Lemma\ ``` lp15@68466 ` 6` lp15@68443 ` 7` ```theory Zassenhaus ``` lp15@68443 ` 8` ``` imports Coset Group_Action ``` lp15@68443 ` 9` ```begin ``` lp15@68443 ` 10` lp15@68466 ` 11` ```text \Proves the second isomorphism theorem and the Zassenhaus lemma.\ ``` lp15@68443 ` 12` lp15@68466 ` 13` ```subsection \Lemmas about normalizer\ ``` lp15@68443 ` 14` lp15@68466 ` 15` ```lemma (in group) subgroup_in_normalizer: ``` lp15@68443 ` 16` ``` assumes "subgroup H G" ``` lp15@68443 ` 17` ``` shows "normal H (G\carrier:= (normalizer G H)\)" ``` lp15@68443 ` 18` ```proof(intro group.normal_invI) ``` lp15@68443 ` 19` ``` show "Group.group (G\carrier := normalizer G H\)" ``` lp15@68452 ` 20` ``` by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset) ``` lp15@68443 ` 21` ``` have K:"H \ (normalizer G H)" unfolding normalizer_def ``` lp15@68443 ` 22` ``` proof ``` lp15@68443 ` 23` ``` fix x assume xH: "x \ H" ``` lp15@68452 ` 24` ``` from xH have xG : "x \ carrier G" using subgroup.subset assms by auto ``` lp15@68443 ` 25` ``` have "x <# H = H" ``` lp15@68443 ` 26` ``` by (metis \x \ H\ assms group.lcos_mult_one is_group ``` lp15@68452 ` 27` ``` l_repr_independence one_closed subgroup.subset) ``` lp15@68466 ` 28` ``` moreover have "H #> inv x = H" ``` lp15@68443 ` 29` ``` by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed) ``` lp15@68443 ` 30` ``` ultimately have "x <# H #> (inv x) = H" by simp ``` lp15@68443 ` 31` ``` thus " x \ stabilizer G (\g. \H\{H. H \ carrier G}. g <# H #> inv g) H" ``` lp15@68452 ` 32` ``` using assms xG subgroup.subset unfolding stabilizer_def by auto ``` lp15@68443 ` 33` ``` qed ``` lp15@68443 ` 34` ``` thus "subgroup H (G\carrier:= (normalizer G H)\)" ``` lp15@68452 ` 35` ``` using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset) ``` lp15@68443 ` 36` ``` show " \x h. x \ carrier (G\carrier := normalizer G H\) \ h \ H \ ``` lp15@68443 ` 37` ``` x \\<^bsub>G\carrier := normalizer G H\\<^esub> h ``` lp15@68443 ` 38` ``` \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x \ H" ``` lp15@68443 ` 39` ``` proof- ``` lp15@68443 ` 40` ``` fix x h assume xnorm : "x \ carrier (G\carrier := normalizer G H\)" and hH : "h \ H" ``` lp15@68443 ` 41` ``` have xnormalizer:"x \ normalizer G H" using xnorm by simp ``` lp15@68443 ` 42` ``` moreover have hnormalizer:"h \ normalizer G H" using hH K by auto ``` lp15@68443 ` 43` ``` ultimately have "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h = x \ h" by simp ``` lp15@68443 ` 44` ``` moreover have " inv\<^bsub>G\carrier := normalizer G H\\<^esub> x = inv x" ``` lp15@68443 ` 45` ``` using xnormalizer ``` lp15@68452 ` 46` ``` by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality) ``` lp15@68443 ` 47` ``` ultimately have xhxegal: "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h ``` lp15@68443 ` 48` ``` \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x ``` lp15@68443 ` 49` ``` = x \h \ inv x" ``` lp15@68443 ` 50` ``` using hnormalizer by simp ``` lp15@68443 ` 51` ``` have "x \h \ inv x \ (x <# H #> inv x)" ``` lp15@68443 ` 52` ``` unfolding l_coset_def r_coset_def using hH by auto ``` lp15@68443 ` 53` ``` moreover have "x <# H #> inv x = H" ``` lp15@68452 ` 54` ``` using xnormalizer assms subgroup.subset[OF assms] ``` lp15@68443 ` 55` ``` unfolding normalizer_def stabilizer_def by auto ``` lp15@68443 ` 56` ``` ultimately have "x \h \ inv x \ H" by simp ``` lp15@68443 ` 57` ``` thus " x \\<^bsub>G\carrier := normalizer G H\\<^esub> h ``` lp15@68443 ` 58` ``` \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x \ H" ``` lp15@68443 ` 59` ``` using xhxegal hH xnorm by simp ``` lp15@68443 ` 60` ``` qed ``` lp15@68443 ` 61` ```qed ``` lp15@68443 ` 62` lp15@68443 ` 63` lp15@68445 ` 64` ```lemma (in group) normal_imp_subgroup_normalizer: ``` lp15@68443 ` 65` ``` assumes "subgroup H G" ``` lp15@68445 ` 66` ``` and "N \ (G\carrier := H\)" ``` lp15@68466 ` 67` ``` shows "subgroup H (G\carrier := normalizer G N\)" ``` lp15@68443 ` 68` ```proof- ``` lp15@68443 ` 69` ``` have N_carrierG : "N \ carrier(G)" ``` lp15@68452 ` 70` ``` using assms normal_imp_subgroup subgroup.subset ``` lp15@68443 ` 71` ``` by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1)) ``` lp15@68443 ` 72` ``` {have "H \ normalizer G N" unfolding normalizer_def stabilizer_def ``` lp15@68443 ` 73` ``` proof ``` lp15@68445 ` 74` ``` fix x assume xH : "x \ H" ``` lp15@68452 ` 75` ``` hence xcarrierG : "x \ carrier(G)" using assms subgroup.subset by auto ``` lp15@68445 ` 76` ``` have " N #> x = x <# N" using assms xH ``` lp15@68445 ` 77` ``` unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto ``` lp15@68445 ` 78` ``` hence "x <# N #> inv x =(N #> x) #> inv x" ``` lp15@68445 ` 79` ``` by simp ``` lp15@68445 ` 80` ``` also have "... = N #> \" ``` lp15@68466 ` 81` ``` using assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp ``` lp15@68445 ` 82` ``` finally have "x <# N #> inv x = N" by (simp add: N_carrierG) ``` lp15@68445 ` 83` ``` thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) N = N}" ``` lp15@68445 ` 84` ``` using xcarrierG by (simp add : N_carrierG) ``` lp15@68445 ` 85` ``` qed} ``` lp15@68443 ` 86` ``` thus "subgroup H (G\carrier := normalizer G N\)" ``` lp15@68443 ` 87` ``` using subgroup_incl[OF assms(1) normalizer_imp_subgroup] ``` lp15@68452 ` 88` ``` assms normal_imp_subgroup subgroup.subset ``` lp15@68443 ` 89` ``` by (metis group.incl_subgroup is_group) ``` lp15@68443 ` 90` ```qed ``` lp15@68443 ` 91` lp15@68443 ` 92` lp15@68443 ` 93` ```subsection \Second Isomorphism Theorem\ ``` lp15@68443 ` 94` lp15@68445 ` 95` ```lemma (in group) mult_norm_subgroup: ``` lp15@68443 ` 96` ``` assumes "normal N G" ``` lp15@68443 ` 97` ``` and "subgroup H G" ``` lp15@68443 ` 98` ``` shows "subgroup (N<#>H) G" unfolding subgroup_def ``` lp15@68443 ` 99` ```proof- ``` lp15@68443 ` 100` ``` have A :"N <#> H \ carrier G" ``` lp15@68452 ` 101` ``` using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset) ``` lp15@68443 ` 102` lp15@68443 ` 103` ``` have B :"\ x y. \x \ (N <#> H); y \ (N <#> H)\ \ (x \ y) \ (N<#>H)" ``` lp15@68443 ` 104` ``` proof- ``` lp15@68443 ` 105` ``` fix x y assume B1a: "x \ (N <#> H)" and B1b: "y \ (N <#> H)" ``` lp15@68443 ` 106` ``` obtain n1 h1 where B2:"n1 \ N \ h1 \ H \ n1\h1 = x" ``` lp15@68443 ` 107` ``` using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD) ``` lp15@68443 ` 108` ``` obtain n2 h2 where B3:"n2 \ N \ h2 \ H \ n2\h2 = y" ``` lp15@68443 ` 109` ``` using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD) ``` lp15@68443 ` 110` ``` have "N #> h1 = h1 <# N" ``` lp15@68452 ` 111` ``` using normalI B2 assms normal.coset_eq subgroup.subset by blast ``` lp15@68466 ` 112` ``` hence "h1\n2 \ N #> h1" ``` lp15@68443 ` 113` ``` using B2 B3 assms l_coset_def by fastforce ``` lp15@68466 ` 114` ``` from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2" ``` lp15@68466 ` 115` ``` using singletonD by (metis (no_types, lifting) UN_E r_coset_def) ``` lp15@68443 ` 116` ``` have " x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3 ``` lp15@68443 ` 117` ``` by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier) ``` lp15@68443 ` 118` ``` moreover have B4 :"n1 \ y2 \N" ``` lp15@68443 ` 119` ``` using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def) ``` lp15@68443 ` 120` ``` moreover have "h1 \ h2 \H" using B2 B3 assms by (simp add: subgroup.m_closed) ``` lp15@68443 ` 121` ``` hence "(n1 \ y2) \ (h1 \ h2) \(N<#>H) " ``` lp15@68443 ` 122` ``` using B4 unfolding set_mult_def by auto ``` lp15@68443 ` 123` ``` hence "n1 \ y2 \ h1 \ h2 \(N<#>H)" ``` lp15@68443 ` 124` ``` using m_assoc B2 B3 assms normal_imp_subgroup by (metis B4 subgroup.mem_carrier) ``` lp15@68443 ` 125` ``` ultimately show "x \ y \ N <#> H" by auto ``` lp15@68443 ` 126` ``` qed ``` lp15@68443 ` 127` ``` have C :"\ x. x\(N<#>H) \ (inv x)\(N<#>H)" ``` lp15@68443 ` 128` lp15@68443 ` 129` ``` proof- ``` lp15@68443 ` 130` ``` fix x assume C1 : "x \ (N<#>H)" ``` lp15@68443 ` 131` ``` obtain n h where C2:"n \ N \ h \ H \ n\h = x" ``` lp15@68443 ` 132` ``` using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD) ``` lp15@68443 ` 133` ``` have C3 :"inv(n\h) = inv(h)\inv(n)" ``` lp15@68443 ` 134` ``` by (meson C2 assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier) ``` lp15@68443 ` 135` ``` hence "... \h \ N" ``` lp15@68443 ` 136` ``` using assms C2 ``` lp15@68443 ` 137` ``` by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier) ``` lp15@68466 ` 138` ``` hence C4:"(inv h \ inv n \ h) \ inv h \ (N<#>H)" ``` lp15@68443 ` 139` ``` using C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto ``` lp15@68443 ` 140` ``` have "inv h \ inv n \ h \ inv h = inv h \ inv n" ``` lp15@68466 ` 141` ``` using subgroup.subset[OF assms(2)] ``` lp15@68443 ` 142` ``` by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE) ``` lp15@68443 ` 143` ``` thus "inv(x)\N<#>H" using C4 C2 C3 by simp ``` lp15@68443 ` 144` ``` qed ``` lp15@68443 ` 145` lp15@68443 ` 146` ``` have D : "\ \ N <#> H" ``` lp15@68443 ` 147` ``` proof- ``` lp15@68443 ` 148` ``` have D1 : "\ \ N" ``` lp15@68443 ` 149` ``` using assms by (simp add: normal_def subgroup.one_closed) ``` lp15@68443 ` 150` ``` have D2 :"\ \ H" ``` lp15@68443 ` 151` ``` using assms by (simp add: subgroup.one_closed) ``` lp15@68443 ` 152` ``` thus "\ \ (N <#> H)" ``` lp15@68443 ` 153` ``` using set_mult_def D1 assms by fastforce ``` lp15@68443 ` 154` ``` qed ``` lp15@68443 ` 155` ``` thus "(N <#> H \ carrier G \ (\x y. x \ N <#> H \ y \ N <#> H \ x \ y \ N <#> H)) \ ``` lp15@68443 ` 156` ``` \ \ N <#> H \ (\x. x \ N <#> H \ inv x \ N <#> H)" using A B C D assms by blast ``` lp15@68443 ` 157` ```qed ``` lp15@68466 ` 158` lp15@68443 ` 159` lp15@68445 ` 160` ```lemma (in group) mult_norm_sub_in_sub: ``` lp15@68443 ` 161` ``` assumes "normal N (G\carrier:=K\)" ``` lp15@68443 ` 162` ``` assumes "subgroup H (G\carrier:=K\)" ``` lp15@68443 ` 163` ``` assumes "subgroup K G" ``` lp15@68443 ` 164` ``` shows "subgroup (N<#>H) (G\carrier:=K\)" ``` lp15@68443 ` 165` ```proof- ``` lp15@68443 ` 166` ``` have Hyp:"subgroup (N <#>\<^bsub>G\carrier := K\\<^esub> H) (G\carrier := K\)" ``` lp15@68443 ` 167` ``` using group.mult_norm_subgroup[where ?G = "G\carrier := K\"] assms subgroup_imp_group by auto ``` lp15@68452 ` 168` ``` have "H \ carrier(G\carrier := K\)" using assms subgroup.subset by blast ``` lp15@68443 ` 169` ``` also have "... \ K" by simp ``` lp15@68443 ` 170` ``` finally have Incl1:"H \ K" by simp ``` lp15@68452 ` 171` ``` have "N \ carrier(G\carrier := K\)" using assms normal_imp_subgroup subgroup.subset by blast ``` lp15@68443 ` 172` ``` also have "... \ K" by simp ``` lp15@68443 ` 173` ``` finally have Incl2:"N \ K" by simp ``` lp15@68443 ` 174` ``` have "(N <#>\<^bsub>G\carrier := K\\<^esub> H) = (N <#> H)" ``` lp15@68445 ` 175` ``` using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp ``` lp15@68443 ` 176` ``` thus "subgroup (N<#>H) (G\carrier:=K\)" using Hyp by auto ``` lp15@68443 ` 177` ```qed ``` lp15@68443 ` 178` lp15@68443 ` 179` lp15@68445 ` 180` ```lemma (in group) subgroup_of_normal_set_mult: ``` lp15@68443 ` 181` ``` assumes "normal N G" ``` lp15@68443 ` 182` ```and "subgroup H G" ``` lp15@68443 ` 183` ```shows "subgroup H (G\carrier := N <#> H\)" ``` lp15@68443 ` 184` ```proof- ``` lp15@68443 ` 185` ``` have "\ \ N" using normal_imp_subgroup assms(1) subgroup_def by blast ``` lp15@68443 ` 186` ``` hence "\ <# H \ N <#> H" unfolding set_mult_def l_coset_def by blast ``` lp15@68443 ` 187` ``` hence H_incl : "H \ N <#> H" ``` lp15@68443 ` 188` ``` by (metis assms(2) lcos_mult_one subgroup_def) ``` lp15@68443 ` 189` ``` show "subgroup H (G\carrier := N <#> H\)" ``` lp15@68443 ` 190` ``` using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] . ``` lp15@68443 ` 191` ```qed ``` lp15@68443 ` 192` lp15@68443 ` 193` lp15@68445 ` 194` ```lemma (in group) normal_in_normal_set_mult: ``` lp15@68443 ` 195` ``` assumes "normal N G" ``` lp15@68443 ` 196` ```and "subgroup H G" ``` lp15@68443 ` 197` ```shows "normal N (G\carrier := N <#> H\)" ``` lp15@68443 ` 198` ```proof- ``` lp15@68443 ` 199` ``` have "\ \ H" using assms(2) subgroup_def by blast ``` lp15@68443 ` 200` ``` hence "N #> \ \ N <#> H" unfolding set_mult_def r_coset_def by blast ``` lp15@68443 ` 201` ``` hence N_incl : "N \ N <#> H" ``` lp15@68443 ` 202` ``` by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def) ``` lp15@68443 ` 203` ``` thus "normal N (G\carrier := N <#> H\)" ``` lp15@68443 ` 204` ``` using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)] ``` lp15@68443 ` 205` ``` by (simp add : inf_absorb1) ``` lp15@68443 ` 206` ```qed ``` lp15@68443 ` 207` lp15@68443 ` 208` lp15@68445 ` 209` ```proposition (in group) weak_snd_iso_thme: ``` lp15@68466 ` 210` ``` assumes "subgroup H G" ``` lp15@68443 ` 211` ``` and "N\G" ``` lp15@68443 ` 212` ``` shows "(G\carrier := N<#>H\ Mod N \ G\carrier:=H\ Mod (N\H))" ``` lp15@68443 ` 213` ```proof- ``` lp15@68443 ` 214` ``` define f where "f = (#>) N" ``` lp15@68443 ` 215` ``` have GroupNH : "Group.group (G\carrier := N<#>H\)" ``` lp15@68443 ` 216` ``` using subgroup_imp_group assms mult_norm_subgroup by simp ``` lp15@68443 ` 217` ``` have HcarrierNH :"H \ carrier(G\carrier := N<#>H\)" ``` lp15@68452 ` 218` ``` using assms subgroup_of_normal_set_mult subgroup.subset by blast ``` lp15@68443 ` 219` ``` hence HNH :"H \ N<#>H" by simp ``` lp15@68443 ` 220` ``` have op_hom : "f \ hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N)" unfolding hom_def ``` lp15@68443 ` 221` ``` proof ``` lp15@68443 ` 222` ``` have "\x . x \ carrier (G\carrier :=H\) \ ``` lp15@68443 ` 223` ``` (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ carrier (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 224` ``` proof- ``` lp15@68443 ` 225` ``` fix x assume "x \ carrier (G\carrier :=H\)" ``` lp15@68443 ` 226` ``` hence xH : "x \ H" by simp ``` lp15@68443 ` 227` ``` hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ rcosets\<^bsub>G\carrier := N <#> H\\<^esub> N" ``` lp15@68443 ` 228` ``` using HcarrierNH RCOSETS_def[where ?G = "G\carrier := N <#> H\"] by blast ``` lp15@68443 ` 229` ``` thus "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ carrier (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 230` ``` unfolding FactGroup_def by simp ``` lp15@68443 ` 231` ``` qed ``` lp15@68443 ` 232` ``` hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N \ carrier (G\carrier :=H\) \ ``` lp15@68443 ` 233` ``` carrier (G\carrier := N <#> H\ Mod N)" by auto ``` lp15@68443 ` 234` ``` hence "f \ carrier (G\carrier :=H\) \ carrier (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 235` ``` unfolding r_coset_def f_def by simp ``` lp15@68443 ` 236` ``` moreover have "\x y. x\carrier (G\carrier := H\) \ y\carrier (G\carrier := H\) \ ``` lp15@68443 ` 237` ``` f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y)" ``` lp15@68443 ` 238` ``` proof- ``` lp15@68443 ` 239` ``` fix x y assume "x\carrier (G\carrier := H\)" "y\carrier (G\carrier := H\)" ``` lp15@68443 ` 240` ``` hence xHyH :"x \ H" "y \ H" by auto ``` lp15@68443 ` 241` ``` have Nxeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> x = N #>x" unfolding r_coset_def by simp ``` lp15@68443 ` 242` ``` have Nyeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> y = N #>y" unfolding r_coset_def by simp ``` lp15@68443 ` 243` lp15@68443 ` 244` ``` have "x \\<^bsub>G\carrier := H\\<^esub> y =x \\<^bsub>G\carrier := N<#>H\\<^esub> y" by simp ``` lp15@68443 ` 245` ``` hence "N #>\<^bsub>G\carrier := N<#>H\\<^esub> x \\<^bsub>G\carrier := H\\<^esub> y ``` lp15@68443 ` 246` ``` = N #>\<^bsub>G\carrier := N<#>H\\<^esub> x \\<^bsub>G\carrier := N<#>H\\<^esub> y" by simp ``` lp15@68443 ` 247` ``` also have "... = (N #>\<^bsub>G\carrier := N<#>H\\<^esub> x) <#>\<^bsub>G\carrier := N<#>H\\<^esub> ``` lp15@68443 ` 248` ``` (N #>\<^bsub>G\carrier := N<#>H\\<^esub> y)" ``` lp15@68443 ` 249` ``` using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y] ``` lp15@68443 ` 250` ``` xHyH assms HcarrierNH by auto ``` lp15@68443 ` 251` ``` finally show "f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y)" ``` lp15@68443 ` 252` ``` unfolding FactGroup_def r_coset_def f_def using Nxeq Nyeq by auto ``` lp15@68443 ` 253` ``` qed ``` lp15@68443 ` 254` ``` hence "(\x\carrier (G\carrier := H\). \y\carrier (G\carrier := H\). ``` lp15@68443 ` 255` ``` f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y))" by blast ``` lp15@68443 ` 256` ``` ultimately show " f \ carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N) \ ``` lp15@68443 ` 257` ``` (\x\carrier (G\carrier := H\). \y\carrier (G\carrier := H\). ``` lp15@68443 ` 258` ``` f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y))" ``` lp15@68443 ` 259` ``` by auto ``` lp15@68443 ` 260` ``` qed ``` lp15@68443 ` 261` ``` hence homomorphism : "group_hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N) f" ``` lp15@68443 ` 262` ``` unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)] ``` lp15@68443 ` 263` ``` normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto ``` lp15@68443 ` 264` ``` moreover have im_f : "(f ` carrier(G\carrier:=H\)) = carrier(G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 265` ``` proof ``` lp15@68443 ` 266` ``` show "f ` carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 267` ``` using op_hom unfolding hom_def using funcset_image by blast ``` lp15@68443 ` 268` ``` next ``` lp15@68443 ` 269` ``` show "carrier (G\carrier := N <#> H\ Mod N) \ f ` carrier (G\carrier := H\)" ``` lp15@68443 ` 270` ``` proof ``` lp15@68443 ` 271` ``` fix x assume p : " x \ carrier (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 272` ``` hence "x \ \{y. \x\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> x}}" ``` lp15@68443 ` 273` ``` unfolding FactGroup_def RCOSETS_def by auto ``` lp15@68443 ` 274` ``` hence hyp :"\y. \h\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> h} \ x \ y" ``` lp15@68443 ` 275` ``` using Union_iff by blast ``` lp15@68443 ` 276` ``` from hyp obtain nh where nhNH:"nh \carrier (G\carrier := N <#> H\)" ``` lp15@68443 ` 277` ``` and "x \ {N #>\<^bsub>G\carrier := N <#> H\\<^esub> nh}" ``` lp15@68443 ` 278` ``` by blast ``` lp15@68443 ` 279` ``` hence K: "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N nh" by simp ``` lp15@68443 ` 280` ``` have "nh \ N <#> H" using nhNH by simp ``` lp15@68443 ` 281` ``` from this obtain n h where nN : "n \ N" and hH : " h \ H" and nhnh: "n \ h = nh" ``` lp15@68443 ` 282` ``` unfolding set_mult_def by blast ``` lp15@68443 ` 283` ``` have "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N (n \ h)" using K nhnh by simp ``` lp15@68443 ` 284` ``` hence "x = (#>) N (n \ h)" using K nhnh unfolding r_coset_def by auto ``` lp15@68443 ` 285` ``` also have "... = (N #> n) #>h" ``` lp15@68452 ` 286` ``` using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup ``` lp15@68443 ` 287` ``` by (metis subgroup.mem_carrier) ``` lp15@68443 ` 288` ``` finally have "x = (#>) N h" ``` lp15@68443 ` 289` ``` using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier) ``` lp15@68443 ` 290` ``` thus "x \ f ` carrier (G\carrier := H\)" using hH unfolding f_def by simp ``` lp15@68443 ` 291` ``` qed ``` lp15@68443 ` 292` ``` qed ``` lp15@68443 ` 293` ``` moreover have ker_f :"kernel (G\carrier := H\) (G\carrier := N<#>H\ Mod N) f = N\H" ``` lp15@68443 ` 294` ``` unfolding kernel_def f_def ``` lp15@68443 ` 295` ``` proof- ``` lp15@68443 ` 296` ``` have "{x \ carrier (G\carrier := H\). N #> x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} = ``` lp15@68443 ` 297` ``` {x \ carrier (G\carrier := H\). N #> x = N}" unfolding FactGroup_def by simp ``` lp15@68443 ` 298` ``` also have "... = {x \ carrier (G\carrier := H\). x \ N}" ``` lp15@68443 ` 299` ``` using coset_join1 ``` lp15@68443 ` 300` ``` by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group ``` lp15@68443 ` 301` ``` normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group) ``` lp15@68443 ` 302` ``` also have "... =N \ (carrier(G\carrier := H\))" by auto ``` lp15@68443 ` 303` ``` finally show "{x \ carrier (G\carrier := H\). N#>x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} = N \ H" ``` lp15@68443 ` 304` ``` by simp ``` lp15@68443 ` 305` ``` qed ``` lp15@68443 ` 306` ``` ultimately have "(G\carrier := H\ Mod N \ H) \ (G\carrier := N <#> H\ Mod N)" ``` lp15@68443 ` 307` ``` using group_hom.FactGroup_iso[OF homomorphism im_f] by auto ``` lp15@68443 ` 308` ``` hence "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H" ``` lp15@68443 ` 309` ``` by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup) ``` lp15@68443 ` 310` ``` thus "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H" by auto ``` lp15@68443 ` 311` ```qed ``` lp15@68443 ` 312` lp15@68443 ` 313` lp15@68445 ` 314` ```theorem (in group) snd_iso_thme: ``` lp15@68443 ` 315` ``` assumes "subgroup H G" ``` lp15@68443 ` 316` ``` and "subgroup N G" ``` lp15@68443 ` 317` ``` and "subgroup H (G\carrier:= (normalizer G N)\)" ``` lp15@68443 ` 318` ``` shows "(G\carrier:= N<#>H\ Mod N) \ (G\carrier:= H\ Mod (H\N))" ``` lp15@68443 ` 319` ```proof- ``` lp15@68443 ` 320` ``` have "G\carrier := normalizer G N, carrier := H\ ``` lp15@68443 ` 321` ``` = G\carrier := H\" by simp ``` lp15@68443 ` 322` ``` hence "G\carrier := normalizer G N, carrier := H\ Mod N \ H = ``` lp15@68443 ` 323` ``` G\carrier := H\ Mod N \ H" by auto ``` lp15@68443 ` 324` ``` moreover have "G\carrier := normalizer G N, ``` lp15@68443 ` 325` ``` carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ = ``` lp15@68443 ` 326` ``` G\carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\" by simp ``` lp15@68443 ` 327` ``` hence "G\carrier := normalizer G N, ``` lp15@68443 ` 328` ``` carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N = ``` lp15@68443 ` 329` ``` G\carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N" by auto ``` lp15@68443 ` 330` ``` hence "G\carrier := normalizer G N, ``` lp15@68443 ` 331` ``` carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ ``` lp15@68443 ` 332` ``` G\carrier := normalizer G N, carrier := H\ Mod N \ H = ``` lp15@68443 ` 333` ``` (G\carrier:= N<#>H\ Mod N) \ ``` lp15@68466 ` 334` ``` G\carrier := normalizer G N, carrier := H\ Mod N \ H" ``` lp15@68466 ` 335` ``` using subgroup_set_mult_equality[OF normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] ``` lp15@68452 ` 336` ``` subgroup.subset[OF assms(3)] ``` lp15@68452 ` 337` ``` subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]] ``` lp15@68443 ` 338` ``` by simp ``` lp15@68443 ` 339` ``` ultimately have "G\carrier := normalizer G N, ``` lp15@68443 ` 340` ``` carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ ``` lp15@68443 ` 341` ``` G\carrier := normalizer G N, carrier := H\ Mod N \ H = ``` lp15@68443 ` 342` ``` (G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod N \ H" by auto ``` lp15@68443 ` 343` ``` moreover have "G\carrier := normalizer G N, ``` lp15@68443 ` 344` ``` carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ ``` lp15@68443 ` 345` ``` G\carrier := normalizer G N, carrier := H\ Mod N \ H" ``` lp15@68443 ` 346` ``` using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF ``` lp15@68452 ` 347` ``` subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]] ``` lp15@68443 ` 348` ``` by simp ``` lp15@68443 ` 349` ``` moreover have "H\N = N\H" using assms by auto ``` lp15@68443 ` 350` ``` ultimately show "(G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod H \ N" by auto ``` lp15@68443 ` 351` ```qed ``` lp15@68466 ` 352` lp15@68443 ` 353` lp15@68443 ` 354` ```corollary (in group) snd_iso_thme_recip : ``` lp15@68443 ` 355` ``` assumes "subgroup H G" ``` lp15@68443 ` 356` ``` and "subgroup N G" ``` lp15@68443 ` 357` ``` and "subgroup H (G\carrier:= (normalizer G N)\)" ``` lp15@68443 ` 358` ``` shows "(G\carrier:= H<#>N\ Mod N) \ (G\carrier:= H\ Mod (H\N))" ``` lp15@68452 ` 359` ``` by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset ``` lp15@68443 ` 360` ``` normalizer_imp_subgroup snd_iso_thme) ``` lp15@68443 ` 361` lp15@68443 ` 362` lp15@68443 ` 363` ```subsection\The Zassenhaus Lemma\ ``` lp15@68443 ` 364` lp15@68443 ` 365` lp15@68445 ` 366` ```lemma (in group) distinc: ``` lp15@68466 ` 367` ``` assumes "subgroup H G" ``` lp15@68466 ` 368` ``` and "H1\G\carrier := H\" ``` lp15@68466 ` 369` ``` and "subgroup K G" ``` lp15@68443 ` 370` ``` and "K1\G\carrier:=K\" ``` lp15@68443 ` 371` ``` shows "subgroup (H\K) (G\carrier:=(normalizer G (H1<#>(H\K1))) \)" ``` lp15@68443 ` 372` ```proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]]) ``` lp15@68443 ` 373` ``` show "subgroup (normalizer G (H1 <#> H \ K1)) G" ``` lp15@68452 ` 374` ``` using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset ``` lp15@68443 ` 375` ``` by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair) ``` lp15@68443 ` 376` ```next ``` lp15@68443 ` 377` ``` show "H \ K \ normalizer G (H1 <#> H \ K1)" unfolding normalizer_def stabilizer_def ``` lp15@68443 ` 378` ``` proof ``` lp15@68443 ` 379` ``` fix x assume xHK : "x \ H \ K" ``` lp15@68443 ` 380` ``` hence xG : "{x} \ carrier G" "{inv x} \ carrier G" ``` lp15@68452 ` 381` ``` using subgroup.subset assms inv_closed xHK by auto ``` lp15@68443 ` 382` ``` have allG : "H \ carrier G" "K \ carrier G" "H1 \ carrier G" "K1 \ carrier G" ``` lp15@68452 ` 383` ``` using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ . ``` lp15@68443 ` 384` ``` have HK1_normal: "H\K1 \ (G\carrier := H \ K\)" using normal_inter[OF assms(3)assms(1)assms(4)] ``` lp15@68443 ` 385` ``` by (simp add : inf_commute) ``` lp15@68443 ` 386` ``` have "H \ K \ normalizer G (H \ K1)" ``` lp15@68452 ` 387` ``` using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF ``` lp15@68443 ` 388` ``` assms(1)assms(3)]HK1_normal]] by auto ``` lp15@68443 ` 389` ``` hence "x <# (H \ K1) #> inv x = (H \ K1)" ``` lp15@68452 ` 390` ``` using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3) ``` lp15@68443 ` 391` ``` normal_imp_subgroup[OF assms(4)]]]] ``` lp15@68443 ` 392` ``` unfolding normalizer_def stabilizer_def by auto ``` lp15@68443 ` 393` ``` moreover have "H \ normalizer G H1" ``` lp15@68452 ` 394` ``` using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto ``` lp15@68443 ` 395` ``` hence "x <# H1 #> inv x = H1" ``` lp15@68452 ` 396` ``` using xHK subgroup.subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]] ``` lp15@68443 ` 397` ``` unfolding normalizer_def stabilizer_def by auto ``` lp15@68443 ` 398` ``` ultimately have "H1 <#> H \ K1 = (x <# H1 #> inv x) <#> (x <# H \ K1 #> inv x)" by auto ``` lp15@68443 ` 399` ``` also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \ K1 <#> {inv x})" ``` lp15@68443 ` 400` ``` by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult) ``` lp15@68443 ` 401` ``` also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \ K1 <#> {inv x})" ``` lp15@68443 ` 402` ``` by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G) ``` lp15@68443 ` 403` ``` also have "... = ({x} <#> H1 <#> {\}) <#> (H \ K1 <#> {inv x})" ``` lp15@68443 ` 404` ``` using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G) ``` lp15@68443 ` 405` ``` also have "... =({x} <#> H1) <#> (H \ K1 <#> {inv x})" ``` lp15@68443 ` 406` ``` using coset_mult_one r_coset_eq_set_mult[of G H1 \] set_mult_assoc[OF xG(1) allG(3)] allG ``` lp15@68443 ` 407` ``` by auto ``` lp15@68443 ` 408` ``` also have "... = {x} <#> (H1 <#> H \ K1) <#> {inv x}" ``` lp15@68443 ` 409` ``` using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2) ``` lp15@68466 ` 410` ``` finally have "H1 <#> H \ K1 = x <# (H1 <#> H \ K1) #> inv x" ``` lp15@68443 ` 411` ``` using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult) ``` lp15@68443 ` 412` ``` thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H1 <#> H \ K1) ``` lp15@68443 ` 413` ``` = H1 <#> H \ K1}" ``` lp15@68443 ` 414` ``` using xG allG setmult_subset_G[OF allG(3), where ?K = "H\K1"] xHK ``` lp15@68443 ` 415` ``` by auto ``` lp15@68443 ` 416` ``` qed ``` lp15@68443 ` 417` ```qed ``` lp15@68443 ` 418` lp15@68445 ` 419` ```lemma (in group) preliminary1: ``` lp15@68466 ` 420` ``` assumes "subgroup H G" ``` lp15@68466 ` 421` ``` and "H1\G\carrier := H\" ``` lp15@68466 ` 422` ``` and "subgroup K G" ``` lp15@68443 ` 423` ``` and "K1\G\carrier:=K\" ``` lp15@68443 ` 424` ``` shows " (H\K) \ (H1<#>(H\K1)) = (H1\K)<#>(H\K1)" ``` lp15@68443 ` 425` ```proof ``` lp15@68443 ` 426` ``` have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" ``` lp15@68452 ` 427` ``` using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. ``` lp15@68443 ` 428` ``` show "H \ K \ (H1 <#> H \ K1) \ H1 \ K <#> H \ K1" ``` lp15@68443 ` 429` ``` proof ``` lp15@68443 ` 430` ``` fix x assume x_def : "x \ (H \ K) \ (H1 <#> (H \ K1))" ``` lp15@68443 ` 431` ``` from x_def have x_incl : "x \ H" "x \ K" "x \ (H1 <#> (H \ K1))" by auto ``` lp15@68443 ` 432` ``` then obtain h1 hk1 where h1hk1_def : "h1 \ H1" "hk1 \ H \ K1" "h1 \ hk1 = x" ``` lp15@68443 ` 433` ``` using assms unfolding set_mult_def by blast ``` lp15@68452 ` 434` ``` hence "hk1 \ H \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto ``` lp15@68443 ` 435` ``` hence "inv hk1 \ H \ K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto ``` lp15@68443 ` 436` ``` moreover have "h1 \ hk1 \ H \ K" using x_incl h1hk1_def by auto ``` lp15@68443 ` 437` ``` ultimately have "h1 \ hk1 \ inv hk1 \ H \ K" ``` lp15@68443 ` 438` ``` using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto ``` lp15@68452 ` 439` ``` hence "h1 \ H \ K" using h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup ``` lp15@68443 ` 440` ``` by (metis Int_iff contra_subsetD inv_solve_right m_closed) ``` lp15@68443 ` 441` ``` hence "h1 \ H1 \ H \ K" using h1hk1_def by auto ``` lp15@68452 ` 442` ``` hence "h1 \ H1 \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto ``` lp15@68443 ` 443` ``` hence "h1 \ hk1 \ (H1\K)<#>(H\K1)" ``` lp15@68443 ` 444` ``` using h1hk1_def unfolding set_mult_def by auto ``` lp15@68443 ` 445` ``` thus " x \ (H1\K)<#>(H\K1)" using h1hk1_def x_def by auto ``` lp15@68443 ` 446` ``` qed ``` lp15@68443 ` 447` ``` show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)" ``` lp15@68443 ` 448` ``` proof- ``` lp15@68452 ` 449` ``` have "H1 \ K \ H \ K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto ``` lp15@68443 ` 450` ``` moreover have "H \ K1 \ H \ K" ``` lp15@68452 ` 451` ``` using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto ``` lp15@68443 ` 452` ``` ultimately have "H1 \ K <#> H \ K1 \ H \ K" unfolding set_mult_def ``` lp15@68443 ` 453` ``` using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast ``` lp15@68443 ` 454` ``` moreover have "H1 \ K \ H1" by auto ``` lp15@68443 ` 455` ``` hence "H1 \ K <#> H \ K1 \ (H1 <#> H \ K1)" unfolding set_mult_def by auto ``` lp15@68443 ` 456` ``` ultimately show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)" by auto ``` lp15@68443 ` 457` ``` qed ``` lp15@68443 ` 458` ```qed ``` lp15@68443 ` 459` lp15@68445 ` 460` ```lemma (in group) preliminary2: ``` lp15@68466 ` 461` ``` assumes "subgroup H G" ``` lp15@68443 ` 462` ``` and "H1\G\carrier := H\" ``` lp15@68466 ` 463` ``` and "subgroup K G" ``` lp15@68443 ` 464` ``` and "K1\G\carrier:=K\" ``` lp15@68443 ` 465` ``` shows "(H1<#>(H\K1)) \ G\carrier:=(H1<#>(H\K))\" ``` lp15@68443 ` 466` ```proof- ``` lp15@68443 ` 467` ``` have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" ``` lp15@68452 ` 468` ``` using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. ``` lp15@68466 ` 469` ``` have subH1:"subgroup (H1 <#> H \ K) (G\carrier := H\)" ``` lp15@68443 ` 470` ``` using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)] ``` lp15@68443 ` 471` ``` assms(1)]] assms by auto ``` lp15@68443 ` 472` ``` have "Group.group (G\carrier:=(H1<#>(H\K))\)" ``` lp15@68443 ` 473` ``` using subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]]. ``` lp15@68443 ` 474` ``` moreover have subH2 : "subgroup (H1 <#> H \ K1) (G\carrier := H\)" ``` lp15@68443 ` 475` ``` using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF ``` lp15@68443 ` 476` ``` assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto ``` lp15@68443 ` 477` ``` hence "(H\K1) \ (H\K)" ``` lp15@68452 ` 478` ``` using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme ``` lp15@68443 ` 479` ``` by (metis inf.mono partial_object.simps(1) partial_object.update_convs(1) subset_refl) ``` lp15@68452 ` 480` ``` hence incl:"(H1<#>(H\K1)) \ H1<#>(H\K)" using assms subgroup.subset normal_imp_subgroup ``` lp15@68443 ` 481` ``` unfolding set_mult_def by blast ``` lp15@68443 ` 482` ``` hence "subgroup (H1 <#> H \ K1) (G\carrier := (H1<#>(H\K))\)" ``` lp15@68443 ` 483` ``` using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1) ``` lp15@68452 ` 484` ``` subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast ``` lp15@68443 ` 485` ``` moreover have " (\ x. x\carrier (G\carrier := H1 <#> H \ K\) \ ``` lp15@68443 ` 486` ``` H1 <#> H\K1 #>\<^bsub>G\carrier := H1 <#> H\K\\<^esub> x = x <#\<^bsub>G\carrier := H1 <#> H\K\\<^esub> (H1 <#> H\K1))" ``` lp15@68443 ` 487` ``` proof- ``` lp15@68443 ` 488` ``` fix x assume "x \carrier (G\carrier := H1 <#> H \ K\)" ``` lp15@68443 ` 489` ``` hence x_def : "x \ H1 <#> H \ K" by simp ``` lp15@68443 ` 490` ``` from this obtain h1 hk where h1hk_def :"h1 \ H1" "hk \ H \ K" "h1 \ hk = x" ``` lp15@68443 ` 491` ``` unfolding set_mult_def by blast ``` lp15@68452 ` 492` ``` have xH : "x \ H" using subgroup.subset[OF subH1] using x_def by auto ``` lp15@68443 ` 493` ``` hence allG : "h1 \ carrier G" "hk \ carrier G" "x \ carrier G" ``` lp15@68452 ` 494` ``` using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+. ``` lp15@68443 ` 495` ``` hence "x <#\<^bsub>G\carrier := H1 <#> H\K\\<^esub> (H1 <#> H\K1) =h1 \ hk <# (H1 <#> H\K1)" ``` lp15@68452 ` 496` ``` using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def) ``` lp15@68443 ` 497` ``` also have "... = h1 <# (hk <# (H1 <#> H\K1))" ``` lp15@68452 ` 498` ``` using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)] ``` lp15@68452 ` 499` ``` by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset) ``` lp15@68443 ` 500` ``` also have "... = h1 <# (hk <# H1 <#> H\K1)" ``` lp15@68443 ` 501` ``` using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1) ``` lp15@68443 ` 502` ``` also have "... = h1 <# (hk <# H1 #> \ <#> H\K1 #> \)" ``` lp15@68443 ` 503` ``` using coset_mult_one allG all_inclG l_coset_subset_G ``` lp15@68443 ` 504` ``` by (smt inf_le2 setmult_subset_G subset_trans) ``` lp15@68443 ` 505` ``` also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\K1 #> inv hk #> hk)" ``` lp15@68443 ` 506` ``` using all_inclG allG coset_mult_assoc l_coset_subset_G ``` lp15@68443 ` 507` ``` by (simp add: inf.coboundedI1 setmult_subset_G) ``` lp15@68443 ` 508` ``` finally have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = ``` lp15@68443 ` 509` ``` h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\K1 #> inv hk) #> hk)" ``` lp15@68443 ` 510` ``` using rcos_assoc_lcos allG all_inclG ``` lp15@68443 ` 511` ``` by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans) ``` lp15@68443 ` 512` ``` moreover have "H \ normalizer G H1" ``` lp15@68452 ` 513` ``` using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp ``` lp15@68443 ` 514` ``` hence "\g. g \ H \ g \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) H1 = H1}" ``` lp15@68443 ` 515` ``` using all_inclG assms unfolding normalizer_def stabilizer_def by auto ``` lp15@68443 ` 516` ``` hence "\g. g \ H \ g <# H1 #> inv g = H1" using all_inclG by simp ``` lp15@68443 ` 517` ``` hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp ``` lp15@68443 ` 518` ``` moreover have "H\K \ normalizer G (H\K1)" ``` lp15@68443 ` 519` ``` using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair ``` lp15@68452 ` 520` ``` subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute) ``` lp15@68443 ` 521` ``` hence "\g. g\H\K \ g\{g\carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H\K1) = H\K1}" ``` lp15@68443 ` 522` ``` using all_inclG assms unfolding normalizer_def stabilizer_def by auto ``` lp15@68443 ` 523` ``` hence "\g. g \ H\K \ g <# (H\K1) #> inv g = H\K1" ``` lp15@68452 ` 524` ``` using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF ``` lp15@68443 ` 525` ``` assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto ``` lp15@68443 ` 526` ``` hence "(hk <# H\K1 #> inv hk) = H\K1" using h1hk_def by simp ``` lp15@68443 ` 527` ``` ultimately have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = h1 <#(H1 <#> (H \ K1)#> hk)" ``` lp15@68443 ` 528` ``` by auto ``` lp15@68443 ` 529` ``` also have "... = h1 <# H1 <#> ((H \ K1)#> hk)" ``` lp15@68443 ` 530` ``` using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \ K1)#> hk"] allG all_inclG ``` lp15@68443 ` 531` ``` by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc) ``` lp15@68443 ` 532` ``` also have "... = H1 <#> ((H \ K1)#> hk)" ``` lp15@68443 ` 533` ``` using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def ``` lp15@68443 ` 534` ``` by auto ``` lp15@68443 ` 535` ``` finally have eq1 : "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = H1 <#> (H \ K1) #> hk" ``` lp15@68443 ` 536` ``` by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc) ``` lp15@68443 ` 537` ``` have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = H1 <#> H \ K1 #> (h1 \ hk)" ``` lp15@68452 ` 538` ``` using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def) ``` lp15@68443 ` 539` ``` also have "... = H1 <#> H \ K1 #> h1 #> hk" ``` lp15@68443 ` 540` ``` using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G) ``` lp15@68443 ` 541` ``` also have"... = H \ K1 <#> H1 #> h1 #> hk" ``` lp15@68443 ` 542` ``` using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF ``` lp15@68443 ` 543` ``` assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp ``` lp15@68443 ` 544` ``` also have "... = H \ K1 <#> H1 #> hk" ``` lp15@68443 ` 545` ``` using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup] ``` lp15@68443 ` 546` ``` h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc) ``` lp15@68443 ` 547` ``` finally have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x =H1 <#> H \ K1 #> hk" ``` lp15@68443 ` 548` ``` using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF ``` lp15@68443 ` 549` ``` assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp ``` lp15@68466 ` 550` ``` thus " H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = ``` lp15@68443 ` 551` ``` x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1)" using eq1 by simp ``` lp15@68443 ` 552` ``` qed ``` lp15@68443 ` 553` ``` ultimately show "H1 <#> H \ K1 \ G\carrier := H1 <#> H \ K\" ``` lp15@68443 ` 554` ``` unfolding normal_def normal_axioms_def by auto ``` lp15@68443 ` 555` ```qed ``` lp15@68443 ` 556` lp15@68443 ` 557` lp15@68445 ` 558` ```proposition (in group) Zassenhaus_1: ``` lp15@68466 ` 559` ``` assumes "subgroup H G" ``` lp15@68466 ` 560` ``` and "H1\G\carrier := H\" ``` lp15@68466 ` 561` ``` and "subgroup K G" ``` lp15@68443 ` 562` ``` and "K1\G\carrier:=K\" ``` lp15@68443 ` 563` ``` shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>H\K1)) \ (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))" ``` lp15@68443 ` 564` ```proof- ``` lp15@68443 ` 565` ``` define N and N1 where "N = (H\K)" and "N1 =H1<#>(H\K1)" ``` lp15@68443 ` 566` ``` have normal_N_N1 : "subgroup N (G\carrier:=(normalizer G N1)\)" ``` lp15@68443 ` 567` ``` by (simp add: N1_def N_def assms distinc normal_imp_subgroup) ``` lp15@68443 ` 568` ``` have Hp:"(G\carrier:= N<#>N1\ Mod N1) \ (G\carrier:= N\ Mod (N\N1))" ``` lp15@68443 ` 569` ``` by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub ``` lp15@68443 ` 570` ``` normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair) ``` lp15@68443 ` 571` ``` have H_simp: "N<#>N1 = H1<#> (H\K)" ``` lp15@68443 ` 572` ``` proof- ``` lp15@68443 ` 573` ``` have H1_incl_G : "H1 \ carrier G" ``` lp15@68452 ` 574` ``` using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast ``` lp15@68443 ` 575` ``` have K1_incl_G :"K1 \ carrier G" ``` lp15@68452 ` 576` ``` using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast ``` lp15@68443 ` 577` ``` have "N<#>N1= (H\K)<#> (H1<#>(H\K1))" by (auto simp add: N_def N1_def) ``` lp15@68443 ` 578` ``` also have "... = ((H\K)<#>H1) <#>(H\K1)" ``` lp15@68443 ` 579` ``` using set_mult_assoc[where ?M = "H\K"] K1_incl_G H1_incl_G assms ``` lp15@68452 ` 580` ``` by (simp add: inf.coboundedI2 subgroup.subset) ``` lp15@68466 ` 581` ``` also have "... = (H1<#>(H\K))<#>(H\K1)" ``` lp15@68443 ` 582` ``` using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto ``` lp15@68443 ` 583` ``` also have "... = H1 <#> ((H\K)<#>(H\K1))" ``` lp15@68443 ` 584` ``` using set_mult_assoc K1_incl_G H1_incl_G assms ``` lp15@68452 ` 585` ``` by (simp add: inf.coboundedI2 subgroup.subset) ``` lp15@68443 ` 586` ``` also have " ((H\K)<#>(H\K1)) = (H\K)" ``` lp15@68443 ` 587` ``` proof (intro set_mult_subgroup_idem[where ?H = "H\K" and ?N="H\K1", ``` lp15@68443 ` 588` ``` OF subgroups_Inter_pair[OF assms(1) assms(3)]]) ``` lp15@68443 ` 589` ``` show "subgroup (H \ K1) (G\carrier := H \ K\)" ``` lp15@68443 ` 590` ``` using subgroup_incl[where ?I = "H\K1" and ?J = "H\K",OF subgroups_Inter_pair[OF assms(1) ``` lp15@68443 ` 591` ``` incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms ``` lp15@68443 ` 592` ``` normal_imp_subgroup by (metis inf_commute normal_inter) ``` lp15@68443 ` 593` ``` qed ``` lp15@68466 ` 594` ``` hence " H1 <#> ((H\K)<#>(H\K1)) = H1 <#> ((H\K))" ``` lp15@68443 ` 595` ``` by simp ``` lp15@68443 ` 596` ``` thus "N <#> N1 = H1 <#> H \ K" ``` lp15@68443 ` 597` ``` by (simp add: calculation) ``` lp15@68443 ` 598` ``` qed ``` lp15@68443 ` 599` lp15@68466 ` 600` ``` have "N\N1 = (H1\K)<#>(H\K1)" ``` lp15@68466 ` 601` ``` using preliminary1 assms N_def N1_def by simp ``` lp15@68443 ` 602` ``` thus "(G\carrier:= H1 <#> (H\K)\ Mod N1) \ (G\carrier:= N\ Mod ((H1\K)<#>(H\K1)))" ``` lp15@68443 ` 603` ``` using H_simp Hp by auto ``` lp15@68443 ` 604` ```qed ``` lp15@68443 ` 605` lp15@68443 ` 606` lp15@68445 ` 607` ```theorem (in group) Zassenhaus: ``` lp15@68466 ` 608` ``` assumes "subgroup H G" ``` lp15@68466 ` 609` ``` and "H1\G\carrier := H\" ``` lp15@68466 ` 610` ``` and "subgroup K G" ``` lp15@68443 ` 611` ``` and "K1\G\carrier:=K\" ``` lp15@68466 ` 612` ``` shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) \ ``` lp15@68443 ` 613` ``` (G\carrier:= K1 <#> (H\K)\ Mod (K1<#>(K\H1)))" ``` lp15@68443 ` 614` ```proof- ``` lp15@68443 ` 615` ``` define Gmod1 Gmod2 Gmod3 Gmod4 ``` lp15@68443 ` 616` ``` where "Gmod1 = (G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) " ``` lp15@68443 ` 617` ``` and "Gmod2 = (G\carrier:= K1 <#> (K\H)\ Mod (K1<#>(K\H1)))" ``` lp15@68443 ` 618` ``` and "Gmod3 = (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))" ``` lp15@68443 ` 619` ``` and "Gmod4 = (G\carrier:= (K\H)\ Mod ((K1\H)<#>(K\H1)))" ``` lp15@68443 ` 620` ``` have Hyp : "Gmod1 \ Gmod3" "Gmod2 \ Gmod4" ``` lp15@68443 ` 621` ``` using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto ``` lp15@68443 ` 622` ``` have Hp : "Gmod3 = G\carrier:= (K\H)\ Mod ((K\H1)<#>(K1\H))" ``` lp15@68443 ` 623` ``` by (simp add: Gmod3_def inf_commute) ``` lp15@68443 ` 624` ``` have "(K\H1)<#>(K1\H) = (K1\H)<#>(K\H1)" ``` lp15@68443 ` 625` ``` proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]]) ``` lp15@68443 ` 626` ``` show "K1 \ H \ G\carrier := H \ K\" ``` lp15@68443 ` 627` ``` using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute) ``` lp15@68443 ` 628` ``` next ``` lp15@68466 ` 629` ``` show "subgroup (K \ H1) (G\carrier := H \ K\)" ``` lp15@68466 ` 630` ``` using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) ``` lp15@68443 ` 631` ``` qed ``` lp15@68443 ` 632` ``` hence "Gmod3 = Gmod4" using Hp Gmod4_def by simp ``` lp15@68443 ` 633` ``` hence "Gmod1 \ Gmod2" ``` lp15@68443 ` 634` ``` using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group ``` lp15@68443 ` 635` ``` by (metis assms Gmod1_def Gmod2_def preliminary2) ``` lp15@68443 ` 636` ``` thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute) ``` lp15@68443 ` 637` ```qed ``` lp15@68443 ` 638` lp15@68443 ` 639` ```end ```