src/HOL/Algebra/Coset.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68517 6b5f15387353 child 68555 22d51874f37d permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/Coset.thy
```
```     2     Authors:     Florian Kammueller, L C Paulson, Stephan Hohe
```
```     3 With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
```
```     4 *)
```
```     5
```
```     6 theory Coset
```
```     7 imports Group
```
```     8 begin
```
```     9
```
```    10 section \<open>Cosets and Quotient Groups\<close>
```
```    11
```
```    12 definition
```
```    13   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
```
```    14   where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
```
```    15
```
```    16 definition
```
```    17   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
```
```    18   where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
```
```    19
```
```    20 definition
```
```    21   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _"  80)
```
```    22   where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
```
```    23
```
```    24 definition
```
```    25   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
```
```    26   where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
```
```    27
```
```    28 definition
```
```    29   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _"  80)
```
```    30   where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
```
```    31
```
```    32
```
```    33 locale normal = subgroup + group +
```
```    34   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
```
```    35
```
```    36 abbreviation
```
```    37   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
```
```    38   "H \<lhd> G \<equiv> normal H G"
```
```    39
```
```    40 (* ************************************************************************** *)
```
```    41 (* Next two lemmas contributed by Martin Baillon.                                  *)
```
```    42
```
```    43 lemma l_coset_eq_set_mult:
```
```    44   fixes G (structure)
```
```    45   shows "x <# H = {x} <#> H"
```
```    46   unfolding l_coset_def set_mult_def by simp
```
```    47
```
```    48 lemma r_coset_eq_set_mult:
```
```    49   fixes G (structure)
```
```    50   shows "H #> x = H <#> {x}"
```
```    51   unfolding r_coset_def set_mult_def by simp
```
```    52
```
```    53 (* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)
```
```    54
```
```    55 lemma (in subgroup) rcosets_non_empty:
```
```    56   assumes "R \<in> rcosets H"
```
```    57   shows "R \<noteq> {}"
```
```    58 proof -
```
```    59   obtain g where "g \<in> carrier G" "R = H #> g"
```
```    60     using assms unfolding RCOSETS_def by blast
```
```    61   hence "\<one> \<otimes> g \<in> R"
```
```    62     using one_closed unfolding r_coset_def by blast
```
```    63   thus ?thesis by blast
```
```    64 qed
```
```    65
```
```    66 lemma (in group) diff_neutralizes:
```
```    67   assumes "subgroup H G" "R \<in> rcosets H"
```
```    68   shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H"
```
```    69 proof -
```
```    70   fix r1 r2 assume r1: "r1 \<in> R" and r2: "r2 \<in> R"
```
```    71   obtain g where g: "g \<in> carrier G" "R = H #> g"
```
```    72     using assms unfolding RCOSETS_def by blast
```
```    73   then obtain h1 h2 where h1: "h1 \<in> H" "r1 = h1 \<otimes> g"
```
```    74                       and h2: "h2 \<in> H" "r2 = h2 \<otimes> g"
```
```    75     using r1 r2 unfolding r_coset_def by blast
```
```    76   hence "r1 \<otimes> (inv r2) = (h1 \<otimes> g) \<otimes> ((inv g) \<otimes> (inv h2))"
```
```    77     using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
```
```    78   also have " ... =  (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
```
```    79     using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
```
```    80           monoid_axioms subgroup.mem_carrier by smt
```
```    81   finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2"
```
```    82     using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
```
```    83   thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
```
```    84 qed
```
```    85
```
```    86 lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'"
```
```    87   unfolding set_mult_def by (simp add: UN_mono)
```
```    88
```
```    89
```
```    90 subsection \<open>Stable Operations for Subgroups\<close>
```
```    91
```
```    92 lemma (in group) subgroup_set_mult_equality[simp]:
```
```    93   assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H"
```
```    94   shows "I <#>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> J = I <#> J"
```
```    95   unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto
```
```    96
```
```    97 lemma (in group) subgroup_rcos_equality[simp]:
```
```    98   assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
```
```    99   shows "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #> h"
```
```   100   using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms)
```
```   101
```
```   102 lemma (in group) subgroup_lcos_equality[simp]:
```
```   103   assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
```
```   104   shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
```
```   105   using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
```
```   106
```
```   107 lemma set_mult_consistent [simp]:
```
```   108   "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
```
```   109   unfolding set_mult_def by simp
```
```   110
```
```   111 lemma r_coset_consistent [simp]:
```
```   112   "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h"
```
```   113   unfolding r_coset_def by simp
```
```   114
```
```   115 lemma l_coset_consistent [simp]:
```
```   116   "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I"
```
```   117   unfolding l_coset_def by simp
```
```   118
```
```   119 subsection \<open>Basic Properties of set multiplication\<close>
```
```   120
```
```   121 lemma (in group) setmult_subset_G:
```
```   122   assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
```
```   123   shows "H <#> K \<subseteq> carrier G" using assms
```
```   124   by (auto simp add: set_mult_def subsetD)
```
```   125
```
```   126 lemma (in monoid) set_mult_closed:
```
```   127   assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
```
```   128   shows "H <#> K \<subseteq> carrier G"
```
```   129   using assms by (auto simp add: set_mult_def subsetD)
```
```   130
```
```   131 (* Next lemma contributed by Martin Baillon.*)
```
```   132 lemma (in group) set_mult_assoc:
```
```   133   assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
```
```   134   shows "(M <#> H) <#> K = M <#> (H <#> K)"
```
```   135 proof
```
```   136   show "(M <#> H) <#> K \<subseteq> M <#> (H <#> K)"
```
```   137   proof
```
```   138     fix x assume "x \<in> (M <#> H) <#> K"
```
```   139     then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = (m \<otimes> h) \<otimes> k"
```
```   140       unfolding set_mult_def by blast
```
```   141     hence "x = m \<otimes> (h \<otimes> k)"
```
```   142       using assms m_assoc by blast
```
```   143     thus "x \<in> M <#> (H <#> K)"
```
```   144       unfolding set_mult_def using x by blast
```
```   145   qed
```
```   146 next
```
```   147   show "M <#> (H <#> K) \<subseteq> (M <#> H) <#> K"
```
```   148   proof
```
```   149     fix x assume "x \<in> M <#> (H <#> K)"
```
```   150     then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = m \<otimes> (h \<otimes> k)"
```
```   151       unfolding set_mult_def by blast
```
```   152     hence "x = (m \<otimes> h) \<otimes> k"
```
```   153       using assms m_assoc rev_subsetD by metis
```
```   154     thus "x \<in> (M <#> H) <#> K"
```
```   155       unfolding set_mult_def using x by blast
```
```   156   qed
```
```   157 qed
```
```   158
```
```   159
```
```   160
```
```   161 subsection \<open>Basic Properties of Cosets\<close>
```
```   162
```
```   163 lemma (in group) coset_mult_assoc:
```
```   164   assumes "M \<subseteq> carrier G" "g \<in> carrier G" "h \<in> carrier G"
```
```   165   shows "(M #> g) #> h = M #> (g \<otimes> h)"
```
```   166   using assms by (force simp add: r_coset_def m_assoc)
```
```   167
```
```   168 lemma (in group) coset_assoc:
```
```   169   assumes "x \<in> carrier G" "y \<in> carrier G" "H \<subseteq> carrier G"
```
```   170   shows "x <# (H #> y) = (x <# H) #> y"
```
```   171   using set_mult_assoc[of "{x}" H "{y}"]
```
```   172   by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)
```
```   173
```
```   174 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
```
```   175 by (force simp add: r_coset_def)
```
```   176
```
```   177 lemma (in group) coset_mult_inv1:
```
```   178   assumes "M #> (x \<otimes> (inv y)) = M"
```
```   179     and "x \<in> carrier G" "y \<in> carrier G" "M \<subseteq> carrier G"
```
```   180   shows "M #> x = M #> y" using assms
```
```   181   by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)
```
```   182
```
```   183 lemma (in group) coset_mult_inv2:
```
```   184   assumes "M #> x = M #> y"
```
```   185     and "x \<in> carrier G"  "y \<in> carrier G" "M \<subseteq> carrier G"
```
```   186   shows "M #> (x \<otimes> (inv y)) = M " using assms
```
```   187   by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)
```
```   188
```
```   189 lemma (in group) coset_join1:
```
```   190   assumes "H #> x = H"
```
```   191     and "x \<in> carrier G" "subgroup H G"
```
```   192   shows "x \<in> H"
```
```   193   using assms r_coset_def l_one subgroup.one_closed sym by fastforce
```
```   194
```
```   195 lemma (in group) solve_equation:
```
```   196   assumes "subgroup H G" "x \<in> H" "y \<in> H"
```
```   197   shows "\<exists>h \<in> H. y = h \<otimes> x"
```
```   198 proof -
```
```   199   have "y = (y \<otimes> (inv x)) \<otimes> x" using assms
```
```   200     by (simp add: m_assoc subgroup.mem_carrier)
```
```   201   moreover have "y \<otimes> (inv x) \<in> H" using assms
```
```   202     by (simp add: subgroup_def)
```
```   203   ultimately show ?thesis by blast
```
```   204 qed
```
```   205
```
```   206 lemma (in group) repr_independence:
```
```   207   assumes "y \<in> H #> x" "x \<in> carrier G" "subgroup H G"
```
```   208   shows "H #> x = H #> y" using assms
```
```   209 by (auto simp add: r_coset_def m_assoc [symmetric]
```
```   210                    subgroup.subset [THEN subsetD]
```
```   211                    subgroup.m_closed solve_equation)
```
```   212
```
```   213 lemma (in group) coset_join2:
```
```   214   assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
```
```   215   shows "H #> x = H" using assms
```
```   216   \<comment> \<open>Alternative proof is to put @{term "x=\<one>"} in \<open>repr_independence\<close>.\<close>
```
```   217 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
```
```   218
```
```   219 lemma (in group) coset_join3:
```
```   220   assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
```
```   221   shows "x <# H = H"
```
```   222 proof
```
```   223   have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> h \<in> H" using assms
```
```   224     by (simp add: subgroup.m_closed)
```
```   225   thus "x <# H \<subseteq> H" unfolding l_coset_def by blast
```
```   226 next
```
```   227   have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> ((inv x) \<otimes> h) = h"
```
```   228     by (smt assms inv_closed l_one m_assoc r_inv subgroup.mem_carrier)
```
```   229   moreover have "\<And>h. h \<in> H \<Longrightarrow> (inv x) \<otimes> h \<in> H"
```
```   230     by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
```
```   231   ultimately show "H \<subseteq> x <# H" unfolding l_coset_def by blast
```
```   232 qed
```
```   233
```
```   234 lemma (in monoid) r_coset_subset_G:
```
```   235   "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier G"
```
```   236 by (auto simp add: r_coset_def)
```
```   237
```
```   238 lemma (in group) rcosI:
```
```   239   "\<lbrakk> h \<in> H; H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> h \<otimes> x \<in> H #> x"
```
```   240 by (auto simp add: r_coset_def)
```
```   241
```
```   242 lemma (in group) rcosetsI:
```
```   243      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
```
```   244 by (auto simp add: RCOSETS_def)
```
```   245
```
```   246 lemma (in group) rcos_self:
```
```   247   "\<lbrakk> x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> x \<in> H #> x"
```
```   248   by (metis l_one rcosI subgroup_def)
```
```   249
```
```   250 text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
```
```   251 lemma (in group) repr_independenceD:
```
```   252   assumes "subgroup H G" "y \<in> carrier G"
```
```   253     and "H #> x = H #> y"
```
```   254   shows "y \<in> H #> x"
```
```   255   using assms by (simp add: rcos_self)
```
```   256
```
```   257 text \<open>Elements of a right coset are in the carrier\<close>
```
```   258 lemma (in subgroup) elemrcos_carrier:
```
```   259   assumes "group G" "a \<in> carrier G"
```
```   260     and "a' \<in> H #> a"
```
```   261   shows "a' \<in> carrier G"
```
```   262   by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE)
```
```   263
```
```   264 lemma (in subgroup) rcos_const:
```
```   265   assumes "group G" "h \<in> H"
```
```   266   shows "H #> h = H"
```
```   267   using group.coset_join2[OF assms(1), of h H]
```
```   268   by (simp add: assms(2) subgroup_axioms)
```
```   269
```
```   270 lemma (in subgroup) rcos_module_imp:
```
```   271   assumes "group G" "x \<in> carrier G"
```
```   272     and "x' \<in> H #> x"
```
```   273   shows "(x' \<otimes> inv x) \<in> H"
```
```   274 proof -
```
```   275   obtain h where h: "h \<in> H" "x' = h \<otimes> x"
```
```   276     using assms(3) unfolding r_coset_def by blast
```
```   277   hence "x' \<otimes> inv x = h"
```
```   278     by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier)
```
```   279   thus ?thesis using h by blast
```
```   280 qed
```
```   281
```
```   282 lemma (in subgroup) rcos_module_rev:
```
```   283   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
```
```   284     and "(x' \<otimes> inv x) \<in> H"
```
```   285   shows "x' \<in> H #> x"
```
```   286 proof -
```
```   287   obtain h where h: "h \<in> H" "x' \<otimes> inv x = h"
```
```   288     using assms(4) unfolding r_coset_def by blast
```
```   289   hence "x' = h \<otimes> x"
```
```   290     by (metis assms group.inv_solve_right mem_carrier)
```
```   291   thus ?thesis using h unfolding r_coset_def by blast
```
```   292 qed
```
```   293
```
```   294 text \<open>Module property of right cosets\<close>
```
```   295 lemma (in subgroup) rcos_module:
```
```   296   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
```
```   297   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
```
```   298   using rcos_module_rev rcos_module_imp assms by blast
```
```   299
```
```   300 text \<open>Right cosets are subsets of the carrier.\<close>
```
```   301 lemma (in subgroup) rcosets_carrier:
```
```   302   assumes "group G" "X \<in> rcosets H"
```
```   303   shows "X \<subseteq> carrier G"
```
```   304   using assms elemrcos_carrier singletonD
```
```   305   subset_eq unfolding RCOSETS_def by force
```
```   306
```
```   307
```
```   308 text \<open>Multiplication of general subsets\<close>
```
```   309
```
```   310 lemma (in comm_group) mult_subgroups:
```
```   311   assumes "subgroup H G" and "subgroup K G"
```
```   312   shows "subgroup (H <#> K) G"
```
```   313 proof (rule subgroup.intro)
```
```   314   show "H <#> K \<subseteq> carrier G"
```
```   315     by (simp add: setmult_subset_G assms subgroup.subset)
```
```   316 next
```
```   317   have "\<one> \<otimes> \<one> \<in> H <#> K"
```
```   318     unfolding set_mult_def using assms subgroup.one_closed by blast
```
```   319   thus "\<one> \<in> H <#> K" by simp
```
```   320 next
```
```   321   show "\<And>x. x \<in> H <#> K \<Longrightarrow> inv x \<in> H <#> K"
```
```   322   proof -
```
```   323     fix x assume "x \<in> H <#> K"
```
```   324     then obtain h k where hk: "h \<in> H" "k \<in> K" "x = h \<otimes> k"
```
```   325       unfolding set_mult_def by blast
```
```   326     hence "inv x = (inv k) \<otimes> (inv h)"
```
```   327       by (meson inv_mult_group assms subgroup.mem_carrier)
```
```   328     hence "inv x = (inv h) \<otimes> (inv k)"
```
```   329       by (metis hk inv_mult assms subgroup.mem_carrier)
```
```   330     thus "inv x \<in> H <#> K"
```
```   331       unfolding set_mult_def using hk assms
```
```   332       by (metis (no_types, lifting) UN_iff singletonI subgroup_def)
```
```   333   qed
```
```   334 next
```
```   335   show "\<And>x y. x \<in> H <#> K \<Longrightarrow> y \<in> H <#> K \<Longrightarrow> x \<otimes> y \<in> H <#> K"
```
```   336   proof -
```
```   337     fix x y assume "x \<in> H <#> K" "y \<in> H <#> K"
```
```   338     then obtain h1 k1 h2 k2 where h1k1: "h1 \<in> H" "k1 \<in> K" "x = h1 \<otimes> k1"
```
```   339                               and h2k2: "h2 \<in> H" "k2 \<in> K" "y = h2 \<otimes> k2"
```
```   340       unfolding set_mult_def by blast
```
```   341     hence "x \<otimes> y = (h1 \<otimes> k1) \<otimes> (h2 \<otimes> k2)" by simp
```
```   342     also have " ... = h1 \<otimes> (k1 \<otimes> h2) \<otimes> k2"
```
```   343       by (smt h1k1 h2k2 m_assoc m_closed assms subgroup.mem_carrier)
```
```   344     also have " ... = h1 \<otimes> (h2 \<otimes> k1) \<otimes> k2"
```
```   345       by (metis (no_types, hide_lams) assms m_comm h1k1(2) h2k2(1) subgroup.mem_carrier)
```
```   346     finally have "x \<otimes> y  = (h1 \<otimes> h2) \<otimes> (k1 \<otimes> k2)"
```
```   347       by (smt assms h1k1 h2k2 m_assoc monoid.m_closed monoid_axioms subgroup.mem_carrier)
```
```   348     thus "x \<otimes> y \<in> H <#> K" unfolding set_mult_def
```
```   349       using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
```
```   350             subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
```
```   351   qed
```
```   352 qed
```
```   353
```
```   354 lemma (in subgroup) lcos_module_rev:
```
```   355   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
```
```   356     and "(inv x \<otimes> x') \<in> H"
```
```   357   shows "x' \<in> x <# H"
```
```   358 proof -
```
```   359   obtain h where h: "h \<in> H" "inv x \<otimes> x' = h"
```
```   360     using assms(4) unfolding l_coset_def by blast
```
```   361   hence "x' = x \<otimes> h"
```
```   362     by (metis assms group.inv_solve_left mem_carrier)
```
```   363   thus ?thesis using h unfolding l_coset_def by blast
```
```   364 qed
```
```   365
```
```   366
```
```   367 subsection \<open>Normal subgroups\<close>
```
```   368
```
```   369 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
```
```   370   by (simp add: normal_def subgroup_def)
```
```   371
```
```   372 lemma (in group) normalI:
```
```   373   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
```
```   374   by (simp add: normal_def normal_axioms_def is_group)
```
```   375
```
```   376 lemma (in normal) inv_op_closed1:
```
```   377   assumes "x \<in> carrier G" and "h \<in> H"
```
```   378   shows "(inv x) \<otimes> h \<otimes> x \<in> H"
```
```   379 proof -
```
```   380   have "h \<otimes> x \<in> x <# H"
```
```   381     using assms coset_eq assms(1) unfolding r_coset_def by blast
```
```   382   then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
```
```   383     unfolding l_coset_def by blast
```
```   384   thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
```
```   385 qed
```
```   386
```
```   387 lemma (in normal) inv_op_closed2:
```
```   388   assumes "x \<in> carrier G" and "h \<in> H"
```
```   389   shows "x \<otimes> h \<otimes> (inv x) \<in> H"
```
```   390   using assms inv_op_closed1 by (metis inv_closed inv_inv)
```
```   391
```
```   392
```
```   393 text\<open>Alternative characterization of normal subgroups\<close>
```
```   394 lemma (in group) normal_inv_iff:
```
```   395      "(N \<lhd> G) =
```
```   396       (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
```
```   397       (is "_ = ?rhs")
```
```   398 proof
```
```   399   assume N: "N \<lhd> G"
```
```   400   show ?rhs
```
```   401     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
```
```   402 next
```
```   403   assume ?rhs
```
```   404   hence sg: "subgroup N G"
```
```   405     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
```
```   406   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
```
```   407   show "N \<lhd> G"
```
```   408   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
```
```   409     fix x
```
```   410     assume x: "x \<in> carrier G"
```
```   411     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
```
```   412     proof
```
```   413       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   414       proof clarify
```
```   415         fix n
```
```   416         assume n: "n \<in> N"
```
```   417         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   418         proof
```
```   419           from closed [of "inv x"]
```
```   420           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
```
```   421           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
```
```   422             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
```
```   423         qed
```
```   424       qed
```
```   425     next
```
```   426       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   427       proof clarify
```
```   428         fix n
```
```   429         assume n: "n \<in> N"
```
```   430         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   431         proof
```
```   432           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
```
```   433           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
```
```   434             by (simp add: x n m_assoc sb [THEN subsetD])
```
```   435         qed
```
```   436       qed
```
```   437     qed
```
```   438   qed
```
```   439 qed
```
```   440
```
```   441 corollary (in group) normal_invI:
```
```   442   assumes "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
```
```   443   shows "N \<lhd> G"
```
```   444   using assms normal_inv_iff by blast
```
```   445
```
```   446 corollary (in group) normal_invE:
```
```   447   assumes "N \<lhd> G"
```
```   448   shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
```
```   449   using assms normal_inv_iff apply blast
```
```   450   by (simp add: assms normal.inv_op_closed2)
```
```   451
```
```   452
```
```   453 lemma (in group) one_is_normal :
```
```   454    "{\<one>} \<lhd> G"
```
```   455 proof(intro normal_invI )
```
```   456   show "subgroup {\<one>} G"
```
```   457     by (simp add: subgroup_def)
```
```   458   show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
```
```   459 qed
```
```   460
```
```   461
```
```   462 subsection\<open>More Properties of Left Cosets\<close>
```
```   463
```
```   464 lemma (in group) l_repr_independence:
```
```   465   assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
```
```   466   shows "x <# H = y <# H"
```
```   467 proof -
```
```   468   obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
```
```   469     using assms(1) unfolding l_coset_def by blast
```
```   470   hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
```
```   471     by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
```
```   472   hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
```
```   473     unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
```
```   474   moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
```
```   475     using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
```
```   476   hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
```
```   477     unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
```
```   478   ultimately show ?thesis by blast
```
```   479 qed
```
```   480
```
```   481 lemma (in group) lcos_m_assoc:
```
```   482   "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <# (h <# M) = (g \<otimes> h) <# M"
```
```   483 by (force simp add: l_coset_def m_assoc)
```
```   484
```
```   485 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G \<Longrightarrow> \<one> <# M = M"
```
```   486 by (force simp add: l_coset_def)
```
```   487
```
```   488 lemma (in group) l_coset_subset_G:
```
```   489   "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier G"
```
```   490 by (auto simp add: l_coset_def subsetD)
```
```   491
```
```   492 lemma (in group) l_coset_carrier:
```
```   493   "\<lbrakk> y \<in> x <# H; x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> y \<in> carrier G"
```
```   494   by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)
```
```   495
```
```   496 lemma (in group) l_coset_swap:
```
```   497   assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
```
```   498   shows "x \<in> y <# H"
```
```   499   using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
```
```   500   unfolding l_coset_def by fastforce
```
```   501
```
```   502 lemma (in group) subgroup_mult_id:
```
```   503   assumes "subgroup H G"
```
```   504   shows "H <#> H = H"
```
```   505 proof
```
```   506   show "H <#> H \<subseteq> H"
```
```   507     unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff)
```
```   508   show "H \<subseteq> H <#> H"
```
```   509   proof
```
```   510     fix x assume x: "x \<in> H" thus "x \<in> H <#> H" unfolding set_mult_def
```
```   511       using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
```
```   512       by (smt UN_iff assms coset_join3 l_coset_def subgroup.mem_carrier)
```
```   513   qed
```
```   514 qed
```
```   515
```
```   516
```
```   517 subsubsection \<open>Set of Inverses of an \<open>r_coset\<close>.\<close>
```
```   518
```
```   519 lemma (in normal) rcos_inv:
```
```   520   assumes x:     "x \<in> carrier G"
```
```   521   shows "set_inv (H #> x) = H #> (inv x)"
```
```   522 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
```
```   523   fix h
```
```   524   assume h: "h \<in> H"
```
```   525   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
```
```   526   proof
```
```   527     show "inv x \<otimes> inv h \<otimes> x \<in> H"
```
```   528       by (simp add: inv_op_closed1 h x)
```
```   529     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
```
```   530       by (simp add: h x m_assoc)
```
```   531   qed
```
```   532   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
```
```   533   proof
```
```   534     show "x \<otimes> inv h \<otimes> inv x \<in> H"
```
```   535       by (simp add: inv_op_closed2 h x)
```
```   536     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
```
```   537       by (simp add: h x m_assoc [symmetric] inv_mult_group)
```
```   538   qed
```
```   539 qed
```
```   540
```
```   541
```
```   542 subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
```
```   543
```
```   544 lemma (in group) setmult_rcos_assoc:
```
```   545   "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
```
```   546     H <#> (K #> x) = (H <#> K) #> x"
```
```   547   using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult)
```
```   548
```
```   549 lemma (in group) rcos_assoc_lcos:
```
```   550   "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
```
```   551    (H #> x) <#> K = H <#> (x <# K)"
```
```   552   using set_mult_assoc[of H "{x}" K]
```
```   553   by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
```
```   554
```
```   555 lemma (in normal) rcos_mult_step1:
```
```   556   "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow>
```
```   557    (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
```
```   558   by (simp add: setmult_rcos_assoc r_coset_subset_G
```
```   559                 subset l_coset_subset_G rcos_assoc_lcos)
```
```   560
```
```   561 lemma (in normal) rcos_mult_step2:
```
```   562      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   563       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
```
```   564 by (insert coset_eq, simp add: normal_def)
```
```   565
```
```   566 lemma (in normal) rcos_mult_step3:
```
```   567      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   568       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
```
```   569 by (simp add: setmult_rcos_assoc coset_mult_assoc
```
```   570               subgroup_mult_id normal.axioms subset normal_axioms)
```
```   571
```
```   572 lemma (in normal) rcos_sum:
```
```   573      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   574       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
```
```   575 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
```
```   576
```
```   577 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
```
```   578   \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
```
```   579   by (auto simp add: RCOSETS_def subset
```
```   580         setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
```
```   581
```
```   582
```
```   583 subsubsection\<open>An Equivalence Relation\<close>
```
```   584
```
```   585 definition
```
```   586   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
```
```   587   where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G \<and> y \<in> carrier G \<and> inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
```
```   588
```
```   589
```
```   590 lemma (in subgroup) equiv_rcong:
```
```   591    assumes "group G"
```
```   592    shows "equiv (carrier G) (rcong H)"
```
```   593 proof -
```
```   594   interpret group G by fact
```
```   595   show ?thesis
```
```   596   proof (intro equivI)
```
```   597     show "refl_on (carrier G) (rcong H)"
```
```   598       by (auto simp add: r_congruent_def refl_on_def)
```
```   599   next
```
```   600     show "sym (rcong H)"
```
```   601     proof (simp add: r_congruent_def sym_def, clarify)
```
```   602       fix x y
```
```   603       assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
```
```   604          and "inv x \<otimes> y \<in> H"
```
```   605       hence "inv (inv x \<otimes> y) \<in> H" by simp
```
```   606       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
```
```   607     qed
```
```   608   next
```
```   609     show "trans (rcong H)"
```
```   610     proof (simp add: r_congruent_def trans_def, clarify)
```
```   611       fix x y z
```
```   612       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
```
```   613          and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
```
```   614       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
```
```   615       hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
```
```   616         by (simp add: m_assoc del: r_inv Units_r_inv)
```
```   617       thus "inv x \<otimes> z \<in> H" by simp
```
```   618     qed
```
```   619   qed
```
```   620 qed
```
```   621
```
```   622 text\<open>Equivalence classes of \<open>rcong\<close> correspond to left cosets.
```
```   623   Was there a mistake in the definitions? I'd have expected them to
```
```   624   correspond to right cosets.\<close>
```
```   625
```
```   626 (* CB: This is correct, but subtle.
```
```   627    We call H #> a the right coset of a relative to H.  According to
```
```   628    Jacobson, this is what the majority of group theory literature does.
```
```   629    He then defines the notion of congruence relation ~ over monoids as
```
```   630    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
```
```   631    Our notion of right congruence induced by K: rcong K appears only in
```
```   632    the context where K is a normal subgroup.  Jacobson doesn't name it.
```
```   633    But in this context left and right cosets are identical.
```
```   634 *)
```
```   635
```
```   636 lemma (in subgroup) l_coset_eq_rcong:
```
```   637   assumes "group G"
```
```   638   assumes a: "a \<in> carrier G"
```
```   639   shows "a <# H = (rcong H) `` {a}"
```
```   640 proof -
```
```   641   interpret group G by fact
```
```   642   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
```
```   643 qed
```
```   644
```
```   645
```
```   646 subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
```
```   647
```
```   648 lemma (in group) rcos_equation:
```
```   649   assumes "subgroup H G"
```
```   650   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"
```
```   651   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
```
```   652 proof -
```
```   653   interpret subgroup H G by fact
```
```   654   from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
```
```   655     apply blast by (simp add: inv_solve_left m_assoc)
```
```   656 qed
```
```   657
```
```   658 lemma (in group) rcos_disjoint:
```
```   659   assumes "subgroup H G"
```
```   660   assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
```
```   661   shows "a \<inter> b = {}"
```
```   662 proof -
```
```   663   interpret subgroup H G by fact
```
```   664   from p show ?thesis
```
```   665     apply (simp add: RCOSETS_def r_coset_def)
```
```   666     apply (blast intro: rcos_equation assms sym)
```
```   667     done
```
```   668 qed
```
```   669
```
```   670
```
```   671 subsection \<open>Further lemmas for \<open>r_congruent\<close>\<close>
```
```   672
```
```   673 text \<open>The relation is a congruence\<close>
```
```   674
```
```   675 lemma (in normal) congruent_rcong:
```
```   676   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
```
```   677 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
```
```   678   fix a b c
```
```   679   assume abrcong: "(a, b) \<in> rcong H"
```
```   680     and ccarr: "c \<in> carrier G"
```
```   681
```
```   682   from abrcong
```
```   683       have acarr: "a \<in> carrier G"
```
```   684         and bcarr: "b \<in> carrier G"
```
```   685         and abH: "inv a \<otimes> b \<in> H"
```
```   686       unfolding r_congruent_def
```
```   687       by fast+
```
```   688
```
```   689   note carr = acarr bcarr ccarr
```
```   690
```
```   691   from ccarr and abH
```
```   692       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
```
```   693   moreover
```
```   694       from carr and inv_closed
```
```   695       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)"
```
```   696       by (force cong: m_assoc)
```
```   697   moreover
```
```   698       from carr and inv_closed
```
```   699       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
```
```   700       by (simp add: inv_mult_group)
```
```   701   ultimately
```
```   702       have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
```
```   703   from carr and this
```
```   704      have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
```
```   705      by (simp add: lcos_module_rev[OF is_group])
```
```   706   from carr and this and is_subgroup
```
```   707      show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
```
```   708 next
```
```   709   fix a b c
```
```   710   assume abrcong: "(a, b) \<in> rcong H"
```
```   711     and ccarr: "c \<in> carrier G"
```
```   712
```
```   713   from ccarr have "c \<in> Units G" by simp
```
```   714   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
```
```   715
```
```   716   from abrcong
```
```   717       have acarr: "a \<in> carrier G"
```
```   718        and bcarr: "b \<in> carrier G"
```
```   719        and abH: "inv a \<otimes> b \<in> H"
```
```   720       by (unfold r_congruent_def, fast+)
```
```   721
```
```   722   note carr = acarr bcarr ccarr
```
```   723
```
```   724   from carr and inv_closed
```
```   725      have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
```
```   726   also from carr and inv_closed
```
```   727       have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
```
```   728   also from carr and inv_closed
```
```   729       have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
```
```   730   also from carr and inv_closed
```
```   731       have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
```
```   732   finally
```
```   733       have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
```
```   734   from abH and this
```
```   735       have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
```
```   736
```
```   737   from carr and this
```
```   738      have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
```
```   739      by (simp add: lcos_module_rev[OF is_group])
```
```   740   from carr and this and is_subgroup
```
```   741      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
```
```   742 qed
```
```   743
```
```   744
```
```   745 subsection \<open>Order of a Group and Lagrange's Theorem\<close>
```
```   746
```
```   747 definition
```
```   748   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
```
```   749   where "order S = card (carrier S)"
```
```   750
```
```   751 lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
```
```   752 by(auto simp add: order_def card_gt_0_iff)
```
```   753
```
```   754 lemma (in group) rcosets_part_G:
```
```   755   assumes "subgroup H G"
```
```   756   shows "\<Union>(rcosets H) = carrier G"
```
```   757 proof -
```
```   758   interpret subgroup H G by fact
```
```   759   show ?thesis
```
```   760     apply (rule equalityI)
```
```   761     apply (force simp add: RCOSETS_def r_coset_def)
```
```   762     apply (auto simp add: RCOSETS_def intro: rcos_self assms)
```
```   763     done
```
```   764 qed
```
```   765
```
```   766 lemma (in group) cosets_finite:
```
```   767      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
```
```   768 apply (auto simp add: RCOSETS_def)
```
```   769 apply (simp add: r_coset_subset_G [THEN finite_subset])
```
```   770 done
```
```   771
```
```   772 text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
```
```   773 lemma (in group) inj_on_f:
```
```   774     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
```
```   775 apply (rule inj_onI)
```
```   776 apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
```
```   777  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
```
```   778 apply (simp add: subsetD)
```
```   779 done
```
```   780
```
```   781 lemma (in group) inj_on_g:
```
```   782     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
```
```   783 by (force simp add: inj_on_def subsetD)
```
```   784
```
```   785 (* ************************************************************************** *)
```
```   786
```
```   787 lemma (in group) card_cosets_equal:
```
```   788   assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
```
```   789   shows "\<exists>f. bij_betw f H R"
```
```   790 proof -
```
```   791   obtain g where g: "g \<in> carrier G" "R = H #> g"
```
```   792     using assms(1) unfolding RCOSETS_def by blast
```
```   793
```
```   794   let ?f = "\<lambda>h. h \<otimes> g"
```
```   795   have "\<And>r. r \<in> R \<Longrightarrow> \<exists>h \<in> H. ?f h = r"
```
```   796   proof -
```
```   797     fix r assume "r \<in> R"
```
```   798     then obtain h where "h \<in> H" "r = h \<otimes> g"
```
```   799       using g unfolding r_coset_def by blast
```
```   800     thus "\<exists>h \<in> H. ?f h = r" by blast
```
```   801   qed
```
```   802   hence "R \<subseteq> ?f ` H" by blast
```
```   803   moreover have "?f ` H \<subseteq> R"
```
```   804     using g unfolding r_coset_def by blast
```
```   805   ultimately show ?thesis using inj_on_g unfolding bij_betw_def
```
```   806     using assms(2) g(1) by auto
```
```   807 qed
```
```   808
```
```   809 corollary (in group) card_rcosets_equal:
```
```   810   assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
```
```   811   shows "card H = card R"
```
```   812   using card_cosets_equal assms bij_betw_same_card by blast
```
```   813
```
```   814 corollary (in group) rcosets_finite:
```
```   815   assumes "R \<in> rcosets H" "H \<subseteq> carrier G" "finite H"
```
```   816   shows "finite R"
```
```   817   using card_cosets_equal assms bij_betw_finite is_group by blast
```
```   818
```
```   819 (* ************************************************************************** *)
```
```   820
```
```   821 lemma (in group) rcosets_subset_PowG:
```
```   822      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
```
```   823   using rcosets_part_G by auto
```
```   824
```
```   825 proposition (in group) lagrange_finite:
```
```   826      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
```
```   827       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
```
```   828 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
```
```   829 apply (subst mult.commute)
```
```   830 apply (rule card_partition)
```
```   831    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
```
```   832   apply (simp add: rcosets_part_G)
```
```   833   apply (simp add: card_rcosets_equal subgroup.subset)
```
```   834 apply (simp add: rcos_disjoint)
```
```   835 done
```
```   836
```
```   837 theorem (in group) lagrange:
```
```   838   assumes "subgroup H G"
```
```   839   shows "card (rcosets H) * card H = order G"
```
```   840 proof (cases "finite (carrier G)")
```
```   841   case True thus ?thesis using lagrange_finite assms by simp
```
```   842 next
```
```   843   case False note inf_G = this
```
```   844   thus ?thesis
```
```   845   proof (cases "finite H")
```
```   846     case False thus ?thesis using inf_G  by (simp add: order_def)
```
```   847   next
```
```   848     case True note finite_H = this
```
```   849     have "infinite (rcosets H)"
```
```   850     proof (rule ccontr)
```
```   851       assume "\<not> infinite (rcosets H)"
```
```   852       hence finite_rcos: "finite (rcosets H)" by simp
```
```   853       hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
```
```   854         using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
```
```   855               rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
```
```   856       hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
```
```   857         by (simp add: assms order_def rcosets_part_G)
```
```   858       hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
```
```   859         using card_rcosets_equal by (simp add: assms subgroup.subset)
```
```   860       hence "order G = (card H) * (card (rcosets H))" by simp
```
```   861       hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
```
```   862                                 rcosets_part_G subgroup.one_closed by fastforce
```
```   863       thus False using inf_G order_gt_0_iff_finite by blast
```
```   864     qed
```
```   865     thus ?thesis using inf_G by (simp add: order_def)
```
```   866   qed
```
```   867 qed
```
```   868
```
```   869
```
```   870 subsection \<open>Quotient Groups: Factorization of a Group\<close>
```
```   871
```
```   872 definition
```
```   873   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
```
```   874     \<comment> \<open>Actually defined for groups rather than monoids\<close>
```
```   875    where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
```
```   876
```
```   877 lemma (in normal) setmult_closed:
```
```   878      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
```
```   879 by (auto simp add: rcos_sum RCOSETS_def)
```
```   880
```
```   881 lemma (in normal) setinv_closed:
```
```   882      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
```
```   883 by (auto simp add: rcos_inv RCOSETS_def)
```
```   884
```
```   885 lemma (in normal) rcosets_assoc:
```
```   886      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
```
```   887       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
```
```   888   by (simp add: group.set_mult_assoc is_group rcosets_carrier)
```
```   889
```
```   890 lemma (in subgroup) subgroup_in_rcosets:
```
```   891   assumes "group G"
```
```   892   shows "H \<in> rcosets H"
```
```   893 proof -
```
```   894   interpret group G by fact
```
```   895   from _ subgroup_axioms have "H #> \<one> = H"
```
```   896     by (rule coset_join2) auto
```
```   897   then show ?thesis
```
```   898     by (auto simp add: RCOSETS_def)
```
```   899 qed
```
```   900
```
```   901 lemma (in normal) rcosets_inv_mult_group_eq:
```
```   902      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
```
```   903 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
```
```   904
```
```   905 theorem (in normal) factorgroup_is_group:
```
```   906   "group (G Mod H)"
```
```   907 apply (simp add: FactGroup_def)
```
```   908 apply (rule groupI)
```
```   909     apply (simp add: setmult_closed)
```
```   910    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
```
```   911   apply (simp add: restrictI setmult_closed rcosets_assoc)
```
```   912  apply (simp add: normal_imp_subgroup
```
```   913                   subgroup_in_rcosets rcosets_mult_eq)
```
```   914 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
```
```   915 done
```
```   916
```
```   917 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
```
```   918   by (simp add: FactGroup_def)
```
```   919
```
```   920 lemma (in normal) inv_FactGroup:
```
```   921      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
```
```   922 apply (rule group.inv_equality [OF factorgroup_is_group])
```
```   923 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
```
```   924 done
```
```   925
```
```   926 text\<open>The coset map is a homomorphism from @{term G} to the quotient group
```
```   927   @{term "G Mod H"}\<close>
```
```   928 lemma (in normal) r_coset_hom_Mod:
```
```   929   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
```
```   930   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
```
```   931
```
```   932
```
```   933 subsection\<open>The First Isomorphism Theorem\<close>
```
```   934
```
```   935 text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
```
```   936   range of that homomorphism.\<close>
```
```   937
```
```   938 definition
```
```   939   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
```
```   940     \<comment> \<open>the kernel of a homomorphism\<close>
```
```   941   where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
```
```   942
```
```   943 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
```
```   944 apply (rule subgroup.intro)
```
```   945 apply (auto simp add: kernel_def group.intro is_group)
```
```   946 done
```
```   947
```
```   948 text\<open>The kernel of a homomorphism is a normal subgroup\<close>
```
```   949 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
```
```   950 apply (simp add: G.normal_inv_iff subgroup_kernel)
```
```   951 apply (simp add: kernel_def)
```
```   952 done
```
```   953
```
```   954 lemma (in group_hom) FactGroup_nonempty:
```
```   955   assumes X: "X \<in> carrier (G Mod kernel G H h)"
```
```   956   shows "X \<noteq> {}"
```
```   957 proof -
```
```   958   from X
```
```   959   obtain g where "g \<in> carrier G"
```
```   960              and "X = kernel G H h #> g"
```
```   961     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   962   thus ?thesis
```
```   963    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
```
```   964 qed
```
```   965
```
```   966
```
```   967 lemma (in group_hom) FactGroup_the_elem_mem:
```
```   968   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
```
```   969   shows "the_elem (h`X) \<in> carrier H"
```
```   970 proof -
```
```   971   from X
```
```   972   obtain g where g: "g \<in> carrier G"
```
```   973              and "X = kernel G H h #> g"
```
```   974     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   975   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
```
```   976   thus ?thesis by (auto simp add: g)
```
```   977 qed
```
```   978
```
```   979 lemma (in group_hom) FactGroup_hom:
```
```   980      "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
```
```   981 apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
```
```   982 proof (intro ballI)
```
```   983   fix X and X'
```
```   984   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```   985      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```   986   then
```
```   987   obtain g and g'
```
```   988            where "g \<in> carrier G" and "g' \<in> carrier G"
```
```   989              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
```
```   990     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   991   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```   992     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
```
```   993     by (force simp add: kernel_def r_coset_def image_def)+
```
```   994   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
```
```   995     by (auto dest!: FactGroup_nonempty intro!: image_eqI
```
```   996              simp add: set_mult_def
```
```   997                        subsetD [OF Xsub] subsetD [OF X'sub])
```
```   998   then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
```
```   999     by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
```
```  1000 qed
```
```  1001
```
```  1002
```
```  1003 text\<open>Lemma for the following injectivity result\<close>
```
```  1004 lemma (in group_hom) FactGroup_subset:
```
```  1005      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
```
```  1006       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
```
```  1007 apply (clarsimp simp add: kernel_def r_coset_def)
```
```  1008 apply (rename_tac y)
```
```  1009 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
```
```  1010 apply (simp add: G.m_assoc)
```
```  1011 done
```
```  1012
```
```  1013 lemma (in group_hom) FactGroup_inj_on:
```
```  1014      "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
```
```  1015 proof (simp add: inj_on_def, clarify)
```
```  1016   fix X and X'
```
```  1017   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```  1018      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```  1019   then
```
```  1020   obtain g and g'
```
```  1021            where gX: "g \<in> carrier G"  "g' \<in> carrier G"
```
```  1022               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
```
```  1023     by (auto simp add: FactGroup_def RCOSETS_def)
```
```  1024   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```  1025     by (force simp add: kernel_def r_coset_def image_def)+
```
```  1026   assume "the_elem (h ` X) = the_elem (h ` X')"
```
```  1027   hence h: "h g = h g'"
```
```  1028     by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
```
```  1029   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
```
```  1030 qed
```
```  1031
```
```  1032 text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
```
```  1033 homomorphism from the quotient group\<close>
```
```  1034 lemma (in group_hom) FactGroup_onto:
```
```  1035   assumes h: "h ` carrier G = carrier H"
```
```  1036   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
```
```  1037 proof
```
```  1038   show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
```
```  1039     by (auto simp add: FactGroup_the_elem_mem)
```
```  1040   show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
```
```  1041   proof
```
```  1042     fix y
```
```  1043     assume y: "y \<in> carrier H"
```
```  1044     with h obtain g where g: "g \<in> carrier G" "h g = y"
```
```  1045       by (blast elim: equalityE)
```
```  1046     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
```
```  1047       by (auto simp add: y kernel_def r_coset_def)
```
```  1048     with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
```
```  1049       apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
```
```  1050       apply (subst the_elem_image_unique)
```
```  1051       apply auto
```
```  1052       done
```
```  1053   qed
```
```  1054 qed
```
```  1055
```
```  1056
```
```  1057 text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
```
```  1058  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
```
```  1059 theorem (in group_hom) FactGroup_iso_set:
```
```  1060   "h ` carrier G = carrier H
```
```  1061    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
```
```  1062 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
```
```  1063               FactGroup_onto)
```
```  1064
```
```  1065 corollary (in group_hom) FactGroup_iso :
```
```  1066   "h ` carrier G = carrier H
```
```  1067    \<Longrightarrow> (G Mod (kernel G H h))\<cong> H"
```
```  1068   using FactGroup_iso_set unfolding is_iso_def by auto
```
```  1069
```
```  1070
```
```  1071 (* Next two lemmas contributed by Paulo Emílio de Vilhena. *)
```
```  1072
```
```  1073 lemma (in group_hom) trivial_hom_iff:
```
```  1074   "(h ` (carrier G) = { \<one>\<^bsub>H\<^esub> }) = (kernel G H h = carrier G)"
```
```  1075   unfolding kernel_def using one_closed by force
```
```  1076
```
```  1077 lemma (in group_hom) trivial_ker_imp_inj:
```
```  1078   assumes "kernel G H h = { \<one> }"
```
```  1079   shows "inj_on h (carrier G)"
```
```  1080 proof (rule inj_onI)
```
```  1081   fix g1 g2 assume A: "g1 \<in> carrier G" "g2 \<in> carrier G" "h g1 = h g2"
```
```  1082   hence "h (g1 \<otimes> (inv g2)) = \<one>\<^bsub>H\<^esub>" by simp
```
```  1083   hence "g1 \<otimes> (inv g2) = \<one>"
```
```  1084     using A assms unfolding kernel_def by blast
```
```  1085   thus "g1 = g2"
```
```  1086     using A G.inv_equality G.inv_inv by blast
```
```  1087 qed
```
```  1088
```
```  1089
```
```  1090 (* Next subsection contributed by Martin Baillon. *)
```
```  1091
```
```  1092 subsection \<open>Theorems about Factor Groups and Direct product\<close>
```
```  1093
```
```  1094 lemma (in group) DirProd_normal :
```
```  1095   assumes "group K"
```
```  1096     and "H \<lhd> G"
```
```  1097     and "N \<lhd> K"
```
```  1098   shows "H \<times> N \<lhd> G \<times>\<times> K"
```
```  1099 proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]])
```
```  1100   show sub : "subgroup (H \<times> N) (G \<times>\<times> K)"
```
```  1101     using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1)
```
```  1102          normal_imp_subgroup[OF assms(3)]].
```
```  1103   show "\<And>x h. x \<in> carrier (G\<times>\<times>K) \<Longrightarrow> h \<in> H\<times>N \<Longrightarrow> x \<otimes>\<^bsub>G\<times>\<times>K\<^esub> h \<otimes>\<^bsub>G\<times>\<times>K\<^esub> inv\<^bsub>G\<times>\<times>K\<^esub> x \<in> H\<times>N"
```
```  1104   proof-
```
```  1105     fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
```
```  1106     hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup.subset[OF sub] by auto
```
```  1107     from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
```
```  1108       unfolding DirProd_def by fastforce
```
```  1109     from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
```
```  1110       unfolding DirProd_def by fastforce
```
```  1111     hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
```
```  1112       using normal_imp_subgroup subgroup.subset assms apply blast+.
```
```  1113     have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
```
```  1114       using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
```
```  1115     hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
```
```  1116       using h1h2 x1x2 h1h2GK by auto
```
```  1117     moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
```
```  1118       using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
```
```  1119     hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
```
```  1120     ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
```
```  1121   qed
```
```  1122 qed
```
```  1123
```
```  1124 lemma (in group) FactGroup_DirProd_multiplication_iso_set :
```
```  1125   assumes "group K"
```
```  1126     and "H \<lhd> G"
```
```  1127     and "N \<lhd> K"
```
```  1128   shows "(\<lambda> (X, Y). X \<times> Y) \<in> iso  ((G Mod H) \<times>\<times> (K Mod N)) (G \<times>\<times> K Mod H \<times> N)"
```
```  1129
```
```  1130 proof-
```
```  1131   have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
```
```  1132     unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
```
```  1133   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
```
```  1134                 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
```
```  1135     unfolding set_mult_def by force
```
```  1136   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
```
```  1137                  \<forall>ya\<in>carrier (K Mod N).  x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
```
```  1138     unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
```
```  1139     by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
```
```  1140   moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
```
```  1141                                      carrier (G \<times>\<times> K Mod H \<times> N)"
```
```  1142     unfolding image_def  apply auto using R apply force
```
```  1143     unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
```
```  1144   ultimately show ?thesis
```
```  1145     unfolding iso_def hom_def bij_betw_def inj_on_def by simp
```
```  1146 qed
```
```  1147
```
```  1148 corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
```
```  1149   assumes "group K"
```
```  1150     and "H \<lhd> G"
```
```  1151     and "N \<lhd> K"
```
```  1152   shows "  ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)"
```
```  1153   unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
```
```  1154
```
```  1155 corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
```
```  1156   assumes "group K"
```
```  1157     and "H \<lhd> G"
```
```  1158     and "N \<lhd> K"
```
```  1159   shows "(G \<times>\<times> K Mod H \<times> N) \<cong> ((G Mod H) \<times>\<times> (K Mod N))"
```
```  1160   using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms
```
```  1161         DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
```
```  1162   by blast
```
```  1163
```
```  1164 subsubsection "More Lemmas about set multiplication"
```
```  1165
```
```  1166 (*A group multiplied by a subgroup stays the same*)
```
```  1167 lemma (in group) set_mult_carrier_idem:
```
```  1168   assumes "subgroup H G"
```
```  1169   shows "(carrier G) <#> H = carrier G"
```
```  1170 proof
```
```  1171   show "(carrier G)<#>H \<subseteq> carrier G"
```
```  1172     unfolding set_mult_def using subgroup.subset assms by blast
```
```  1173 next
```
```  1174   have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
```
```  1175   moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
```
```  1176     using assms subgroup.one_closed[OF assms] by blast
```
```  1177   ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
```
```  1178 qed
```
```  1179
```
```  1180 (*Same lemma as above, but everything is included in a subgroup*)
```
```  1181 lemma (in group) set_mult_subgroup_idem:
```
```  1182   assumes "subgroup H G"
```
```  1183     and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
```
```  1184   shows "H<#>N = H"
```
```  1185   using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
```
```  1186   by (metis monoid.cases_scheme order_refl partial_object.simps(1)
```
```  1187       partial_object.update_convs(1) subgroup_set_mult_equality)
```
```  1188
```
```  1189 (*A normal subgroup is commutative with set_mult*)
```
```  1190 lemma (in group) commut_normal:
```
```  1191   assumes "subgroup H G"
```
```  1192     and "N\<lhd>G"
```
```  1193   shows "H<#>N = N<#>H"
```
```  1194 proof-
```
```  1195   have aux1: "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
```
```  1196   also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
```
```  1197   moreover have aux2: "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
```
```  1198   ultimately show "H<#>N = N<#>H" by simp
```
```  1199 qed
```
```  1200
```
```  1201 (*Same lemma as above, but everything is included in a subgroup*)
```
```  1202 lemma (in group) commut_normal_subgroup:
```
```  1203   assumes "subgroup H G"
```
```  1204     and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
```
```  1205     and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
```
```  1206   shows "K<#>N = N<#>K"
```
```  1207 proof-
```
```  1208   have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
```
```  1209   hence NH : "N \<subseteq> H" by simp
```
```  1210   have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
```
```  1211   hence KH : "K \<subseteq> H" by simp
```
```  1212   have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
```
```  1213   using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
```
```  1214                assms(3) assms(2)] by auto
```
```  1215   also have "... = N <#> K" using subgroup_set_mult_equality[of H N K, OF assms(1) NH KH] by auto
```
```  1216   moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
```
```  1217     using subgroup_set_mult_equality[of H K N, OF assms(1) KH NH] by auto
```
```  1218   ultimately show "K<#>N = N<#>K" by auto
```
```  1219 qed
```
```  1220
```
```  1221
```
```  1222
```
```  1223 subsubsection "Lemmas about intersection and normal subgroups"
```
```  1224
```
```  1225 lemma (in group) normal_inter:
```
```  1226   assumes "subgroup H G"
```
```  1227     and "subgroup K G"
```
```  1228     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
```
```  1229   shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
```
```  1230 proof-
```
```  1231   define HK and H1K and GH and GHK
```
```  1232     where "HK = H\<inter>K" and "H1K=H1\<inter>K" and "GH =G\<lparr>carrier := H\<rparr>" and "GHK = (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
```
```  1233   show "H1K\<lhd>GHK"
```
```  1234   proof (intro group.normal_invI[of GHK H1K])
```
```  1235     show "Group.group GHK"
```
```  1236       using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
```
```  1237
```
```  1238   next
```
```  1239     have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
```
```  1240     proof(intro subgroup_incl)
```
```  1241       show "subgroup H1K G"
```
```  1242         using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
```
```  1243     next
```
```  1244       show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
```
```  1245     next
```
```  1246       have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))"
```
```  1247         using  assms(3) normal_imp_subgroup subgroup.subset by blast
```
```  1248       also have "... \<subseteq> H" by simp
```
```  1249       thus "H1K \<subseteq>H\<inter>K"
```
```  1250         using H1K_def calculation by auto
```
```  1251     qed
```
```  1252     thus "subgroup H1K GHK" using GHK_def by simp
```
```  1253   next
```
```  1254     show "\<And> x h. x\<in>carrier GHK \<Longrightarrow> h\<in>H1K \<Longrightarrow> x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x\<in> H1K"
```
```  1255     proof-
```
```  1256       have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
```
```  1257         using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
```
```  1258       have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
```
```  1259         using HK_def by simp
```
```  1260       fix x assume p: "x\<in>carrier GHK"
```
```  1261       fix h assume p2 : "h:H1K"
```
```  1262       have "carrier(GHK)\<subseteq>HK"
```
```  1263         using GHK_def HK_def by simp
```
```  1264       hence xHK:"x\<in>HK" using p by auto
```
```  1265       hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
```
```  1266         using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
```
```  1267       have "H1\<subseteq>carrier(GH)"
```
```  1268         using assms GH_def normal_imp_subgroup subgroup.subset by blast
```
```  1269       hence hHK:"h\<in>HK"
```
```  1270         using p2 H1K_def HK_def GH_def by auto
```
```  1271       hence xhx_egal : "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x =  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x"
```
```  1272         using invx invHK multHK GHK_def GH_def by auto
```
```  1273       have xH:"x\<in>carrier(GH)"
```
```  1274         using xHK HK_def GH_def by auto
```
```  1275       have hH:"h\<in>carrier(GH)"
```
```  1276         using hHK HK_def GH_def by auto
```
```  1277       have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
```
```  1278         using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
```
```  1279       hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
```
```  1280         using  xH H1K_def p2 by blast
```
```  1281       have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
```
```  1282         using assms HK_def subgroups_Inter_pair hHK xHK
```
```  1283         by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
```
```  1284       hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
```
```  1285       hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1K" using INCL_1 H1K_def by auto
```
```  1286       thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
```
```  1287     qed
```
```  1288   qed
```
```  1289 qed
```
```  1290
```
```  1291
```
```  1292 lemma (in group) normal_inter_subgroup:
```
```  1293   assumes "subgroup H G"
```
```  1294     and "N \<lhd> G"
```
```  1295   shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
```
```  1296 proof -
```
```  1297   define K where "K = carrier G"
```
```  1298   have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
```
```  1299   moreover have "subgroup K G" using K_def subgroup_self by blast
```
```  1300   moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
```
```  1301   ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
```
```  1302     using normal_inter[of K H N] assms(1) by blast
```
```  1303   moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
```
```  1304   ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
```
```  1305 qed
```
```  1306
```
```  1307
```
```  1308 end
```