(* 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 ‹The Second Isomorphism Theorem for Groups› text ‹This theory provides a proof of the second isomorphism theorems for groups. The theorems consist of several facts about normal subgroups.› text ‹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}› 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 moreover have "S ∩ H ⊆ S" by simp ultimately show "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⇘G⦇carrier := S⦈⇙ g ∈ H" by (metis inv_op_closed2 subgroup.mem_carrier m_inv_consistent) from g hS subgrpS show "g ⊗ h ⊗ inv⇘G⦇carrier := S⦈⇙ 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" then obtain 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) moreover from h' s subgrpS have "inv h' ∈ H" "inv s ∈ S" using subgroup.m_inv_closed m_inv_closed by auto ultimately show "inv g ∈ H <#> S" unfolding set_mult_def by auto next fix g g' assume g: "g ∈ H <#> S" and h: "g' ∈ H <#> S" then obtain 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 also from 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 also from 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 also from h'' inG have "... = (h ⊗ h'') ⊗ (s ⊗ s')" using m_assoc mem_carrier by auto finally have "g ⊗ g' = h ⊗ h'' ⊗ (s ⊗ s')". moreover have "... ∈ H <#> S" unfolding set_mult_def using h'' hh'ss' subgrpS subgroup.m_closed by fastforce ultimately show "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" then have "𝟭 ⊗ 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) moreover { fix g assume g: "g ∈ S" with g have "g ∈ H <#> S" using S_contained_in_set_mult by blast hence "H #> g ∈ carrier ((G⦇carrier := H <#> S⦈) Mod H)" unfolding FactGroup_def RCOSETS_def r_coset_def by auto } moreover have "⋀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 ultimately show ?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 ∈ S. H #> g = 𝟭⇘(G⦇carrier := H <#> S⦈) Mod H⇙}" unfolding kernel_def by auto also have "... = {g ∈ S. H #> g = H}" unfolding FactGroup_def by auto also have "... = {g ∈ S. g ∈ H}" by (meson coset_join1 is_group rcos_const subgroupE(1) subgroup_axioms subgrpS subset_eq) also have "... = H ∩ S" by auto finally show ?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)" then obtain 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) also have "... = H #> s" by (metis h is_group rcos_const) finally have "x = H #> s". with s show "x ∈ (#>) H ` S" by simp qed text ‹Finally we can prove the actual isomorphism theorem:› 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) also have "… = M <#> (x <# N)" by (metis assms(2) normal.coset_eq x) also have "… = (M #> x) <#> N" by (metis assms normal_imp_subgroup rcos_assoc_lcos subgroup.subset x) also have "… = 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