39 "H \<lhd> G \<equiv> normal H G" |
39 "H \<lhd> G \<equiv> normal H G" |
40 |
40 |
41 lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G" |
41 lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G" |
42 by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier) |
42 by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier) |
43 |
43 |
44 (*Next two lemmas contributed by Martin Baillon.*) |
44 lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
45 |
|
46 lemma l_coset_eq_set_mult: |
|
47 fixes G (structure) |
45 fixes G (structure) |
48 shows "x <# H = {x} <#> H" |
46 shows "x <# H = {x} <#> H" |
49 unfolding l_coset_def set_mult_def by simp |
47 unfolding l_coset_def set_mult_def by simp |
50 |
48 |
51 lemma r_coset_eq_set_mult: |
49 lemma r_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
52 fixes G (structure) |
50 fixes G (structure) |
53 shows "H #> x = H <#> {x}" |
51 shows "H #> x = H <#> {x}" |
54 unfolding r_coset_def set_mult_def by simp |
52 unfolding r_coset_def set_mult_def by simp |
55 |
53 |
56 (* Next five lemmas contributed by Paulo Emílio de Vilhena. *) |
54 lemma (in subgroup) rcosets_non_empty: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
57 |
|
58 lemma (in subgroup) rcosets_non_empty: |
|
59 assumes "R \<in> rcosets H" |
55 assumes "R \<in> rcosets H" |
60 shows "R \<noteq> {}" |
56 shows "R \<noteq> {}" |
61 proof - |
57 proof - |
62 obtain g where "g \<in> carrier G" "R = H #> g" |
58 obtain g where "g \<in> carrier G" "R = H #> g" |
63 using assms unfolding RCOSETS_def by blast |
59 using assms unfolding RCOSETS_def by blast |
64 hence "\<one> \<otimes> g \<in> R" |
60 hence "\<one> \<otimes> g \<in> R" |
65 using one_closed unfolding r_coset_def by blast |
61 using one_closed unfolding r_coset_def by blast |
66 thus ?thesis by blast |
62 thus ?thesis by blast |
67 qed |
63 qed |
68 |
64 |
69 lemma (in group) diff_neutralizes: |
65 lemma (in group) diff_neutralizes: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
70 assumes "subgroup H G" "R \<in> rcosets H" |
66 assumes "subgroup H G" "R \<in> rcosets H" |
71 shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H" |
67 shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H" |
72 proof - |
68 proof - |
73 fix r1 r2 assume r1: "r1 \<in> R" and r2: "r2 \<in> R" |
69 fix r1 r2 assume r1: "r1 \<in> R" and r2: "r2 \<in> R" |
74 obtain g where g: "g \<in> carrier G" "R = H #> g" |
70 obtain g where g: "g \<in> carrier G" "R = H #> g" |
92 finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2" |
88 finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2" |
93 using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce |
89 using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce |
94 thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def) |
90 thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def) |
95 qed |
91 qed |
96 |
92 |
97 lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'" |
93 lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
98 unfolding set_mult_def by (simp add: UN_mono) |
94 unfolding set_mult_def by (simp add: UN_mono) |
99 |
95 |
100 |
96 |
101 subsection \<open>Stable Operations for Subgroups\<close> |
97 subsection \<open>Stable Operations for Subgroups\<close> |
102 |
98 |
103 lemma set_mult_consistent [simp]: |
99 lemma set_mult_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
104 "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K" |
100 "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K" |
105 unfolding set_mult_def by simp |
101 unfolding set_mult_def by simp |
106 |
102 |
107 lemma r_coset_consistent [simp]: |
103 lemma r_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
108 "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h" |
104 "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h" |
109 unfolding r_coset_def by simp |
105 unfolding r_coset_def by simp |
110 |
106 |
111 lemma l_coset_consistent [simp]: |
107 lemma l_coset_consistent [simp]: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
112 "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I" |
108 "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I" |
113 unfolding l_coset_def by simp |
109 unfolding l_coset_def by simp |
|
110 |
114 |
111 |
115 subsection \<open>Basic Properties of set multiplication\<close> |
112 subsection \<open>Basic Properties of set multiplication\<close> |
116 |
113 |
117 lemma (in group) setmult_subset_G: |
114 lemma (in group) setmult_subset_G: |
118 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
115 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
122 lemma (in monoid) set_mult_closed: |
119 lemma (in monoid) set_mult_closed: |
123 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
120 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
124 shows "H <#> K \<subseteq> carrier G" |
121 shows "H <#> K \<subseteq> carrier G" |
125 using assms by (auto simp add: set_mult_def subsetD) |
122 using assms by (auto simp add: set_mult_def subsetD) |
126 |
123 |
127 (* Next lemma contributed by Martin Baillon.*) |
124 lemma (in group) set_mult_assoc: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
128 lemma (in group) set_mult_assoc: |
|
129 assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
125 assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
130 shows "(M <#> H) <#> K = M <#> (H <#> K)" |
126 shows "(M <#> H) <#> K = M <#> (H <#> K)" |
131 proof |
127 proof |
132 show "(M <#> H) <#> K \<subseteq> M <#> (H <#> K)" |
128 show "(M <#> H) <#> K \<subseteq> M <#> (H <#> K)" |
133 proof |
129 proof |
1092 "h ` carrier G = carrier H |
1088 "h ` carrier G = carrier H |
1093 \<Longrightarrow> (G Mod (kernel G H h))\<cong> H" |
1089 \<Longrightarrow> (G Mod (kernel G H h))\<cong> H" |
1094 using FactGroup_iso_set unfolding is_iso_def by auto |
1090 using FactGroup_iso_set unfolding is_iso_def by auto |
1095 |
1091 |
1096 |
1092 |
1097 (* Next two lemmas contributed by Paulo Emílio de Vilhena. *) |
1093 lemma (in group_hom) trivial_hom_iff: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
1098 |
|
1099 lemma (in group_hom) trivial_hom_iff: |
|
1100 "h ` (carrier G) = { \<one>\<^bsub>H\<^esub> } \<longleftrightarrow> kernel G H h = carrier G" |
1094 "h ` (carrier G) = { \<one>\<^bsub>H\<^esub> } \<longleftrightarrow> kernel G H h = carrier G" |
1101 unfolding kernel_def using one_closed by force |
1095 unfolding kernel_def using one_closed by force |
1102 |
1096 |
1103 lemma (in group_hom) trivial_ker_imp_inj: |
1097 lemma (in group_hom) trivial_ker_imp_inj: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
1104 assumes "kernel G H h = { \<one> }" |
1098 assumes "kernel G H h = { \<one> }" |
1105 shows "inj_on h (carrier G)" |
1099 shows "inj_on h (carrier G)" |
1106 proof (rule inj_onI) |
1100 proof (rule inj_onI) |
1107 fix g1 g2 assume A: "g1 \<in> carrier G" "g2 \<in> carrier G" "h g1 = h g2" |
1101 fix g1 g2 assume A: "g1 \<in> carrier G" "g2 \<in> carrier G" "h g1 = h g2" |
1108 hence "h (g1 \<otimes> (inv g2)) = \<one>\<^bsub>H\<^esub>" by simp |
1102 hence "h (g1 \<otimes> (inv g2)) = \<one>\<^bsub>H\<^esub>" by simp |
1195 ultimately show "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I" |
1189 ultimately show "h ` (I <#> (kernel G H h)) = h ` I" and "h ` ((kernel G H h) <#> I) = h ` I" |
1196 using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+ |
1190 using set_mult_hom[OF homh assms ker_in_carrier] set_mult_hom[OF homh ker_in_carrier assms] by simp+ |
1197 qed |
1191 qed |
1198 |
1192 |
1199 |
1193 |
1200 (* Next subsection contributed by Martin Baillon. *) |
|
1201 |
|
1202 subsection \<open>Theorems about Factor Groups and Direct product\<close> |
1194 subsection \<open>Theorems about Factor Groups and Direct product\<close> |
1203 |
1195 |
1204 lemma (in group) DirProd_normal : |
1196 lemma (in group) DirProd_normal : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
1205 assumes "group K" |
1197 assumes "group K" |
1206 and "H \<lhd> G" |
1198 and "H \<lhd> G" |
1207 and "N \<lhd> K" |
1199 and "N \<lhd> K" |
1208 shows "H \<times> N \<lhd> G \<times>\<times> K" |
1200 shows "H \<times> N \<lhd> G \<times>\<times> K" |
1209 proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]]) |
1201 proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]]) |
1229 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 |
1221 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 |
1230 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 |
1222 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 |
1231 qed |
1223 qed |
1232 qed |
1224 qed |
1233 |
1225 |
1234 lemma (in group) FactGroup_DirProd_multiplication_iso_set : |
1226 lemma (in group) FactGroup_DirProd_multiplication_iso_set : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
1235 assumes "group K" |
1227 assumes "group K" |
1236 and "H \<lhd> G" |
1228 and "H \<lhd> G" |
1237 and "N \<lhd> K" |
1229 and "N \<lhd> K" |
1238 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)" |
1230 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)" |
1239 |
1231 |
1259 qed |
1251 qed |
1260 ultimately show ?thesis |
1252 ultimately show ?thesis |
1261 unfolding iso_def hom_def bij_betw_def inj_on_def by simp |
1253 unfolding iso_def hom_def bij_betw_def inj_on_def by simp |
1262 qed |
1254 qed |
1263 |
1255 |
1264 corollary (in group) FactGroup_DirProd_multiplication_iso_1 : |
1256 corollary (in group) FactGroup_DirProd_multiplication_iso_1 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
1265 assumes "group K" |
1257 assumes "group K" |
1266 and "H \<lhd> G" |
1258 and "H \<lhd> G" |
1267 and "N \<lhd> K" |
1259 and "N \<lhd> K" |
1268 shows " ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)" |
1260 shows " ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)" |
1269 unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto |
1261 unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto |
1270 |
1262 |
1271 corollary (in group) FactGroup_DirProd_multiplication_iso_2 : |
1263 corollary (in group) FactGroup_DirProd_multiplication_iso_2 : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close> |
1272 assumes "group K" |
1264 assumes "group K" |
1273 and "H \<lhd> G" |
1265 and "H \<lhd> G" |
1274 and "N \<lhd> K" |
1266 and "N \<lhd> K" |
1275 shows "(G \<times>\<times> K Mod H \<times> N) \<cong> ((G Mod H) \<times>\<times> (K Mod N))" |
1267 shows "(G \<times>\<times> K Mod H \<times> N) \<cong> ((G Mod H) \<times>\<times> (K Mod N))" |
1276 using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms |
1268 using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms |