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