# Theory Coset

Up to index of Isabelle/HOL/Free-Groups

theory Coset
imports Group
`(*  Title:      HOL/Algebra/Coset.thy    Author:     Florian Kammueller    Author:     L C Paulson    Author:     Stephan Hohe*)theory Cosetimports Groupbeginsection {*Cosets and Quotient Groups*}definition  r_coset    :: "[_, 'a set, 'a] => 'a set"    (infixl "#>\<index>" 60)  where "H #>⇘G⇙ a = (\<Union>h∈H. {h ⊗⇘G⇙ a})"definition  l_coset    :: "[_, 'a, 'a set] => 'a set"    (infixl "<#\<index>" 60)  where "a <#⇘G⇙ H = (\<Union>h∈H. {a ⊗⇘G⇙ h})"definition  RCOSETS  :: "[_, 'a set] => ('a set)set"   ("rcosets\<index> _" [81] 80)  where "rcosets⇘G⇙ H = (\<Union>a∈carrier G. {H #>⇘G⇙ a})"definition  set_mult  :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)  where "H <#>⇘G⇙ K = (\<Union>h∈H. \<Union>k∈K. {h ⊗⇘G⇙ k})"definition  SET_INV :: "[_,'a set] => 'a set"  ("set'_inv\<index> _" [81] 80)  where "set_inv⇘G⇙ H = (\<Union>h∈H. {inv⇘G⇙ h})"locale normal = subgroup + group +  assumes coset_eq: "(∀x ∈ carrier G. H #> x = x <# H)"abbreviation  normal_rel :: "['a set, ('a, 'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60) where  "H \<lhd> G ≡ normal H G"subsection {*Basic Properties of Cosets*}lemma (in group) coset_mult_assoc:     "[| M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]      ==> (M #> g) #> h = M #> (g ⊗ h)"by (force simp add: r_coset_def m_assoc)lemma (in group) coset_mult_one [simp]: "M ⊆ carrier G ==> M #> \<one> = M"by (force simp add: r_coset_def)lemma (in group) coset_mult_inv1:     "[| M #> (x ⊗ (inv y)) = M;  x ∈ carrier G ; y ∈ carrier G;         M ⊆ carrier G |] ==> M #> x = M #> y"apply (erule subst [of concl: "%z. M #> x = z #> y"])apply (simp add: coset_mult_assoc m_assoc)donelemma (in group) coset_mult_inv2:     "[| M #> x = M #> y;  x ∈ carrier G;  y ∈ carrier G;  M ⊆ carrier G |]      ==> M #> (x ⊗ (inv y)) = M "apply (simp add: coset_mult_assoc [symmetric])apply (simp add: coset_mult_assoc)donelemma (in group) coset_join1:     "[| H #> x = H;  x ∈ carrier G;  subgroup H G |] ==> x ∈ H"apply (erule subst)apply (simp add: r_coset_def)apply (blast intro: l_one subgroup.one_closed sym)donelemma (in group) solve_equation:    "[|subgroup H G; x ∈ H; y ∈ H|] ==> ∃h∈H. y = h ⊗ x"apply (rule bexI [of _ "y ⊗ (inv x)"])apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc                      subgroup.subset [THEN subsetD])donelemma (in group) repr_independence:     "[|y ∈ H #> x;  x ∈ carrier G; subgroup H G|] ==> H #> x = H #> y"by (auto simp add: r_coset_def m_assoc [symmetric]                   subgroup.subset [THEN subsetD]                   subgroup.m_closed solve_equation)lemma (in group) coset_join2:     "[|x ∈ carrier G;  subgroup H G;  x∈H|] ==> H #> x = H"  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}by (force simp add: subgroup.m_closed r_coset_def solve_equation)lemma (in monoid) r_coset_subset_G:     "[| H ⊆ carrier G; x ∈ carrier G |] ==> H #> x ⊆ carrier G"by (auto simp add: r_coset_def)lemma (in group) rcosI:     "[| h ∈ H; H ⊆ carrier G; x ∈ carrier G|] ==> h ⊗ x ∈ H #> x"by (auto simp add: r_coset_def)lemma (in group) rcosetsI:     "[|H ⊆ carrier G; x ∈ carrier G|] ==> H #> x ∈ rcosets H"by (auto simp add: RCOSETS_def)text{*Really needed?*}lemma (in group) transpose_inv:     "[| x ⊗ y = z;  x ∈ carrier G;  y ∈ carrier G;  z ∈ carrier G |]      ==> (inv x) ⊗ z = y"by (force simp add: m_assoc [symmetric])lemma (in group) rcos_self: "[| x ∈ carrier G; subgroup H G |] ==> x ∈ H #> x"apply (simp add: r_coset_def)apply (blast intro: sym l_one subgroup.subset [THEN subsetD]                    subgroup.one_closed)donetext (in group) {* Opposite of @{thm [source] "repr_independence"} *}lemma (in group) repr_independenceD:  assumes "subgroup H G"  assumes ycarr: "y ∈ carrier G"      and repr:  "H #> x = H #> y"  shows "y ∈ H #> x"proof -  interpret subgroup H G by fact  show ?thesis  apply (subst repr)  apply (intro rcos_self)   apply (rule ycarr)   apply (rule is_subgroup)  doneqedtext {* Elements of a right coset are in the carrier *}lemma (in subgroup) elemrcos_carrier:  assumes "group G"  assumes acarr: "a ∈ carrier G"    and a': "a' ∈ H #> a"  shows "a' ∈ carrier G"proof -  interpret group G by fact  from subset and acarr  have "H #> a ⊆ carrier G" by (rule r_coset_subset_G)  from this and a'  show "a' ∈ carrier G"    by fastqedlemma (in subgroup) rcos_const:  assumes "group G"  assumes hH: "h ∈ H"  shows "H #> h = H"proof -  interpret group G by fact  show ?thesis apply (unfold r_coset_def)    apply rule    apply rule    apply clarsimp    apply (intro subgroup.m_closed)    apply (rule is_subgroup)    apply assumption    apply (rule hH)    apply rule    apply simp  proof -    fix h'    assume h'H: "h' ∈ H"    note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]    from carr    have a: "h' = (h' ⊗ inv h) ⊗ h" by (simp add: m_assoc)    from h'H hH    have "h' ⊗ inv h ∈ H" by simp    from this and a    show "∃x∈H. h' = x ⊗ h" by fast  qedqedtext {* Step one for lemma @{text "rcos_module"} *}lemma (in subgroup) rcos_module_imp:  assumes "group G"  assumes xcarr: "x ∈ carrier G"      and x'cos: "x' ∈ H #> x"  shows "(x' ⊗ inv x) ∈ H"proof -  interpret group G by fact  from xcarr x'cos      have x'carr: "x' ∈ carrier G"      by (rule elemrcos_carrier[OF is_group])  from xcarr      have ixcarr: "inv x ∈ carrier G"      by simp  from x'cos      have "∃h∈H. x' = h ⊗ x"      unfolding r_coset_def      by fast  from this      obtain h        where hH: "h ∈ H"        and x': "x' = h ⊗ x"      by auto  from hH and subset      have hcarr: "h ∈ carrier G" by fast  note carr = xcarr x'carr hcarr  from x' and carr      have "x' ⊗ (inv x) = (h ⊗ x) ⊗ (inv x)" by fast  also from carr      have "… = h ⊗ (x ⊗ inv x)" by (simp add: m_assoc)  also from carr      have "… = h ⊗ \<one>" by simp  also from carr      have "… = h" by simp  finally      have "x' ⊗ (inv x) = h" by simp  from hH this      show "x' ⊗ (inv x) ∈ H" by simpqedtext {* Step two for lemma @{text "rcos_module"} *}lemma (in subgroup) rcos_module_rev:  assumes "group G"  assumes carr: "x ∈ carrier G" "x' ∈ carrier G"      and xixH: "(x' ⊗ inv x) ∈ H"  shows "x' ∈ H #> x"proof -  interpret group G by fact  from xixH      have "∃h∈H. x' ⊗ (inv x) = h" by fast  from this      obtain h        where hH: "h ∈ H"        and hsym: "x' ⊗ (inv x) = h"      by fast  from hH subset have hcarr: "h ∈ carrier G" by simp  note carr = carr hcarr  from hsym[symmetric] have "h ⊗ x = x' ⊗ (inv x) ⊗ x" by fast  also from carr      have "… = x' ⊗ ((inv x) ⊗ x)" by (simp add: m_assoc)  also from carr      have "… = x' ⊗ \<one>" by simp  also from carr      have "… = x'" by simp  finally      have "h ⊗ x = x'" by simp  from this[symmetric] and hH      show "x' ∈ H #> x"      unfolding r_coset_def      by fastqedtext {* Module property of right cosets *}lemma (in subgroup) rcos_module:  assumes "group G"  assumes carr: "x ∈ carrier G" "x' ∈ carrier G"  shows "(x' ∈ H #> x) = (x' ⊗ inv x ∈ H)"proof -  interpret group G by fact  show ?thesis proof  assume "x' ∈ H #> x"    from this and carr    show "x' ⊗ inv x ∈ H"      by (intro rcos_module_imp[OF is_group])  next    assume "x' ⊗ inv x ∈ H"    from this and carr    show "x' ∈ H #> x"      by (intro rcos_module_rev[OF is_group])  qedqedtext {* Right cosets are subsets of the carrier. *} lemma (in subgroup) rcosets_carrier:  assumes "group G"  assumes XH: "X ∈ rcosets H"  shows "X ⊆ carrier G"proof -  interpret group G by fact  from XH have "∃x∈ carrier G. X = H #> x"      unfolding RCOSETS_def      by fast  from this      obtain x        where xcarr: "x∈ carrier G"        and X: "X = H #> x"      by fast  from subset and xcarr      show "X ⊆ carrier G"      unfolding X      by (rule r_coset_subset_G)qedtext {* Multiplication of general subsets *}lemma (in monoid) set_mult_closed:  assumes Acarr: "A ⊆ carrier G"      and Bcarr: "B ⊆ carrier G"  shows "A <#> B ⊆ carrier G"apply rule apply (simp add: set_mult_def, clarsimp)proof -  fix a b  assume "a ∈ A"  from this and Acarr      have acarr: "a ∈ carrier G" by fast  assume "b ∈ B"  from this and Bcarr      have bcarr: "b ∈ carrier G" by fast  from acarr bcarr      show "a ⊗ b ∈ carrier G" by (rule m_closed)qedlemma (in comm_group) mult_subgroups:  assumes subH: "subgroup H G"      and subK: "subgroup K G"  shows "subgroup (H <#> K) G"apply (rule subgroup.intro)   apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])  apply (simp add: set_mult_def) apply clarsimp defer 1  apply (simp add: set_mult_def) defer 1  apply (simp add: set_mult_def, clarsimp) defer 1proof -  fix ha hb ka kb  assume haH: "ha ∈ H" and hbH: "hb ∈ H" and kaK: "ka ∈ K" and kbK: "kb ∈ K"  note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]              kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]  from carr      have "(ha ⊗ ka) ⊗ (hb ⊗ kb) = ha ⊗ (ka ⊗ hb) ⊗ kb" by (simp add: m_assoc)  also from carr      have "… = ha ⊗ (hb ⊗ ka) ⊗ kb" by (simp add: m_comm)  also from carr      have "… = (ha ⊗ hb) ⊗ (ka ⊗ kb)" by (simp add: m_assoc)  finally      have eq: "(ha ⊗ ka) ⊗ (hb ⊗ kb) = (ha ⊗ hb) ⊗ (ka ⊗ kb)" .  from haH hbH have hH: "ha ⊗ hb ∈ H" by (simp add: subgroup.m_closed[OF subH])  from kaK kbK have kK: "ka ⊗ kb ∈ K" by (simp add: subgroup.m_closed[OF subK])    from hH and kK and eq      show "∃h'∈H. ∃k'∈K. (ha ⊗ ka) ⊗ (hb ⊗ kb) = h' ⊗ k'" by fastnext  have "\<one> = \<one> ⊗ \<one>" by simp  from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this      show "∃h∈H. ∃k∈K. \<one> = h ⊗ k" by fastnext  fix h k  assume hH: "h ∈ H"     and kK: "k ∈ K"  from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]      have "inv (h ⊗ k) = inv h ⊗ inv k" by (simp add: inv_mult_group m_comm)  from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this      show "∃ha∈H. ∃ka∈K. inv (h ⊗ k) = ha ⊗ ka" by fastqedlemma (in subgroup) lcos_module_rev:  assumes "group G"  assumes carr: "x ∈ carrier G" "x' ∈ carrier G"      and xixH: "(inv x ⊗ x') ∈ H"  shows "x' ∈ x <# H"proof -  interpret group G by fact  from xixH      have "∃h∈H. (inv x) ⊗ x' = h" by fast  from this      obtain h        where hH: "h ∈ H"        and hsym: "(inv x) ⊗ x' = h"      by fast  from hH subset have hcarr: "h ∈ carrier G" by simp  note carr = carr hcarr  from hsym[symmetric] have "x ⊗ h = x ⊗ ((inv x) ⊗ x')" by fast  also from carr      have "… = (x ⊗ (inv x)) ⊗ x'" by (simp add: m_assoc[symmetric])  also from carr      have "… = \<one> ⊗ x'" by simp  also from carr      have "… = x'" by simp  finally      have "x ⊗ h = x'" by simp  from this[symmetric] and hH      show "x' ∈ x <# H"      unfolding l_coset_def      by fastqedsubsection {* Normal subgroups *}lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup H G"  by (simp add: normal_def subgroup_def)lemma (in group) normalI:   "subgroup H G ==> (∀x ∈ carrier G. H #> x = x <# H) ==> H \<lhd> G"  by (simp add: normal_def normal_axioms_def is_group)lemma (in normal) inv_op_closed1:     "[|x ∈ carrier G; h ∈ H|] ==> (inv x) ⊗ h ⊗ x ∈ H"apply (insert coset_eq) apply (auto simp add: l_coset_def r_coset_def)apply (drule bspec, assumption)apply (drule equalityD1 [THEN subsetD], blast, clarify)apply (simp add: m_assoc)apply (simp add: m_assoc [symmetric])donelemma (in normal) inv_op_closed2:     "[|x ∈ carrier G; h ∈ H|] ==> x ⊗ h ⊗ (inv x) ∈ H"apply (subgoal_tac "inv (inv x) ⊗ h ⊗ (inv x) ∈ H") apply (simp add: ) apply (blast intro: inv_op_closed1) donetext{*Alternative characterization of normal subgroups*}lemma (in group) normal_inv_iff:     "(N \<lhd> G) =       (subgroup N G & (∀x ∈ carrier G. ∀h ∈ N. x ⊗ h ⊗ (inv x) ∈ N))"      (is "_ = ?rhs")proof  assume N: "N \<lhd> G"  show ?rhs    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) next  assume ?rhs  hence sg: "subgroup N G"     and closed: "!!x. x∈carrier G ==> ∀h∈N. x ⊗ h ⊗ inv x ∈ N" by auto  hence sb: "N ⊆ carrier G" by (simp add: subgroup.subset)   show "N \<lhd> G"  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)    fix x    assume x: "x ∈ carrier G"    show "(\<Union>h∈N. {h ⊗ x}) = (\<Union>h∈N. {x ⊗ h})"    proof      show "(\<Union>h∈N. {h ⊗ x}) ⊆ (\<Union>h∈N. {x ⊗ h})"      proof clarify        fix n        assume n: "n ∈ N"         show "n ⊗ x ∈ (\<Union>h∈N. {x ⊗ h})"        proof           from closed [of "inv x"]          show "inv x ⊗ n ⊗ x ∈ N" by (simp add: x n)          show "n ⊗ x ∈ {x ⊗ (inv x ⊗ n ⊗ x)}"            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])        qed      qed    next      show "(\<Union>h∈N. {x ⊗ h}) ⊆ (\<Union>h∈N. {h ⊗ x})"      proof clarify        fix n        assume n: "n ∈ N"         show "x ⊗ n ∈ (\<Union>h∈N. {h ⊗ x})"        proof           show "x ⊗ n ⊗ inv x ∈ N" by (simp add: x n closed)          show "x ⊗ n ∈ {x ⊗ n ⊗ inv x ⊗ x}"            by (simp add: x n m_assoc sb [THEN subsetD])        qed      qed    qed  qedqedsubsection{*More Properties of Cosets*}lemma (in group) lcos_m_assoc:     "[| M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]      ==> g <# (h <# M) = (g ⊗ h) <# M"by (force simp add: l_coset_def m_assoc)lemma (in group) lcos_mult_one: "M ⊆ carrier G ==> \<one> <# M = M"by (force simp add: l_coset_def)lemma (in group) l_coset_subset_G:     "[| H ⊆ carrier G; x ∈ carrier G |] ==> x <# H ⊆ carrier G"by (auto simp add: l_coset_def subsetD)lemma (in group) l_coset_swap:     "[|y ∈ x <# H;  x ∈ carrier G;  subgroup H G|] ==> x ∈ y <# H"proof (simp add: l_coset_def)  assume "∃h∈H. y = x ⊗ h"    and x: "x ∈ carrier G"    and sb: "subgroup H G"  then obtain h' where h': "h' ∈ H & x ⊗ h' = y" by blast  show "∃h∈H. x = y ⊗ h"  proof    show "x = y ⊗ inv h'" using h' x sb      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])    show "inv h' ∈ H" using h' sb      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)  qedqedlemma (in group) l_coset_carrier:     "[| y ∈ x <# H;  x ∈ carrier G;  subgroup H G |] ==> y ∈ carrier G"by (auto simp add: l_coset_def m_assoc                   subgroup.subset [THEN subsetD] subgroup.m_closed)lemma (in group) l_repr_imp_subset:  assumes y: "y ∈ x <# H" and x: "x ∈ carrier G" and sb: "subgroup H G"  shows "y <# H ⊆ x <# H"proof -  from y  obtain h' where "h' ∈ H" "x ⊗ h' = y" by (auto simp add: l_coset_def)  thus ?thesis using x sb    by (auto simp add: l_coset_def m_assoc                       subgroup.subset [THEN subsetD] subgroup.m_closed)qedlemma (in group) l_repr_independence:  assumes y: "y ∈ x <# H" and x: "x ∈ carrier G" and sb: "subgroup H G"  shows "x <# H = y <# H"proof  show "x <# H ⊆ y <# H"    by (rule l_repr_imp_subset,        (blast intro: l_coset_swap l_coset_carrier y x sb)+)  show "y <# H ⊆ x <# H" by (rule l_repr_imp_subset [OF y x sb])qedlemma (in group) setmult_subset_G:     "[|H ⊆ carrier G; K ⊆ carrier G|] ==> H <#> K ⊆ carrier G"by (auto simp add: set_mult_def subsetD)lemma (in group) subgroup_mult_id: "subgroup H G ==> H <#> H = H"apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)apply (rule_tac x = x in bexI)apply (rule bexI [of _ "\<one>"])apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])donesubsubsection {* Set of Inverses of an @{text r_coset}. *}lemma (in normal) rcos_inv:  assumes x:     "x ∈ carrier G"  shows "set_inv (H #> x) = H #> (inv x)" proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)  fix h  assume h: "h ∈ H"  show "inv x ⊗ inv h ∈ (\<Union>j∈H. {j ⊗ inv x})"  proof    show "inv x ⊗ inv h ⊗ x ∈ H"      by (simp add: inv_op_closed1 h x)    show "inv x ⊗ inv h ∈ {inv x ⊗ inv h ⊗ x ⊗ inv x}"      by (simp add: h x m_assoc)  qed  show "h ⊗ inv x ∈ (\<Union>j∈H. {inv x ⊗ inv j})"  proof    show "x ⊗ inv h ⊗ inv x ∈ H"      by (simp add: inv_op_closed2 h x)    show "h ⊗ inv x ∈ {inv x ⊗ inv (x ⊗ inv h ⊗ inv x)}"      by (simp add: h x m_assoc [symmetric] inv_mult_group)  qedqedsubsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}lemma (in group) setmult_rcos_assoc:     "[|H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G|]      ==> H <#> (K #> x) = (H <#> K) #> x"by (force simp add: r_coset_def set_mult_def m_assoc)lemma (in group) rcos_assoc_lcos:     "[|H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G|]      ==> (H #> x) <#> K = H <#> (x <# K)"by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)lemma (in normal) rcos_mult_step1:     "[|x ∈ carrier G; y ∈ carrier G|]      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"by (simp add: setmult_rcos_assoc subset              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)lemma (in normal) rcos_mult_step2:     "[|x ∈ carrier G; y ∈ carrier G|]      ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"by (insert coset_eq, simp add: normal_def)lemma (in normal) rcos_mult_step3:     "[|x ∈ carrier G; y ∈ carrier G|]      ==> (H <#> (H #> x)) #> y = H #> (x ⊗ y)"by (simp add: setmult_rcos_assoc coset_mult_assoc              subgroup_mult_id normal.axioms subset normal_axioms)lemma (in normal) rcos_sum:     "[|x ∈ carrier G; y ∈ carrier G|]      ==> (H #> x) <#> (H #> y) = H #> (x ⊗ y)"by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)lemma (in normal) rcosets_mult_eq: "M ∈ rcosets H ==> H <#> M = M"  -- {* generalizes @{text subgroup_mult_id} *}  by (auto simp add: RCOSETS_def subset        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)subsubsection{*An Equivalence Relation*}definition  r_congruent :: "[('a,'b)monoid_scheme, 'a set] => ('a*'a)set"  ("rcong\<index> _")  where "rcong⇘G⇙ H = {(x,y). x ∈ carrier G & y ∈ carrier G & inv⇘G⇙ x ⊗⇘G⇙ y ∈ H}"lemma (in subgroup) equiv_rcong:   assumes "group G"   shows "equiv (carrier G) (rcong H)"proof -  interpret group G by fact  show ?thesis  proof (intro equivI)    show "refl_on (carrier G) (rcong H)"      by (auto simp add: r_congruent_def refl_on_def)   next    show "sym (rcong H)"    proof (simp add: r_congruent_def sym_def, clarify)      fix x y      assume [simp]: "x ∈ carrier G" "y ∈ carrier G"          and "inv x ⊗ y ∈ H"      hence "inv (inv x ⊗ y) ∈ H" by simp      thus "inv y ⊗ x ∈ H" by (simp add: inv_mult_group)    qed  next    show "trans (rcong H)"    proof (simp add: r_congruent_def trans_def, clarify)      fix x y z      assume [simp]: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"         and "inv x ⊗ y ∈ H" and "inv y ⊗ z ∈ H"      hence "(inv x ⊗ y) ⊗ (inv y ⊗ z) ∈ H" by simp      hence "inv x ⊗ (y ⊗ inv y) ⊗ z ∈ H"        by (simp add: m_assoc del: r_inv Units_r_inv)       thus "inv x ⊗ z ∈ H" by simp    qed  qedqedtext{*Equivalence classes of @{text rcong} correspond to left cosets.  Was there a mistake in the definitions? I'd have expected them to  correspond to right cosets.*}(* CB: This is correct, but subtle.   We call H #> a the right coset of a relative to H.  According to   Jacobson, this is what the majority of group theory literature does.   He then defines the notion of congruence relation ~ over monoids as   equivalence relation with a ~ a' & b ~ b' ==> a*b ~ a'*b'.   Our notion of right congruence induced by K: rcong K appears only in   the context where K is a normal subgroup.  Jacobson doesn't name it.   But in this context left and right cosets are identical.*)lemma (in subgroup) l_coset_eq_rcong:  assumes "group G"  assumes a: "a ∈ carrier G"  shows "a <# H = rcong H `` {a}"proof -  interpret group G by fact  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) qedsubsubsection{*Two Distinct Right Cosets are Disjoint*}lemma (in group) rcos_equation:  assumes "subgroup H G"  assumes p: "ha ⊗ a = h ⊗ b" "a ∈ carrier G" "b ∈ carrier G" "h ∈ H" "ha ∈ H" "hb ∈ H"  shows "hb ⊗ a ∈ (\<Union>h∈H. {h ⊗ b})"proof -  interpret subgroup H G by fact  from p show ?thesis apply (rule_tac UN_I [of "hb ⊗ ((inv ha) ⊗ h)"])    apply (simp add: )    apply (simp add: m_assoc transpose_inv)    doneqedlemma (in group) rcos_disjoint:  assumes "subgroup H G"  assumes p: "a ∈ rcosets H" "b ∈ rcosets H" "a≠b"  shows "a ∩ b = {}"proof -  interpret subgroup H G by fact  from p show ?thesis    apply (simp add: RCOSETS_def r_coset_def)    apply (blast intro: rcos_equation assms sym)    doneqedsubsection {* Further lemmas for @{text "r_congruent"} *}text {* The relation is a congruence *}lemma (in normal) congruent_rcong:  shows "congruent2 (rcong H) (rcong H) (λa b. a ⊗ b <# H)"proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)  fix a b c  assume abrcong: "(a, b) ∈ rcong H"    and ccarr: "c ∈ carrier G"  from abrcong      have acarr: "a ∈ carrier G"        and bcarr: "b ∈ carrier G"        and abH: "inv a ⊗ b ∈ H"      unfolding r_congruent_def      by fast+  note carr = acarr bcarr ccarr  from ccarr and abH      have "inv c ⊗ (inv a ⊗ b) ⊗ c ∈ H" by (rule inv_op_closed1)  moreover      from carr and inv_closed      have "inv c ⊗ (inv a ⊗ b) ⊗ c = (inv c ⊗ inv a) ⊗ (b ⊗ c)"       by (force cong: m_assoc)  moreover       from carr and inv_closed      have "… = (inv (a ⊗ c)) ⊗ (b ⊗ c)"      by (simp add: inv_mult_group)  ultimately      have "(inv (a ⊗ c)) ⊗ (b ⊗ c) ∈ H" by simp  from carr and this     have "(b ⊗ c) ∈ (a ⊗ c) <# H"     by (simp add: lcos_module_rev[OF is_group])  from carr and this and is_subgroup     show "(a ⊗ c) <# H = (b ⊗ c) <# H" by (intro l_repr_independence, simp+)next  fix a b c  assume abrcong: "(a, b) ∈ rcong H"    and ccarr: "c ∈ carrier G"  from ccarr have "c ∈ Units G" by simp  hence cinvc_one: "inv c ⊗ c = \<one>" by (rule Units_l_inv)  from abrcong      have acarr: "a ∈ carrier G"       and bcarr: "b ∈ carrier G"       and abH: "inv a ⊗ b ∈ H"      by (unfold r_congruent_def, fast+)  note carr = acarr bcarr ccarr  from carr and inv_closed     have "inv a ⊗ b = inv a ⊗ (\<one> ⊗ b)" by simp  also from carr and inv_closed      have "… = inv a ⊗ (inv c ⊗ c) ⊗ b" by simp  also from carr and inv_closed      have "… = (inv a ⊗ inv c) ⊗ (c ⊗ b)" by (force cong: m_assoc)  also from carr and inv_closed      have "… = inv (c ⊗ a) ⊗ (c ⊗ b)" by (simp add: inv_mult_group)  finally      have "inv a ⊗ b = inv (c ⊗ a) ⊗ (c ⊗ b)" .  from abH and this      have "inv (c ⊗ a) ⊗ (c ⊗ b) ∈ H" by simp  from carr and this     have "(c ⊗ b) ∈ (c ⊗ a) <# H"     by (simp add: lcos_module_rev[OF is_group])  from carr and this and is_subgroup     show "(c ⊗ a) <# H = (c ⊗ b) <# H" by (intro l_repr_independence, simp+)qedsubsection {*Order of a Group and Lagrange's Theorem*}definition  order :: "('a, 'b) monoid_scheme => nat"  where "order S = card (carrier S)"lemma (in group) rcosets_part_G:  assumes "subgroup H G"  shows "\<Union>(rcosets H) = carrier G"proof -  interpret subgroup H G by fact  show ?thesis    apply (rule equalityI)    apply (force simp add: RCOSETS_def r_coset_def)    apply (auto simp add: RCOSETS_def intro: rcos_self assms)    doneqedlemma (in group) cosets_finite:     "[|c ∈ rcosets H;  H ⊆ carrier G;  finite (carrier G)|] ==> finite c"apply (auto simp add: RCOSETS_def)apply (simp add: r_coset_subset_G [THEN finite_subset])donetext{*The next two lemmas support the proof of @{text card_cosets_equal}.*}lemma (in group) inj_on_f:    "[|H ⊆ carrier G;  a ∈ carrier G|] ==> inj_on (λy. y ⊗ inv a) (H #> a)"apply (rule inj_onI)apply (subgoal_tac "x ∈ carrier G & y ∈ carrier G") prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])apply (simp add: subsetD)donelemma (in group) inj_on_g:    "[|H ⊆ carrier G;  a ∈ carrier G|] ==> inj_on (λy. y ⊗ a) H"by (force simp add: inj_on_def subsetD)lemma (in group) card_cosets_equal:     "[|c ∈ rcosets H;  H ⊆ carrier G; finite(carrier G)|]      ==> card c = card H"apply (auto simp add: RCOSETS_def)apply (rule card_bij_eq)     apply (rule inj_on_f, assumption+)    apply (force simp add: m_assoc subsetD r_coset_def)   apply (rule inj_on_g, assumption+)  apply (force simp add: m_assoc subsetD r_coset_def) txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*} apply (simp add: r_coset_subset_G [THEN finite_subset])apply (blast intro: finite_subset)donelemma (in group) rcosets_subset_PowG:     "subgroup H G  ==> rcosets H ⊆ Pow(carrier G)"apply (simp add: RCOSETS_def)apply (blast dest: r_coset_subset_G subgroup.subset)donetheorem (in group) lagrange:     "[|finite(carrier G); subgroup H G|]      ==> card(rcosets H) * card(H) = order(G)"apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])apply (subst mult_commute)apply (rule card_partition)   apply (simp add: rcosets_subset_PowG [THEN finite_subset])  apply (simp add: rcosets_part_G) apply (simp add: card_cosets_equal subgroup.subset)apply (simp add: rcos_disjoint)donesubsection {*Quotient Groups: Factorization of a Group*}definition  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid" (infixl "Mod" 65)    --{*Actually defined for groups rather than monoids*}   where "FactGroup G H = (|carrier = rcosets⇘G⇙ H, mult = set_mult G, one = H|)),"lemma (in normal) setmult_closed:     "[|K1 ∈ rcosets H; K2 ∈ rcosets H|] ==> K1 <#> K2 ∈ rcosets H"by (auto simp add: rcos_sum RCOSETS_def)lemma (in normal) setinv_closed:     "K ∈ rcosets H ==> set_inv K ∈ rcosets H"by (auto simp add: rcos_inv RCOSETS_def)lemma (in normal) rcosets_assoc:     "[|M1 ∈ rcosets H; M2 ∈ rcosets H; M3 ∈ rcosets H|]      ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"by (auto simp add: RCOSETS_def rcos_sum m_assoc)lemma (in subgroup) subgroup_in_rcosets:  assumes "group G"  shows "H ∈ rcosets H"proof -  interpret group G by fact  from _ subgroup_axioms have "H #> \<one> = H"    by (rule coset_join2) auto  then show ?thesis    by (auto simp add: RCOSETS_def)qedlemma (in normal) rcosets_inv_mult_group_eq:     "M ∈ rcosets H ==> set_inv M <#> M = H"by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)theorem (in normal) factorgroup_is_group:  "group (G Mod H)"apply (simp add: FactGroup_def)apply (rule groupI)    apply (simp add: setmult_closed)   apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])  apply (simp add: restrictI setmult_closed rcosets_assoc) apply (simp add: normal_imp_subgroup                  subgroup_in_rcosets rcosets_mult_eq)apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)donelemma mult_FactGroup [simp]: "X ⊗⇘(G Mod H)⇙ X' = X <#>⇘G⇙ X'"  by (simp add: FactGroup_def) lemma (in normal) inv_FactGroup:     "X ∈ carrier (G Mod H) ==> inv⇘G Mod H⇙ X = set_inv X"apply (rule group.inv_equality [OF factorgroup_is_group]) apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)donetext{*The coset map is a homomorphism from @{term G} to the quotient group  @{term "G Mod H"}*}lemma (in normal) r_coset_hom_Mod:  "(λa. H #> a) ∈ hom G (G Mod H)"  by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum) subsection{*The First Isomorphism Theorem*}text{*The quotient by the kernel of a homomorphism is isomorphic to the   range of that homomorphism.*}definition  kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme =>  ('a => 'b) => 'a set"    --{*the kernel of a homomorphism*}  where "kernel G H h = {x. x ∈ carrier G & h x = \<one>⇘H⇙}"lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"apply (rule subgroup.intro) apply (auto simp add: kernel_def group.intro is_group) donetext{*The kernel of a homomorphism is a normal subgroup*}lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"apply (simp add: G.normal_inv_iff subgroup_kernel)apply (simp add: kernel_def)donelemma (in group_hom) FactGroup_nonempty:  assumes X: "X ∈ carrier (G Mod kernel G H h)"  shows "X ≠ {}"proof -  from X  obtain g where "g ∈ carrier G"              and "X = kernel G H h #> g"    by (auto simp add: FactGroup_def RCOSETS_def)  thus ?thesis    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)qedlemma (in group_hom) FactGroup_the_elem_mem:  assumes X: "X ∈ carrier (G Mod (kernel G H h))"  shows "the_elem (h`X) ∈ carrier H"proof -  from X  obtain g where g: "g ∈ carrier G"              and "X = kernel G H h #> g"    by (auto simp add: FactGroup_def RCOSETS_def)  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)  thus ?thesis by (auto simp add: g)qedlemma (in group_hom) FactGroup_hom:     "(λX. the_elem (h`X)) ∈ hom (G Mod (kernel G H h)) H"apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)proof (intro ballI)  fix X and X'  assume X:  "X  ∈ carrier (G Mod kernel G H h)"     and X': "X' ∈ carrier (G Mod kernel G H h)"  then  obtain g and g'           where "g ∈ carrier G" and "g' ∈ carrier G"              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"    by (auto simp add: FactGroup_def RCOSETS_def)  hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"     and Xsub: "X ⊆ carrier G" and X'sub: "X' ⊆ carrier G"    by (force simp add: kernel_def r_coset_def image_def)+  hence "h ` (X <#> X') = {h g ⊗⇘H⇙ h g'}" using X X'    by (auto dest!: FactGroup_nonempty             simp add: set_mult_def image_eq_UN                        subsetD [OF Xsub] subsetD [OF X'sub])   thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) ⊗⇘H⇙ the_elem (h ` X')"    by (simp add: all image_eq_UN FactGroup_nonempty X X')qedtext{*Lemma for the following injectivity result*}lemma (in group_hom) FactGroup_subset:     "[|g ∈ carrier G; g' ∈ carrier G; h g = h g'|]      ==>  kernel G H h #> g ⊆ kernel G H h #> g'"apply (clarsimp simp add: kernel_def r_coset_def image_def)apply (rename_tac y)  apply (rule_tac x="y ⊗ g ⊗ inv g'" in exI) apply (simp add: G.m_assoc) donelemma (in group_hom) FactGroup_inj_on:     "inj_on (λX. the_elem (h ` X)) (carrier (G Mod kernel G H h))"proof (simp add: inj_on_def, clarify)   fix X and X'  assume X:  "X  ∈ carrier (G Mod kernel G H h)"     and X': "X' ∈ carrier (G Mod kernel G H h)"  then  obtain g and g'           where gX: "g ∈ carrier G"  "g' ∈ carrier G"               "X = kernel G H h #> g" "X' = kernel G H h #> g'"    by (auto simp add: FactGroup_def RCOSETS_def)  hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"     by (force simp add: kernel_def r_coset_def image_def)+  assume "the_elem (h ` X) = the_elem (h ` X')"  hence h: "h g = h g'"    by (simp add: image_eq_UN all FactGroup_nonempty X X')   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) qedtext{*If the homomorphism @{term h} is onto @{term H}, then so is thehomomorphism from the quotient group*}lemma (in group_hom) FactGroup_onto:  assumes h: "h ` carrier G = carrier H"  shows "(λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"proof  show "(λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h) ⊆ carrier H"    by (auto simp add: FactGroup_the_elem_mem)  show "carrier H ⊆ (λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"  proof    fix y    assume y: "y ∈ carrier H"    with h obtain g where g: "g ∈ carrier G" "h g = y"      by (blast elim: equalityE)     hence "(\<Union>x∈kernel G H h #> g. {h x}) = {y}"       by (auto simp add: y kernel_def r_coset_def)     with g show "y ∈ (λX. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)  qedqedtext{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}theorem (in group_hom) FactGroup_iso:  "h ` carrier G = carrier H   ==> (λX. the_elem (h`X)) ∈ (G Mod (kernel G H h)) ≅ H"by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def               FactGroup_onto) end`