Quelle  SndIsomorphismGrp.thy   Sprache: Isabelle

(*  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\<^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"
  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 have "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
  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 = 1🚫(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