(* Title: HOL/Algebra/Zassenhaus.thy Author: Martin Baillon *) section ‹The Zassenhaus Lemma› theory Zassenhaus imports Coset Group_Action begin text ‹Proves the second isomorphism theorem and the Zassenhaus lemma.› subsection ‹Lemmas about normalizer› 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 ‹x ∈ H› 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 ⊗⇘G⦇carrier := normalizer G H⦈⇙ h ⊗⇘G⦇carrier := normalizer G H⦈⇙ inv⇘G⦇carrier := normalizer G H⦈⇙ x ∈ 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 ⊗⇘G⦇carrier := normalizer G H⦈⇙ h = x ⊗ h" by simp moreover have " inv⇘G⦇carrier := normalizer G H⦈⇙ x = inv x" using xnormalizer by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent) ultimately have xhxegal: "x ⊗⇘G⦇carrier := normalizer G H⦈⇙ h ⊗⇘G⦇carrier := normalizer G H⦈⇙ inv⇘G⦇carrier := normalizer G H⦈⇙ x = x ⊗h ⊗ 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 ⊗⇘G⦇carrier := normalizer G H⦈⇙ h ⊗⇘G⦇carrier := normalizer G H⦈⇙ inv⇘G⦇carrier := normalizer G H⦈⇙ x ∈ 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 ‹Second Isomorphism Theorem› 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 ‹⋀a. a ∈ N ⟹ a ∈ carrier G› 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)) ∧ 𝟭 ∈ N <#> H ∧ (∀x. x ∈ N <#> H ⟶ inv x ∈ 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 <#>⇘G⦇carrier := K⦈⇙ 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 <#>⇘G⦇carrier := K⦈⇙ 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⦈) ⟹ (#>⇘G⦇carrier := N <#> H⦈⇙) N x ∈ carrier (G⦇carrier := N <#> H⦈ Mod N)" proof- fix x assume "x ∈ carrier (G⦇carrier :=H⦈)" hence xH : "x ∈ H" by simp hence "(#>⇘G⦇carrier := N <#> H⦈⇙) N x ∈ rcosets⇘G⦇carrier := N <#> H⦈⇙ N" using HcarrierNH RCOSETS_def[where ?G = "G⦇carrier := N <#> H⦈"] by blast thus "(#>⇘G⦇carrier := N <#> H⦈⇙) N x ∈ carrier (G⦇carrier := N <#> H⦈ Mod N)" unfolding FactGroup_def by simp qed hence "(#>⇘G⦇carrier := N <#> H⦈⇙) N ∈ carrier (G⦇carrier :=H⦈) → carrier (G⦇carrier := N <#> H⦈ 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 ⊗⇘G⦇carrier := H⦈⇙ y) = f(x) ⊗⇘G⦇carrier := N <#> H⦈ Mod N⇙ 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 #>⇘G⦇carrier := N<#>H⦈⇙ x = N #>x" unfolding r_coset_def by simp have Nyeq :"N #>⇘G⦇carrier := N<#>H⦈⇙ y = N #>y" unfolding r_coset_def by simp have "x ⊗⇘G⦇carrier := H⦈⇙ y =x ⊗⇘G⦇carrier := N<#>H⦈⇙ y" by simp hence "N #>⇘G⦇carrier := N<#>H⦈⇙ x ⊗⇘G⦇carrier := H⦈⇙ y = N #>⇘G⦇carrier := N<#>H⦈⇙ x ⊗⇘G⦇carrier := N<#>H⦈⇙ y" by simp also have "... = (N #>⇘G⦇carrier := N<#>H⦈⇙ x) <#>⇘G⦇carrier := N<#>H⦈⇙ (N #>⇘G⦇carrier := N<#>H⦈⇙ 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 ⊗⇘G⦇carrier := H⦈⇙ y) = f(x) ⊗⇘G⦇carrier := N <#> H⦈ Mod N⇙ 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 ⊗⇘G⦇carrier := H⦈⇙ y) = f(x) ⊗⇘G⦇carrier := N <#> H⦈ Mod N⇙ f(y))" by blast ultimately show " f ∈ carrier (G⦇carrier := H⦈) → carrier (G⦇carrier := N <#> H⦈ Mod N) ∧ (∀x∈carrier (G⦇carrier := H⦈). ∀y∈carrier (G⦇carrier := H⦈). f (x ⊗⇘G⦇carrier := H⦈⇙ y) = f(x) ⊗⇘G⦇carrier := N <#> H⦈ Mod N⇙ 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 #>⇘G⦇carrier := N <#> H⦈⇙ x}}" unfolding FactGroup_def RCOSETS_def by auto hence hyp :"∃y. ∃h∈carrier (G⦇carrier := N <#> H⦈). y = {N #>⇘G⦇carrier := N <#> H⦈⇙ h} ∧ x ∈ y" using Union_iff by blast from hyp obtain nh where nhNH:"nh ∈carrier (G⦇carrier := N <#> H⦈)" and "x ∈ {N #>⇘G⦇carrier := N <#> H⦈⇙ nh}" by blast hence K: "x = (#>⇘G⦇carrier := N <#> H⦈⇙) 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 = (#>⇘G⦇carrier := N <#> H⦈⇙) 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 = 𝟭⇘G⦇carrier := N <#> H⦈ Mod N⇙} = {x ∈ carrier (G⦇carrier := H⦈). 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 = 𝟭⇘G⦇carrier := N <#> H⦈ Mod N⇙} = 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⦇carrier := H⦈" by simp hence "G⦇carrier := normalizer G N, carrier := H⦈ Mod N ∩ H = G⦇carrier := H⦈ Mod N ∩ H" by auto moreover have "G⦇carrier := normalizer G N, carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ = G⦇carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈" by simp hence "G⦇carrier := normalizer G N, carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ Mod N = G⦇carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ Mod N" by auto hence "G⦇carrier := normalizer G N, carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ Mod N ≅ G⦇carrier := normalizer G N, carrier := H⦈ Mod N ∩ H = (G⦇carrier:= N<#>H⦈ Mod N) ≅ G⦇carrier := normalizer G N, carrier := H⦈ Mod N ∩ 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 <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ Mod N ≅ G⦇carrier := normalizer G N, carrier := H⦈ Mod N ∩ H = (G⦇carrier:= N<#>H⦈ Mod N) ≅ G⦇carrier := H⦈ Mod N ∩ H" by auto moreover have "G⦇carrier := normalizer G N, carrier := N <#>⇘G⦇carrier := normalizer G N⦈⇙ H⦈ Mod N ≅ G⦇carrier := normalizer G N, carrier := H⦈ Mod N ∩ 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‹The Zassenhaus Lemma› 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 𝟭] 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 ∩ 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∩K1 #>⇘G⦇carrier := H1 <#> H∩K⦈⇙ x = x <#⇘G⦇carrier := H1 <#> H∩K⦈⇙ (H1 <#> H∩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 <#⇘G⦇carrier := H1 <#> H∩K⦈⇙ (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 <#⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ (H1 <#> H ∩ K1) = h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H∩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 <#⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ (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 <#⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ (H1 <#> H ∩ K1) = H1 <#> (H ∩ K1) #> hk" by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc) have "H1 <#> H ∩ K1 #>⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ 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 #>⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ 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 #>⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ x = x <#⇘G⦇carrier := H1 <#> H ∩ K⦈⇙ (H1 <#> H ∩ 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⦇carrier:= K1 <#> (H∩K)⦈ Mod (K1<#>(K∩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