author | wenzelm |
Mon, 17 Sep 2007 16:36:41 +0200 | |
changeset 24612 | d1b315bdb8d7 |
parent 22931 | 11cc1ccad58e |
child 26199 | 04817a8802f2 |
permissions | -rw-r--r-- |
14884 | 1 |
(* Title: ZF/ex/Group.thy |
2 |
Id: $Id$ |
|
3 |
||
4 |
*) |
|
5 |
||
6 |
header {* Groups *} |
|
7 |
||
16417 | 8 |
theory Group imports Main begin |
14884 | 9 |
|
10 |
text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and |
|
11 |
Markus Wenzel.*} |
|
12 |
||
13 |
||
14 |
subsection {* Monoids *} |
|
15 |
||
16 |
(*First, we must simulate a record declaration: |
|
17 |
record monoid = |
|
18 |
carrier :: i |
|
14891 | 19 |
mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70) |
14884 | 20 |
one :: i ("\<one>\<index>") |
21 |
*) |
|
22 |
||
21233 | 23 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
24 |
carrier :: "i => i" where |
21233 | 25 |
"carrier(M) == fst(M)" |
14884 | 26 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
27 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
28 |
mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where |
21233 | 29 |
"mmult(M,x,y) == fst(snd(M)) ` <x,y>" |
14884 | 30 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
31 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
32 |
one :: "i => i" ("\<one>\<index>") where |
21233 | 33 |
"one(M) == fst(snd(snd(M)))" |
14884 | 34 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
35 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
36 |
update_carrier :: "[i,i] => i" where |
21233 | 37 |
"update_carrier(M,A) == <A,snd(M)>" |
14884 | 38 |
|
21233 | 39 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
40 |
m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where |
21233 | 41 |
"inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)" |
14884 | 42 |
|
43 |
locale monoid = struct G + |
|
44 |
assumes m_closed [intro, simp]: |
|
45 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)" |
|
46 |
and m_assoc: |
|
47 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> |
|
48 |
\<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
49 |
and one_closed [intro, simp]: "\<one> \<in> carrier(G)" |
|
50 |
and l_one [simp]: "x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x" |
|
51 |
and r_one [simp]: "x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x" |
|
52 |
||
53 |
text{*Simulating the record*} |
|
54 |
lemma carrier_eq [simp]: "carrier(<A,Z>) = A" |
|
55 |
by (simp add: carrier_def) |
|
56 |
||
57 |
lemma mult_eq [simp]: "mmult(<A,M,Z>, x, y) = M ` <x,y>" |
|
58 |
by (simp add: mmult_def) |
|
59 |
||
60 |
lemma one_eq [simp]: "one(<A,M,I,Z>) = I" |
|
61 |
by (simp add: one_def) |
|
62 |
||
63 |
lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>" |
|
64 |
by (simp add: update_carrier_def) |
|
65 |
||
66 |
lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B" |
|
22931 | 67 |
by (simp add: update_carrier_def) |
14884 | 68 |
|
69 |
lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)" |
|
22931 | 70 |
by (simp add: update_carrier_def mmult_def) |
14884 | 71 |
|
72 |
lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)" |
|
22931 | 73 |
by (simp add: update_carrier_def one_def) |
14884 | 74 |
|
75 |
||
76 |
lemma (in monoid) inv_unique: |
|
77 |
assumes eq: "y \<cdot> x = \<one>" "x \<cdot> y' = \<one>" |
|
78 |
and G: "x \<in> carrier(G)" "y \<in> carrier(G)" "y' \<in> carrier(G)" |
|
79 |
shows "y = y'" |
|
80 |
proof - |
|
81 |
from G eq have "y = y \<cdot> (x \<cdot> y')" by simp |
|
82 |
also from G have "... = (y \<cdot> x) \<cdot> y'" by (simp add: m_assoc) |
|
83 |
also from G eq have "... = y'" by simp |
|
84 |
finally show ?thesis . |
|
85 |
qed |
|
86 |
||
87 |
text {* |
|
88 |
A group is a monoid all of whose elements are invertible. |
|
89 |
*} |
|
90 |
||
91 |
locale group = monoid + |
|
92 |
assumes inv_ex: |
|
93 |
"\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>" |
|
94 |
||
22931 | 95 |
lemma (in group) is_group [simp]: "group(G)" by fact |
14884 | 96 |
|
97 |
theorem groupI: |
|
98 |
includes struct G |
|
99 |
assumes m_closed [simp]: |
|
100 |
"\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)" |
|
101 |
and one_closed [simp]: "\<one> \<in> carrier(G)" |
|
102 |
and m_assoc: |
|
103 |
"\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow> |
|
104 |
(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
105 |
and l_one [simp]: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x" |
|
106 |
and l_inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one>" |
|
107 |
shows "group(G)" |
|
108 |
proof - |
|
109 |
have l_cancel [simp]: |
|
110 |
"\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow> |
|
111 |
(x \<cdot> y = x \<cdot> z) <-> (y = z)" |
|
112 |
proof |
|
113 |
fix x y z |
|
114 |
assume G: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)" |
|
115 |
{ |
|
116 |
assume eq: "x \<cdot> y = x \<cdot> z" |
|
117 |
with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)" |
|
118 |
and l_inv: "x_inv \<cdot> x = \<one>" by fast |
|
119 |
from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z" |
|
120 |
by (simp add: m_assoc) |
|
121 |
with G show "y = z" by (simp add: l_inv) |
|
122 |
next |
|
123 |
assume eq: "y = z" |
|
124 |
with G show "x \<cdot> y = x \<cdot> z" by simp |
|
125 |
} |
|
126 |
qed |
|
127 |
have r_one: |
|
128 |
"\<And>x. x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x" |
|
129 |
proof - |
|
130 |
fix x |
|
131 |
assume x: "x \<in> carrier(G)" |
|
132 |
with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)" |
|
133 |
and l_inv: "x_inv \<cdot> x = \<one>" by fast |
|
134 |
from x xG have "x_inv \<cdot> (x \<cdot> \<one>) = x_inv \<cdot> x" |
|
135 |
by (simp add: m_assoc [symmetric] l_inv) |
|
136 |
with x xG show "x \<cdot> \<one> = x" by simp |
|
137 |
qed |
|
138 |
have inv_ex: |
|
139 |
"!!x. x \<in> carrier(G) ==> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>" |
|
140 |
proof - |
|
141 |
fix x |
|
142 |
assume x: "x \<in> carrier(G)" |
|
143 |
with l_inv_ex obtain y where y: "y \<in> carrier(G)" |
|
144 |
and l_inv: "y \<cdot> x = \<one>" by fast |
|
145 |
from x y have "y \<cdot> (x \<cdot> y) = y \<cdot> \<one>" |
|
146 |
by (simp add: m_assoc [symmetric] l_inv r_one) |
|
147 |
with x y have r_inv: "x \<cdot> y = \<one>" |
|
148 |
by simp |
|
149 |
from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>" |
|
150 |
by (fast intro: l_inv r_inv) |
|
151 |
qed |
|
152 |
show ?thesis |
|
153 |
by (blast intro: group.intro monoid.intro group_axioms.intro |
|
154 |
prems r_one inv_ex) |
|
155 |
qed |
|
156 |
||
157 |
lemma (in group) inv [simp]: |
|
158 |
"x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>" |
|
159 |
apply (frule inv_ex) |
|
160 |
apply (unfold Bex_def m_inv_def) |
|
161 |
apply (erule exE) |
|
162 |
apply (rule theI) |
|
163 |
apply (rule ex1I, assumption) |
|
164 |
apply (blast intro: inv_unique) |
|
165 |
done |
|
166 |
||
167 |
lemma (in group) inv_closed [intro!]: |
|
168 |
"x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G)" |
|
169 |
by simp |
|
170 |
||
171 |
lemma (in group) l_inv: |
|
172 |
"x \<in> carrier(G) \<Longrightarrow> inv x \<cdot> x = \<one>" |
|
173 |
by simp |
|
174 |
||
175 |
lemma (in group) r_inv: |
|
176 |
"x \<in> carrier(G) \<Longrightarrow> x \<cdot> inv x = \<one>" |
|
177 |
by simp |
|
178 |
||
179 |
||
180 |
subsection {* Cancellation Laws and Basic Properties *} |
|
181 |
||
182 |
lemma (in group) l_cancel [simp]: |
|
183 |
assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)" |
|
184 |
shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)" |
|
185 |
proof |
|
186 |
assume eq: "x \<cdot> y = x \<cdot> z" |
|
187 |
hence "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z" |
|
188 |
by (simp only: m_assoc inv_closed prems) |
|
189 |
thus "y = z" by simp |
|
190 |
next |
|
191 |
assume eq: "y = z" |
|
192 |
then show "x \<cdot> y = x \<cdot> z" by simp |
|
193 |
qed |
|
194 |
||
195 |
lemma (in group) r_cancel [simp]: |
|
196 |
assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)" |
|
197 |
shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)" |
|
198 |
proof |
|
199 |
assume eq: "y \<cdot> x = z \<cdot> x" |
|
200 |
then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)" |
|
201 |
by (simp only: m_assoc [symmetric] inv_closed prems) |
|
202 |
thus "y = z" by simp |
|
203 |
next |
|
204 |
assume eq: "y = z" |
|
205 |
thus "y \<cdot> x = z \<cdot> x" by simp |
|
206 |
qed |
|
207 |
||
208 |
lemma (in group) inv_comm: |
|
209 |
assumes inv: "x \<cdot> y = \<one>" |
|
210 |
and G: "x \<in> carrier(G)" "y \<in> carrier(G)" |
|
211 |
shows "y \<cdot> x = \<one>" |
|
212 |
proof - |
|
213 |
from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv) |
|
214 |
with G show ?thesis by (simp del: r_one add: m_assoc) |
|
215 |
qed |
|
216 |
||
217 |
lemma (in group) inv_equality: |
|
218 |
"\<lbrakk>y \<cdot> x = \<one>; x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv x = y" |
|
219 |
apply (simp add: m_inv_def) |
|
220 |
apply (rule the_equality) |
|
221 |
apply (simp add: inv_comm [of y x]) |
|
222 |
apply (rule r_cancel [THEN iffD1], auto) |
|
223 |
done |
|
224 |
||
225 |
lemma (in group) inv_one [simp]: |
|
226 |
"inv \<one> = \<one>" |
|
227 |
by (auto intro: inv_equality) |
|
228 |
||
229 |
lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x" |
|
230 |
by (auto intro: inv_equality) |
|
231 |
||
232 |
text{*This proof is by cancellation*} |
|
233 |
lemma (in group) inv_mult_group: |
|
234 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x" |
|
235 |
proof - |
|
236 |
assume G: "x \<in> carrier(G)" "y \<in> carrier(G)" |
|
237 |
then have "inv (x \<cdot> y) \<cdot> (x \<cdot> y) = (inv y \<cdot> inv x) \<cdot> (x \<cdot> y)" |
|
238 |
by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv) |
|
239 |
with G show ?thesis by (simp_all del: inv add: inv_closed) |
|
240 |
qed |
|
241 |
||
242 |
||
243 |
subsection {* Substructures *} |
|
244 |
||
245 |
locale subgroup = var H + struct G + |
|
246 |
assumes subset: "H \<subseteq> carrier(G)" |
|
247 |
and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H" |
|
248 |
and one_closed [simp]: "\<one> \<in> H" |
|
249 |
and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H" |
|
250 |
||
251 |
||
252 |
lemma (in subgroup) mem_carrier [simp]: |
|
253 |
"x \<in> H \<Longrightarrow> x \<in> carrier(G)" |
|
254 |
using subset by blast |
|
255 |
||
256 |
||
257 |
lemma subgroup_imp_subset: |
|
258 |
"subgroup(H,G) \<Longrightarrow> H \<subseteq> carrier(G)" |
|
259 |
by (rule subgroup.subset) |
|
260 |
||
261 |
lemma (in subgroup) group_axiomsI [intro]: |
|
262 |
includes group G |
|
263 |
shows "group_axioms (update_carrier(G,H))" |
|
264 |
by (force intro: group_axioms.intro l_inv r_inv) |
|
265 |
||
14891 | 266 |
lemma (in subgroup) is_group [intro]: |
14884 | 267 |
includes group G |
14891 | 268 |
shows "group (update_carrier(G,H))" |
14884 | 269 |
by (rule groupI) (auto intro: m_assoc l_inv mem_carrier) |
270 |
||
271 |
text {* |
|
272 |
Since @{term H} is nonempty, it contains some element @{term x}. Since |
|
273 |
it is closed under inverse, it contains @{text "inv x"}. Since |
|
274 |
it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}. |
|
275 |
*} |
|
276 |
||
277 |
text {* |
|
278 |
Since @{term H} is nonempty, it contains some element @{term x}. Since |
|
279 |
it is closed under inverse, it contains @{text "inv x"}. Since |
|
280 |
it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}. |
|
281 |
*} |
|
282 |
||
283 |
lemma (in group) one_in_subset: |
|
284 |
"\<lbrakk>H \<subseteq> carrier(G); H \<noteq> 0; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<cdot> b \<in> H\<rbrakk> |
|
285 |
\<Longrightarrow> \<one> \<in> H" |
|
286 |
by (force simp add: l_inv) |
|
287 |
||
288 |
text {* A characterization of subgroups: closed, non-empty subset. *} |
|
289 |
||
290 |
declare monoid.one_closed [simp] group.inv_closed [simp] |
|
291 |
monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] |
|
292 |
||
293 |
lemma subgroup_nonempty: |
|
294 |
"~ subgroup(0,G)" |
|
295 |
by (blast dest: subgroup.one_closed) |
|
296 |
||
297 |
||
298 |
subsection {* Direct Products *} |
|
299 |
||
21233 | 300 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
301 |
DirProdGroup :: "[i,i] => i" (infixr "\<Otimes>" 80) where |
14884 | 302 |
"G \<Otimes> H == <carrier(G) \<times> carrier(H), |
303 |
(\<lambda><<g,h>, <g', h'>> |
|
304 |
\<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)). |
|
305 |
<g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>), |
|
306 |
<\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>, 0>" |
|
307 |
||
308 |
lemma DirProdGroup_group: |
|
309 |
includes group G + group H |
|
310 |
shows "group (G \<Otimes> H)" |
|
22931 | 311 |
by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv |
14884 | 312 |
simp add: DirProdGroup_def) |
313 |
||
314 |
lemma carrier_DirProdGroup [simp]: |
|
315 |
"carrier (G \<Otimes> H) = carrier(G) \<times> carrier(H)" |
|
316 |
by (simp add: DirProdGroup_def) |
|
317 |
||
318 |
lemma one_DirProdGroup [simp]: |
|
319 |
"\<one>\<^bsub>G \<Otimes> H\<^esub> = <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>" |
|
320 |
by (simp add: DirProdGroup_def) |
|
321 |
||
322 |
lemma mult_DirProdGroup [simp]: |
|
323 |
"[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|] |
|
324 |
==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>" |
|
22931 | 325 |
by (simp add: DirProdGroup_def) |
14884 | 326 |
|
327 |
lemma inv_DirProdGroup [simp]: |
|
328 |
includes group G + group H |
|
329 |
assumes g: "g \<in> carrier(G)" |
|
330 |
and h: "h \<in> carrier(H)" |
|
331 |
shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>" |
|
332 |
apply (rule group.inv_equality [OF DirProdGroup_group]) |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
333 |
apply (simp_all add: prems group.l_inv) |
14884 | 334 |
done |
335 |
||
336 |
subsection {* Isomorphisms *} |
|
337 |
||
21233 | 338 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
339 |
hom :: "[i,i] => i" where |
14884 | 340 |
"hom(G,H) == |
341 |
{h \<in> carrier(G) -> carrier(H). |
|
342 |
(\<forall>x \<in> carrier(G). \<forall>y \<in> carrier(G). h ` (x \<cdot>\<^bsub>G\<^esub> y) = (h ` x) \<cdot>\<^bsub>H\<^esub> (h ` y))}" |
|
343 |
||
344 |
lemma hom_mult: |
|
345 |
"\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> |
|
346 |
\<Longrightarrow> h ` (x \<cdot>\<^bsub>G\<^esub> y) = h ` x \<cdot>\<^bsub>H\<^esub> h ` y" |
|
347 |
by (simp add: hom_def) |
|
348 |
||
349 |
lemma hom_closed: |
|
350 |
"\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(H)" |
|
351 |
by (auto simp add: hom_def) |
|
352 |
||
353 |
lemma (in group) hom_compose: |
|
354 |
"\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)" |
|
355 |
by (force simp add: hom_def comp_fun) |
|
356 |
||
357 |
lemma hom_is_fun: |
|
358 |
"h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)" |
|
359 |
by (simp add: hom_def) |
|
360 |
||
361 |
||
362 |
subsection {* Isomorphisms *} |
|
363 |
||
21233 | 364 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
365 |
iso :: "[i,i] => i" (infixr "\<cong>" 60) where |
14884 | 366 |
"G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))" |
367 |
||
368 |
lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G" |
|
22931 | 369 |
by (simp add: iso_def hom_def id_type id_bij) |
14884 | 370 |
|
371 |
||
372 |
lemma (in group) iso_sym: |
|
373 |
"h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G" |
|
374 |
apply (simp add: iso_def bij_converse_bij, clarify) |
|
375 |
apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)") |
|
376 |
prefer 2 apply (simp add: bij_converse_bij bij_is_fun) |
|
377 |
apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"] |
|
378 |
simp add: hom_def bij_is_inj right_inverse_bij); |
|
379 |
done |
|
380 |
||
381 |
lemma (in group) iso_trans: |
|
382 |
"\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I" |
|
22931 | 383 |
by (auto simp add: iso_def hom_compose comp_bij) |
14884 | 384 |
|
385 |
lemma DirProdGroup_commute_iso: |
|
386 |
includes group G + group H |
|
387 |
shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)" |
|
22931 | 388 |
by (auto simp add: iso_def hom_def inj_def surj_def bij_def) |
14884 | 389 |
|
390 |
lemma DirProdGroup_assoc_iso: |
|
391 |
includes group G + group H + group I |
|
392 |
shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>) |
|
393 |
\<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))" |
|
22931 | 394 |
by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) |
14884 | 395 |
|
396 |
text{*Basis for homomorphism proofs: we assume two groups @{term G} and |
|
397 |
@term{H}, with a homomorphism @{term h} between them*} |
|
398 |
locale group_hom = group G + group H + var h + |
|
399 |
assumes homh: "h \<in> hom(G,H)" |
|
400 |
notes hom_mult [simp] = hom_mult [OF homh] |
|
401 |
and hom_closed [simp] = hom_closed [OF homh] |
|
402 |
and hom_is_fun [simp] = hom_is_fun [OF homh] |
|
403 |
||
404 |
lemma (in group_hom) one_closed [simp]: |
|
405 |
"h ` \<one> \<in> carrier(H)" |
|
406 |
by simp |
|
407 |
||
408 |
lemma (in group_hom) hom_one [simp]: |
|
409 |
"h ` \<one> = \<one>\<^bsub>H\<^esub>" |
|
410 |
proof - |
|
411 |
have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)" |
|
412 |
by (simp add: hom_mult [symmetric] del: hom_mult) |
|
413 |
then show ?thesis by (simp del: r_one) |
|
414 |
qed |
|
415 |
||
416 |
lemma (in group_hom) inv_closed [simp]: |
|
417 |
"x \<in> carrier(G) \<Longrightarrow> h ` (inv x) \<in> carrier(H)" |
|
418 |
by simp |
|
419 |
||
420 |
lemma (in group_hom) hom_inv [simp]: |
|
421 |
"x \<in> carrier(G) \<Longrightarrow> h ` (inv x) = inv\<^bsub>H\<^esub> (h ` x)" |
|
422 |
proof - |
|
423 |
assume x: "x \<in> carrier(G)" |
|
424 |
then have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = \<one>\<^bsub>H\<^esub>" |
|
425 |
by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult) |
|
426 |
also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" |
|
427 |
by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult) |
|
428 |
finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" . |
|
429 |
with x show ?thesis by (simp del: inv add: is_group) |
|
430 |
qed |
|
431 |
||
432 |
subsection {* Commutative Structures *} |
|
433 |
||
434 |
text {* |
|
435 |
Naming convention: multiplicative structures that are commutative |
|
436 |
are called \emph{commutative}, additive structures are called |
|
437 |
\emph{Abelian}. |
|
438 |
*} |
|
439 |
||
440 |
subsection {* Definition *} |
|
441 |
||
442 |
locale comm_monoid = monoid + |
|
443 |
assumes m_comm: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x" |
|
444 |
||
445 |
lemma (in comm_monoid) m_lcomm: |
|
446 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow> |
|
447 |
x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
448 |
proof - |
|
449 |
assume xyz: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)" |
|
450 |
from xyz have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by (simp add: m_assoc) |
|
451 |
also from xyz have "... = (y \<cdot> x) \<cdot> z" by (simp add: m_comm) |
|
452 |
also from xyz have "... = y \<cdot> (x \<cdot> z)" by (simp add: m_assoc) |
|
453 |
finally show ?thesis . |
|
454 |
qed |
|
455 |
||
456 |
lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm |
|
457 |
||
458 |
locale comm_group = comm_monoid + group |
|
459 |
||
460 |
lemma (in comm_group) inv_mult: |
|
461 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y" |
|
462 |
by (simp add: m_ac inv_mult_group) |
|
463 |
||
464 |
||
465 |
lemma (in group) subgroup_self: "subgroup (carrier(G),G)" |
|
466 |
by (simp add: subgroup_def prems) |
|
467 |
||
468 |
lemma (in group) subgroup_imp_group: |
|
469 |
"subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))" |
|
14891 | 470 |
by (simp add: subgroup.is_group) |
14884 | 471 |
|
472 |
lemma (in group) subgroupI: |
|
473 |
assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0" |
|
474 |
and inv: "!!a. a \<in> H ==> inv a \<in> H" |
|
475 |
and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H" |
|
476 |
shows "subgroup(H,G)" |
|
477 |
proof (simp add: subgroup_def prems) |
|
478 |
show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems) |
|
479 |
qed |
|
480 |
||
481 |
||
482 |
subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *} |
|
483 |
||
21233 | 484 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
485 |
BijGroup :: "i=>i" where |
14884 | 486 |
"BijGroup(S) == |
487 |
<bij(S,S), |
|
488 |
\<lambda><g,f> \<in> bij(S,S) \<times> bij(S,S). g O f, |
|
489 |
id(S), 0>" |
|
490 |
||
491 |
||
492 |
subsection {*Bijections Form a Group *} |
|
493 |
||
494 |
theorem group_BijGroup: "group(BijGroup(S))" |
|
495 |
apply (simp add: BijGroup_def) |
|
496 |
apply (rule groupI) |
|
497 |
apply (simp_all add: id_bij comp_bij comp_assoc) |
|
498 |
apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel) |
|
499 |
apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij) |
|
500 |
done |
|
501 |
||
502 |
||
503 |
subsection{*Automorphisms Form a Group*} |
|
504 |
||
505 |
lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S); x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S" |
|
506 |
by (blast intro: apply_funtype bij_is_fun bij_converse_bij) |
|
507 |
||
508 |
lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)" |
|
509 |
apply (rule group.inv_equality) |
|
510 |
apply (rule group_BijGroup) |
|
511 |
apply (simp_all add: BijGroup_def bij_converse_bij |
|
512 |
left_comp_inverse [OF bij_is_inj]) |
|
513 |
done |
|
514 |
||
515 |
lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))" |
|
516 |
by (simp add: iso_def) |
|
517 |
||
518 |
||
21233 | 519 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
520 |
auto :: "i=>i" where |
14884 | 521 |
"auto(G) == iso(G,G)" |
522 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
523 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
524 |
AutoGroup :: "i=>i" where |
14884 | 525 |
"AutoGroup(G) == update_carrier(BijGroup(carrier(G)), auto(G))" |
526 |
||
527 |
||
528 |
lemma (in group) id_in_auto: "id(carrier(G)) \<in> auto(G)" |
|
529 |
by (simp add: iso_refl auto_def) |
|
530 |
||
531 |
lemma (in group) subgroup_auto: |
|
532 |
"subgroup (auto(G)) (BijGroup (carrier(G)))" |
|
533 |
proof (rule subgroup.intro) |
|
534 |
show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))" |
|
535 |
by (auto simp add: auto_def BijGroup_def iso_def) |
|
536 |
next |
|
537 |
fix x y |
|
538 |
assume "x \<in> auto(G)" "y \<in> auto(G)" |
|
539 |
thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)" |
|
540 |
by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun |
|
541 |
group.hom_compose comp_bij) |
|
542 |
next |
|
543 |
show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add: BijGroup_def id_in_auto) |
|
544 |
next |
|
545 |
fix x |
|
546 |
assume "x \<in> auto(G)" |
|
547 |
thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)" |
|
548 |
by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym) |
|
549 |
qed |
|
550 |
||
551 |
theorem (in group) AutoGroup: "group (AutoGroup(G))" |
|
14891 | 552 |
by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup) |
14884 | 553 |
|
554 |
||
555 |
||
556 |
subsection{*Cosets and Quotient Groups*} |
|
557 |
||
21233 | 558 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
559 |
r_coset :: "[i,i,i] => i" (infixl "#>\<index>" 60) where |
21233 | 560 |
"H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}" |
14884 | 561 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
562 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
563 |
l_coset :: "[i,i,i] => i" (infixl "<#\<index>" 60) where |
21233 | 564 |
"a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}" |
14884 | 565 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
566 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
567 |
RCOSETS :: "[i,i] => i" ("rcosets\<index> _" [81] 80) where |
21233 | 568 |
"rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}" |
14884 | 569 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
570 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
571 |
set_mult :: "[i,i,i] => i" (infixl "<#>\<index>" 60) where |
21233 | 572 |
"H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}" |
14884 | 573 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
574 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
575 |
SET_INV :: "[i,i] => i" ("set'_inv\<index> _" [81] 80) where |
21233 | 576 |
"set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}" |
14884 | 577 |
|
578 |
||
579 |
locale normal = subgroup + group + |
|
580 |
assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)" |
|
581 |
||
21233 | 582 |
notation |
583 |
normal (infixl "\<lhd>" 60) |
|
14884 | 584 |
|
585 |
||
586 |
subsection {*Basic Properties of Cosets*} |
|
587 |
||
588 |
lemma (in group) coset_mult_assoc: |
|
589 |
"\<lbrakk>M \<subseteq> carrier(G); g \<in> carrier(G); h \<in> carrier(G)\<rbrakk> |
|
590 |
\<Longrightarrow> (M #> g) #> h = M #> (g \<cdot> h)" |
|
591 |
by (force simp add: r_coset_def m_assoc) |
|
592 |
||
593 |
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier(G) \<Longrightarrow> M #> \<one> = M" |
|
594 |
by (force simp add: r_coset_def) |
|
595 |
||
596 |
lemma (in group) solve_equation: |
|
597 |
"\<lbrakk>subgroup(H,G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<cdot> x" |
|
598 |
apply (rule bexI [of _ "y \<cdot> (inv x)"]) |
|
599 |
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc |
|
600 |
subgroup.subset [THEN subsetD]) |
|
601 |
done |
|
602 |
||
603 |
lemma (in group) repr_independence: |
|
604 |
"\<lbrakk>y \<in> H #> x; x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> H #> x = H #> y" |
|
605 |
by (auto simp add: r_coset_def m_assoc [symmetric] |
|
606 |
subgroup.subset [THEN subsetD] |
|
607 |
subgroup.m_closed solve_equation) |
|
608 |
||
609 |
lemma (in group) coset_join2: |
|
610 |
"\<lbrakk>x \<in> carrier(G); subgroup(H,G); x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H" |
|
611 |
--{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*} |
|
612 |
by (force simp add: subgroup.m_closed r_coset_def solve_equation) |
|
613 |
||
614 |
lemma (in group) r_coset_subset_G: |
|
615 |
"\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier(G)" |
|
616 |
by (auto simp add: r_coset_def) |
|
617 |
||
618 |
lemma (in group) rcosI: |
|
619 |
"\<lbrakk>h \<in> H; H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h \<cdot> x \<in> H #> x" |
|
620 |
by (auto simp add: r_coset_def) |
|
621 |
||
622 |
lemma (in group) rcosetsI: |
|
623 |
"\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H" |
|
624 |
by (auto simp add: RCOSETS_def) |
|
625 |
||
626 |
||
627 |
text{*Really needed?*} |
|
628 |
lemma (in group) transpose_inv: |
|
629 |
"\<lbrakk>x \<cdot> y = z; x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> |
|
630 |
\<Longrightarrow> (inv x) \<cdot> z = y" |
|
631 |
by (force simp add: m_assoc [symmetric]) |
|
632 |
||
633 |
||
634 |
||
635 |
subsection {* Normal subgroups *} |
|
636 |
||
637 |
lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)" |
|
638 |
by (simp add: normal_def subgroup_def) |
|
639 |
||
640 |
lemma (in group) normalI: |
|
641 |
"subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G"; |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
642 |
by (simp add: normal_def normal_axioms_def) |
14884 | 643 |
|
644 |
lemma (in normal) inv_op_closed1: |
|
645 |
"\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H" |
|
646 |
apply (insert coset_eq) |
|
647 |
apply (auto simp add: l_coset_def r_coset_def) |
|
648 |
apply (drule bspec, assumption) |
|
649 |
apply (drule equalityD1 [THEN subsetD], blast, clarify) |
|
650 |
apply (simp add: m_assoc) |
|
651 |
apply (simp add: m_assoc [symmetric]) |
|
652 |
done |
|
653 |
||
654 |
lemma (in normal) inv_op_closed2: |
|
655 |
"\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H" |
|
656 |
apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H") |
|
657 |
apply simp |
|
658 |
apply (blast intro: inv_op_closed1) |
|
659 |
done |
|
660 |
||
661 |
text{*Alternative characterization of normal subgroups*} |
|
662 |
lemma (in group) normal_inv_iff: |
|
663 |
"(N \<lhd> G) <-> |
|
664 |
(subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))" |
|
665 |
(is "_ <-> ?rhs") |
|
666 |
proof |
|
667 |
assume N: "N \<lhd> G" |
|
668 |
show ?rhs |
|
669 |
by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) |
|
670 |
next |
|
671 |
assume ?rhs |
|
672 |
hence sg: "subgroup(N,G)" |
|
673 |
and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto |
|
674 |
hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset) |
|
675 |
show "N \<lhd> G" |
|
676 |
proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify) |
|
677 |
fix x |
|
678 |
assume x: "x \<in> carrier(G)" |
|
679 |
show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})" |
|
680 |
proof |
|
681 |
show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})" |
|
682 |
proof clarify |
|
683 |
fix n |
|
684 |
assume n: "n \<in> N" |
|
685 |
show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})" |
|
686 |
proof (rule UN_I) |
|
687 |
from closed [of "inv x"] |
|
688 |
show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n) |
|
689 |
show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}" |
|
690 |
by (simp add: x n m_assoc [symmetric] sb [THEN subsetD]) |
|
691 |
qed |
|
692 |
qed |
|
693 |
next |
|
694 |
show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})" |
|
695 |
proof clarify |
|
696 |
fix n |
|
697 |
assume n: "n \<in> N" |
|
698 |
show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})" |
|
699 |
proof (rule UN_I) |
|
700 |
show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed) |
|
701 |
show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}" |
|
702 |
by (simp add: x n m_assoc sb [THEN subsetD]) |
|
703 |
qed |
|
704 |
qed |
|
705 |
qed |
|
706 |
qed |
|
707 |
qed |
|
708 |
||
709 |
||
710 |
subsection{*More Properties of Cosets*} |
|
711 |
||
712 |
lemma (in group) l_coset_subset_G: |
|
713 |
"\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier(G)" |
|
714 |
by (auto simp add: l_coset_def subsetD) |
|
715 |
||
716 |
lemma (in group) l_coset_swap: |
|
717 |
"\<lbrakk>y \<in> x <# H; x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> x \<in> y <# H" |
|
718 |
proof (simp add: l_coset_def) |
|
719 |
assume "\<exists>h\<in>H. y = x \<cdot> h" |
|
720 |
and x: "x \<in> carrier(G)" |
|
721 |
and sb: "subgroup(H,G)" |
|
722 |
then obtain h' where h': "h' \<in> H & x \<cdot> h' = y" by blast |
|
723 |
show "\<exists>h\<in>H. x = y \<cdot> h" |
|
724 |
proof |
|
725 |
show "x = y \<cdot> inv h'" using h' x sb |
|
726 |
by (auto simp add: m_assoc subgroup.subset [THEN subsetD]) |
|
727 |
show "inv h' \<in> H" using h' sb |
|
728 |
by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed) |
|
729 |
qed |
|
730 |
qed |
|
731 |
||
732 |
lemma (in group) l_coset_carrier: |
|
733 |
"\<lbrakk>y \<in> x <# H; x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> y \<in> carrier(G)" |
|
734 |
by (auto simp add: l_coset_def m_assoc |
|
735 |
subgroup.subset [THEN subsetD] subgroup.m_closed) |
|
736 |
||
737 |
lemma (in group) l_repr_imp_subset: |
|
738 |
assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)" |
|
739 |
shows "y <# H \<subseteq> x <# H" |
|
740 |
proof - |
|
741 |
from y |
|
742 |
obtain h' where "h' \<in> H" "x \<cdot> h' = y" by (auto simp add: l_coset_def) |
|
743 |
thus ?thesis using x sb |
|
744 |
by (auto simp add: l_coset_def m_assoc |
|
745 |
subgroup.subset [THEN subsetD] subgroup.m_closed) |
|
746 |
qed |
|
747 |
||
748 |
lemma (in group) l_repr_independence: |
|
749 |
assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)" |
|
750 |
shows "x <# H = y <# H" |
|
751 |
proof |
|
752 |
show "x <# H \<subseteq> y <# H" |
|
753 |
by (rule l_repr_imp_subset, |
|
754 |
(blast intro: l_coset_swap l_coset_carrier y x sb)+) |
|
755 |
show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb]) |
|
756 |
qed |
|
757 |
||
758 |
lemma (in group) setmult_subset_G: |
|
759 |
"\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)" |
|
760 |
by (auto simp add: set_mult_def subsetD) |
|
761 |
||
762 |
lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H" |
|
763 |
apply (rule equalityI) |
|
764 |
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def) |
|
765 |
apply (rule_tac x = x in bexI) |
|
766 |
apply (rule bexI [of _ "\<one>"]) |
|
767 |
apply (auto simp add: subgroup.m_closed subgroup.one_closed |
|
768 |
r_one subgroup.subset [THEN subsetD]) |
|
769 |
done |
|
770 |
||
771 |
||
772 |
subsubsection {* Set of inverses of an @{text r_coset}. *} |
|
773 |
||
774 |
lemma (in normal) rcos_inv: |
|
775 |
assumes x: "x \<in> carrier(G)" |
|
776 |
shows "set_inv (H #> x) = H #> (inv x)" |
|
777 |
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI) |
|
778 |
fix h |
|
779 |
assume "h \<in> H" |
|
780 |
show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})" |
|
781 |
proof (rule UN_I) |
|
782 |
show "inv x \<cdot> inv h \<cdot> x \<in> H" |
|
783 |
by (simp add: inv_op_closed1 prems) |
|
784 |
show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}" |
|
785 |
by (simp add: prems m_assoc) |
|
786 |
qed |
|
787 |
next |
|
788 |
fix h |
|
789 |
assume "h \<in> H" |
|
790 |
show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})" |
|
791 |
proof (rule UN_I) |
|
792 |
show "x \<cdot> inv h \<cdot> inv x \<in> H" |
|
793 |
by (simp add: inv_op_closed2 prems) |
|
794 |
show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}" |
|
795 |
by (simp add: prems m_assoc [symmetric] inv_mult_group) |
|
796 |
qed |
|
797 |
qed |
|
798 |
||
799 |
||
800 |
||
801 |
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*} |
|
802 |
||
803 |
lemma (in group) setmult_rcos_assoc: |
|
804 |
"\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> |
|
805 |
\<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x" |
|
806 |
by (force simp add: r_coset_def set_mult_def m_assoc) |
|
807 |
||
808 |
lemma (in group) rcos_assoc_lcos: |
|
809 |
"\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> |
|
810 |
\<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)" |
|
811 |
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc) |
|
812 |
||
813 |
lemma (in normal) rcos_mult_step1: |
|
814 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> |
|
815 |
\<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" |
|
816 |
by (simp add: setmult_rcos_assoc subset |
|
817 |
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos) |
|
818 |
||
819 |
lemma (in normal) rcos_mult_step2: |
|
820 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> |
|
821 |
\<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y" |
|
822 |
by (insert coset_eq, simp add: normal_def) |
|
823 |
||
824 |
lemma (in normal) rcos_mult_step3: |
|
825 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> |
|
826 |
\<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)" |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
827 |
by (simp add: setmult_rcos_assoc coset_mult_assoc |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
828 |
subgroup_mult_id subset prems normal.axioms) |
14884 | 829 |
|
830 |
lemma (in normal) rcos_sum: |
|
831 |
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> |
|
832 |
\<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<cdot> y)" |
|
833 |
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3) |
|
834 |
||
835 |
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M" |
|
836 |
-- {* generalizes @{text subgroup_mult_id} *} |
|
837 |
by (auto simp add: RCOSETS_def subset |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
838 |
setmult_rcos_assoc subgroup_mult_id prems normal.axioms) |
14884 | 839 |
|
840 |
||
841 |
subsubsection{*Two distinct right cosets are disjoint*} |
|
842 |
||
21233 | 843 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
844 |
r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where |
21233 | 845 |
"rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}" |
14884 | 846 |
|
847 |
||
848 |
lemma (in subgroup) equiv_rcong: |
|
849 |
includes group G |
|
850 |
shows "equiv (carrier(G), rcong H)" |
|
851 |
proof (simp add: equiv_def, intro conjI) |
|
852 |
show "rcong H \<subseteq> carrier(G) \<times> carrier(G)" |
|
853 |
by (auto simp add: r_congruent_def) |
|
854 |
next |
|
855 |
show "refl (carrier(G), rcong H)" |
|
856 |
by (auto simp add: r_congruent_def refl_def) |
|
857 |
next |
|
858 |
show "sym (rcong H)" |
|
859 |
proof (simp add: r_congruent_def sym_def, clarify) |
|
860 |
fix x y |
|
861 |
assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" |
|
862 |
and "inv x \<cdot> y \<in> H" |
|
863 |
hence "inv (inv x \<cdot> y) \<in> H" by (simp add: m_inv_closed) |
|
864 |
thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group) |
|
865 |
qed |
|
866 |
next |
|
867 |
show "trans (rcong H)" |
|
868 |
proof (simp add: r_congruent_def trans_def, clarify) |
|
869 |
fix x y z |
|
870 |
assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)" |
|
871 |
and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H" |
|
872 |
hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp |
|
873 |
hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv) |
|
874 |
thus "inv x \<cdot> z \<in> H" by simp |
|
875 |
qed |
|
876 |
qed |
|
877 |
||
878 |
text{*Equivalence classes of @{text rcong} correspond to left cosets. |
|
879 |
Was there a mistake in the definitions? I'd have expected them to |
|
880 |
correspond to right cosets.*} |
|
881 |
lemma (in subgroup) l_coset_eq_rcong: |
|
882 |
includes group G |
|
883 |
assumes a: "a \<in> carrier(G)" |
|
884 |
shows "a <# H = (rcong H) `` {a}" |
|
885 |
by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a |
|
886 |
Collect_image_eq) |
|
887 |
||
888 |
||
889 |
lemma (in group) rcos_equation: |
|
890 |
includes subgroup H G |
|
891 |
shows |
|
892 |
"\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G); b \<in> carrier(G); |
|
893 |
h \<in> H; ha \<in> H; hb \<in> H\<rbrakk> |
|
894 |
\<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" |
|
895 |
apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp) |
|
896 |
apply (simp add: m_assoc transpose_inv) |
|
897 |
done |
|
898 |
||
899 |
||
900 |
lemma (in group) rcos_disjoint: |
|
901 |
includes subgroup H G |
|
902 |
shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" |
|
903 |
apply (simp add: RCOSETS_def r_coset_def) |
|
904 |
apply (blast intro: rcos_equation prems sym) |
|
905 |
done |
|
906 |
||
907 |
||
908 |
subsection {*Order of a Group and Lagrange's Theorem*} |
|
909 |
||
21233 | 910 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
911 |
order :: "i => i" where |
14884 | 912 |
"order(S) == |carrier(S)|" |
913 |
||
914 |
lemma (in group) rcos_self: |
|
915 |
includes subgroup |
|
916 |
shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" |
|
917 |
apply (simp add: r_coset_def) |
|
918 |
apply (rule_tac x="\<one>" in bexI, auto) |
|
919 |
done |
|
920 |
||
921 |
lemma (in group) rcosets_part_G: |
|
922 |
includes subgroup |
|
923 |
shows "\<Union>(rcosets H) = carrier(G)" |
|
924 |
apply (rule equalityI) |
|
925 |
apply (force simp add: RCOSETS_def r_coset_def) |
|
926 |
apply (auto simp add: RCOSETS_def intro: rcos_self prems) |
|
927 |
done |
|
928 |
||
929 |
lemma (in group) cosets_finite: |
|
930 |
"\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier(G); Finite (carrier(G))\<rbrakk> \<Longrightarrow> Finite(c)" |
|
931 |
apply (auto simp add: RCOSETS_def) |
|
932 |
apply (simp add: r_coset_subset_G [THEN subset_Finite]) |
|
933 |
done |
|
934 |
||
935 |
text{*More general than the HOL version, which also requires @{term G} to |
|
936 |
be finite.*} |
|
937 |
lemma (in group) card_cosets_equal: |
|
938 |
assumes H: "H \<subseteq> carrier(G)" |
|
939 |
shows "c \<in> rcosets H \<Longrightarrow> |c| = |H|" |
|
940 |
proof (simp add: RCOSETS_def, clarify) |
|
941 |
fix a |
|
942 |
assume a: "a \<in> carrier(G)" |
|
943 |
show "|H #> a| = |H|" |
|
944 |
proof (rule eqpollI [THEN cardinal_cong]) |
|
945 |
show "H #> a \<lesssim> H" |
|
946 |
proof (simp add: lepoll_def, intro exI) |
|
947 |
show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)" |
|
948 |
by (auto intro: lam_type |
|
949 |
simp add: inj_def r_coset_def m_assoc subsetD [OF H] a) |
|
950 |
qed |
|
951 |
show "H \<lesssim> H #> a" |
|
952 |
proof (simp add: lepoll_def, intro exI) |
|
953 |
show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)" |
|
954 |
by (auto intro: lam_type |
|
955 |
simp add: inj_def r_coset_def subsetD [OF H] a) |
|
956 |
qed |
|
957 |
qed |
|
958 |
qed |
|
959 |
||
960 |
||
961 |
lemma (in group) rcosets_subset_PowG: |
|
962 |
"subgroup(H,G) \<Longrightarrow> rcosets H \<subseteq> Pow(carrier(G))" |
|
963 |
apply (simp add: RCOSETS_def) |
|
964 |
apply (blast dest: r_coset_subset_G subgroup.subset) |
|
965 |
done |
|
966 |
||
967 |
theorem (in group) lagrange: |
|
968 |
"\<lbrakk>Finite(carrier(G)); subgroup(H,G)\<rbrakk> |
|
969 |
\<Longrightarrow> |rcosets H| #* |H| = order(G)" |
|
970 |
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric]) |
|
971 |
apply (subst mult_commute) |
|
972 |
apply (rule card_partition) |
|
973 |
apply (simp add: rcosets_subset_PowG [THEN subset_Finite]) |
|
974 |
apply (simp add: rcosets_part_G) |
|
975 |
apply (simp add: card_cosets_equal [OF subgroup.subset]) |
|
976 |
apply (simp add: rcos_disjoint) |
|
977 |
done |
|
978 |
||
979 |
||
980 |
subsection {*Quotient Groups: Factorization of a Group*} |
|
981 |
||
21233 | 982 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
983 |
FactGroup :: "[i,i] => i" (infixl "Mod" 65) where |
14884 | 984 |
--{*Actually defined for groups rather than monoids*} |
985 |
"G Mod H == |
|
21233 | 986 |
<rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>" |
14884 | 987 |
|
988 |
lemma (in normal) setmult_closed: |
|
989 |
"\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H" |
|
990 |
by (auto simp add: rcos_sum RCOSETS_def) |
|
991 |
||
992 |
lemma (in normal) setinv_closed: |
|
993 |
"K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H" |
|
994 |
by (auto simp add: rcos_inv RCOSETS_def) |
|
995 |
||
996 |
lemma (in normal) rcosets_assoc: |
|
997 |
"\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk> |
|
998 |
\<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)" |
|
999 |
by (auto simp add: RCOSETS_def rcos_sum m_assoc) |
|
1000 |
||
1001 |
lemma (in subgroup) subgroup_in_rcosets: |
|
1002 |
includes group G |
|
1003 |
shows "H \<in> rcosets H" |
|
1004 |
proof - |
|
1005 |
have "H #> \<one> = H" |
|
22931 | 1006 |
using _ `subgroup(H, G)` by (rule coset_join2) simp_all |
14884 | 1007 |
then show ?thesis |
1008 |
by (auto simp add: RCOSETS_def intro: sym) |
|
1009 |
qed |
|
1010 |
||
1011 |
lemma (in normal) rcosets_inv_mult_group_eq: |
|
1012 |
"M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H" |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset
|
1013 |
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms) |
14884 | 1014 |
|
1015 |
theorem (in normal) factorgroup_is_group: |
|
1016 |
"group (G Mod H)" |
|
1017 |
apply (simp add: FactGroup_def) |
|
14891 | 1018 |
apply (rule groupI) |
14884 | 1019 |
apply (simp add: setmult_closed) |
1020 |
apply (simp add: normal_imp_subgroup subgroup_in_rcosets) |
|
1021 |
apply (simp add: setmult_closed rcosets_assoc) |
|
1022 |
apply (simp add: normal_imp_subgroup |
|
1023 |
subgroup_in_rcosets rcosets_mult_eq) |
|
1024 |
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed) |
|
1025 |
done |
|
1026 |
||
1027 |
lemma (in normal) inv_FactGroup: |
|
1028 |
"X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X" |
|
1029 |
apply (rule group.inv_equality [OF factorgroup_is_group]) |
|
1030 |
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq) |
|
1031 |
done |
|
1032 |
||
1033 |
text{*The coset map is a homomorphism from @{term G} to the quotient group |
|
1034 |
@{term "G Mod H"}*} |
|
1035 |
lemma (in normal) r_coset_hom_Mod: |
|
1036 |
"(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)" |
|
1037 |
by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type) |
|
1038 |
||
1039 |
||
14891 | 1040 |
subsection{*The First Isomorphism Theorem*} |
1041 |
||
1042 |
text{*The quotient by the kernel of a homomorphism is isomorphic to the |
|
1043 |
range of that homomorphism.*} |
|
14884 | 1044 |
|
21233 | 1045 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
1046 |
kernel :: "[i,i,i] => i" where |
14884 | 1047 |
--{*the kernel of a homomorphism*} |
1048 |
"kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"; |
|
1049 |
||
1050 |
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)" |
|
1051 |
apply (rule subgroup.intro) |
|
1052 |
apply (auto simp add: kernel_def group.intro prems) |
|
1053 |
done |
|
1054 |
||
1055 |
text{*The kernel of a homomorphism is a normal subgroup*} |
|
1056 |
lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G" |
|
1057 |
apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems) |
|
1058 |
apply (simp add: kernel_def) |
|
1059 |
done |
|
1060 |
||
1061 |
lemma (in group_hom) FactGroup_nonempty: |
|
1062 |
assumes X: "X \<in> carrier (G Mod kernel(G,H,h))" |
|
1063 |
shows "X \<noteq> 0" |
|
1064 |
proof - |
|
1065 |
from X |
|
1066 |
obtain g where "g \<in> carrier(G)" |
|
1067 |
and "X = kernel(G,H,h) #> g" |
|
1068 |
by (auto simp add: FactGroup_def RCOSETS_def) |
|
1069 |
thus ?thesis |
|
1070 |
by (auto simp add: kernel_def r_coset_def image_def intro: hom_one) |
|
1071 |
qed |
|
1072 |
||
1073 |
||
1074 |
lemma (in group_hom) FactGroup_contents_mem: |
|
1075 |
assumes X: "X \<in> carrier (G Mod (kernel(G,H,h)))" |
|
1076 |
shows "contents (h``X) \<in> carrier(H)" |
|
1077 |
proof - |
|
1078 |
from X |
|
1079 |
obtain g where g: "g \<in> carrier(G)" |
|
1080 |
and "X = kernel(G,H,h) #> g" |
|
1081 |
by (auto simp add: FactGroup_def RCOSETS_def) |
|
1082 |
hence "h `` X = {h ` g}" |
|
1083 |
by (auto simp add: kernel_def r_coset_def image_UN |
|
1084 |
image_eq_UN [OF hom_is_fun] g) |
|
1085 |
thus ?thesis by (auto simp add: g) |
|
1086 |
qed |
|
1087 |
||
1088 |
lemma mult_FactGroup: |
|
1089 |
"[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] |
|
1090 |
==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'" |
|
1091 |
by (simp add: FactGroup_def) |
|
1092 |
||
1093 |
lemma (in normal) FactGroup_m_closed: |
|
1094 |
"[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] |
|
1095 |
==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)" |
|
1096 |
by (simp add: FactGroup_def setmult_closed) |
|
1097 |
||
1098 |
lemma (in group_hom) FactGroup_hom: |
|
1099 |
"(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (h``X)) |
|
1100 |
\<in> hom (G Mod (kernel(G,H,h)), H)" |
|
1101 |
proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI) |
|
1102 |
fix X and X' |
|
1103 |
assume X: "X \<in> carrier (G Mod kernel(G,H,h))" |
|
1104 |
and X': "X' \<in> carrier (G Mod kernel(G,H,h))" |
|
1105 |
then |
|
1106 |
obtain g and g' |
|
1107 |
where "g \<in> carrier(G)" and "g' \<in> carrier(G)" |
|
1108 |
and "X = kernel(G,H,h) #> g" and "X' = kernel(G,H,h) #> g'" |
|
1109 |
by (auto simp add: FactGroup_def RCOSETS_def) |
|
1110 |
hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" |
|
1111 |
and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)" |
|
1112 |
by (force simp add: kernel_def r_coset_def image_def)+ |
|
1113 |
hence "h `` (X <#> X') = {h ` g \<cdot>\<^bsub>H\<^esub> h ` g'}" using X X' |
|
1114 |
by (auto dest!: FactGroup_nonempty |
|
1115 |
simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN |
|
1116 |
subsetD [OF Xsub] subsetD [OF X'sub]) |
|
1117 |
thus "contents (h `` (X <#> X')) = contents (h `` X) \<cdot>\<^bsub>H\<^esub> contents (h `` X')" |
|
1118 |
by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty |
|
1119 |
X X' Xsub X'sub) |
|
1120 |
qed |
|
1121 |
||
1122 |
||
1123 |
text{*Lemma for the following injectivity result*} |
|
1124 |
lemma (in group_hom) FactGroup_subset: |
|
1125 |
"\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk> |
|
1126 |
\<Longrightarrow> kernel(G,H,h) #> g \<subseteq> kernel(G,H,h) #> g'" |
|
1127 |
apply (clarsimp simp add: kernel_def r_coset_def image_def) |
|
1128 |
apply (rename_tac y) |
|
1129 |
apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI) |
|
1130 |
apply (simp_all add: G.m_assoc) |
|
1131 |
done |
|
1132 |
||
1133 |
lemma (in group_hom) FactGroup_inj: |
|
1134 |
"(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X)) |
|
1135 |
\<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))" |
|
1136 |
proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify) |
|
1137 |
fix X and X' |
|
1138 |
assume X: "X \<in> carrier (G Mod kernel(G,H,h))" |
|
1139 |
and X': "X' \<in> carrier (G Mod kernel(G,H,h))" |
|
1140 |
then |
|
1141 |
obtain g and g' |
|
1142 |
where gX: "g \<in> carrier(G)" "g' \<in> carrier(G)" |
|
1143 |
"X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'" |
|
1144 |
by (auto simp add: FactGroup_def RCOSETS_def) |
|
1145 |
hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" |
|
1146 |
and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)" |
|
1147 |
by (force simp add: kernel_def r_coset_def image_def)+ |
|
1148 |
assume "contents (h `` X) = contents (h `` X')" |
|
1149 |
hence h: "h ` g = h ` g'" |
|
1150 |
by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty |
|
1151 |
X X' Xsub X'sub) |
|
1152 |
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) |
|
1153 |
qed |
|
1154 |
||
1155 |
||
1156 |
lemma (in group_hom) kernel_rcoset_subset: |
|
1157 |
assumes g: "g \<in> carrier(G)" |
|
1158 |
shows "kernel(G,H,h) #> g \<subseteq> carrier (G)" |
|
1159 |
by (auto simp add: g kernel_def r_coset_def) |
|
1160 |
||
1161 |
||
1162 |
||
1163 |
text{*If the homomorphism @{term h} is onto @{term H}, then so is the |
|
1164 |
homomorphism from the quotient group*} |
|
1165 |
lemma (in group_hom) FactGroup_surj: |
|
1166 |
assumes h: "h \<in> surj(carrier(G), carrier(H))" |
|
1167 |
shows "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X)) |
|
1168 |
\<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))" |
|
1169 |
proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify) |
|
1170 |
fix y |
|
1171 |
assume y: "y \<in> carrier(H)" |
|
1172 |
with h obtain g where g: "g \<in> carrier(G)" "h ` g = y" |
|
1173 |
by (auto simp add: surj_def) |
|
1174 |
hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}" |
|
1175 |
by (auto simp add: y kernel_def r_coset_def) |
|
1176 |
with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y" |
|
1177 |
--{*The witness is @{term "kernel(G,H,h) #> g"}*} |
|
1178 |
by (force simp add: FactGroup_def RCOSETS_def |
|
1179 |
image_eq_UN [OF hom_is_fun] kernel_rcoset_subset) |
|
1180 |
qed |
|
1181 |
||
1182 |
||
1183 |
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the |
|
1184 |
quotient group @{term "G Mod (kernel(G,H,h))"} is isomorphic to @{term H}.*} |
|
1185 |
theorem (in group_hom) FactGroup_iso: |
|
1186 |
"h \<in> surj(carrier(G), carrier(H)) |
|
1187 |
\<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h``X)) \<in> (G Mod (kernel(G,H,h))) \<cong> H" |
|
1188 |
by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj) |
|
1189 |
||
1190 |
end |