--- a/src/HOL/Algebra/Algebra.thy Mon Feb 27 20:51:47 2023 +0100
+++ b/src/HOL/Algebra/Algebra.thy Tue Feb 28 11:20:01 2023 +0000
@@ -3,6 +3,6 @@
theory Algebra
imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
- Left_Coset
+ Left_Coset SimpleGroups SndIsomorphismGrp
begin
end
--- a/src/HOL/Algebra/Coset.thy Mon Feb 27 20:51:47 2023 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Feb 28 11:20:01 2023 +0000
@@ -39,7 +39,7 @@
"H \<lhd> G \<equiv> normal H G"
lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
- by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+ by (simp add: normal_def normal_axioms_def l_coset_def r_coset_def m_comm subgroup.mem_carrier)
lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
fixes G (structure)
@@ -468,13 +468,65 @@
using assms normal_inv_iff apply blast
by (simp add: assms normal.inv_op_closed2)
+lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
+ using normal_invI triv_subgroup by force
-lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
-proof(intro normal_invI)
- show "subgroup {\<one>} G"
- by (simp add: subgroup_def)
-qed simp
+text \<open>The intersection of two normal subgroups is, again, a normal subgroup.\<close>
+lemma (in group) normal_subgroup_intersect:
+ assumes "M \<lhd> G" and "N \<lhd> G" shows "M \<inter> N \<lhd> G"
+ using assms normal_inv_iff subgroups_Inter_pair by force
+
+
+text \<open>Being a normal subgroup is preserved by surjective homomorphisms.\<close>
+lemma (in normal) surj_hom_normal_subgroup:
+ assumes \<phi>: "group_hom G F \<phi>"
+ assumes \<phi>surj: "\<phi> ` (carrier G) = carrier F"
+ shows "(\<phi> ` H) \<lhd> F"
+proof (rule group.normalI)
+ show "group F"
+ using \<phi> group_hom.axioms(2) by blast
+next
+ show "subgroup (\<phi> ` H) F"
+ using \<phi> group_hom.subgroup_img_is_subgroup subgroup_axioms by blast
+next
+ show "\<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H"
+ proof
+ fix f
+ assume f: "f \<in> carrier F"
+ with \<phi>surj obtain g where g: "g \<in> carrier G" "f = \<phi> g" by auto
+ hence "\<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g" by simp
+ also have "... = (\<lambda>x. (\<phi> x) \<otimes>\<^bsub>F\<^esub> (\<phi> g)) ` H"
+ unfolding r_coset_def image_def by auto
+ also have "... = (\<lambda>x. \<phi> (x \<otimes> g)) ` H"
+ using subset g \<phi> group_hom.hom_mult unfolding image_def by fastforce
+ also have "... = \<phi> ` (H #> g)"
+ using \<phi> unfolding r_coset_def by auto
+ also have "... = \<phi> ` (g <# H)"
+ by (metis coset_eq g(1))
+ also have "... = (\<lambda>x. \<phi> (g \<otimes> x)) ` H"
+ using \<phi> unfolding l_coset_def by auto
+ also have "... = (\<lambda>x. (\<phi> g) \<otimes>\<^bsub>F\<^esub> (\<phi> x)) ` H"
+ using subset g \<phi> group_hom.hom_mult by fastforce
+ also have "... = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H"
+ unfolding l_coset_def image_def by auto
+ also have "... = f <#\<^bsub>F\<^esub> \<phi> ` H"
+ using g by simp
+ finally show "\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H".
+ qed
+qed
+
+text \<open>Being a normal subgroup is preserved by group isomorphisms.\<close>
+lemma iso_normal_subgroup:
+ assumes \<phi>: "\<phi> \<in> iso G F" "group G" "group F" "H \<lhd> G"
+ shows "(\<phi> ` H) \<lhd> F"
+ by (meson assms Group.iso_iff group_hom_axioms_def group_hom_def normal.surj_hom_normal_subgroup)
+
+text \<open>The set product of two normal subgroups is a normal subgroup.\<close>
+lemma (in group) setmult_lcos_assoc:
+ "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
+ \<Longrightarrow> (x <# H) <#> K = x <# (H <#> K)"
+ by (force simp add: l_coset_def set_mult_def m_assoc)
subsection\<open>More Properties of Left Cosets\<close>
@@ -770,8 +822,17 @@
order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
where "order S = card (carrier S)"
+lemma iso_same_order:
+ assumes "\<phi> \<in> iso G H"
+ shows "order G = order H"
+ by (metis assms is_isoI iso_same_card order_def order_def)
+
lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
-by(auto simp add: order_def card_gt_0_iff)
+ by(auto simp add: order_def card_gt_0_iff)
+
+lemma (in group) order_one_triv_iff:
+ shows "(order G = 1) = (carrier G = {\<one>})"
+ by (metis One_nat_def card.empty card_Suc_eq empty_iff one_closed order_def singleton_iff)
lemma (in group) rcosets_part_G:
assumes "subgroup H G"
@@ -889,6 +950,11 @@
qed
qed
+text \<open>The cardinality of the right cosets of the trivial subgroup is the cardinality of the group itself:\<close>
+corollary (in group) card_rcosets_triv:
+ assumes "finite (carrier G)"
+ shows "card (rcosets {\<one>}) = order G"
+ using lagrange triv_subgroup by fastforce
subsection \<open>Quotient Groups: Factorization of a Group\<close>
@@ -1523,7 +1589,7 @@
subsubsection "More Lemmas about set multiplication"
-(*A group multiplied by a subgroup stays the same*)
+text \<open>A group multiplied by a subgroup stays the same\<close>
lemma (in group) set_mult_carrier_idem:
assumes "subgroup H G"
shows "(carrier G) <#> H = carrier G"
@@ -1537,13 +1603,13 @@
ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
qed
-(*Same lemma as above, but everything is included in a subgroup*)
+text \<open>Same lemma as above, but everything is included in a subgroup\<close>
lemma (in group) set_mult_subgroup_idem:
assumes HG: "subgroup H G" and NG: "subgroup N (G \<lparr> carrier := H \<rparr>)"
shows "H <#> N = H"
using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp
-(*A normal subgroup is commutative with set_mult*)
+text \<open>A normal subgroup is commutative with set multiplication\<close>
lemma (in group) commut_normal:
assumes "subgroup H G" and "N\<lhd>G"
shows "H<#>N = N<#>H"
@@ -1554,22 +1620,22 @@
ultimately show "H<#>N = N<#>H" by simp
qed
-(*Same lemma as above, but everything is included in a subgroup*)
+text \<open>Same lemma as above, but everything is included in a subgroup\<close>
lemma (in group) commut_normal_subgroup:
assumes "subgroup H G" and "N \<lhd> (G\<lparr> carrier := H \<rparr>)"
and "subgroup K (G \<lparr> carrier := H \<rparr>)"
shows "K <#> N = N <#> K"
- using group.commut_normal[OF subgroup.subgroup_is_group[OF assms(1) group_axioms] assms(3,2)] by simp
-
+ by (metis assms(2) assms(3) group.commut_normal normal.axioms(2) set_mult_consistent)
subsubsection "Lemmas about intersection and normal subgroups"
+text \<open>Mostly by Jakob von Raumer\<close>
lemma (in group) normal_inter:
assumes "subgroup H G"
and "subgroup K G"
and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
- shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
+ shows "(H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
proof-
define HK and H1K and GH and GHK
where "HK = H\<inter>K" and "H1K=H1\<inter>K" and "GH =G\<lparr>carrier := H\<rparr>" and "GHK = (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
@@ -1647,4 +1713,337 @@
by auto
qed
+lemma (in group) normal_restrict_supergroup:
+ assumes "subgroup S G" "N \<lhd> G" "N \<subseteq> S"
+ shows "N \<lhd> (G\<lparr>carrier := S\<rparr>)"
+ by (metis assms inf.absorb_iff1 normal_Int_subgroup)
+
+text \<open>A subgroup relation survives factoring by a normal subgroup.\<close>
+lemma (in group) normal_subgroup_factorize:
+ assumes "N \<lhd> G" and "N \<subseteq> H" and "subgroup H G"
+ shows "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)"
+proof -
+ interpret GModN: group "G Mod N"
+ using assms(1) by (rule normal.factorgroup_is_group)
+ have "N \<lhd> G\<lparr>carrier := H\<rparr>"
+ using assms by (metis normal_restrict_supergroup)
+ hence grpHN: "group (G\<lparr>carrier := H\<rparr> Mod N)"
+ by (rule normal.factorgroup_is_group)
+ have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}))"
+ using set_mult_def by metis
+ moreover have "\<dots> = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}))"
+ by auto
+ moreover have "(<#>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k}))"
+ using set_mult_def by metis
+ ultimately have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (<#>\<^bsub>G\<^esub>)"
+ by simp
+ with grpHN have "group ((G Mod N)\<lparr>carrier := (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N)\<rparr>)"
+ unfolding FactGroup_def by auto
+ moreover have "rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)"
+ unfolding FactGroup_def RCOSETS_def r_coset_def using assms(3) subgroup.subset
+ by fastforce
+ ultimately show ?thesis
+ using GModN.group_incl_imp_subgroup by blast
+qed
+
+text \<open>A normality relation survives factoring by a normal subgroup.\<close>
+lemma (in group) normality_factorization:
+ assumes NG: "N \<lhd> G" and NH: "N \<subseteq> H" and HG: "H \<lhd> G"
+ shows "(rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) \<lhd> (G Mod N)"
+proof -
+ from assms(1) interpret GModN: group "G Mod N" by (metis normal.factorgroup_is_group)
+ show ?thesis
+ unfolding GModN.normal_inv_iff
+ proof (intro conjI strip)
+ show "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)"
+ using assms normal_imp_subgroup normal_subgroup_factorize by force
+ next
+ fix U V
+ assume U: "U \<in> carrier (G Mod N)" and V: "V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N"
+ then obtain g where g: "g \<in> carrier G" "U = N #> g"
+ unfolding FactGroup_def RCOSETS_def by auto
+ from V obtain h where h: "h \<in> H" "V = N #> h"
+ unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+ hence hG: "h \<in> carrier G"
+ using HG normal_imp_subgroup subgroup.mem_carrier by force
+ hence ghG: "g \<otimes> h \<in> carrier G"
+ using g m_closed by auto
+ from g h have "g \<otimes> h \<otimes> inv g \<in> H"
+ using HG normal_inv_iff by auto
+ moreover have "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> (g \<otimes> h \<otimes> inv g)"
+ proof -
+ from g U have "inv\<^bsub>G Mod N\<^esub> U = N #> inv g"
+ using NG normal.inv_FactGroup normal.rcos_inv by fastforce
+ hence "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = (N #> g) <#> (N #> h) <#> (N #> inv g)"
+ using g h by simp
+ also have "\<dots> = N #> (g \<otimes> h \<otimes> inv g)"
+ using g hG NG inv_closed ghG normal.rcos_sum by force
+ finally show ?thesis .
+ qed
+ ultimately show "U \<otimes>\<^bsub>G Mod N\<^esub> V \<otimes>\<^bsub>G Mod N\<^esub> inv\<^bsub>G Mod N\<^esub> U \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N"
+ unfolding RCOSETS_def r_coset_def by auto
+ qed
+qed
+
+text \<open>Factorizing by the trivial subgroup is an isomorphism.\<close>
+lemma (in group) trivial_factor_iso:
+ shows "the_elem \<in> iso (G Mod {\<one>}) G"
+proof -
+ have "group_hom G G (\<lambda>x. x)"
+ unfolding group_hom_def group_hom_axioms_def hom_def using is_group by simp
+ moreover have "(\<lambda>x. x) ` carrier G = carrier G"
+ by simp
+ moreover have "kernel G G (\<lambda>x. x) = {\<one>}"
+ unfolding kernel_def by auto
+ ultimately show ?thesis using group_hom.FactGroup_iso_set
+ by force
+qed
+
+text \<open>And the dual theorem to the previous one: Factorizing by the group itself gives the trivial group\<close>
+
+lemma (in group) self_factor_iso:
+ shows "(\<lambda>X. the_elem ((\<lambda>x. \<one>) ` X)) \<in> iso (G Mod (carrier G)) (G\<lparr> carrier := {\<one>} \<rparr>)"
+proof -
+ have "group (G\<lparr>carrier := {\<one>}\<rparr>)"
+ by (metis subgroup_imp_group triv_subgroup)
+ hence "group_hom G (G\<lparr>carrier := {\<one>}\<rparr>) (\<lambda>x. \<one>)"
+ unfolding group_hom_def group_hom_axioms_def hom_def using is_group by auto
+ moreover have "(\<lambda>x. \<one>) ` carrier G = carrier (G\<lparr>carrier := {\<one>}\<rparr>)"
+ by auto
+ moreover have "kernel G (G\<lparr>carrier := {\<one>}\<rparr>) (\<lambda>x. \<one>) = carrier G"
+ unfolding kernel_def by auto
+ ultimately show ?thesis using group_hom.FactGroup_iso_set
+ by force
+qed
+
+text \<open>Factoring by a normal subgroups yields the trivial group iff the subgroup is the whole group.\<close>
+lemma (in normal) fact_group_trivial_iff:
+ assumes "finite (carrier G)"
+ shows "(carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}) \<longleftrightarrow> (H = carrier G)"
+proof
+ assume "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}"
+ moreover have "order (G Mod H) * card H = order G"
+ by (simp add: FactGroup_def lagrange order_def subgroup_axioms)
+ ultimately have "card H = order G" unfolding order_def by auto
+ thus "H = carrier G"
+ by (simp add: assms card_subset_eq order_def subset)
+next
+ assume "H = carrier G"
+ with assms is_subgroup lagrange
+ have "card (rcosets H) * order G = order G"
+ by (simp add: order_def)
+ then have "card (rcosets H) = 1"
+ using assms order_gt_0_iff_finite by auto
+ hence "order (G Mod H) = 1"
+ unfolding order_def FactGroup_def by auto
+ thus "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}"
+ using factorgroup_is_group by (metis group.order_one_triv_iff)
+qed
+
+text \<open>The union of all the cosets contained in a subgroup of a quotient group acts as a represenation for that subgroup.\<close>
+
+lemma (in normal) factgroup_subgroup_union_char:
+ assumes "subgroup A (G Mod H)"
+ shows "(\<Union>A) = {x \<in> carrier G. H #> x \<in> A}"
+proof
+ show "\<Union>A \<subseteq> {x \<in> carrier G. H #> x \<in> A}"
+ proof
+ fix x
+ assume x: "x \<in> \<Union>A"
+ then obtain a where a: "a \<in> A" "x \<in> a" and xx: "x \<in> carrier G"
+ using subgroup.subset assms by (force simp add: FactGroup_def RCOSETS_def r_coset_def)
+ from assms a obtain y where y: "y \<in> carrier G" "a = H #> y"
+ using subgroup.subset unfolding FactGroup_def RCOSETS_def by force
+ with a have "x \<in> H #> y" by simp
+ hence "H #> y = H #> x" using y is_subgroup repr_independence by auto
+ with y(2) a(1) have "H #> x \<in> A"
+ by auto
+ with xx show "x \<in> {x \<in> carrier G. H #> x \<in> A}" by simp
+ qed
+next
+ show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union>A"
+ using rcos_self subgroup_axioms by auto
+qed
+
+lemma (in normal) factgroup_subgroup_union_subgroup:
+ assumes "subgroup A (G Mod H)"
+ shows "subgroup (\<Union>A) G"
+proof -
+ have "subgroup {x \<in> carrier G. H #> x \<in> A} G"
+ proof
+ show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G" by auto
+ next
+ fix x y
+ assume xy: "x \<in> {x \<in> carrier G. H #> x \<in> A}" "y \<in> {x \<in> carrier G. H #> x \<in> A}"
+ then have "(H #> x) <#> (H #> y) \<in> A"
+ using subgroup.m_closed assms unfolding FactGroup_def by fastforce
+ hence "H #> (x \<otimes> y) \<in> A"
+ using xy rcos_sum by force
+ with xy show "x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}" by blast
+ next
+ have "H #> \<one> \<in> A"
+ using assms subgroup.one_closed subset by fastforce
+ with assms one_closed show "\<one> \<in> {x \<in> carrier G. H #> x \<in> A}" by simp
+ next
+ fix x
+ assume x: "x \<in> {x \<in> carrier G. H #> x \<in> A}"
+ hence invx: "inv x \<in> carrier G" using inv_closed by simp
+ from assms x have "set_inv (H #> x) \<in> A" using subgroup.m_inv_closed
+ using inv_FactGroup subgroup.mem_carrier by fastforce
+ with invx show "inv x \<in> {x \<in> carrier G. H #> x \<in> A}"
+ using rcos_inv x by force
+ qed
+ with assms factgroup_subgroup_union_char show ?thesis by auto
+qed
+
+lemma (in normal) factgroup_subgroup_union_normal:
+ assumes "A \<lhd> (G Mod H)"
+ shows "\<Union>A \<lhd> G"
+proof -
+ have "{x \<in> carrier G. H #> x \<in> A} \<lhd> G"
+ unfolding normal_def normal_axioms_def
+ proof (intro conjI strip)
+ from assms show "subgroup {x \<in> carrier G. H #> x \<in> A} G"
+ by (metis (full_types) factgroup_subgroup_union_char factgroup_subgroup_union_subgroup normal_imp_subgroup)
+ next
+ interpret Anormal: normal A "(G Mod H)" using assms by simp
+ show "{x \<in> carrier G. H #> x \<in> A} #> x = x <# {x \<in> carrier G. H #> x \<in> A}" if x: "x \<in> carrier G" for x
+ proof -
+ { fix y
+ assume y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
+ then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x"
+ unfolding r_coset_def by auto
+ from x(1) have Hx: "H #> x \<in> carrier (G Mod H)"
+ unfolding FactGroup_def RCOSETS_def by force
+ with x' have "(inv\<^bsub>G Mod H\<^esub> (H #> x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A"
+ using Anormal.inv_op_closed1 by auto
+ hence "(set_inv (H #> x)) <#> (H #> x') <#> (H #> x) \<in> A"
+ using inv_FactGroup Hx unfolding FactGroup_def by auto
+ hence "(H #> (inv x)) <#> (H #> x') <#> (H #> x) \<in> A"
+ using x(1) by (metis rcos_inv)
+ hence "H #> (inv x \<otimes> x' \<otimes> x) \<in> A"
+ by (metis inv_closed m_closed rcos_sum x'(1) x(1))
+ moreover have "inv x \<otimes> x' \<otimes> x \<in> carrier G"
+ using x x' by (metis inv_closed m_closed)
+ ultimately have xcoset: "x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
+ unfolding l_coset_def using x(1) by auto
+ have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = (x \<otimes> inv x) \<otimes> x' \<otimes> x"
+ by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
+ also have "\<dots> = y"
+ by (simp add: x x')
+ finally have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = y" .
+ with xcoset have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" by auto}
+ moreover
+ { fix y
+ assume y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
+ then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
+ from x(1) have invx: "inv x \<in> carrier G"
+ by (rule inv_closed)
+ hence Hinvx: "H #> (inv x) \<in> carrier (G Mod H)"
+ unfolding FactGroup_def RCOSETS_def by force
+ with x' have "(inv\<^bsub>G Mod H\<^esub> (H #> inv x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A"
+ using invx Anormal.inv_op_closed1 by auto
+ hence "(set_inv (H #> inv x)) <#> (H #> x') <#> (H #> inv x) \<in> A"
+ using inv_FactGroup Hinvx unfolding FactGroup_def by auto
+ hence "H #> (x \<otimes> x' \<otimes> inv x) \<in> A"
+ by (simp add: rcos_inv rcos_sum x x'(1))
+ moreover have "x \<otimes> x' \<otimes> inv x \<in> carrier G" using x x' by (metis inv_closed m_closed)
+ ultimately have xcoset: "(x \<otimes> x' \<otimes> inv x) \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
+ unfolding r_coset_def using invx by auto
+ have "(x \<otimes> x' \<otimes> inv x) \<otimes> x = (x \<otimes> x') \<otimes> (inv x \<otimes> x)"
+ by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
+ also have "\<dots> = y"
+ by (simp add: x x')
+ finally have "x \<otimes> x' \<otimes> inv x \<otimes> x = y".
+ with xcoset have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" by auto }
+ ultimately show ?thesis
+ by auto
+ qed
+ qed auto
+ with assms show ?thesis
+ by (metis (full_types) factgroup_subgroup_union_char normal_imp_subgroup)
+qed
+
+lemma (in normal) factgroup_subgroup_union_factor:
+ assumes "subgroup A (G Mod H)"
+ shows "A = rcosets\<^bsub>G\<lparr>carrier := \<Union>A\<rparr>\<^esub> H"
+ using assms subgroup.mem_carrier factgroup_subgroup_union_char by (fastforce simp: RCOSETS_def FactGroup_def)
+
+
+section \<open>Flattening the type of group carriers\<close>
+
+text \<open>Flattening here means to convert the type of group elements from 'a set to 'a.
+This is possible whenever the empty set is not an element of the group. By Jakob von Raumer\<close>
+
+
+definition flatten where
+ "flatten (G::('a set, 'b) monoid_scheme) rep = \<lparr>carrier=(rep ` (carrier G)),
+ monoid.mult=(\<lambda> x y. rep ((the_inv_into (carrier G) rep x) \<otimes>\<^bsub>G\<^esub> (the_inv_into (carrier G) rep y))),
+ one=rep \<one>\<^bsub>G\<^esub> \<rparr>"
+
+lemma flatten_set_group_hom:
+ assumes group: "group G"
+ assumes inj: "inj_on rep (carrier G)"
+ shows "rep \<in> hom G (flatten G rep)"
+ by (force simp add: hom_def flatten_def inj the_inv_into_f_f)
+
+lemma flatten_set_group:
+ assumes "group G" "inj_on rep (carrier G)"
+ shows "group (flatten G rep)"
+proof (rule groupI)
+ fix x y
+ assume "x \<in> carrier (flatten G rep)" and "y \<in> carrier (flatten G rep)"
+ then show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)"
+ using assms group.surj_const_mult the_inv_into_f_f by (fastforce simp: flatten_def)
+next
+ show "\<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)"
+ unfolding flatten_def by (simp add: assms group.is_monoid)
+next
+ fix x y z
+ assume "x \<in> carrier (flatten G rep)" "y \<in> carrier (flatten G rep)" "z \<in> carrier (flatten G rep)"
+ then show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)"
+ by (auto simp: assms flatten_def group.is_monoid monoid.m_assoc monoid.m_closed the_inv_into_f_f)
+next
+ fix x
+ assume x: "x \<in> carrier (flatten G rep)"
+ then show "\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x"
+ by (auto simp: assms group.is_monoid the_inv_into_f_f flatten_def)
+ then have "\<exists>y\<in>carrier G. rep (y \<otimes>\<^bsub>G\<^esub> z) = rep \<one>\<^bsub>G\<^esub>" if "z \<in> carrier G" for z
+ by (metis \<open>group G\<close> group.l_inv_ex that)
+ with assms x show "\<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>"
+ by (auto simp: flatten_def the_inv_into_f_f)
+qed
+
+lemma (in normal) flatten_set_group_mod_inj:
+ shows "inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))"
+proof (rule inj_onI)
+ fix U V
+ assume U: "U \<in> carrier (G Mod H)" and V: "V \<in> carrier (G Mod H)"
+ then obtain g h where g: "U = H #> g" "g \<in> carrier G" and h: "V = H #> h" "h \<in> carrier G"
+ unfolding FactGroup_def RCOSETS_def by auto
+ hence notempty: "U \<noteq> {}" "V \<noteq> {}"
+ by (metis empty_iff is_subgroup rcos_self)+
+ assume "(SOME g. g \<in> U) = (SOME g. g \<in> V)"
+ with notempty have "(SOME g. g \<in> U) \<in> U \<inter> V"
+ by (metis IntI ex_in_conv someI)
+ thus "U = V"
+ by (metis Int_iff g h is_subgroup repr_independence)
+qed
+
+lemma (in normal) flatten_set_group_mod:
+ shows "group (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+ by (simp add: factorgroup_is_group flatten_set_group flatten_set_group_mod_inj)
+
+lemma (in normal) flatten_set_group_mod_iso:
+ shows "(\<lambda>U. SOME g. g \<in> U) \<in> iso (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+proof -
+ have "(\<lambda>U. SOME g. g \<in> U) \<in> hom (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+ using factorgroup_is_group flatten_set_group_hom flatten_set_group_mod_inj by blast
+ moreover
+ have "inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))"
+ using flatten_set_group_mod_inj by blast
+ ultimately show ?thesis
+ by (simp add: iso_def bij_betw_def flatten_def)
+qed
+
end
--- a/src/HOL/Algebra/Group.thy Mon Feb 27 20:51:47 2023 +0100
+++ b/src/HOL/Algebra/Group.thy Tue Feb 28 11:20:01 2023 +0000
@@ -674,6 +674,9 @@
by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
qed
+lemma (in group) triv_subgroup: "subgroup {\<one>} G"
+ by (auto simp: subgroup_def)
+
lemma subgroup_is_submonoid:
assumes "subgroup H G" shows "submonoid H G"
using assms by (auto intro: submonoid.intro simp add: subgroup_def)
@@ -1362,6 +1365,12 @@
using group_hom.img_is_subgroup[of "G \<lparr> carrier := I \<rparr>" H h] by simp
qed
+lemma (in subgroup) iso_subgroup: \<^marker>\<open>contributor \<open>Jakob von Raumer\<close>\<close>
+ assumes "group G" "group F"
+ assumes "\<phi> \<in> iso G F"
+ shows "subgroup (\<phi> ` H) F"
+ by (metis assms Group.iso_iff group_hom.intro group_hom_axioms_def group_hom.subgroup_img_is_subgroup subgroup_axioms)
+
lemma (in group_hom) induced_group_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "subgroup I G"
shows "group_hom (G \<lparr> carrier := I \<rparr>) (H \<lparr> carrier := h ` I \<rparr>) h"
@@ -1374,6 +1383,24 @@
subgroup.subgroup_is_group[OF subgroup_img_is_subgroup[OF assms] is_group] by simp
qed
+text \<open>An isomorphism restricts to an isomorphism of subgroups.\<close>
+
+lemma iso_restrict:
+ assumes "\<phi> \<in> iso G F"
+ assumes groups: "group G" "group F"
+ assumes HG: "subgroup H G"
+ shows "(restrict \<phi> H) \<in> iso (G\<lparr>carrier := H\<rparr>) (F\<lparr>carrier := \<phi> ` H\<rparr>)"
+proof -
+ have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y"
+ by (meson assms hom_mult iso_imp_homomorphism subgroup.mem_carrier)
+ moreover have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y = undefined"
+ by (simp add: HG subgroup.m_closed)
+ moreover have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y"
+ by (smt (verit, ccfv_SIG) assms group.iso_iff_group_isomorphisms group_isomorphisms_def subgroup.mem_carrier)
+ ultimately show ?thesis
+ by (auto simp: iso_def hom_def bij_betw_def inj_on_def)
+qed
+
lemma (in group) canonical_inj_is_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "subgroup H G"
shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
@@ -1636,9 +1663,8 @@
qed
lemma (in group) subgroups_Inter_pair :
- assumes "subgroup I G"
- and "subgroup J G"
- shows "subgroup (I\<inter>J) G" using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
+ assumes "subgroup I G" "subgroup J G" shows "subgroup (I\<inter>J) G"
+ using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
theorem (in group) subgroups_complete_lattice:
"complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = (=), le = (\<subseteq>)\<rparr>"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/SimpleGroups.thy Tue Feb 28 11:20:01 2023 +0000
@@ -0,0 +1,95 @@
+(* Title: Simple Groups
+ Author: Jakob von Raumer, Karlsruhe Institute of Technology
+ Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
+*)
+
+theory SimpleGroups
+imports Coset "HOL-Computational_Algebra.Primes"
+begin
+
+section \<open>Simple Groups\<close>
+
+locale simple_group = group +
+ assumes order_gt_one: "order G > 1"
+ assumes no_real_normal_subgroup: "\<And>H. H \<lhd> G \<Longrightarrow> (H = carrier G \<or> H = {\<one>})"
+
+lemma (in simple_group) is_simple_group: "simple_group G"
+ by (rule simple_group_axioms)
+
+text \<open>Simple groups are non-trivial.\<close>
+
+lemma (in simple_group) simple_not_triv: "carrier G \<noteq> {\<one>}"
+ using order_gt_one unfolding order_def by auto
+
+text \<open>Every group of prime order is simple\<close>
+
+lemma (in group) prime_order_simple:
+ assumes prime: "prime (order G)"
+ shows "simple_group G"
+proof
+ from prime show "1 < order G"
+ unfolding prime_nat_iff by auto
+next
+ fix H
+ assume "H \<lhd> G"
+ hence HG: "subgroup H G" unfolding normal_def by simp
+ hence "card H dvd order G"
+ by (metis dvd_triv_right lagrange)
+ with prime have "card H = 1 \<or> card H = order G"
+ unfolding prime_nat_iff by simp
+ thus "H = carrier G \<or> H = {\<one>}"
+ proof
+ assume "card H = 1"
+ moreover from HG have "\<one> \<in> H" by (metis subgroup.one_closed)
+ ultimately show ?thesis by (auto simp: card_Suc_eq)
+ next
+ assume "card H = order G"
+ moreover from HG have "H \<subseteq> carrier G" unfolding subgroup_def by simp
+ moreover from prime have "finite (carrier G)"
+ using order_gt_0_iff_finite by force
+ ultimately show ?thesis
+ unfolding order_def by (metis card_subset_eq)
+ qed
+qed
+
+text \<open>Being simple is a property that is preserved by isomorphisms.\<close>
+
+lemma (in simple_group) iso_simple:
+ assumes H: "group H"
+ assumes iso: "\<phi> \<in> iso G H"
+ shows "simple_group H"
+unfolding simple_group_def simple_group_axioms_def
+proof (intro conjI strip H)
+ from iso have "order G = order H" unfolding iso_def order_def using bij_betw_same_card by auto
+ with order_gt_one show "1 < order H" by simp
+next
+ have inv_iso: "(inv_into (carrier G) \<phi>) \<in> iso H G" using iso
+ by (simp add: iso_set_sym)
+ fix N
+ assume NH: "N \<lhd> H"
+ then interpret Nnormal: normal N H by simp
+ define M where "M = (inv_into (carrier G) \<phi>) ` N"
+ hence MG: "M \<lhd> G"
+ using inv_iso NH H by (metis is_group iso_normal_subgroup)
+ have surj: "\<phi> ` carrier G = carrier H"
+ using iso unfolding iso_def bij_betw_def by simp
+ hence MN: "\<phi> ` M = N"
+ unfolding M_def using Nnormal.subset image_inv_into_cancel by metis
+ then have "N = {\<one>\<^bsub>H\<^esub>}" if "M = {\<one>}"
+ using Nnormal.subgroup_axioms subgroup.one_closed that by force
+ then show "N = carrier H \<or> N = {\<one>\<^bsub>H\<^esub>}"
+ by (metis MG MN no_real_normal_subgroup surj)
+qed
+
+text \<open>As a corollary of this: Factorizing a group by itself does not result in a simple group!\<close>
+
+lemma (in group) self_factor_not_simple: "\<not> simple_group (G Mod (carrier G))"
+proof
+ assume assm: "simple_group (G Mod (carrier G))"
+ with self_factor_iso simple_group.iso_simple have "simple_group (G\<lparr>carrier := {\<one>}\<rparr>)"
+ using subgroup_imp_group triv_subgroup by blast
+ thus False
+ using simple_group.simple_not_triv by force
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/SndIsomorphismGrp.thy Tue Feb 28 11:20:01 2023 +0000
@@ -0,0 +1,207 @@
+(* Title: The Second Isomorphism Theorem for Groups
+ Author: Jakob von Raumer, Karlsruhe Institute of Technology
+ Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
+*)
+
+theory SndIsomorphismGrp
+imports Coset
+begin
+
+section \<open>The Second Isomorphism Theorem for Groups\<close>
+
+text \<open>This theory provides a proof of the second isomorphism theorems for groups.
+The theorems consist of several facts about normal subgroups.\<close>
+
+text \<open>The first lemma states that whenever we have a subgroup @{term S} and
+a normal subgroup @{term H} of a group @{term G}, their intersection is normal
+in @{term G}\<close>
+
+locale second_isomorphism_grp = normal +
+ fixes S:: "'a set"
+ assumes subgrpS: "subgroup S G"
+
+context second_isomorphism_grp
+begin
+
+interpretation groupS: group "G\<lparr>carrier := S\<rparr>"
+ using subgrpS
+ by (metis subgroup_imp_group)
+
+lemma normal_subgrp_intersection_normal:
+ shows "S \<inter> H \<lhd> (G\<lparr>carrier := S\<rparr>)"
+proof(auto simp: groupS.normal_inv_iff)
+ from subgrpS is_subgroup have "\<And>x. x \<in> {S, H} \<Longrightarrow> subgroup x G" by auto
+ hence "subgroup (\<Inter> {S, H}) G" using subgroups_Inter by blast
+ hence "subgroup (S \<inter> H) G" by auto
+ moreover have "S \<inter> H \<subseteq> S" by simp
+ ultimately show "subgroup (S \<inter> H) (G\<lparr>carrier := S\<rparr>)"
+ by (simp add: subgroup_incl subgrpS)
+next
+ fix g h
+ assume g: "g \<in> S" and hH: "h \<in> H" and hS: "h \<in> S"
+ from g hH subgrpS show "g \<otimes> h \<otimes> inv\<^bsub>G\<lparr>carrier := S\<rparr>\<^esub> g \<in> H"
+ by (metis inv_op_closed2 subgroup.mem_carrier m_inv_consistent)
+ from g hS subgrpS show "g \<otimes> h \<otimes> inv\<^bsub>G\<lparr>carrier := S\<rparr>\<^esub> g \<in> S"
+ by (metis subgroup.m_closed subgroup.m_inv_closed m_inv_consistent)
+qed
+
+lemma normal_set_mult_subgroup:
+ shows "subgroup (H <#> S) G"
+proof(rule subgroupI)
+ show "H <#> S \<subseteq> carrier G"
+ by (metis setmult_subset_G subgroup.subset subgrpS subset)
+next
+ have "\<one> \<in> H" "\<one> \<in> S"
+ using is_subgroup subgrpS subgroup.one_closed by auto
+ hence "\<one> \<otimes> \<one> \<in> H <#> S"
+ unfolding set_mult_def by blast
+ thus "H <#> S \<noteq> {}" by auto
+next
+ fix g
+ assume g: "g \<in> H <#> S"
+ then obtain h s where h: "h \<in> H" and s: "s \<in> S" and ghs: "g = h \<otimes> s" unfolding set_mult_def
+ by auto
+ hence "s \<in> carrier G" by (metis subgroup.mem_carrier subgrpS)
+ with h ghs obtain h' where h': "h' \<in> H" and "g = s \<otimes> h'"
+ using coset_eq unfolding r_coset_def l_coset_def by auto
+ with s have "inv g = (inv h') \<otimes> (inv s)"
+ by (metis inv_mult_group mem_carrier subgroup.mem_carrier subgrpS)
+ moreover from h' s subgrpS have "inv h' \<in> H" "inv s \<in> S"
+ using subgroup.m_inv_closed m_inv_closed by auto
+ ultimately show "inv g \<in> H <#> S"
+ unfolding set_mult_def by auto
+next
+ fix g g'
+ assume g: "g \<in> H <#> S" and h: "g' \<in> H <#> S"
+ then obtain h h' s s' where hh'ss': "h \<in> H" "h' \<in> H" "s \<in> S" "s' \<in> S" and "g = h \<otimes> s" and "g' = h' \<otimes> s'"
+ unfolding set_mult_def by auto
+ hence "g \<otimes> g' = (h \<otimes> s) \<otimes> (h' \<otimes> s')" by metis
+ also from hh'ss' have inG: "h \<in> carrier G" "h' \<in> carrier G" "s \<in> carrier G" "s' \<in> carrier G"
+ using subgrpS mem_carrier subgroup.mem_carrier by force+
+ hence "(h \<otimes> s) \<otimes> (h' \<otimes> s') = h \<otimes> (s \<otimes> h') \<otimes> s'"
+ using m_assoc by auto
+ also from hh'ss' inG obtain h'' where h'': "h'' \<in> H" and "s \<otimes> h' = h'' \<otimes> s"
+ using coset_eq unfolding r_coset_def l_coset_def
+ by fastforce
+ hence "h \<otimes> (s \<otimes> h') \<otimes> s' = h \<otimes> (h'' \<otimes> s) \<otimes> s'"
+ by simp
+ also from h'' inG have "... = (h \<otimes> h'') \<otimes> (s \<otimes> s')"
+ using m_assoc mem_carrier by auto
+ finally have "g \<otimes> g' = h \<otimes> h'' \<otimes> (s \<otimes> s')".
+ moreover have "... \<in> H <#> S"
+ unfolding set_mult_def using h'' hh'ss' subgrpS subgroup.m_closed by fastforce
+ ultimately show "g \<otimes> g' \<in> H <#> S"
+ by simp
+qed
+
+lemma H_contained_in_set_mult:
+ shows "H \<subseteq> H <#> S"
+proof
+ fix x
+ assume x: "x \<in> H"
+ have "x \<otimes> \<one> \<in> H <#> S" unfolding set_mult_def
+ using second_isomorphism_grp.subgrpS second_isomorphism_grp_axioms subgroup.one_closed x by force
+ with x show "x \<in> H <#> S" by (metis mem_carrier r_one)
+qed
+
+lemma S_contained_in_set_mult:
+ shows "S \<subseteq> H <#> S"
+proof
+ fix s
+ assume s: "s \<in> S"
+ then have "\<one> \<otimes> s \<in> H <#> S" unfolding set_mult_def by force
+ with s show "s \<in> H <#> S" using subgrpS subgroup.mem_carrier l_one by force
+qed
+
+lemma normal_intersection_hom:
+ shows "group_hom (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g)"
+proof -
+ have "group ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+ by (simp add: H_contained_in_set_mult normal.factorgroup_is_group normal_axioms
+ normal_restrict_supergroup normal_set_mult_subgroup)
+ moreover
+ { fix g
+ assume g: "g \<in> S"
+ with g have "g \<in> H <#> S"
+ using S_contained_in_set_mult by blast
+ hence "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+ unfolding FactGroup_def RCOSETS_def r_coset_def by auto }
+ moreover
+ have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
+ using normal.rcos_sum normal_axioms subgroup.mem_carrier subgrpS by fastforce
+ ultimately show ?thesis
+ by (auto simp: group_hom_def group_hom_axioms_def hom_def)
+qed
+
+lemma normal_intersection_hom_kernel:
+ shows "kernel (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g) = H \<inter> S"
+proof -
+ have "kernel (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g)
+ = {g \<in> S. H #> g = \<one>\<^bsub>(G\<lparr>carrier := H <#> S\<rparr>) Mod H\<^esub>}"
+ unfolding kernel_def by auto
+ also have "... = {g \<in> S. H #> g = H}"
+ unfolding FactGroup_def by auto
+ also have "... = {g \<in> S. g \<in> H}"
+ by (meson coset_join1 is_group rcos_const subgroupE(1) subgroup_axioms subgrpS subset_eq)
+ also have "... = H \<inter> S" by auto
+ finally show ?thesis.
+qed
+
+lemma normal_intersection_hom_surj:
+ shows "(\<lambda>g. H #> g) ` carrier (G\<lparr>carrier := S\<rparr>) = carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+proof auto
+ fix g
+ assume "g \<in> S"
+ hence "g \<in> H <#> S"
+ using S_contained_in_set_mult by auto
+ thus "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+ unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+next
+ fix x
+ assume "x \<in> carrier (G\<lparr>carrier := H <#> S\<rparr> Mod H)"
+ then obtain h s where h: "h \<in> H" and s: "s \<in> S" and "x = H #> (h \<otimes> s)"
+ unfolding FactGroup_def RCOSETS_def r_coset_def set_mult_def by auto
+ hence "x = (H #> h) #> s"
+ by (metis h s coset_mult_assoc mem_carrier subgroup.mem_carrier subgrpS subset)
+ also have "... = H #> s"
+ by (metis h is_group rcos_const)
+ finally have "x = H #> s".
+ with s show "x \<in> (#>) H ` S"
+ by simp
+qed
+
+text \<open>Finally we can prove the actual isomorphism theorem:\<close>
+
+theorem normal_intersection_quotient_isom:
+ shows "(\<lambda>X. the_elem ((\<lambda>g. H #> g) ` X)) \<in> iso ((G\<lparr>carrier := S\<rparr>) Mod (H \<inter> S)) (((G\<lparr>carrier := H <#> S\<rparr>)) Mod H)"
+using normal_intersection_hom_kernel[symmetric] normal_intersection_hom normal_intersection_hom_surj
+by (metis group_hom.FactGroup_iso_set)
+
+end
+
+
+corollary (in group) normal_subgroup_set_mult_closed:
+ assumes "M \<lhd> G" and "N \<lhd> G"
+ shows "M <#> N \<lhd> G"
+proof (rule normalI)
+ from assms show "subgroup (M <#> N) G"
+ using second_isomorphism_grp.normal_set_mult_subgroup normal_imp_subgroup
+ unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def by force
+next
+ show "\<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)"
+ proof
+ fix x
+ assume x: "x \<in> carrier G"
+ have "M <#> N #> x = M <#> (N #> x)"
+ by (metis assms normal_inv_iff setmult_rcos_assoc subgroup.subset x)
+ also have "\<dots> = M <#> (x <# N)"
+ by (metis assms(2) normal.coset_eq x)
+ also have "\<dots> = (M #> x) <#> N"
+ by (metis assms normal_imp_subgroup rcos_assoc_lcos subgroup.subset x)
+ also have "\<dots> = x <# (M <#> N)"
+ by (simp add: assms normal.coset_eq normal_imp_subgroup setmult_lcos_assoc subgroup.subset x)
+ finally show "M <#> N #> x = x <# (M <#> N)" .
+ qed
+qed
+
+end