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