src/HOL/Algebra/AbelCoset.thy
 author wenzelm Sun Mar 21 16:51:37 2010 +0100 (2010-03-21) changeset 35848 5443079512ea parent 35847 19f1f7066917 child 35849 b5522b51cb1e permissions -rw-r--r--
slightly more uniform definitions -- eliminated old-style meta-equality;
1 (*
2   Title:     HOL/Algebra/AbelCoset.thy
3   Author:    Stephan Hohe, TU Muenchen
4 *)
6 theory AbelCoset
7 imports Coset Ring
8 begin
11 subsection {* More Lifting from Groups to Abelian Groups *}
13 subsubsection {* Definitions *}
15 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
16   up with better syntax here *}
18 no_notation Plus (infixr "<+>" 65)
20 definition
21   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
22   where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
24 definition
25   a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
26   where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
28 definition
29   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _"  80)
30   where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
32 definition
33   set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
34   where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
36 definition
37   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _"  80)
38   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
40 definition
41   a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
42   where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
44 definition
45   A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
46     --{*Actually defined for groups rather than monoids*}
47   where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
49 definition
50   a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
51     --{*the kernel of a homomorphism (additive)*}
52   where "a_kernel G H h =
53     kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
54       \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
56 locale abelian_group_hom = G: abelian_group G + H: abelian_group H
57     for G (structure) and H (structure) +
58   fixes h
59   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
60                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
62 lemmas a_r_coset_defs =
63   a_r_coset_def r_coset_def
65 lemma a_r_coset_def':
66   fixes G (structure)
67   shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
68 unfolding a_r_coset_defs
69 by simp
71 lemmas a_l_coset_defs =
72   a_l_coset_def l_coset_def
74 lemma a_l_coset_def':
75   fixes G (structure)
76   shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
77 unfolding a_l_coset_defs
78 by simp
80 lemmas A_RCOSETS_defs =
81   A_RCOSETS_def RCOSETS_def
83 lemma A_RCOSETS_def':
84   fixes G (structure)
85   shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
86 unfolding A_RCOSETS_defs
87 by (fold a_r_coset_def, simp)
89 lemmas set_add_defs =
93   fixes G (structure)
94   shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
96 by simp
98 lemmas A_SET_INV_defs =
99   A_SET_INV_def SET_INV_def
101 lemma A_SET_INV_def':
102   fixes G (structure)
103   shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
104 unfolding A_SET_INV_defs
105 by (fold a_inv_def)
108 subsubsection {* Cosets *}
110 lemma (in abelian_group) a_coset_add_assoc:
111      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
112       ==> (M +> g) +> h = M +> (g \<oplus> h)"
113 by (rule group.coset_mult_assoc [OF a_group,
114     folded a_r_coset_def, simplified monoid_record_simps])
116 lemma (in abelian_group) a_coset_add_zero [simp]:
117   "M \<subseteq> carrier G ==> M +> \<zero> = M"
118 by (rule group.coset_mult_one [OF a_group,
119     folded a_r_coset_def, simplified monoid_record_simps])
121 lemma (in abelian_group) a_coset_add_inv1:
122      "[| M +> (x \<oplus> (\<ominus> y)) = M;  x \<in> carrier G ; y \<in> carrier G;
123          M \<subseteq> carrier G |] ==> M +> x = M +> y"
124 by (rule group.coset_mult_inv1 [OF a_group,
125     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
127 lemma (in abelian_group) a_coset_add_inv2:
128      "[| M +> x = M +> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
129       ==> M +> (x \<oplus> (\<ominus> y)) = M"
130 by (rule group.coset_mult_inv2 [OF a_group,
131     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
133 lemma (in abelian_group) a_coset_join1:
134      "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
135 by (rule group.coset_join1 [OF a_group,
136     folded a_r_coset_def, simplified monoid_record_simps])
138 lemma (in abelian_group) a_solve_equation:
139     "\<lbrakk>subgroup H (|carrier = carrier G, mult = add G, one = zero G|); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
140 by (rule group.solve_equation [OF a_group,
141     folded a_r_coset_def, simplified monoid_record_simps])
143 lemma (in abelian_group) a_repr_independence:
144      "\<lbrakk>y \<in> H +> x;  x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<rbrakk> \<Longrightarrow> H +> x = H +> y"
145 by (rule group.repr_independence [OF a_group,
146     folded a_r_coset_def, simplified monoid_record_simps])
148 lemma (in abelian_group) a_coset_join2:
149      "\<lbrakk>x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>; x\<in>H\<rbrakk> \<Longrightarrow> H +> x = H"
150 by (rule group.coset_join2 [OF a_group,
151     folded a_r_coset_def, simplified monoid_record_simps])
153 lemma (in abelian_monoid) a_r_coset_subset_G:
154      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G"
155 by (rule monoid.r_coset_subset_G [OF a_monoid,
156     folded a_r_coset_def, simplified monoid_record_simps])
158 lemma (in abelian_group) a_rcosI:
159      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x"
160 by (rule group.rcosI [OF a_group,
161     folded a_r_coset_def, simplified monoid_record_simps])
163 lemma (in abelian_group) a_rcosetsI:
164      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H"
165 by (rule group.rcosetsI [OF a_group,
166     folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
168 text{*Really needed?*}
169 lemma (in abelian_group) a_transpose_inv:
170      "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
171       ==> (\<ominus> x) \<oplus> z = y"
172 by (rule group.transpose_inv [OF a_group,
173     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
175 (*
176 --"duplicate"
177 lemma (in abelian_group) a_rcos_self:
178      "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
179 by (rule group.rcos_self [OF a_group,
180     folded a_r_coset_def, simplified monoid_record_simps])
181 *)
184 subsubsection {* Subgroups *}
186 locale additive_subgroup =
187   fixes H and G (structure)
188   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
191   shows "additive_subgroup H G"
192 by (rule additive_subgroup_axioms)
195   fixes G (structure)
196   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
197   shows "additive_subgroup H G"
198 by (rule additive_subgroup.intro) (rule a_subgroup)
200 lemma (in additive_subgroup) a_subset:
201      "H \<subseteq> carrier G"
202 by (rule subgroup.subset[OF a_subgroup,
203     simplified monoid_record_simps])
205 lemma (in additive_subgroup) a_closed [intro, simp]:
206      "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H"
207 by (rule subgroup.m_closed[OF a_subgroup,
208     simplified monoid_record_simps])
210 lemma (in additive_subgroup) zero_closed [simp]:
211      "\<zero> \<in> H"
212 by (rule subgroup.one_closed[OF a_subgroup,
213     simplified monoid_record_simps])
215 lemma (in additive_subgroup) a_inv_closed [intro,simp]:
216      "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
217 by (rule subgroup.m_inv_closed[OF a_subgroup,
218     folded a_inv_def, simplified monoid_record_simps])
221 subsubsection {* Additive subgroups are normal *}
223 text {* Every subgroup of an @{text "abelian_group"} is normal *}
225 locale abelian_subgroup = additive_subgroup + abelian_group G +
226   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
228 lemma (in abelian_subgroup) is_abelian_subgroup:
229   shows "abelian_subgroup H G"
230 by (rule abelian_subgroup_axioms)
232 lemma abelian_subgroupI:
233   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
234       and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x"
235   shows "abelian_subgroup H G"
236 proof -
237   interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
238   by (rule a_normal)
240   show "abelian_subgroup H G"
241   proof qed (simp add: a_comm)
242 qed
244 lemma abelian_subgroupI2:
245   fixes G (structure)
246   assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
247       and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
248   shows "abelian_subgroup H G"
249 proof -
250   interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
251   by (rule a_comm_group)
252   interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
253   by (rule a_subgroup)
255   show "abelian_subgroup H G"
256   apply unfold_locales
257   proof (simp add: r_coset_def l_coset_def, clarsimp)
258     fix x
259     assume xcarr: "x \<in> carrier G"
260     from a_subgroup
261         have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
262     from xcarr Hcarr
263         show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
264         using m_comm[simplified]
265         by fast
266   qed
267 qed
269 lemma abelian_subgroupI3:
270   fixes G (structure)
271   assumes asg: "additive_subgroup H G"
272       and ag: "abelian_group G"
273   shows "abelian_subgroup H G"
274 apply (rule abelian_subgroupI2)
275  apply (rule abelian_group.a_comm_group[OF ag])
276 apply (rule additive_subgroup.a_subgroup[OF asg])
277 done
279 lemma (in abelian_subgroup) a_coset_eq:
280      "(\<forall>x \<in> carrier G. H +> x = x <+ H)"
281 by (rule normal.coset_eq[OF a_normal,
282     folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
284 lemma (in abelian_subgroup) a_inv_op_closed1:
285   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H"
286 by (rule normal.inv_op_closed1 [OF a_normal,
287     folded a_inv_def, simplified monoid_record_simps])
289 lemma (in abelian_subgroup) a_inv_op_closed2:
290   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H"
291 by (rule normal.inv_op_closed2 [OF a_normal,
292     folded a_inv_def, simplified monoid_record_simps])
294 text{*Alternative characterization of normal subgroups*}
295 lemma (in abelian_group) a_normal_inv_iff:
296      "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) =
297       (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
298       (is "_ = ?rhs")
299 by (rule group.normal_inv_iff [OF a_group,
300     folded a_inv_def, simplified monoid_record_simps])
302 lemma (in abelian_group) a_lcos_m_assoc:
303      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
304       ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
305 by (rule group.lcos_m_assoc [OF a_group,
306     folded a_l_coset_def, simplified monoid_record_simps])
308 lemma (in abelian_group) a_lcos_mult_one:
309      "M \<subseteq> carrier G ==> \<zero> <+ M = M"
310 by (rule group.lcos_mult_one [OF a_group,
311     folded a_l_coset_def, simplified monoid_record_simps])
314 lemma (in abelian_group) a_l_coset_subset_G:
315      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
316 by (rule group.l_coset_subset_G [OF a_group,
317     folded a_l_coset_def, simplified monoid_record_simps])
320 lemma (in abelian_group) a_l_coset_swap:
321      "\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
322 by (rule group.l_coset_swap [OF a_group,
323     folded a_l_coset_def, simplified monoid_record_simps])
325 lemma (in abelian_group) a_l_coset_carrier:
326      "[| y \<in> x <+ H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> y \<in> carrier G"
327 by (rule group.l_coset_carrier [OF a_group,
328     folded a_l_coset_def, simplified monoid_record_simps])
330 lemma (in abelian_group) a_l_repr_imp_subset:
331   assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
332   shows "y <+ H \<subseteq> x <+ H"
333 apply (rule group.l_repr_imp_subset [OF a_group,
334     folded a_l_coset_def, simplified monoid_record_simps])
335 apply (rule y)
336 apply (rule x)
337 apply (rule sb)
338 done
340 lemma (in abelian_group) a_l_repr_independence:
341   assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
342   shows "x <+ H = y <+ H"
343 apply (rule group.l_repr_independence [OF a_group,
344     folded a_l_coset_def, simplified monoid_record_simps])
345 apply (rule y)
346 apply (rule x)
347 apply (rule sb)
348 done
350 lemma (in abelian_group) setadd_subset_G:
351      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
352 by (rule group.setmult_subset_G [OF a_group,
353     folded set_add_def, simplified monoid_record_simps])
355 lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
356 by (rule group.subgroup_mult_id [OF a_group,
357     folded set_add_def, simplified monoid_record_simps])
359 lemma (in abelian_subgroup) a_rcos_inv:
360   assumes x:     "x \<in> carrier G"
361   shows "a_set_inv (H +> x) = H +> (\<ominus> x)"
362 by (rule normal.rcos_inv [OF a_normal,
363   folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
365 lemma (in abelian_group) a_setmult_rcos_assoc:
366      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
367       \<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x"
368 by (rule group.setmult_rcos_assoc [OF a_group,
369     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
371 lemma (in abelian_group) a_rcos_assoc_lcos:
372      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
373       \<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)"
374 by (rule group.rcos_assoc_lcos [OF a_group,
375      folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
377 lemma (in abelian_subgroup) a_rcos_sum:
378      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
379       \<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)"
380 by (rule normal.rcos_sum [OF a_normal,
381     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
383 lemma (in abelian_subgroup) rcosets_add_eq:
384   "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
385   -- {* generalizes @{text subgroup_mult_id} *}
386 by (rule normal.rcosets_mult_eq [OF a_normal,
387     folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
390 subsubsection {* Congruence Relation *}
392 lemma (in abelian_subgroup) a_equiv_rcong:
393    shows "equiv (carrier G) (racong H)"
394 by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
395     folded a_r_congruent_def, simplified monoid_record_simps])
397 lemma (in abelian_subgroup) a_l_coset_eq_rcong:
398   assumes a: "a \<in> carrier G"
399   shows "a <+ H = racong H  {a}"
400 by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
401     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
403 lemma (in abelian_subgroup) a_rcos_equation:
404   shows
405      "\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G;  b \<in> carrier G;
406         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
407       \<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})"
408 by (rule group.rcos_equation [OF a_group a_subgroup,
409     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
411 lemma (in abelian_subgroup) a_rcos_disjoint:
412   shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
413 by (rule group.rcos_disjoint [OF a_group a_subgroup,
414     folded A_RCOSETS_def, simplified monoid_record_simps])
416 lemma (in abelian_subgroup) a_rcos_self:
417   shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
418 by (rule group.rcos_self [OF a_group _ a_subgroup,
419     folded a_r_coset_def, simplified monoid_record_simps])
421 lemma (in abelian_subgroup) a_rcosets_part_G:
422   shows "\<Union>(a_rcosets H) = carrier G"
423 by (rule group.rcosets_part_G [OF a_group a_subgroup,
424     folded A_RCOSETS_def, simplified monoid_record_simps])
426 lemma (in abelian_subgroup) a_cosets_finite:
427      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
428 by (rule group.cosets_finite [OF a_group,
429     folded A_RCOSETS_def, simplified monoid_record_simps])
431 lemma (in abelian_group) a_card_cosets_equal:
432      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
433       \<Longrightarrow> card c = card H"
434 by (rule group.card_cosets_equal [OF a_group,
435     folded A_RCOSETS_def, simplified monoid_record_simps])
437 lemma (in abelian_group) rcosets_subset_PowG:
438      "additive_subgroup H G  \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
439 by (rule group.rcosets_subset_PowG [OF a_group,
440     folded A_RCOSETS_def, simplified monoid_record_simps],
443 theorem (in abelian_group) a_lagrange:
444      "\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk>
445       \<Longrightarrow> card(a_rcosets H) * card(H) = order(G)"
446 by (rule group.lagrange [OF a_group,
447     folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
448     (fast intro!: additive_subgroup.a_subgroup)+
451 subsubsection {* Factorization *}
453 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
455 lemma A_FactGroup_def':
456   fixes G (structure)
457   shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
458 unfolding A_FactGroup_defs
459 by (fold A_RCOSETS_def set_add_def)
462 lemma (in abelian_subgroup) a_setmult_closed:
463      "\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H"
464 by (rule normal.setmult_closed [OF a_normal,
465     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
467 lemma (in abelian_subgroup) a_setinv_closed:
468      "K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H"
469 by (rule normal.setinv_closed [OF a_normal,
470     folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])
472 lemma (in abelian_subgroup) a_rcosets_assoc:
473      "\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk>
474       \<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
475 by (rule normal.rcosets_assoc [OF a_normal,
476     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
478 lemma (in abelian_subgroup) a_subgroup_in_rcosets:
479      "H \<in> a_rcosets H"
480 by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
481     folded A_RCOSETS_def, simplified monoid_record_simps])
483 lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
484      "M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H"
485 by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
486     folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])
488 theorem (in abelian_subgroup) a_factorgroup_is_group:
489   "group (G A_Mod H)"
490 by (rule normal.factorgroup_is_group [OF a_normal,
491     folded A_FactGroup_def, simplified monoid_record_simps])
493 text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in
494         a commutative group *}
495 theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
496   "comm_group (G A_Mod H)"
497 apply (intro comm_group.intro comm_monoid.intro) prefer 3
498   apply (rule a_factorgroup_is_group)
499  apply (rule group.axioms[OF a_factorgroup_is_group])
500 apply (rule comm_monoid_axioms.intro)
501 apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
502 apply (simp add: a_rcos_sum a_comm)
503 done
505 lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
508 lemma (in abelian_subgroup) a_inv_FactGroup:
509      "X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"
510 by (rule normal.inv_FactGroup [OF a_normal,
511     folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
513 text{*The coset map is a homomorphism from @{term G} to the quotient group
514   @{term "G Mod H"}*}
515 lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
516   "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
517 by (rule normal.r_coset_hom_Mod [OF a_normal,
518     folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
520 text {* The isomorphism theorems have been omitted from lifting, at
521   least for now *}
523 subsubsection{*The First Isomorphism Theorem*}
525 text{*The quotient by the kernel of a homomorphism is isomorphic to the
526   range of that homomorphism.*}
528 lemmas a_kernel_defs =
529   a_kernel_def kernel_def
531 lemma a_kernel_def':
532   "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
533 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
536 subsubsection {* Homomorphisms *}
538 lemma abelian_group_homI:
539   assumes "abelian_group G"
540   assumes "abelian_group H"
541   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
542                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
543   shows "abelian_group_hom G H h"
544 proof -
545   interpret G: abelian_group G by fact
546   interpret H: abelian_group H by fact
547   show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
548     apply fact
549     apply fact
550     apply (rule a_group_hom)
551     done
552 qed
554 lemma (in abelian_group_hom) is_abelian_group_hom:
555   "abelian_group_hom G H h"
556   ..
558 lemma (in abelian_group_hom) hom_add [simp]:
559   "[| x : carrier G; y : carrier G |]
560         ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
561 by (rule group_hom.hom_mult[OF a_group_hom,
562     simplified ring_record_simps])
564 lemma (in abelian_group_hom) hom_closed [simp]:
565   "x \<in> carrier G \<Longrightarrow> h x \<in> carrier H"
566 by (rule group_hom.hom_closed[OF a_group_hom,
567     simplified ring_record_simps])
569 lemma (in abelian_group_hom) zero_closed [simp]:
570   "h \<zero> \<in> carrier H"
571 by (rule group_hom.one_closed[OF a_group_hom,
572     simplified ring_record_simps])
574 lemma (in abelian_group_hom) hom_zero [simp]:
575   "h \<zero> = \<zero>\<^bsub>H\<^esub>"
576 by (rule group_hom.hom_one[OF a_group_hom,
577     simplified ring_record_simps])
579 lemma (in abelian_group_hom) a_inv_closed [simp]:
580   "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
581 by (rule group_hom.inv_closed[OF a_group_hom,
582     folded a_inv_def, simplified ring_record_simps])
584 lemma (in abelian_group_hom) hom_a_inv [simp]:
585   "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
586 by (rule group_hom.hom_inv[OF a_group_hom,
587     folded a_inv_def, simplified ring_record_simps])
589 lemma (in abelian_group_hom) additive_subgroup_a_kernel:
590   "additive_subgroup (a_kernel G H h) G"
591 apply (rule additive_subgroup.intro)
592 apply (rule group_hom.subgroup_kernel[OF a_group_hom,
593        folded a_kernel_def, simplified ring_record_simps])
594 done
596 text{*The kernel of a homomorphism is an abelian subgroup*}
597 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
598   "abelian_subgroup (a_kernel G H h) G"
599 apply (rule abelian_subgroupI)
600 apply (rule group_hom.normal_kernel[OF a_group_hom,
601        folded a_kernel_def, simplified ring_record_simps])
602 apply (simp add: G.a_comm)
603 done
605 lemma (in abelian_group_hom) A_FactGroup_nonempty:
606   assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
607   shows "X \<noteq> {}"
608 by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
609     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
611 lemma (in abelian_group_hom) FactGroup_contents_mem:
612   assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
613   shows "contents (hX) \<in> carrier H"
614 by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
615     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
617 lemma (in abelian_group_hom) A_FactGroup_hom:
618      "(\<lambda>X. contents (hX)) \<in> hom (G A_Mod (a_kernel G H h))
619           \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
620 by (rule group_hom.FactGroup_hom[OF a_group_hom,
621     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
623 lemma (in abelian_group_hom) A_FactGroup_inj_on:
624      "inj_on (\<lambda>X. contents (h  X)) (carrier (G A_Mod a_kernel G H h))"
625 by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
626     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
628 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
629 homomorphism from the quotient group*}
630 lemma (in abelian_group_hom) A_FactGroup_onto:
631   assumes h: "h  carrier G = carrier H"
632   shows "(\<lambda>X. contents (h  X))  carrier (G A_Mod a_kernel G H h) = carrier H"
633 by (rule group_hom.FactGroup_onto[OF a_group_hom,
634     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
636 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
637  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
638 theorem (in abelian_group_hom) A_FactGroup_iso:
639   "h  carrier G = carrier H
640    \<Longrightarrow> (\<lambda>X. contents (hX)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
641           (| carrier = carrier H, mult = add H, one = zero H |)"
642 by (rule group_hom.FactGroup_iso[OF a_group_hom,
643     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
645 subsubsection {* Cosets *}
647 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
649 lemma (in additive_subgroup) a_Hcarr [simp]:
650   assumes hH: "h \<in> H"
651   shows "h \<in> carrier G"
652 by (rule subgroup.mem_carrier [OF a_subgroup,
653     simplified monoid_record_simps]) (rule hH)
656 lemma (in abelian_subgroup) a_elemrcos_carrier:
657   assumes acarr: "a \<in> carrier G"
658       and a': "a' \<in> H +> a"
659   shows "a' \<in> carrier G"
660 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
661     folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
663 lemma (in abelian_subgroup) a_rcos_const:
664   assumes hH: "h \<in> H"
665   shows "H +> h = H"
666 by (rule subgroup.rcos_const [OF a_subgroup a_group,
667     folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
669 lemma (in abelian_subgroup) a_rcos_module_imp:
670   assumes xcarr: "x \<in> carrier G"
671       and x'cos: "x' \<in> H +> x"
672   shows "(x' \<oplus> \<ominus>x) \<in> H"
673 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
674     folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
676 lemma (in abelian_subgroup) a_rcos_module_rev:
677   assumes "x \<in> carrier G" "x' \<in> carrier G"
678       and "(x' \<oplus> \<ominus>x) \<in> H"
679   shows "x' \<in> H +> x"
680 using assms
681 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
682     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
684 lemma (in abelian_subgroup) a_rcos_module:
685   assumes "x \<in> carrier G" "x' \<in> carrier G"
686   shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
687 using assms
688 by (rule subgroup.rcos_module [OF a_subgroup a_group,
689     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
691 --"variant"
692 lemma (in abelian_subgroup) a_rcos_module_minus:
693   assumes "ring G"
694   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
695   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
696 proof -
697   interpret G: ring G by fact
698   from carr
699   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
700   with carr
701   show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
702     by (simp add: minus_eq)
703 qed
705 lemma (in abelian_subgroup) a_repr_independence':
706   assumes y: "y \<in> H +> x"
707       and xcarr: "x \<in> carrier G"
708   shows "H +> x = H +> y"
709   apply (rule a_repr_independence)
710     apply (rule y)
711    apply (rule xcarr)
712   apply (rule a_subgroup)
713   done
715 lemma (in abelian_subgroup) a_repr_independenceD:
716   assumes ycarr: "y \<in> carrier G"
717       and repr:  "H +> x = H +> y"
718   shows "y \<in> H +> x"
719 by (rule group.repr_independenceD [OF a_group a_subgroup,
720     folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
723 lemma (in abelian_subgroup) a_rcosets_carrier:
724   "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
725 by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
726     folded A_RCOSETS_def, simplified monoid_record_simps])
730 subsubsection {* Addition of Subgroups *}
732 lemma (in abelian_monoid) set_add_closed:
733   assumes Acarr: "A \<subseteq> carrier G"
734       and Bcarr: "B \<subseteq> carrier G"
735   shows "A <+> B \<subseteq> carrier G"
736 by (rule monoid.set_mult_closed [OF a_monoid,
737     folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)