(* 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\carrier := S\" using subgrpS by (metis subgroup_imp_group)
lemma normal_subgrp_intersection_normal: shows"S \ H \ (G\carrier := S\)" proof(auto simp: groupS.normal_inv_iff) from subgrpS is_subgroup have"\x. x \ {S, H} \ subgroup x G" by auto hence"subgroup (\ {S, H}) G" using subgroups_Inter by blast hence"subgroup (S \ H) G" by auto moreoverhave"S \ H \ S" by simp ultimatelyshow"subgroup (S \ H) (G\carrier := S\)" by (simp add: subgroup_incl subgrpS) next fix g h assume g: "g \ S" and hH: "h \ H" and hS: "h \ S" from g hH subgrpS show"g \ h \ inv\<^bsub>G\carrier := S\\<^esub> g \ H" by (metis inv_op_closed2 subgroup.mem_carrier m_inv_consistent) from g hS subgrpS show"g \ h \ inv\<^bsub>G\carrier := S\\<^esub> g \ 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 \ carrier G" by (metis setmult_subset_G subgroup.subset subgrpS subset) next have"\ \ H" "\ \ S" using is_subgroup subgrpS subgroup.one_closed by auto hence"\ \ \ \ H <#> S" unfolding set_mult_def by blast thus"H <#> S \ {}" by auto next fix g assume g: "g \ H <#> S" thenobtain h s where h: "h \ H" and s: "s \ S" and ghs: "g = h \ s" unfolding set_mult_def by auto hence"s \ carrier G" by (metis subgroup.mem_carrier subgrpS) with h ghs obtain h' where h': "h' \ H" and "g = s \ h'" using coset_eq unfolding r_coset_def l_coset_def by auto with s have"inv g = (inv h') \ (inv s)" by (metis inv_mult_group mem_carrier subgroup.mem_carrier subgrpS) moreoverfrom h' s subgrpS have "inv h'\<in> H" "inv s \<in> S" using subgroup.m_inv_closed m_inv_closed by auto ultimatelyshow"inv g \ H <#> S" unfolding set_mult_def by auto next fix g g' assume g: "g \ H <#> S" and h: "g' \ H <#> S" thenobtain h h' s s'where hh'ss': "h \ H" "h' \ H" "s \ S" "s' \ S" and "g = h \ s" and "g' = h' \ s'" unfolding set_mult_def by auto hence"g \ g' = (h \ s) \ (h' \ s')" by metis alsofrom hh'ss'have inG: "h \ carrier G" "h' \ carrier G" "s \ carrier G" "s' \ carrier G" using subgrpS mem_carrier subgroup.mem_carrier by force+ hence"(h \ s) \ (h' \ s') = h \ (s \ h') \ s'" using m_assoc by auto alsofrom hh'ss' inG obtain h''where h'': "h'' \ H" and "s \ h' = h'' \ s" using coset_eq unfolding r_coset_def l_coset_def by fastforce hence"h \ (s \ h') \ s' = h \ (h'' \ s) \ s'" by simp alsofrom h'' inG have"... = (h \ h'') \ (s \ s')" using m_assoc mem_carrier by auto finallyhave"g \ g' = h \ h'' \ (s \ s')". moreoverhave"... \ H <#> S" unfolding set_mult_def using h'' hh'ss' subgrpS subgroup.m_closed by fastforce ultimatelyshow"g \ g' \ H <#> S" by simp qed
lemma H_contained_in_set_mult: shows"H \ H <#> S" proof fix x assume x: "x \ H" have"x \ \ \ 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 \ H <#> S" by (metis mem_carrier r_one) qed
lemma S_contained_in_set_mult: shows"S \ H <#> S" proof fix s assume s: "s \ S" thenhave"\ \ s \ H <#> S" unfolding set_mult_def by force with s show"s \ H <#> S" using subgrpS subgroup.mem_carrier l_one by force qed
lemma normal_intersection_hom: shows"group_hom (G\carrier := S\) ((G\carrier := H <#> S\) Mod H) (\g. H #> g)" proof - have"group ((G\carrier := H <#> S\) Mod H)" by (simp add: H_contained_in_set_mult normal.factorgroup_is_group normal_axioms
normal_restrict_supergroup normal_set_mult_subgroup) moreoverhave"H #> g \ carrier ((G\carrier := H <#> S\) Mod H)" if g: "g \ S" for g proof - from g that have"g \ H <#> S" using S_contained_in_set_mult by blast thus"H #> g \ carrier ((G\carrier := H <#> S\) Mod H)" unfolding FactGroup_def RCOSETS_def r_coset_def by auto qed moreoverhave"\x y. \x \ S; y \ S\ \ H #> x \ y = H #> x <#> (H #> y)" using normal.rcos_sum normal_axioms subgroup.mem_carrier subgrpS by fastforce ultimatelyshow ?thesis by (auto simp: group_hom_def group_hom_axioms_def hom_def) qed
lemma normal_intersection_hom_kernel: shows"kernel (G\carrier := S\) ((G\carrier := H <#> S\) Mod H) (\g. H #> g) = H \ S" proof - have"kernel (G\carrier := S\) ((G\carrier := H <#> S\) Mod H) (\g. H #> g)
= {g \<in> S. H #> g = \<one>\<^bsub>(G\<lparr>carrier := H <#> S\<rparr>) Mod H\<^esub>}" unfolding kernel_def by auto alsohave"... = {g \ S. H #> g = H}" unfolding FactGroup_def by auto alsohave"... = {g \ S. g \ H}" by (meson coset_join1 is_group rcos_const subgroupE(1) subgroup_axioms subgrpS subset_eq) alsohave"... = H \ S" by auto finallyshow ?thesis. qed
lemma normal_intersection_hom_surj: shows"(\g. H #> g) ` carrier (G\carrier := S\) = carrier ((G\carrier := H <#> S\) Mod H)" proof auto fix g assume"g \ S" hence"g \ H <#> S" using S_contained_in_set_mult by auto thus"H #> g \ carrier ((G\carrier := H <#> S\) Mod H)" unfolding FactGroup_def RCOSETS_def r_coset_def by auto next fix x assume"x \ carrier (G\carrier := H <#> S\ Mod H)" thenobtain h s where h: "h \ H" and s: "s \ S" and "x = H #> (h \ 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) alsohave"... = H #> s" by (metis h is_group rcos_const) finallyhave"x = H #> s". with s show"x \ (#>) H ` S" by simp qed
text\<open>Finally we can prove the actual isomorphism theorem:\<close>
theorem normal_intersection_quotient_isom: shows"(\X. the_elem ((\g. H #> g) ` X)) \ iso ((G\carrier := S\) Mod (H \ S)) (((G\carrier := H <#> S\)) 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 \ G" and "N \ G" shows"M <#> N \ 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"\x\carrier G. M <#> N #> x = x <# (M <#> N)" proof fix x assume x: "x \ carrier G" have"M <#> N #> x = M <#> (N #> x)" by (metis assms normal_inv_iff setmult_rcos_assoc subgroup.subset x) alsohave"\ = M <#> (x <# N)" by (metis assms(2) normal.coset_eq x) alsohave"\ = (M #> x) <#> N" by (metis assms normal_imp_subgroup rcos_assoc_lcos subgroup.subset x) alsohave"\ = x <# (M <#> N)" by (simp add: assms normal.coset_eq normal_imp_subgroup setmult_lcos_assoc subgroup.subset x) finallyshow"M <#> N #> x = x <# (M <#> N)" . qed qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
