2 Title: HOL/Algebra/Group.thy
4 Author: Clemens Ballarin, started 4 February 2003
6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
11 theory Group imports FuncSet Lattice begin
14 section {* Monoids and Groups *}
17 Definitions follow \cite{Jacobson:1985}.
20 subsection {* Definitions *}
22 record 'a monoid = "'a partial_object" +
23 mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
24 one :: 'a ("\<one>\<index>")
26 constdefs (structure G)
27 m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
28 "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
30 Units :: "_ => 'a set"
31 --{*The set of invertible elements*}
32 "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
35 pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
38 nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
39 int_pow_def: "pow G a z ==
40 let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
41 in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
43 locale monoid = struct G +
44 assumes m_closed [intro, simp]:
45 "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
47 "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk>
48 \<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
49 and one_closed [intro, simp]: "\<one> \<in> carrier G"
50 and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x"
51 and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x"
56 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
57 and one_closed: "\<one> \<in> carrier G"
59 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
60 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
61 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
62 and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
64 by (fast intro!: monoid.intro intro: prems)
66 lemma (in monoid) Units_closed [dest]:
67 "x \<in> Units G ==> x \<in> carrier G"
68 by (unfold Units_def) fast
70 lemma (in monoid) inv_unique:
71 assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
72 and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
75 from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
76 also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
77 also from G eq have "... = y'" by simp
78 finally show ?thesis .
81 lemma (in monoid) Units_one_closed [intro, simp]:
82 "\<one> \<in> Units G"
83 by (unfold Units_def) auto
85 lemma (in monoid) Units_inv_closed [intro, simp]:
86 "x \<in> Units G ==> inv x \<in> carrier G"
87 apply (unfold Units_def m_inv_def, auto)
88 apply (rule theI2, fast)
89 apply (fast intro: inv_unique, fast)
92 lemma (in monoid) Units_l_inv:
93 "x \<in> Units G ==> inv x \<otimes> x = \<one>"
94 apply (unfold Units_def m_inv_def, auto)
95 apply (rule theI2, fast)
96 apply (fast intro: inv_unique, fast)
99 lemma (in monoid) Units_r_inv:
100 "x \<in> Units G ==> x \<otimes> inv x = \<one>"
101 apply (unfold Units_def m_inv_def, auto)
102 apply (rule theI2, fast)
103 apply (fast intro: inv_unique, fast)
106 lemma (in monoid) Units_inv_Units [intro, simp]:
107 "x \<in> Units G ==> inv x \<in> Units G"
109 assume x: "x \<in> Units G"
110 show "inv x \<in> Units G"
111 by (auto simp add: Units_def
112 intro: Units_l_inv Units_r_inv x Units_closed [OF x])
115 lemma (in monoid) Units_l_cancel [simp]:
116 "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
117 (x \<otimes> y = x \<otimes> z) = (y = z)"
119 assume eq: "x \<otimes> y = x \<otimes> z"
120 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
121 then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
122 by (simp add: m_assoc Units_closed)
123 with G show "y = z" by (simp add: Units_l_inv)
126 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
127 then show "x \<otimes> y = x \<otimes> z" by simp
130 lemma (in monoid) Units_inv_inv [simp]:
131 "x \<in> Units G ==> inv (inv x) = x"
133 assume x: "x \<in> Units G"
134 then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
135 by (simp add: Units_l_inv Units_r_inv)
136 with x show ?thesis by (simp add: Units_closed)
139 lemma (in monoid) inv_inj_on_Units:
140 "inj_on (m_inv G) (Units G)"
143 assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
144 then have "inv (inv x) = inv (inv y)" by simp
145 with G show "x = y" by simp
148 lemma (in monoid) Units_inv_comm:
149 assumes inv: "x \<otimes> y = \<one>"
150 and G: "x \<in> Units G" "y \<in> Units G"
151 shows "y \<otimes> x = \<one>"
153 from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
154 with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
159 lemma (in monoid) nat_pow_closed [intro, simp]:
160 "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
161 by (induct n) (simp_all add: nat_pow_def)
163 lemma (in monoid) nat_pow_0 [simp]:
164 "x (^) (0::nat) = \<one>"
165 by (simp add: nat_pow_def)
167 lemma (in monoid) nat_pow_Suc [simp]:
168 "x (^) (Suc n) = x (^) n \<otimes> x"
169 by (simp add: nat_pow_def)
171 lemma (in monoid) nat_pow_one [simp]:
172 "\<one> (^) (n::nat) = \<one>"
173 by (induct n) simp_all
175 lemma (in monoid) nat_pow_mult:
176 "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
177 by (induct m) (simp_all add: m_assoc [THEN sym])
179 lemma (in monoid) nat_pow_pow:
180 "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
181 by (induct m) (simp, simp add: nat_pow_mult add_commute)
184 A group is a monoid all of whose elements are invertible.
187 locale group = monoid +
188 assumes Units: "carrier G <= Units G"
191 lemma (in group) is_group: "group G"
192 by (rule group.intro [OF prems])
196 assumes m_closed [simp]:
197 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
198 and one_closed [simp]: "\<one> \<in> carrier G"
200 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
201 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
202 and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
203 and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
206 have l_cancel [simp]:
207 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
208 (x \<otimes> y = x \<otimes> z) = (y = z)"
211 assume eq: "x \<otimes> y = x \<otimes> z"
212 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
213 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
214 and l_inv: "x_inv \<otimes> x = \<one>" by fast
215 from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z"
216 by (simp add: m_assoc)
217 with G show "y = z" by (simp add: l_inv)
221 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
222 then show "x \<otimes> y = x \<otimes> z" by simp
225 "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
228 assume x: "x \<in> carrier G"
229 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
230 and l_inv: "x_inv \<otimes> x = \<one>" by fast
231 from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x"
232 by (simp add: m_assoc [symmetric] l_inv)
233 with x xG show "x \<otimes> \<one> = x" by simp
236 "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
239 assume x: "x \<in> carrier G"
240 with l_inv_ex obtain y where y: "y \<in> carrier G"
241 and l_inv: "y \<otimes> x = \<one>" by fast
242 from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>"
243 by (simp add: m_assoc [symmetric] l_inv r_one)
244 with x y have r_inv: "x \<otimes> y = \<one>"
246 from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
247 by (fast intro: l_inv r_inv)
249 then have carrier_subset_Units: "carrier G <= Units G"
250 by (unfold Units_def) fast
252 by (fast intro!: group.intro monoid.intro group_axioms.intro
253 carrier_subset_Units intro: prems r_one)
256 lemma (in monoid) monoid_groupI:
258 "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
260 by (rule groupI) (auto intro: m_assoc l_inv_ex)
262 lemma (in group) Units_eq [simp]:
263 "Units G = carrier G"
265 show "Units G <= carrier G" by fast
267 show "carrier G <= Units G" by (rule Units)
270 lemma (in group) inv_closed [intro, simp]:
271 "x \<in> carrier G ==> inv x \<in> carrier G"
272 using Units_inv_closed by simp
274 lemma (in group) l_inv [simp]:
275 "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
276 using Units_l_inv by simp
278 subsection {* Cancellation Laws and Basic Properties *}
280 lemma (in group) l_cancel [simp]:
281 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
282 (x \<otimes> y = x \<otimes> z) = (y = z)"
283 using Units_l_inv by simp
285 lemma (in group) r_inv [simp]:
286 "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
288 assume x: "x \<in> carrier G"
289 then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
290 by (simp add: m_assoc [symmetric] l_inv)
291 with x show ?thesis by (simp del: r_one)
294 lemma (in group) r_cancel [simp]:
295 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
296 (y \<otimes> x = z \<otimes> x) = (y = z)"
298 assume eq: "y \<otimes> x = z \<otimes> x"
299 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
300 then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
301 by (simp add: m_assoc [symmetric] del: r_inv)
302 with G show "y = z" by simp
305 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
306 then show "y \<otimes> x = z \<otimes> x" by simp
309 lemma (in group) inv_one [simp]:
310 "inv \<one> = \<one>"
312 have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
313 moreover have "... = \<one>" by simp
314 finally show ?thesis .
317 lemma (in group) inv_inv [simp]:
318 "x \<in> carrier G ==> inv (inv x) = x"
319 using Units_inv_inv by simp
321 lemma (in group) inv_inj:
322 "inj_on (m_inv G) (carrier G)"
323 using inv_inj_on_Units by simp
325 lemma (in group) inv_mult_group:
326 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
328 assume G: "x \<in> carrier G" "y \<in> carrier G"
329 then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
330 by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
331 with G show ?thesis by (simp del: l_inv)
334 lemma (in group) inv_comm:
335 "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
336 by (rule Units_inv_comm) auto
338 lemma (in group) inv_equality:
339 "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
340 apply (simp add: m_inv_def)
341 apply (rule the_equality)
342 apply (simp add: inv_comm [of y x])
343 apply (rule r_cancel [THEN iffD1], auto)
348 lemma (in group) int_pow_def2:
349 "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
350 by (simp add: int_pow_def nat_pow_def Let_def)
352 lemma (in group) int_pow_0 [simp]:
353 "x (^) (0::int) = \<one>"
354 by (simp add: int_pow_def2)
356 lemma (in group) int_pow_one [simp]:
357 "\<one> (^) (z::int) = \<one>"
358 by (simp add: int_pow_def2)
360 subsection {* Subgroups *}
362 locale subgroup = var H + struct G +
363 assumes subset: "H \<subseteq> carrier G"
364 and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
365 and one_closed [simp]: "\<one> \<in> H"
366 and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
368 declare (in subgroup) group.intro [intro]
370 lemma (in subgroup) mem_carrier [simp]:
371 "x \<in> H \<Longrightarrow> x \<in> carrier G"
372 using subset by blast
374 lemma subgroup_imp_subset:
375 "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
376 by (rule subgroup.subset)
378 lemma (in subgroup) subgroup_is_group [intro]:
380 shows "group (G\<lparr>carrier := H\<rparr>)"
381 by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
384 Since @{term H} is nonempty, it contains some element @{term x}. Since
385 it is closed under inverse, it contains @{text "inv x"}. Since
386 it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
389 lemma (in group) one_in_subset:
390 "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
392 by (force simp add: l_inv)
394 text {* A characterization of subgroups: closed, non-empty subset. *}
396 lemma (in group) subgroupI:
397 assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
398 and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H"
399 and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
401 proof (simp add: subgroup_def prems)
402 show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
405 declare monoid.one_closed [iff] group.inv_closed [simp]
406 monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
408 lemma subgroup_nonempty:
410 by (blast dest: subgroup.one_closed)
412 lemma (in subgroup) finite_imp_card_positive:
413 "finite (carrier G) ==> 0 < card H"
414 proof (rule classical)
415 assume "finite (carrier G)" "~ 0 < card H"
416 then have "finite H" by (blast intro: finite_subset [OF subset])
417 with prems have "subgroup {} G" by simp
418 with subgroup_nonempty show ?thesis by contradiction
422 lemma (in monoid) Units_subgroup:
423 "subgroup (Units G) G"
426 subsection {* Direct Products *}
429 DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80)
430 "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
431 mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
432 one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
434 lemma DirProd_monoid:
435 includes monoid G + monoid H
436 shows "monoid (G \<times>\<times> H)"
439 show ?thesis by (unfold monoid_def DirProd_def, auto)
443 text{*Does not use the previous result because it's easier just to use auto.*}
445 includes group G + group H
446 shows "group (G \<times>\<times> H)"
448 (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
449 simp add: DirProd_def)
451 lemma carrier_DirProd [simp]:
452 "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
453 by (simp add: DirProd_def)
455 lemma one_DirProd [simp]:
456 "\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
457 by (simp add: DirProd_def)
459 lemma mult_DirProd [simp]:
460 "(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
461 by (simp add: DirProd_def)
463 lemma inv_DirProd [simp]:
464 includes group G + group H
465 assumes g: "g \<in> carrier G"
466 and h: "h \<in> carrier H"
467 shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
468 apply (rule group.inv_equality [OF DirProd_group])
469 apply (simp_all add: prems group_def group.l_inv)
472 text{*This alternative proof of the previous result demonstrates interpret.
473 It uses @{text Prod.inv_equality} (available after @{text interpret})
474 instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
476 includes group G + group H
477 assumes g: "g \<in> carrier G"
478 and h: "h \<in> carrier H"
479 shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
481 interpret Prod: group ["G \<times>\<times> H"]
482 by (auto intro: DirProd_group group.intro group.axioms prems)
483 show ?thesis by (simp add: Prod.inv_equality g h)
487 subsection {* Homomorphisms and Isomorphisms *}
489 constdefs (structure G and H)
490 hom :: "_ => _ => ('a => 'b) set"
492 {h. h \<in> carrier G -> carrier H &
493 (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
496 "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
497 ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
498 by (simp add: hom_def)
501 "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
502 by (auto simp add: hom_def funcset_mem)
504 lemma (in group) hom_compose:
505 "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
506 apply (auto simp add: hom_def funcset_compose)
507 apply (simp add: compose_def funcset_mem)
511 subsection {* Isomorphisms *}
514 iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
515 "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
517 lemma iso_refl: "(%x. x) \<in> G \<cong> G"
518 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
520 lemma (in group) iso_sym:
521 "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
522 apply (simp add: iso_def bij_betw_Inv)
523 apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
524 prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
525 apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
528 lemma (in group) iso_trans:
529 "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
530 by (auto simp add: iso_def hom_compose bij_betw_compose)
532 lemma DirProd_commute_iso:
533 shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
534 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
536 lemma DirProd_assoc_iso:
537 shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
538 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
541 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
542 @{term H}, with a homomorphism @{term h} between them*}
543 locale group_hom = group G + group H + var h +
544 assumes homh: "h \<in> hom G H"
545 notes hom_mult [simp] = hom_mult [OF homh]
546 and hom_closed [simp] = hom_closed [OF homh]
548 lemma (in group_hom) one_closed [simp]:
549 "h \<one> \<in> carrier H"
552 lemma (in group_hom) hom_one [simp]:
553 "h \<one> = \<one>\<^bsub>H\<^esub>"
555 have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
556 by (simp add: hom_mult [symmetric] del: hom_mult)
557 then show ?thesis by (simp del: r_one)
560 lemma (in group_hom) inv_closed [simp]:
561 "x \<in> carrier G ==> h (inv x) \<in> carrier H"
564 lemma (in group_hom) hom_inv [simp]:
565 "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
567 assume x: "x \<in> carrier G"
568 then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
569 by (simp add: hom_mult [symmetric] del: hom_mult)
570 also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
571 by (simp add: hom_mult [symmetric] del: hom_mult)
572 finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
573 with x show ?thesis by (simp del: H.r_inv)
576 subsection {* Commutative Structures *}
579 Naming convention: multiplicative structures that are commutative
580 are called \emph{commutative}, additive structures are called
584 subsection {* Definition *}
586 locale comm_monoid = monoid +
587 assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
589 lemma (in comm_monoid) m_lcomm:
590 "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow>
591 x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
593 assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
594 from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
595 also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
596 also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
597 finally show ?thesis .
600 lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
605 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
606 and one_closed: "\<one> \<in> carrier G"
608 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
609 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
610 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
612 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
613 shows "comm_monoid G"
615 by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
616 intro: prems simp: m_closed one_closed m_comm)
618 lemma (in monoid) monoid_comm_monoidI:
620 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
621 shows "comm_monoid G"
622 by (rule comm_monoidI) (auto intro: m_assoc m_comm)
624 (*lemma (in comm_monoid) r_one [simp]:
625 "x \<in> carrier G ==> x \<otimes> \<one> = x"
627 assume G: "x \<in> carrier G"
628 then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
629 also from G have "... = x" by simp
630 finally show ?thesis .
633 lemma (in comm_monoid) nat_pow_distr:
634 "[| x \<in> carrier G; y \<in> carrier G |] ==>
635 (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
636 by (induct n) (simp, simp add: m_ac)
638 locale comm_group = comm_monoid + group
640 lemma (in group) group_comm_groupI:
641 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
642 x \<otimes> y = y \<otimes> x"
644 by (fast intro: comm_group.intro comm_monoid_axioms.intro
650 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
651 and one_closed: "\<one> \<in> carrier G"
653 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
654 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
656 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
657 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
658 and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
660 by (fast intro: group.group_comm_groupI groupI prems)
662 lemma (in comm_group) inv_mult:
663 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
664 by (simp add: m_ac inv_mult_group)
666 subsection {* Lattice of subgroups of a group *}
668 text_raw {* \label{sec:subgroup-lattice} *}
670 theorem (in group) subgroups_partial_order:
671 "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
672 by (rule partial_order.intro) simp_all
674 lemma (in group) subgroup_self:
675 "subgroup (carrier G) G"
676 by (rule subgroupI) auto
678 lemma (in group) subgroup_imp_group:
679 "subgroup H G ==> group (G(| carrier := H |))"
680 using subgroup.subgroup_is_group [OF _ group.intro] .
682 lemma (in group) is_monoid [intro, simp]:
684 by (auto intro: monoid.intro m_assoc)
686 lemma (in group) subgroup_inv_equality:
687 "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
688 apply (rule_tac inv_equality [THEN sym])
689 apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
690 apply (rule subsetD [OF subgroup.subset], assumption+)
691 apply (rule subsetD [OF subgroup.subset], assumption)
692 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
695 theorem (in group) subgroups_Inter:
696 assumes subgr: "(!!H. H \<in> A ==> subgroup H G)"
697 and not_empty: "A ~= {}"
698 shows "subgroup (\<Inter>A) G"
699 proof (rule subgroupI)
700 from subgr [THEN subgroup.subset] and not_empty
701 show "\<Inter>A \<subseteq> carrier G" by blast
703 from subgr [THEN subgroup.one_closed]
704 show "\<Inter>A ~= {}" by blast
706 fix x assume "x \<in> \<Inter>A"
707 with subgr [THEN subgroup.m_inv_closed]
708 show "inv x \<in> \<Inter>A" by blast
710 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A"
711 with subgr [THEN subgroup.m_closed]
712 show "x \<otimes> y \<in> \<Inter>A" by blast
715 theorem (in group) subgroups_complete_lattice:
716 "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
717 (is "complete_lattice ?L")
718 proof (rule partial_order.complete_lattice_criterion1)
719 show "partial_order ?L" by (rule subgroups_partial_order)
721 have "greatest ?L (carrier G) (carrier ?L)"
722 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
723 then show "\<exists>G. greatest ?L G (carrier ?L)" ..
726 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
727 then have Int_subgroup: "subgroup (\<Inter>A) G"
728 by (fastsimp intro: subgroups_Inter)
729 have "greatest ?L (\<Inter>A) (Lower ?L A)"
730 (is "greatest ?L ?Int _")
731 proof (rule greatest_LowerI)
733 assume H: "H \<in> A"
734 with L have subgroupH: "subgroup H G" by auto
735 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
736 by (rule subgroup_imp_group)
737 from groupH have monoidH: "monoid ?H"
738 by (rule group.is_monoid)
739 from H have Int_subset: "?Int \<subseteq> H" by fastsimp
740 then show "le ?L ?Int H" by simp
743 assume H: "H \<in> Lower ?L A"
744 with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest)
746 show "A \<subseteq> carrier ?L" by (rule L)
748 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
750 then show "\<exists>I. greatest ?L I (Lower ?L A)" ..