src/HOL/Algebra/Coset.thy
 author hoelzl Tue Nov 05 09:44:57 2013 +0100 (2013-11-05) changeset 54257 5c7a3b6b05a9 parent 46721 f88b187ad8ca child 57512 cc97b347b301 permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
```     1 (*  Title:      HOL/Algebra/Coset.thy
```
```     2     Author:     Florian Kammueller
```
```     3     Author:     L C Paulson
```
```     4     Author:     Stephan Hohe
```
```     5 *)
```
```     6
```
```     7 theory Coset
```
```     8 imports Group
```
```     9 begin
```
```    10
```
```    11 section {*Cosets and Quotient Groups*}
```
```    12
```
```    13 definition
```
```    14   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
```
```    15   where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
```
```    16
```
```    17 definition
```
```    18   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
```
```    19   where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
```
```    20
```
```    21 definition
```
```    22   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _"  80)
```
```    23   where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
```
```    24
```
```    25 definition
```
```    26   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
```
```    27   where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
```
```    28
```
```    29 definition
```
```    30   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _"  80)
```
```    31   where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
```
```    32
```
```    33
```
```    34 locale normal = subgroup + group +
```
```    35   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
```
```    36
```
```    37 abbreviation
```
```    38   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
```
```    39   "H \<lhd> G \<equiv> normal H G"
```
```    40
```
```    41
```
```    42 subsection {*Basic Properties of Cosets*}
```
```    43
```
```    44 lemma (in group) coset_mult_assoc:
```
```    45      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
```
```    46       ==> (M #> g) #> h = M #> (g \<otimes> h)"
```
```    47 by (force simp add: r_coset_def m_assoc)
```
```    48
```
```    49 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
```
```    50 by (force simp add: r_coset_def)
```
```    51
```
```    52 lemma (in group) coset_mult_inv1:
```
```    53      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
```
```    54          M \<subseteq> carrier G |] ==> M #> x = M #> y"
```
```    55 apply (erule subst [of concl: "%z. M #> x = z #> y"])
```
```    56 apply (simp add: coset_mult_assoc m_assoc)
```
```    57 done
```
```    58
```
```    59 lemma (in group) coset_mult_inv2:
```
```    60      "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
```
```    61       ==> M #> (x \<otimes> (inv y)) = M "
```
```    62 apply (simp add: coset_mult_assoc [symmetric])
```
```    63 apply (simp add: coset_mult_assoc)
```
```    64 done
```
```    65
```
```    66 lemma (in group) coset_join1:
```
```    67      "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
```
```    68 apply (erule subst)
```
```    69 apply (simp add: r_coset_def)
```
```    70 apply (blast intro: l_one subgroup.one_closed sym)
```
```    71 done
```
```    72
```
```    73 lemma (in group) solve_equation:
```
```    74     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
```
```    75 apply (rule bexI [of _ "y \<otimes> (inv x)"])
```
```    76 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
```
```    77                       subgroup.subset [THEN subsetD])
```
```    78 done
```
```    79
```
```    80 lemma (in group) repr_independence:
```
```    81      "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
```
```    82 by (auto simp add: r_coset_def m_assoc [symmetric]
```
```    83                    subgroup.subset [THEN subsetD]
```
```    84                    subgroup.m_closed solve_equation)
```
```    85
```
```    86 lemma (in group) coset_join2:
```
```    87      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
```
```    88   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
```
```    89 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
```
```    90
```
```    91 lemma (in monoid) r_coset_subset_G:
```
```    92      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
```
```    93 by (auto simp add: r_coset_def)
```
```    94
```
```    95 lemma (in group) rcosI:
```
```    96      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
```
```    97 by (auto simp add: r_coset_def)
```
```    98
```
```    99 lemma (in group) rcosetsI:
```
```   100      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
```
```   101 by (auto simp add: RCOSETS_def)
```
```   102
```
```   103 text{*Really needed?*}
```
```   104 lemma (in group) transpose_inv:
```
```   105      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
```
```   106       ==> (inv x) \<otimes> z = y"
```
```   107 by (force simp add: m_assoc [symmetric])
```
```   108
```
```   109 lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
```
```   110 apply (simp add: r_coset_def)
```
```   111 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
```
```   112                     subgroup.one_closed)
```
```   113 done
```
```   114
```
```   115 text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
```
```   116 lemma (in group) repr_independenceD:
```
```   117   assumes "subgroup H G"
```
```   118   assumes ycarr: "y \<in> carrier G"
```
```   119       and repr:  "H #> x = H #> y"
```
```   120   shows "y \<in> H #> x"
```
```   121 proof -
```
```   122   interpret subgroup H G by fact
```
```   123   show ?thesis  apply (subst repr)
```
```   124   apply (intro rcos_self)
```
```   125    apply (rule ycarr)
```
```   126    apply (rule is_subgroup)
```
```   127   done
```
```   128 qed
```
```   129
```
```   130 text {* Elements of a right coset are in the carrier *}
```
```   131 lemma (in subgroup) elemrcos_carrier:
```
```   132   assumes "group G"
```
```   133   assumes acarr: "a \<in> carrier G"
```
```   134     and a': "a' \<in> H #> a"
```
```   135   shows "a' \<in> carrier G"
```
```   136 proof -
```
```   137   interpret group G by fact
```
```   138   from subset and acarr
```
```   139   have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
```
```   140   from this and a'
```
```   141   show "a' \<in> carrier G"
```
```   142     by fast
```
```   143 qed
```
```   144
```
```   145 lemma (in subgroup) rcos_const:
```
```   146   assumes "group G"
```
```   147   assumes hH: "h \<in> H"
```
```   148   shows "H #> h = H"
```
```   149 proof -
```
```   150   interpret group G by fact
```
```   151   show ?thesis apply (unfold r_coset_def)
```
```   152     apply rule
```
```   153     apply rule
```
```   154     apply clarsimp
```
```   155     apply (intro subgroup.m_closed)
```
```   156     apply (rule is_subgroup)
```
```   157     apply assumption
```
```   158     apply (rule hH)
```
```   159     apply rule
```
```   160     apply simp
```
```   161   proof -
```
```   162     fix h'
```
```   163     assume h'H: "h' \<in> H"
```
```   164     note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
```
```   165     from carr
```
```   166     have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
```
```   167     from h'H hH
```
```   168     have "h' \<otimes> inv h \<in> H" by simp
```
```   169     from this and a
```
```   170     show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
```
```   171   qed
```
```   172 qed
```
```   173
```
```   174 text {* Step one for lemma @{text "rcos_module"} *}
```
```   175 lemma (in subgroup) rcos_module_imp:
```
```   176   assumes "group G"
```
```   177   assumes xcarr: "x \<in> carrier G"
```
```   178       and x'cos: "x' \<in> H #> x"
```
```   179   shows "(x' \<otimes> inv x) \<in> H"
```
```   180 proof -
```
```   181   interpret group G by fact
```
```   182   from xcarr x'cos
```
```   183       have x'carr: "x' \<in> carrier G"
```
```   184       by (rule elemrcos_carrier[OF is_group])
```
```   185   from xcarr
```
```   186       have ixcarr: "inv x \<in> carrier G"
```
```   187       by simp
```
```   188   from x'cos
```
```   189       have "\<exists>h\<in>H. x' = h \<otimes> x"
```
```   190       unfolding r_coset_def
```
```   191       by fast
```
```   192   from this
```
```   193       obtain h
```
```   194         where hH: "h \<in> H"
```
```   195         and x': "x' = h \<otimes> x"
```
```   196       by auto
```
```   197   from hH and subset
```
```   198       have hcarr: "h \<in> carrier G" by fast
```
```   199   note carr = xcarr x'carr hcarr
```
```   200   from x' and carr
```
```   201       have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
```
```   202   also from carr
```
```   203       have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
```
```   204   also from carr
```
```   205       have "\<dots> = h \<otimes> \<one>" by simp
```
```   206   also from carr
```
```   207       have "\<dots> = h" by simp
```
```   208   finally
```
```   209       have "x' \<otimes> (inv x) = h" by simp
```
```   210   from hH this
```
```   211       show "x' \<otimes> (inv x) \<in> H" by simp
```
```   212 qed
```
```   213
```
```   214 text {* Step two for lemma @{text "rcos_module"} *}
```
```   215 lemma (in subgroup) rcos_module_rev:
```
```   216   assumes "group G"
```
```   217   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
```
```   218       and xixH: "(x' \<otimes> inv x) \<in> H"
```
```   219   shows "x' \<in> H #> x"
```
```   220 proof -
```
```   221   interpret group G by fact
```
```   222   from xixH
```
```   223       have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
```
```   224   from this
```
```   225       obtain h
```
```   226         where hH: "h \<in> H"
```
```   227         and hsym: "x' \<otimes> (inv x) = h"
```
```   228       by fast
```
```   229   from hH subset have hcarr: "h \<in> carrier G" by simp
```
```   230   note carr = carr hcarr
```
```   231   from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
```
```   232   also from carr
```
```   233       have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
```
```   234   also from carr
```
```   235       have "\<dots> = x' \<otimes> \<one>" by simp
```
```   236   also from carr
```
```   237       have "\<dots> = x'" by simp
```
```   238   finally
```
```   239       have "h \<otimes> x = x'" by simp
```
```   240   from this[symmetric] and hH
```
```   241       show "x' \<in> H #> x"
```
```   242       unfolding r_coset_def
```
```   243       by fast
```
```   244 qed
```
```   245
```
```   246 text {* Module property of right cosets *}
```
```   247 lemma (in subgroup) rcos_module:
```
```   248   assumes "group G"
```
```   249   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
```
```   250   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
```
```   251 proof -
```
```   252   interpret group G by fact
```
```   253   show ?thesis proof  assume "x' \<in> H #> x"
```
```   254     from this and carr
```
```   255     show "x' \<otimes> inv x \<in> H"
```
```   256       by (intro rcos_module_imp[OF is_group])
```
```   257   next
```
```   258     assume "x' \<otimes> inv x \<in> H"
```
```   259     from this and carr
```
```   260     show "x' \<in> H #> x"
```
```   261       by (intro rcos_module_rev[OF is_group])
```
```   262   qed
```
```   263 qed
```
```   264
```
```   265 text {* Right cosets are subsets of the carrier. *}
```
```   266 lemma (in subgroup) rcosets_carrier:
```
```   267   assumes "group G"
```
```   268   assumes XH: "X \<in> rcosets H"
```
```   269   shows "X \<subseteq> carrier G"
```
```   270 proof -
```
```   271   interpret group G by fact
```
```   272   from XH have "\<exists>x\<in> carrier G. X = H #> x"
```
```   273       unfolding RCOSETS_def
```
```   274       by fast
```
```   275   from this
```
```   276       obtain x
```
```   277         where xcarr: "x\<in> carrier G"
```
```   278         and X: "X = H #> x"
```
```   279       by fast
```
```   280   from subset and xcarr
```
```   281       show "X \<subseteq> carrier G"
```
```   282       unfolding X
```
```   283       by (rule r_coset_subset_G)
```
```   284 qed
```
```   285
```
```   286 text {* Multiplication of general subsets *}
```
```   287 lemma (in monoid) set_mult_closed:
```
```   288   assumes Acarr: "A \<subseteq> carrier G"
```
```   289       and Bcarr: "B \<subseteq> carrier G"
```
```   290   shows "A <#> B \<subseteq> carrier G"
```
```   291 apply rule apply (simp add: set_mult_def, clarsimp)
```
```   292 proof -
```
```   293   fix a b
```
```   294   assume "a \<in> A"
```
```   295   from this and Acarr
```
```   296       have acarr: "a \<in> carrier G" by fast
```
```   297
```
```   298   assume "b \<in> B"
```
```   299   from this and Bcarr
```
```   300       have bcarr: "b \<in> carrier G" by fast
```
```   301
```
```   302   from acarr bcarr
```
```   303       show "a \<otimes> b \<in> carrier G" by (rule m_closed)
```
```   304 qed
```
```   305
```
```   306 lemma (in comm_group) mult_subgroups:
```
```   307   assumes subH: "subgroup H G"
```
```   308       and subK: "subgroup K G"
```
```   309   shows "subgroup (H <#> K) G"
```
```   310 apply (rule subgroup.intro)
```
```   311    apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
```
```   312   apply (simp add: set_mult_def) apply clarsimp defer 1
```
```   313   apply (simp add: set_mult_def) defer 1
```
```   314   apply (simp add: set_mult_def, clarsimp) defer 1
```
```   315 proof -
```
```   316   fix ha hb ka kb
```
```   317   assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
```
```   318   note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
```
```   319               kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
```
```   320   from carr
```
```   321       have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
```
```   322   also from carr
```
```   323       have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
```
```   324   also from carr
```
```   325       have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
```
```   326   finally
```
```   327       have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
```
```   328
```
```   329   from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
```
```   330   from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
```
```   331
```
```   332   from hH and kK and eq
```
```   333       show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
```
```   334 next
```
```   335   have "\<one> = \<one> \<otimes> \<one>" by simp
```
```   336   from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
```
```   337       show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
```
```   338 next
```
```   339   fix h k
```
```   340   assume hH: "h \<in> H"
```
```   341      and kK: "k \<in> K"
```
```   342
```
```   343   from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
```
```   344       have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
```
```   345
```
```   346   from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
```
```   347       show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
```
```   348 qed
```
```   349
```
```   350 lemma (in subgroup) lcos_module_rev:
```
```   351   assumes "group G"
```
```   352   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
```
```   353       and xixH: "(inv x \<otimes> x') \<in> H"
```
```   354   shows "x' \<in> x <# H"
```
```   355 proof -
```
```   356   interpret group G by fact
```
```   357   from xixH
```
```   358       have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
```
```   359   from this
```
```   360       obtain h
```
```   361         where hH: "h \<in> H"
```
```   362         and hsym: "(inv x) \<otimes> x' = h"
```
```   363       by fast
```
```   364
```
```   365   from hH subset have hcarr: "h \<in> carrier G" by simp
```
```   366   note carr = carr hcarr
```
```   367   from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
```
```   368   also from carr
```
```   369       have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
```
```   370   also from carr
```
```   371       have "\<dots> = \<one> \<otimes> x'" by simp
```
```   372   also from carr
```
```   373       have "\<dots> = x'" by simp
```
```   374   finally
```
```   375       have "x \<otimes> h = x'" by simp
```
```   376
```
```   377   from this[symmetric] and hH
```
```   378       show "x' \<in> x <# H"
```
```   379       unfolding l_coset_def
```
```   380       by fast
```
```   381 qed
```
```   382
```
```   383
```
```   384 subsection {* Normal subgroups *}
```
```   385
```
```   386 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
```
```   387   by (simp add: normal_def subgroup_def)
```
```   388
```
```   389 lemma (in group) normalI:
```
```   390   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
```
```   391   by (simp add: normal_def normal_axioms_def is_group)
```
```   392
```
```   393 lemma (in normal) inv_op_closed1:
```
```   394      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
```
```   395 apply (insert coset_eq)
```
```   396 apply (auto simp add: l_coset_def r_coset_def)
```
```   397 apply (drule bspec, assumption)
```
```   398 apply (drule equalityD1 [THEN subsetD], blast, clarify)
```
```   399 apply (simp add: m_assoc)
```
```   400 apply (simp add: m_assoc [symmetric])
```
```   401 done
```
```   402
```
```   403 lemma (in normal) inv_op_closed2:
```
```   404      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
```
```   405 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
```
```   406 apply (simp add: )
```
```   407 apply (blast intro: inv_op_closed1)
```
```   408 done
```
```   409
```
```   410 text{*Alternative characterization of normal subgroups*}
```
```   411 lemma (in group) normal_inv_iff:
```
```   412      "(N \<lhd> G) =
```
```   413       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
```
```   414       (is "_ = ?rhs")
```
```   415 proof
```
```   416   assume N: "N \<lhd> G"
```
```   417   show ?rhs
```
```   418     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
```
```   419 next
```
```   420   assume ?rhs
```
```   421   hence sg: "subgroup N G"
```
```   422     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
```
```   423   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
```
```   424   show "N \<lhd> G"
```
```   425   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
```
```   426     fix x
```
```   427     assume x: "x \<in> carrier G"
```
```   428     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
```
```   429     proof
```
```   430       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   431       proof clarify
```
```   432         fix n
```
```   433         assume n: "n \<in> N"
```
```   434         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   435         proof
```
```   436           from closed [of "inv x"]
```
```   437           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
```
```   438           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
```
```   439             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
```
```   440         qed
```
```   441       qed
```
```   442     next
```
```   443       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   444       proof clarify
```
```   445         fix n
```
```   446         assume n: "n \<in> N"
```
```   447         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   448         proof
```
```   449           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
```
```   450           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
```
```   451             by (simp add: x n m_assoc sb [THEN subsetD])
```
```   452         qed
```
```   453       qed
```
```   454     qed
```
```   455   qed
```
```   456 qed
```
```   457
```
```   458
```
```   459 subsection{*More Properties of Cosets*}
```
```   460
```
```   461 lemma (in group) lcos_m_assoc:
```
```   462      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
```
```   463       ==> g <# (h <# M) = (g \<otimes> h) <# M"
```
```   464 by (force simp add: l_coset_def m_assoc)
```
```   465
```
```   466 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
```
```   467 by (force simp add: l_coset_def)
```
```   468
```
```   469 lemma (in group) l_coset_subset_G:
```
```   470      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
```
```   471 by (auto simp add: l_coset_def subsetD)
```
```   472
```
```   473 lemma (in group) l_coset_swap:
```
```   474      "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
```
```   475 proof (simp add: l_coset_def)
```
```   476   assume "\<exists>h\<in>H. y = x \<otimes> h"
```
```   477     and x: "x \<in> carrier G"
```
```   478     and sb: "subgroup H G"
```
```   479   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
```
```   480   show "\<exists>h\<in>H. x = y \<otimes> h"
```
```   481   proof
```
```   482     show "x = y \<otimes> inv h'" using h' x sb
```
```   483       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
```
```   484     show "inv h' \<in> H" using h' sb
```
```   485       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
```
```   486   qed
```
```   487 qed
```
```   488
```
```   489 lemma (in group) l_coset_carrier:
```
```   490      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
```
```   491 by (auto simp add: l_coset_def m_assoc
```
```   492                    subgroup.subset [THEN subsetD] subgroup.m_closed)
```
```   493
```
```   494 lemma (in group) l_repr_imp_subset:
```
```   495   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
```
```   496   shows "y <# H \<subseteq> x <# H"
```
```   497 proof -
```
```   498   from y
```
```   499   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
```
```   500   thus ?thesis using x sb
```
```   501     by (auto simp add: l_coset_def m_assoc
```
```   502                        subgroup.subset [THEN subsetD] subgroup.m_closed)
```
```   503 qed
```
```   504
```
```   505 lemma (in group) l_repr_independence:
```
```   506   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
```
```   507   shows "x <# H = y <# H"
```
```   508 proof
```
```   509   show "x <# H \<subseteq> y <# H"
```
```   510     by (rule l_repr_imp_subset,
```
```   511         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
```
```   512   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
```
```   513 qed
```
```   514
```
```   515 lemma (in group) setmult_subset_G:
```
```   516      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
```
```   517 by (auto simp add: set_mult_def subsetD)
```
```   518
```
```   519 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
```
```   520 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
```
```   521 apply (rule_tac x = x in bexI)
```
```   522 apply (rule bexI [of _ "\<one>"])
```
```   523 apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
```
```   524 done
```
```   525
```
```   526
```
```   527 subsubsection {* Set of Inverses of an @{text r_coset}. *}
```
```   528
```
```   529 lemma (in normal) rcos_inv:
```
```   530   assumes x:     "x \<in> carrier G"
```
```   531   shows "set_inv (H #> x) = H #> (inv x)"
```
```   532 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
```
```   533   fix h
```
```   534   assume h: "h \<in> H"
```
```   535   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
```
```   536   proof
```
```   537     show "inv x \<otimes> inv h \<otimes> x \<in> H"
```
```   538       by (simp add: inv_op_closed1 h x)
```
```   539     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
```
```   540       by (simp add: h x m_assoc)
```
```   541   qed
```
```   542   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
```
```   543   proof
```
```   544     show "x \<otimes> inv h \<otimes> inv x \<in> H"
```
```   545       by (simp add: inv_op_closed2 h x)
```
```   546     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
```
```   547       by (simp add: h x m_assoc [symmetric] inv_mult_group)
```
```   548   qed
```
```   549 qed
```
```   550
```
```   551
```
```   552 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
```
```   553
```
```   554 lemma (in group) setmult_rcos_assoc:
```
```   555      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
```
```   556       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
```
```   557 by (force simp add: r_coset_def set_mult_def m_assoc)
```
```   558
```
```   559 lemma (in group) rcos_assoc_lcos:
```
```   560      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
```
```   561       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
```
```   562 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
```
```   563
```
```   564 lemma (in normal) rcos_mult_step1:
```
```   565      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   566       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
```
```   567 by (simp add: setmult_rcos_assoc subset
```
```   568               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
```
```   569
```
```   570 lemma (in normal) rcos_mult_step2:
```
```   571      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   572       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
```
```   573 by (insert coset_eq, simp add: normal_def)
```
```   574
```
```   575 lemma (in normal) rcos_mult_step3:
```
```   576      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   577       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
```
```   578 by (simp add: setmult_rcos_assoc coset_mult_assoc
```
```   579               subgroup_mult_id normal.axioms subset normal_axioms)
```
```   580
```
```   581 lemma (in normal) rcos_sum:
```
```   582      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   583       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
```
```   584 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
```
```   585
```
```   586 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
```
```   587   -- {* generalizes @{text subgroup_mult_id} *}
```
```   588   by (auto simp add: RCOSETS_def subset
```
```   589         setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
```
```   590
```
```   591
```
```   592 subsubsection{*An Equivalence Relation*}
```
```   593
```
```   594 definition
```
```   595   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
```
```   596   where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
```
```   597
```
```   598
```
```   599 lemma (in subgroup) equiv_rcong:
```
```   600    assumes "group G"
```
```   601    shows "equiv (carrier G) (rcong H)"
```
```   602 proof -
```
```   603   interpret group G by fact
```
```   604   show ?thesis
```
```   605   proof (intro equivI)
```
```   606     show "refl_on (carrier G) (rcong H)"
```
```   607       by (auto simp add: r_congruent_def refl_on_def)
```
```   608   next
```
```   609     show "sym (rcong H)"
```
```   610     proof (simp add: r_congruent_def sym_def, clarify)
```
```   611       fix x y
```
```   612       assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
```
```   613          and "inv x \<otimes> y \<in> H"
```
```   614       hence "inv (inv x \<otimes> y) \<in> H" by simp
```
```   615       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
```
```   616     qed
```
```   617   next
```
```   618     show "trans (rcong H)"
```
```   619     proof (simp add: r_congruent_def trans_def, clarify)
```
```   620       fix x y z
```
```   621       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
```
```   622          and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
```
```   623       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
```
```   624       hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
```
```   625         by (simp add: m_assoc del: r_inv Units_r_inv)
```
```   626       thus "inv x \<otimes> z \<in> H" by simp
```
```   627     qed
```
```   628   qed
```
```   629 qed
```
```   630
```
```   631 text{*Equivalence classes of @{text rcong} correspond to left cosets.
```
```   632   Was there a mistake in the definitions? I'd have expected them to
```
```   633   correspond to right cosets.*}
```
```   634
```
```   635 (* CB: This is correct, but subtle.
```
```   636    We call H #> a the right coset of a relative to H.  According to
```
```   637    Jacobson, this is what the majority of group theory literature does.
```
```   638    He then defines the notion of congruence relation ~ over monoids as
```
```   639    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
```
```   640    Our notion of right congruence induced by K: rcong K appears only in
```
```   641    the context where K is a normal subgroup.  Jacobson doesn't name it.
```
```   642    But in this context left and right cosets are identical.
```
```   643 *)
```
```   644
```
```   645 lemma (in subgroup) l_coset_eq_rcong:
```
```   646   assumes "group G"
```
```   647   assumes a: "a \<in> carrier G"
```
```   648   shows "a <# H = rcong H `` {a}"
```
```   649 proof -
```
```   650   interpret group G by fact
```
```   651   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
```
```   652 qed
```
```   653
```
```   654
```
```   655 subsubsection{*Two Distinct Right Cosets are Disjoint*}
```
```   656
```
```   657 lemma (in group) rcos_equation:
```
```   658   assumes "subgroup H G"
```
```   659   assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
```
```   660   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
```
```   661 proof -
```
```   662   interpret subgroup H G by fact
```
```   663   from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
```
```   664     apply (simp add: )
```
```   665     apply (simp add: m_assoc transpose_inv)
```
```   666     done
```
```   667 qed
```
```   668
```
```   669 lemma (in group) rcos_disjoint:
```
```   670   assumes "subgroup H G"
```
```   671   assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
```
```   672   shows "a \<inter> b = {}"
```
```   673 proof -
```
```   674   interpret subgroup H G by fact
```
```   675   from p show ?thesis
```
```   676     apply (simp add: RCOSETS_def r_coset_def)
```
```   677     apply (blast intro: rcos_equation assms sym)
```
```   678     done
```
```   679 qed
```
```   680
```
```   681
```
```   682 subsection {* Further lemmas for @{text "r_congruent"} *}
```
```   683
```
```   684 text {* The relation is a congruence *}
```
```   685
```
```   686 lemma (in normal) congruent_rcong:
```
```   687   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
```
```   688 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
```
```   689   fix a b c
```
```   690   assume abrcong: "(a, b) \<in> rcong H"
```
```   691     and ccarr: "c \<in> carrier G"
```
```   692
```
```   693   from abrcong
```
```   694       have acarr: "a \<in> carrier G"
```
```   695         and bcarr: "b \<in> carrier G"
```
```   696         and abH: "inv a \<otimes> b \<in> H"
```
```   697       unfolding r_congruent_def
```
```   698       by fast+
```
```   699
```
```   700   note carr = acarr bcarr ccarr
```
```   701
```
```   702   from ccarr and abH
```
```   703       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
```
```   704   moreover
```
```   705       from carr and inv_closed
```
```   706       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)"
```
```   707       by (force cong: m_assoc)
```
```   708   moreover
```
```   709       from carr and inv_closed
```
```   710       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
```
```   711       by (simp add: inv_mult_group)
```
```   712   ultimately
```
```   713       have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
```
```   714   from carr and this
```
```   715      have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
```
```   716      by (simp add: lcos_module_rev[OF is_group])
```
```   717   from carr and this and is_subgroup
```
```   718      show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
```
```   719 next
```
```   720   fix a b c
```
```   721   assume abrcong: "(a, b) \<in> rcong H"
```
```   722     and ccarr: "c \<in> carrier G"
```
```   723
```
```   724   from ccarr have "c \<in> Units G" by simp
```
```   725   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
```
```   726
```
```   727   from abrcong
```
```   728       have acarr: "a \<in> carrier G"
```
```   729        and bcarr: "b \<in> carrier G"
```
```   730        and abH: "inv a \<otimes> b \<in> H"
```
```   731       by (unfold r_congruent_def, fast+)
```
```   732
```
```   733   note carr = acarr bcarr ccarr
```
```   734
```
```   735   from carr and inv_closed
```
```   736      have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
```
```   737   also from carr and inv_closed
```
```   738       have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
```
```   739   also from carr and inv_closed
```
```   740       have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
```
```   741   also from carr and inv_closed
```
```   742       have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
```
```   743   finally
```
```   744       have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
```
```   745   from abH and this
```
```   746       have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
```
```   747
```
```   748   from carr and this
```
```   749      have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
```
```   750      by (simp add: lcos_module_rev[OF is_group])
```
```   751   from carr and this and is_subgroup
```
```   752      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
```
```   753 qed
```
```   754
```
```   755
```
```   756 subsection {*Order of a Group and Lagrange's Theorem*}
```
```   757
```
```   758 definition
```
```   759   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
```
```   760   where "order S = card (carrier S)"
```
```   761
```
```   762 lemma (in group) rcosets_part_G:
```
```   763   assumes "subgroup H G"
```
```   764   shows "\<Union>(rcosets H) = carrier G"
```
```   765 proof -
```
```   766   interpret subgroup H G by fact
```
```   767   show ?thesis
```
```   768     apply (rule equalityI)
```
```   769     apply (force simp add: RCOSETS_def r_coset_def)
```
```   770     apply (auto simp add: RCOSETS_def intro: rcos_self assms)
```
```   771     done
```
```   772 qed
```
```   773
```
```   774 lemma (in group) cosets_finite:
```
```   775      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
```
```   776 apply (auto simp add: RCOSETS_def)
```
```   777 apply (simp add: r_coset_subset_G [THEN finite_subset])
```
```   778 done
```
```   779
```
```   780 text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
```
```   781 lemma (in group) inj_on_f:
```
```   782     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
```
```   783 apply (rule inj_onI)
```
```   784 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
```
```   785  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
```
```   786 apply (simp add: subsetD)
```
```   787 done
```
```   788
```
```   789 lemma (in group) inj_on_g:
```
```   790     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
```
```   791 by (force simp add: inj_on_def subsetD)
```
```   792
```
```   793 lemma (in group) card_cosets_equal:
```
```   794      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
```
```   795       \<Longrightarrow> card c = card H"
```
```   796 apply (auto simp add: RCOSETS_def)
```
```   797 apply (rule card_bij_eq)
```
```   798      apply (rule inj_on_f, assumption+)
```
```   799     apply (force simp add: m_assoc subsetD r_coset_def)
```
```   800    apply (rule inj_on_g, assumption+)
```
```   801   apply (force simp add: m_assoc subsetD r_coset_def)
```
```   802  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
```
```   803  apply (simp add: r_coset_subset_G [THEN finite_subset])
```
```   804 apply (blast intro: finite_subset)
```
```   805 done
```
```   806
```
```   807 lemma (in group) rcosets_subset_PowG:
```
```   808      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
```
```   809 apply (simp add: RCOSETS_def)
```
```   810 apply (blast dest: r_coset_subset_G subgroup.subset)
```
```   811 done
```
```   812
```
```   813
```
```   814 theorem (in group) lagrange:
```
```   815      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
```
```   816       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
```
```   817 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
```
```   818 apply (subst mult_commute)
```
```   819 apply (rule card_partition)
```
```   820    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
```
```   821   apply (simp add: rcosets_part_G)
```
```   822  apply (simp add: card_cosets_equal subgroup.subset)
```
```   823 apply (simp add: rcos_disjoint)
```
```   824 done
```
```   825
```
```   826
```
```   827 subsection {*Quotient Groups: Factorization of a Group*}
```
```   828
```
```   829 definition
```
```   830   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
```
```   831     --{*Actually defined for groups rather than monoids*}
```
```   832    where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
```
```   833
```
```   834 lemma (in normal) setmult_closed:
```
```   835      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
```
```   836 by (auto simp add: rcos_sum RCOSETS_def)
```
```   837
```
```   838 lemma (in normal) setinv_closed:
```
```   839      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
```
```   840 by (auto simp add: rcos_inv RCOSETS_def)
```
```   841
```
```   842 lemma (in normal) rcosets_assoc:
```
```   843      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
```
```   844       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
```
```   845 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
```
```   846
```
```   847 lemma (in subgroup) subgroup_in_rcosets:
```
```   848   assumes "group G"
```
```   849   shows "H \<in> rcosets H"
```
```   850 proof -
```
```   851   interpret group G by fact
```
```   852   from _ subgroup_axioms have "H #> \<one> = H"
```
```   853     by (rule coset_join2) auto
```
```   854   then show ?thesis
```
```   855     by (auto simp add: RCOSETS_def)
```
```   856 qed
```
```   857
```
```   858 lemma (in normal) rcosets_inv_mult_group_eq:
```
```   859      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
```
```   860 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
```
```   861
```
```   862 theorem (in normal) factorgroup_is_group:
```
```   863   "group (G Mod H)"
```
```   864 apply (simp add: FactGroup_def)
```
```   865 apply (rule groupI)
```
```   866     apply (simp add: setmult_closed)
```
```   867    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
```
```   868   apply (simp add: restrictI setmult_closed rcosets_assoc)
```
```   869  apply (simp add: normal_imp_subgroup
```
```   870                   subgroup_in_rcosets rcosets_mult_eq)
```
```   871 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
```
```   872 done
```
```   873
```
```   874 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
```
```   875   by (simp add: FactGroup_def)
```
```   876
```
```   877 lemma (in normal) inv_FactGroup:
```
```   878      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
```
```   879 apply (rule group.inv_equality [OF factorgroup_is_group])
```
```   880 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
```
```   881 done
```
```   882
```
```   883 text{*The coset map is a homomorphism from @{term G} to the quotient group
```
```   884   @{term "G Mod H"}*}
```
```   885 lemma (in normal) r_coset_hom_Mod:
```
```   886   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
```
```   887   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
```
```   888
```
```   889
```
```   890 subsection{*The First Isomorphism Theorem*}
```
```   891
```
```   892 text{*The quotient by the kernel of a homomorphism is isomorphic to the
```
```   893   range of that homomorphism.*}
```
```   894
```
```   895 definition
```
```   896   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
```
```   897     --{*the kernel of a homomorphism*}
```
```   898   where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
```
```   899
```
```   900 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
```
```   901 apply (rule subgroup.intro)
```
```   902 apply (auto simp add: kernel_def group.intro is_group)
```
```   903 done
```
```   904
```
```   905 text{*The kernel of a homomorphism is a normal subgroup*}
```
```   906 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
```
```   907 apply (simp add: G.normal_inv_iff subgroup_kernel)
```
```   908 apply (simp add: kernel_def)
```
```   909 done
```
```   910
```
```   911 lemma (in group_hom) FactGroup_nonempty:
```
```   912   assumes X: "X \<in> carrier (G Mod kernel G H h)"
```
```   913   shows "X \<noteq> {}"
```
```   914 proof -
```
```   915   from X
```
```   916   obtain g where "g \<in> carrier G"
```
```   917              and "X = kernel G H h #> g"
```
```   918     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   919   thus ?thesis
```
```   920    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
```
```   921 qed
```
```   922
```
```   923
```
```   924 lemma (in group_hom) FactGroup_the_elem_mem:
```
```   925   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
```
```   926   shows "the_elem (h`X) \<in> carrier H"
```
```   927 proof -
```
```   928   from X
```
```   929   obtain g where g: "g \<in> carrier G"
```
```   930              and "X = kernel G H h #> g"
```
```   931     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   932   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
```
```   933   thus ?thesis by (auto simp add: g)
```
```   934 qed
```
```   935
```
```   936 lemma (in group_hom) FactGroup_hom:
```
```   937      "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
```
```   938 apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
```
```   939 proof (intro ballI)
```
```   940   fix X and X'
```
```   941   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```   942      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```   943   then
```
```   944   obtain g and g'
```
```   945            where "g \<in> carrier G" and "g' \<in> carrier G"
```
```   946              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
```
```   947     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   948   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```   949     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
```
```   950     by (force simp add: kernel_def r_coset_def image_def)+
```
```   951   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
```
```   952     by (auto dest!: FactGroup_nonempty
```
```   953              simp add: set_mult_def image_eq_UN
```
```   954                        subsetD [OF Xsub] subsetD [OF X'sub])
```
```   955   thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
```
```   956     by (simp add: all image_eq_UN FactGroup_nonempty X X')
```
```   957 qed
```
```   958
```
```   959
```
```   960 text{*Lemma for the following injectivity result*}
```
```   961 lemma (in group_hom) FactGroup_subset:
```
```   962      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
```
```   963       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
```
```   964 apply (clarsimp simp add: kernel_def r_coset_def image_def)
```
```   965 apply (rename_tac y)
```
```   966 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
```
```   967 apply (simp add: G.m_assoc)
```
```   968 done
```
```   969
```
```   970 lemma (in group_hom) FactGroup_inj_on:
```
```   971      "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
```
```   972 proof (simp add: inj_on_def, clarify)
```
```   973   fix X and X'
```
```   974   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```   975      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```   976   then
```
```   977   obtain g and g'
```
```   978            where gX: "g \<in> carrier G"  "g' \<in> carrier G"
```
```   979               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
```
```   980     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   981   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```   982     by (force simp add: kernel_def r_coset_def image_def)+
```
```   983   assume "the_elem (h ` X) = the_elem (h ` X')"
```
```   984   hence h: "h g = h g'"
```
```   985     by (simp add: image_eq_UN all FactGroup_nonempty X X')
```
```   986   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
```
```   987 qed
```
```   988
```
```   989 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
```
```   990 homomorphism from the quotient group*}
```
```   991 lemma (in group_hom) FactGroup_onto:
```
```   992   assumes h: "h ` carrier G = carrier H"
```
```   993   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
```
```   994 proof
```
```   995   show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
```
```   996     by (auto simp add: FactGroup_the_elem_mem)
```
```   997   show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
```
```   998   proof
```
```   999     fix y
```
```  1000     assume y: "y \<in> carrier H"
```
```  1001     with h obtain g where g: "g \<in> carrier G" "h g = y"
```
```  1002       by (blast elim: equalityE)
```
```  1003     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
```
```  1004       by (auto simp add: y kernel_def r_coset_def)
```
```  1005     with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
```
```  1006       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
```
```  1007   qed
```
```  1008 qed
```
```  1009
```
```  1010
```
```  1011 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
```
```  1012  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
```
```  1013 theorem (in group_hom) FactGroup_iso:
```
```  1014   "h ` carrier G = carrier H
```
```  1015    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
```
```  1016 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
```
```  1017               FactGroup_onto)
```
```  1018
```
```  1019
```
```  1020 end
```