src/HOL/Algebra/AbelCoset.thy
 author haftmann Sun Jun 23 21:16:07 2013 +0200 (2013-06-23) changeset 52435 6646bb548c6b parent 45388 121b2db078b1 child 55926 3ef14caf5637 permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
1 (*  Title:      HOL/Algebra/AbelCoset.thy
2     Author:     Stephan Hohe, TU Muenchen
3 *)
5 theory AbelCoset
6 imports Coset Ring
7 begin
9 subsection {* More Lifting from Groups to Abelian Groups *}
11 subsubsection {* Definitions *}
13 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
14   up with better syntax here *}
16 no_notation Sum_Type.Plus (infixr "<+>" 65)
18 definition
19   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
20   where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
22 definition
23   a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
24   where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
26 definition
27   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _"  80)
28   where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
30 definition
31   set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
32   where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
34 definition
35   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _"  80)
36   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
38 definition
39   a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index>")
40   where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
42 definition
43   A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
44     --{*Actually defined for groups rather than monoids*}
45   where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
47 definition
48   a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
49     --{*the kernel of a homomorphism (additive)*}
50   where "a_kernel G H h =
51     kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
52       \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
54 locale abelian_group_hom = G: abelian_group G + H: abelian_group H
55     for G (structure) and H (structure) +
56   fixes h
57   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
58                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
60 lemmas a_r_coset_defs =
61   a_r_coset_def r_coset_def
63 lemma a_r_coset_def':
64   fixes G (structure)
65   shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
66 unfolding a_r_coset_defs
67 by simp
69 lemmas a_l_coset_defs =
70   a_l_coset_def l_coset_def
72 lemma a_l_coset_def':
73   fixes G (structure)
74   shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
75 unfolding a_l_coset_defs
76 by simp
78 lemmas A_RCOSETS_defs =
79   A_RCOSETS_def RCOSETS_def
81 lemma A_RCOSETS_def':
82   fixes G (structure)
83   shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
84 unfolding A_RCOSETS_defs
85 by (fold a_r_coset_def, simp)
87 lemmas set_add_defs =
91   fixes G (structure)
92   shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
94 by simp
96 lemmas A_SET_INV_defs =
97   A_SET_INV_def SET_INV_def
99 lemma A_SET_INV_def':
100   fixes G (structure)
101   shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
102 unfolding A_SET_INV_defs
103 by (fold a_inv_def)
106 subsubsection {* Cosets *}
108 lemma (in abelian_group) a_coset_add_assoc:
109      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
110       ==> (M +> g) +> h = M +> (g \<oplus> h)"
111 by (rule group.coset_mult_assoc [OF a_group,
112     folded a_r_coset_def, simplified monoid_record_simps])
114 lemma (in abelian_group) a_coset_add_zero [simp]:
115   "M \<subseteq> carrier G ==> M +> \<zero> = M"
116 by (rule group.coset_mult_one [OF a_group,
117     folded a_r_coset_def, simplified monoid_record_simps])
119 lemma (in abelian_group) a_coset_add_inv1:
120      "[| M +> (x \<oplus> (\<ominus> y)) = M;  x \<in> carrier G ; y \<in> carrier G;
121          M \<subseteq> carrier G |] ==> M +> x = M +> y"
122 by (rule group.coset_mult_inv1 [OF a_group,
123     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
125 lemma (in abelian_group) a_coset_add_inv2:
126      "[| M +> x = M +> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
127       ==> M +> (x \<oplus> (\<ominus> y)) = M"
128 by (rule group.coset_mult_inv2 [OF a_group,
129     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
131 lemma (in abelian_group) a_coset_join1:
132      "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
133 by (rule group.coset_join1 [OF a_group,
134     folded a_r_coset_def, simplified monoid_record_simps])
136 lemma (in abelian_group) a_solve_equation:
137     "\<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"
138 by (rule group.solve_equation [OF a_group,
139     folded a_r_coset_def, simplified monoid_record_simps])
141 lemma (in abelian_group) a_repr_independence:
142      "\<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"
143 by (rule group.repr_independence [OF a_group,
144     folded a_r_coset_def, simplified monoid_record_simps])
146 lemma (in abelian_group) a_coset_join2:
147      "\<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"
148 by (rule group.coset_join2 [OF a_group,
149     folded a_r_coset_def, simplified monoid_record_simps])
151 lemma (in abelian_monoid) a_r_coset_subset_G:
152      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G"
153 by (rule monoid.r_coset_subset_G [OF a_monoid,
154     folded a_r_coset_def, simplified monoid_record_simps])
156 lemma (in abelian_group) a_rcosI:
157      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x"
158 by (rule group.rcosI [OF a_group,
159     folded a_r_coset_def, simplified monoid_record_simps])
161 lemma (in abelian_group) a_rcosetsI:
162      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H"
163 by (rule group.rcosetsI [OF a_group,
164     folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
166 text{*Really needed?*}
167 lemma (in abelian_group) a_transpose_inv:
168      "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
169       ==> (\<ominus> x) \<oplus> z = y"
170 by (rule group.transpose_inv [OF a_group,
171     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
173 (*
174 --"duplicate"
175 lemma (in abelian_group) a_rcos_self:
176      "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
177 by (rule group.rcos_self [OF a_group,
178     folded a_r_coset_def, simplified monoid_record_simps])
179 *)
182 subsubsection {* Subgroups *}
184 locale additive_subgroup =
185   fixes H and G (structure)
186   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
189   shows "additive_subgroup H G"
190 by (rule additive_subgroup_axioms)
193   fixes G (structure)
194   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
195   shows "additive_subgroup H G"
196 by (rule additive_subgroup.intro) (rule a_subgroup)
198 lemma (in additive_subgroup) a_subset:
199      "H \<subseteq> carrier G"
200 by (rule subgroup.subset[OF a_subgroup,
201     simplified monoid_record_simps])
203 lemma (in additive_subgroup) a_closed [intro, simp]:
204      "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H"
205 by (rule subgroup.m_closed[OF a_subgroup,
206     simplified monoid_record_simps])
208 lemma (in additive_subgroup) zero_closed [simp]:
209      "\<zero> \<in> H"
210 by (rule subgroup.one_closed[OF a_subgroup,
211     simplified monoid_record_simps])
213 lemma (in additive_subgroup) a_inv_closed [intro,simp]:
214      "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
215 by (rule subgroup.m_inv_closed[OF a_subgroup,
216     folded a_inv_def, simplified monoid_record_simps])
219 subsubsection {* Additive subgroups are normal *}
221 text {* Every subgroup of an @{text "abelian_group"} is normal *}
223 locale abelian_subgroup = additive_subgroup + abelian_group G +
224   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
226 lemma (in abelian_subgroup) is_abelian_subgroup:
227   shows "abelian_subgroup H G"
228 by (rule abelian_subgroup_axioms)
230 lemma abelian_subgroupI:
231   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
232       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"
233   shows "abelian_subgroup H G"
234 proof -
235   interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
236     by (rule a_normal)
238   show "abelian_subgroup H G"
239     by default (simp add: a_comm)
240 qed
242 lemma abelian_subgroupI2:
243   fixes G (structure)
244   assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
245       and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
246   shows "abelian_subgroup H G"
247 proof -
248   interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
249     by (rule a_comm_group)
250   interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
251     by (rule a_subgroup)
253   show "abelian_subgroup H G"
254     apply unfold_locales
255   proof (simp add: r_coset_def l_coset_def, clarsimp)
256     fix x
257     assume xcarr: "x \<in> carrier G"
258     from a_subgroup have Hcarr: "H \<subseteq> carrier G"
259       unfolding subgroup_def by simp
260     from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
261       using m_comm [simplified] by fast
262   qed
263 qed
265 lemma abelian_subgroupI3:
266   fixes G (structure)
267   assumes asg: "additive_subgroup H G"
268       and ag: "abelian_group G"
269   shows "abelian_subgroup H G"
270 apply (rule abelian_subgroupI2)
271  apply (rule abelian_group.a_comm_group[OF ag])
272 apply (rule additive_subgroup.a_subgroup[OF asg])
273 done
275 lemma (in abelian_subgroup) a_coset_eq:
276      "(\<forall>x \<in> carrier G. H +> x = x <+ H)"
277 by (rule normal.coset_eq[OF a_normal,
278     folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
280 lemma (in abelian_subgroup) a_inv_op_closed1:
281   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H"
282 by (rule normal.inv_op_closed1 [OF a_normal,
283     folded a_inv_def, simplified monoid_record_simps])
285 lemma (in abelian_subgroup) a_inv_op_closed2:
286   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H"
287 by (rule normal.inv_op_closed2 [OF a_normal,
288     folded a_inv_def, simplified monoid_record_simps])
290 text{*Alternative characterization of normal subgroups*}
291 lemma (in abelian_group) a_normal_inv_iff:
292      "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) =
293       (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))"
294       (is "_ = ?rhs")
295 by (rule group.normal_inv_iff [OF a_group,
296     folded a_inv_def, simplified monoid_record_simps])
298 lemma (in abelian_group) a_lcos_m_assoc:
299      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
300       ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
301 by (rule group.lcos_m_assoc [OF a_group,
302     folded a_l_coset_def, simplified monoid_record_simps])
304 lemma (in abelian_group) a_lcos_mult_one:
305      "M \<subseteq> carrier G ==> \<zero> <+ M = M"
306 by (rule group.lcos_mult_one [OF a_group,
307     folded a_l_coset_def, simplified monoid_record_simps])
310 lemma (in abelian_group) a_l_coset_subset_G:
311      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
312 by (rule group.l_coset_subset_G [OF a_group,
313     folded a_l_coset_def, simplified monoid_record_simps])
316 lemma (in abelian_group) a_l_coset_swap:
317      "\<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"
318 by (rule group.l_coset_swap [OF a_group,
319     folded a_l_coset_def, simplified monoid_record_simps])
321 lemma (in abelian_group) a_l_coset_carrier:
322      "[| 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"
323 by (rule group.l_coset_carrier [OF a_group,
324     folded a_l_coset_def, simplified monoid_record_simps])
326 lemma (in abelian_group) a_l_repr_imp_subset:
327   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>"
328   shows "y <+ H \<subseteq> x <+ H"
329 apply (rule group.l_repr_imp_subset [OF a_group,
330     folded a_l_coset_def, simplified monoid_record_simps])
331 apply (rule y)
332 apply (rule x)
333 apply (rule sb)
334 done
336 lemma (in abelian_group) a_l_repr_independence:
337   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>"
338   shows "x <+ H = y <+ H"
339 apply (rule group.l_repr_independence [OF a_group,
340     folded a_l_coset_def, simplified monoid_record_simps])
341 apply (rule y)
342 apply (rule x)
343 apply (rule sb)
344 done
346 lemma (in abelian_group) setadd_subset_G:
347      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
348 by (rule group.setmult_subset_G [OF a_group,
349     folded set_add_def, simplified monoid_record_simps])
351 lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
352 by (rule group.subgroup_mult_id [OF a_group,
353     folded set_add_def, simplified monoid_record_simps])
355 lemma (in abelian_subgroup) a_rcos_inv:
356   assumes x:     "x \<in> carrier G"
357   shows "a_set_inv (H +> x) = H +> (\<ominus> x)"
358 by (rule normal.rcos_inv [OF a_normal,
359   folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
361 lemma (in abelian_group) a_setmult_rcos_assoc:
362      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
363       \<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x"
364 by (rule group.setmult_rcos_assoc [OF a_group,
365     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
367 lemma (in abelian_group) a_rcos_assoc_lcos:
368      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
369       \<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)"
370 by (rule group.rcos_assoc_lcos [OF a_group,
371      folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
373 lemma (in abelian_subgroup) a_rcos_sum:
374      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
375       \<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)"
376 by (rule normal.rcos_sum [OF a_normal,
377     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
379 lemma (in abelian_subgroup) rcosets_add_eq:
380   "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
381   -- {* generalizes @{text subgroup_mult_id} *}
382 by (rule normal.rcosets_mult_eq [OF a_normal,
383     folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
386 subsubsection {* Congruence Relation *}
388 lemma (in abelian_subgroup) a_equiv_rcong:
389    shows "equiv (carrier G) (racong H)"
390 by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
391     folded a_r_congruent_def, simplified monoid_record_simps])
393 lemma (in abelian_subgroup) a_l_coset_eq_rcong:
394   assumes a: "a \<in> carrier G"
395   shows "a <+ H = racong H  {a}"
396 by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
397     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
399 lemma (in abelian_subgroup) a_rcos_equation:
400   shows
401      "\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G;  b \<in> carrier G;
402         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
403       \<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})"
404 by (rule group.rcos_equation [OF a_group a_subgroup,
405     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
407 lemma (in abelian_subgroup) a_rcos_disjoint:
408   shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
409 by (rule group.rcos_disjoint [OF a_group a_subgroup,
410     folded A_RCOSETS_def, simplified monoid_record_simps])
412 lemma (in abelian_subgroup) a_rcos_self:
413   shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
414 by (rule group.rcos_self [OF a_group _ a_subgroup,
415     folded a_r_coset_def, simplified monoid_record_simps])
417 lemma (in abelian_subgroup) a_rcosets_part_G:
418   shows "\<Union>(a_rcosets H) = carrier G"
419 by (rule group.rcosets_part_G [OF a_group a_subgroup,
420     folded A_RCOSETS_def, simplified monoid_record_simps])
422 lemma (in abelian_subgroup) a_cosets_finite:
423      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
424 by (rule group.cosets_finite [OF a_group,
425     folded A_RCOSETS_def, simplified monoid_record_simps])
427 lemma (in abelian_group) a_card_cosets_equal:
428      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
429       \<Longrightarrow> card c = card H"
430 by (rule group.card_cosets_equal [OF a_group,
431     folded A_RCOSETS_def, simplified monoid_record_simps])
433 lemma (in abelian_group) rcosets_subset_PowG:
434      "additive_subgroup H G  \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
435 by (rule group.rcosets_subset_PowG [OF a_group,
436     folded A_RCOSETS_def, simplified monoid_record_simps],
439 theorem (in abelian_group) a_lagrange:
440      "\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk>
441       \<Longrightarrow> card(a_rcosets H) * card(H) = order(G)"
442 by (rule group.lagrange [OF a_group,
443     folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
444     (fast intro!: additive_subgroup.a_subgroup)+
447 subsubsection {* Factorization *}
449 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
451 lemma A_FactGroup_def':
452   fixes G (structure)
453   shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
454 unfolding A_FactGroup_defs
455 by (fold A_RCOSETS_def set_add_def)
458 lemma (in abelian_subgroup) a_setmult_closed:
459      "\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H"
460 by (rule normal.setmult_closed [OF a_normal,
461     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
463 lemma (in abelian_subgroup) a_setinv_closed:
464      "K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H"
465 by (rule normal.setinv_closed [OF a_normal,
466     folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])
468 lemma (in abelian_subgroup) a_rcosets_assoc:
469      "\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk>
470       \<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
471 by (rule normal.rcosets_assoc [OF a_normal,
472     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
474 lemma (in abelian_subgroup) a_subgroup_in_rcosets:
475      "H \<in> a_rcosets H"
476 by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
477     folded A_RCOSETS_def, simplified monoid_record_simps])
479 lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
480      "M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H"
481 by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
482     folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])
484 theorem (in abelian_subgroup) a_factorgroup_is_group:
485   "group (G A_Mod H)"
486 by (rule normal.factorgroup_is_group [OF a_normal,
487     folded A_FactGroup_def, simplified monoid_record_simps])
489 text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in
490         a commutative group *}
491 theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
492   "comm_group (G A_Mod H)"
493 apply (intro comm_group.intro comm_monoid.intro) prefer 3
494   apply (rule a_factorgroup_is_group)
495  apply (rule group.axioms[OF a_factorgroup_is_group])
496 apply (rule comm_monoid_axioms.intro)
497 apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
498 apply (simp add: a_rcos_sum a_comm)
499 done
501 lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
504 lemma (in abelian_subgroup) a_inv_FactGroup:
505      "X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"
506 by (rule normal.inv_FactGroup [OF a_normal,
507     folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
509 text{*The coset map is a homomorphism from @{term G} to the quotient group
510   @{term "G Mod H"}*}
511 lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
512   "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
513 by (rule normal.r_coset_hom_Mod [OF a_normal,
514     folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
516 text {* The isomorphism theorems have been omitted from lifting, at
517   least for now *}
520 subsubsection{*The First Isomorphism Theorem*}
522 text{*The quotient by the kernel of a homomorphism is isomorphic to the
523   range of that homomorphism.*}
525 lemmas a_kernel_defs =
526   a_kernel_def kernel_def
528 lemma a_kernel_def':
529   "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
530 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
533 subsubsection {* Homomorphisms *}
535 lemma abelian_group_homI:
536   assumes "abelian_group G"
537   assumes "abelian_group H"
538   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
539                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
540   shows "abelian_group_hom G H h"
541 proof -
542   interpret G: abelian_group G by fact
543   interpret H: abelian_group H by fact
544   show ?thesis
545     apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
546       apply fact
547      apply fact
548     apply (rule a_group_hom)
549     done
550 qed
552 lemma (in abelian_group_hom) is_abelian_group_hom:
553   "abelian_group_hom G H h"
554   ..
556 lemma (in abelian_group_hom) hom_add [simp]:
557   "[| x : carrier G; y : carrier G |]
558         ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
559 by (rule group_hom.hom_mult[OF a_group_hom,
560     simplified ring_record_simps])
562 lemma (in abelian_group_hom) hom_closed [simp]:
563   "x \<in> carrier G \<Longrightarrow> h x \<in> carrier H"
564 by (rule group_hom.hom_closed[OF a_group_hom,
565     simplified ring_record_simps])
567 lemma (in abelian_group_hom) zero_closed [simp]:
568   "h \<zero> \<in> carrier H"
569 by (rule group_hom.one_closed[OF a_group_hom,
570     simplified ring_record_simps])
572 lemma (in abelian_group_hom) hom_zero [simp]:
573   "h \<zero> = \<zero>\<^bsub>H\<^esub>"
574 by (rule group_hom.hom_one[OF a_group_hom,
575     simplified ring_record_simps])
577 lemma (in abelian_group_hom) a_inv_closed [simp]:
578   "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
579 by (rule group_hom.inv_closed[OF a_group_hom,
580     folded a_inv_def, simplified ring_record_simps])
582 lemma (in abelian_group_hom) hom_a_inv [simp]:
583   "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
584 by (rule group_hom.hom_inv[OF a_group_hom,
585     folded a_inv_def, simplified ring_record_simps])
587 lemma (in abelian_group_hom) additive_subgroup_a_kernel:
588   "additive_subgroup (a_kernel G H h) G"
589 apply (rule additive_subgroup.intro)
590 apply (rule group_hom.subgroup_kernel[OF a_group_hom,
591        folded a_kernel_def, simplified ring_record_simps])
592 done
594 text{*The kernel of a homomorphism is an abelian subgroup*}
595 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
596   "abelian_subgroup (a_kernel G H h) G"
597 apply (rule abelian_subgroupI)
598 apply (rule group_hom.normal_kernel[OF a_group_hom,
599        folded a_kernel_def, simplified ring_record_simps])
600 apply (simp add: G.a_comm)
601 done
603 lemma (in abelian_group_hom) A_FactGroup_nonempty:
604   assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
605   shows "X \<noteq> {}"
606 by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
607     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
609 lemma (in abelian_group_hom) FactGroup_the_elem_mem:
610   assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
611   shows "the_elem (hX) \<in> carrier H"
612 by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,
613     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
615 lemma (in abelian_group_hom) A_FactGroup_hom:
616      "(\<lambda>X. the_elem (hX)) \<in> hom (G A_Mod (a_kernel G H h))
617           \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
618 by (rule group_hom.FactGroup_hom[OF a_group_hom,
619     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
621 lemma (in abelian_group_hom) A_FactGroup_inj_on:
622      "inj_on (\<lambda>X. the_elem (h  X)) (carrier (G A_Mod a_kernel G H h))"
623 by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
624     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
626 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
627 homomorphism from the quotient group*}
628 lemma (in abelian_group_hom) A_FactGroup_onto:
629   assumes h: "h  carrier G = carrier H"
630   shows "(\<lambda>X. the_elem (h  X))  carrier (G A_Mod a_kernel G H h) = carrier H"
631 by (rule group_hom.FactGroup_onto[OF a_group_hom,
632     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
634 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
635  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
636 theorem (in abelian_group_hom) A_FactGroup_iso:
637   "h  carrier G = carrier H
638    \<Longrightarrow> (\<lambda>X. the_elem (hX)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
639           (| carrier = carrier H, mult = add H, one = zero H |)"
640 by (rule group_hom.FactGroup_iso[OF a_group_hom,
641     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
644 subsubsection {* Cosets *}
646 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
648 lemma (in additive_subgroup) a_Hcarr [simp]:
649   assumes hH: "h \<in> H"
650   shows "h \<in> carrier G"
651 by (rule subgroup.mem_carrier [OF a_subgroup,
652     simplified monoid_record_simps]) (rule hH)
655 lemma (in abelian_subgroup) a_elemrcos_carrier:
656   assumes acarr: "a \<in> carrier G"
657       and a': "a' \<in> H +> a"
658   shows "a' \<in> carrier G"
659 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
660     folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
662 lemma (in abelian_subgroup) a_rcos_const:
663   assumes hH: "h \<in> H"
664   shows "H +> h = H"
665 by (rule subgroup.rcos_const [OF a_subgroup a_group,
666     folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
668 lemma (in abelian_subgroup) a_rcos_module_imp:
669   assumes xcarr: "x \<in> carrier G"
670       and x'cos: "x' \<in> H +> x"
671   shows "(x' \<oplus> \<ominus>x) \<in> H"
672 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
673     folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
675 lemma (in abelian_subgroup) a_rcos_module_rev:
676   assumes "x \<in> carrier G" "x' \<in> carrier G"
677       and "(x' \<oplus> \<ominus>x) \<in> H"
678   shows "x' \<in> H +> x"
679 using assms
680 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
681     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
683 lemma (in abelian_subgroup) a_rcos_module:
684   assumes "x \<in> carrier G" "x' \<in> carrier G"
685   shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
686 using assms
687 by (rule subgroup.rcos_module [OF a_subgroup a_group,
688     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
690 --"variant"
691 lemma (in abelian_subgroup) a_rcos_module_minus:
692   assumes "ring G"
693   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
694   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
695 proof -
696   interpret G: ring G by fact
697   from carr
698   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
699   with carr
700   show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
701     by (simp add: minus_eq)
702 qed
704 lemma (in abelian_subgroup) a_repr_independence':
705   assumes y: "y \<in> H +> x"
706       and xcarr: "x \<in> carrier G"
707   shows "H +> x = H +> y"
708   apply (rule a_repr_independence)
709     apply (rule y)
710    apply (rule xcarr)
711   apply (rule a_subgroup)
712   done
714 lemma (in abelian_subgroup) a_repr_independenceD:
715   assumes ycarr: "y \<in> carrier G"
716       and repr:  "H +> x = H +> y"
717   shows "y \<in> H +> x"
718 by (rule group.repr_independenceD [OF a_group a_subgroup,
719     folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
722 lemma (in abelian_subgroup) a_rcosets_carrier:
723   "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
724 by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
725     folded A_RCOSETS_def, simplified monoid_record_simps])
728 subsubsection {* Addition of Subgroups *}
730 lemma (in abelian_monoid) set_add_closed:
731   assumes Acarr: "A \<subseteq> carrier G"
732       and Bcarr: "B \<subseteq> carrier G"
733   shows "A <+> B \<subseteq> carrier G"
734 by (rule monoid.set_mult_closed [OF a_monoid,
735     folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)