src/HOL/Algebra/AbelCoset.thy
 author wenzelm Thu Jun 21 17:28:53 2007 +0200 (2007-06-21) changeset 23463 9953ff53cc64 parent 23383 5460951833fa child 26203 9625f3579b48 permissions -rw-r--r--
tuned proofs -- avoid implicit prems;
1 (*
2   Title:     HOL/Algebra/AbelCoset.thy
3   Id:        $Id$
4   Author:    Stephan Hohe, TU Muenchen
5 *)
7 theory AbelCoset
8 imports Coset Ring
9 begin
12 section {* More Lifting from Groups to Abelian Groups *}
14 subsection {* Definitions *}
16 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
17   up with better syntax here *}
19 hide const Plus
21 constdefs (structure G)
22   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
23   "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
25   a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
26   "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
28   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _"  80)
29   "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
31   set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
32   "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
34   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _"  80)
35   "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
37 constdefs (structure G)
38   a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
39                   ("racong\<index> _")
40    "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
42 constdefs
43   A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid"
44      (infixl "A'_Mod" 65)
45     --{*Actually defined for groups rather than monoids*}
46   "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
48 constdefs
49   a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>
50              ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
51     --{*the kernel of a homomorphism (additive)*}
52   "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
53                               \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
55 locale abelian_group_hom = abelian_group G + abelian_group H + var h +
56   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
57                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
59 lemmas a_r_coset_defs =
60   a_r_coset_def r_coset_def
62 lemma a_r_coset_def':
63   includes struct G
64   shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
65 unfolding a_r_coset_defs
66 by simp
68 lemmas a_l_coset_defs =
69   a_l_coset_def l_coset_def
71 lemma a_l_coset_def':
72   includes struct G
73   shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
74 unfolding a_l_coset_defs
75 by simp
77 lemmas A_RCOSETS_defs =
78   A_RCOSETS_def RCOSETS_def
80 lemma A_RCOSETS_def':
81   includes struct G
82   shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
83 unfolding A_RCOSETS_defs
84 by (fold a_r_coset_def, simp)
86 lemmas set_add_defs =
90   includes struct G
91   shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
93 by simp
95 lemmas A_SET_INV_defs =
96   A_SET_INV_def SET_INV_def
98 lemma A_SET_INV_def':
99   includes struct G
100   shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
101 unfolding A_SET_INV_defs
102 by (fold a_inv_def)
105 subsection {* Cosets *}
107 lemma (in abelian_group) a_coset_add_assoc:
108      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
109       ==> (M +> g) +> h = M +> (g \<oplus> h)"
110 by (rule group.coset_mult_assoc [OF a_group,
111     folded a_r_coset_def, simplified monoid_record_simps])
113 lemma (in abelian_group) a_coset_add_zero [simp]:
114   "M \<subseteq> carrier G ==> M +> \<zero> = M"
115 by (rule group.coset_mult_one [OF a_group,
116     folded a_r_coset_def, simplified monoid_record_simps])
118 lemma (in abelian_group) a_coset_add_inv1:
119      "[| M +> (x \<oplus> (\<ominus> y)) = M;  x \<in> carrier G ; y \<in> carrier G;
120          M \<subseteq> carrier G |] ==> M +> x = M +> y"
121 by (rule group.coset_mult_inv1 [OF a_group,
122     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
124 lemma (in abelian_group) a_coset_add_inv2:
125      "[| M +> x = M +> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
126       ==> M +> (x \<oplus> (\<ominus> y)) = M"
127 by (rule group.coset_mult_inv2 [OF a_group,
128     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
130 lemma (in abelian_group) a_coset_join1:
131      "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
132 by (rule group.coset_join1 [OF a_group,
133     folded a_r_coset_def, simplified monoid_record_simps])
135 lemma (in abelian_group) a_solve_equation:
136     "\<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"
137 by (rule group.solve_equation [OF a_group,
138     folded a_r_coset_def, simplified monoid_record_simps])
140 lemma (in abelian_group) a_repr_independence:
141      "\<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"
142 by (rule group.repr_independence [OF a_group,
143     folded a_r_coset_def, simplified monoid_record_simps])
145 lemma (in abelian_group) a_coset_join2:
146      "\<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"
147 by (rule group.coset_join2 [OF a_group,
148     folded a_r_coset_def, simplified monoid_record_simps])
150 lemma (in abelian_monoid) a_r_coset_subset_G:
151      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G"
152 by (rule monoid.r_coset_subset_G [OF a_monoid,
153     folded a_r_coset_def, simplified monoid_record_simps])
155 lemma (in abelian_group) a_rcosI:
156      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x"
157 by (rule group.rcosI [OF a_group,
158     folded a_r_coset_def, simplified monoid_record_simps])
160 lemma (in abelian_group) a_rcosetsI:
161      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H"
162 by (rule group.rcosetsI [OF a_group,
163     folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
165 text{*Really needed?*}
166 lemma (in abelian_group) a_transpose_inv:
167      "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
168       ==> (\<ominus> x) \<oplus> z = y"
169 by (rule group.transpose_inv [OF a_group,
170     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
172 (*
173 --"duplicate"
174 lemma (in abelian_group) a_rcos_self:
175      "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
176 by (rule group.rcos_self [OF a_group,
177     folded a_r_coset_def, simplified monoid_record_simps])
178 *)
181 subsection {* Subgroups *}
183 locale additive_subgroup = var H + struct G +
184   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
187   shows "additive_subgroup H G"
188 by fact
191   includes struct G
192   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
193   shows "additive_subgroup H G"
194 by (rule additive_subgroup.intro) (rule a_subgroup)
196 lemma (in additive_subgroup) a_subset:
197      "H \<subseteq> carrier G"
198 by (rule subgroup.subset[OF a_subgroup,
199     simplified monoid_record_simps])
201 lemma (in additive_subgroup) a_closed [intro, simp]:
202      "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H"
203 by (rule subgroup.m_closed[OF a_subgroup,
204     simplified monoid_record_simps])
206 lemma (in additive_subgroup) zero_closed [simp]:
207      "\<zero> \<in> H"
208 by (rule subgroup.one_closed[OF a_subgroup,
209     simplified monoid_record_simps])
211 lemma (in additive_subgroup) a_inv_closed [intro,simp]:
212      "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
213 by (rule subgroup.m_inv_closed[OF a_subgroup,
214     folded a_inv_def, simplified monoid_record_simps])
217 subsection {* Normal additive subgroups *}
219 subsubsection {* Definition of @{text "abelian_subgroup"} *}
221 text {* Every subgroup of an @{text "abelian_group"} is normal *}
223 locale abelian_subgroup = additive_subgroup H G + 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 fact
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 (unfold_locales, simp add: a_comm)
240 qed
242 lemma abelian_subgroupI2:
243   includes struct G
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
259         have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
260     from xcarr Hcarr
261         show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
262         using m_comm[simplified]
263         by fast
264   qed
265 qed
267 lemma abelian_subgroupI3:
268   includes struct G
269   assumes asg: "additive_subgroup H G"
270       and ag: "abelian_group G"
271   shows "abelian_subgroup H G"
272 apply (rule abelian_subgroupI2)
273  apply (rule abelian_group.a_comm_group[OF ag])
274 apply (rule additive_subgroup.a_subgroup[OF asg])
275 done
277 lemma (in abelian_subgroup) a_coset_eq:
278      "(\<forall>x \<in> carrier G. H +> x = x <+ H)"
279 by (rule normal.coset_eq[OF a_normal,
280     folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
282 lemma (in abelian_subgroup) a_inv_op_closed1:
283   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H"
284 by (rule normal.inv_op_closed1 [OF a_normal,
285     folded a_inv_def, simplified monoid_record_simps])
287 lemma (in abelian_subgroup) a_inv_op_closed2:
288   shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H"
289 by (rule normal.inv_op_closed2 [OF a_normal,
290     folded a_inv_def, simplified monoid_record_simps])
292 text{*Alternative characterization of normal subgroups*}
293 lemma (in abelian_group) a_normal_inv_iff:
294      "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) =
295       (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))"
296       (is "_ = ?rhs")
297 by (rule group.normal_inv_iff [OF a_group,
298     folded a_inv_def, simplified monoid_record_simps])
300 lemma (in abelian_group) a_lcos_m_assoc:
301      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
302       ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
303 by (rule group.lcos_m_assoc [OF a_group,
304     folded a_l_coset_def, simplified monoid_record_simps])
306 lemma (in abelian_group) a_lcos_mult_one:
307      "M \<subseteq> carrier G ==> \<zero> <+ M = M"
308 by (rule group.lcos_mult_one [OF a_group,
309     folded a_l_coset_def, simplified monoid_record_simps])
312 lemma (in abelian_group) a_l_coset_subset_G:
313      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
314 by (rule group.l_coset_subset_G [OF a_group,
315     folded a_l_coset_def, simplified monoid_record_simps])
318 lemma (in abelian_group) a_l_coset_swap:
319      "\<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"
320 by (rule group.l_coset_swap [OF a_group,
321     folded a_l_coset_def, simplified monoid_record_simps])
323 lemma (in abelian_group) a_l_coset_carrier:
324      "[| 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"
325 by (rule group.l_coset_carrier [OF a_group,
326     folded a_l_coset_def, simplified monoid_record_simps])
328 lemma (in abelian_group) a_l_repr_imp_subset:
329   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>"
330   shows "y <+ H \<subseteq> x <+ H"
331 apply (rule group.l_repr_imp_subset [OF a_group,
332     folded a_l_coset_def, simplified monoid_record_simps])
333 apply (rule y)
334 apply (rule x)
335 apply (rule sb)
336 done
338 lemma (in abelian_group) a_l_repr_independence:
339   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>"
340   shows "x <+ H = y <+ H"
341 apply (rule group.l_repr_independence [OF a_group,
342     folded a_l_coset_def, simplified monoid_record_simps])
343 apply (rule y)
344 apply (rule x)
345 apply (rule sb)
346 done
348 lemma (in abelian_group) setadd_subset_G:
349      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
350 by (rule group.setmult_subset_G [OF a_group,
351     folded set_add_def, simplified monoid_record_simps])
353 lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
354 by (rule group.subgroup_mult_id [OF a_group,
355     folded set_add_def, simplified monoid_record_simps])
357 lemma (in abelian_subgroup) a_rcos_inv:
358   assumes x:     "x \<in> carrier G"
359   shows "a_set_inv (H +> x) = H +> (\<ominus> x)"
360 by (rule normal.rcos_inv [OF a_normal,
361   folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
363 lemma (in abelian_group) a_setmult_rcos_assoc:
364      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
365       \<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x"
366 by (rule group.setmult_rcos_assoc [OF a_group,
367     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
369 lemma (in abelian_group) a_rcos_assoc_lcos:
370      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
371       \<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)"
372 by (rule group.rcos_assoc_lcos [OF a_group,
373      folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
375 lemma (in abelian_subgroup) a_rcos_sum:
376      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
377       \<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)"
378 by (rule normal.rcos_sum [OF a_normal,
379     folded set_add_def a_r_coset_def, simplified monoid_record_simps])
381 lemma (in abelian_subgroup) rcosets_add_eq:
382   "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
383   -- {* generalizes @{text subgroup_mult_id} *}
384 by (rule normal.rcosets_mult_eq [OF a_normal,
385     folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
388 subsection {* Congruence Relation *}
390 lemma (in abelian_subgroup) a_equiv_rcong:
391    shows "equiv (carrier G) (racong H)"
392 by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
393     folded a_r_congruent_def, simplified monoid_record_simps])
395 lemma (in abelian_subgroup) a_l_coset_eq_rcong:
396   assumes a: "a \<in> carrier G"
397   shows "a <+ H = racong H  {a}"
398 by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
399     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
401 lemma (in abelian_subgroup) a_rcos_equation:
402   shows
403      "\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G;  b \<in> carrier G;
404         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
405       \<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})"
406 by (rule group.rcos_equation [OF a_group a_subgroup,
407     folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
409 lemma (in abelian_subgroup) a_rcos_disjoint:
410   shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
411 by (rule group.rcos_disjoint [OF a_group a_subgroup,
412     folded A_RCOSETS_def, simplified monoid_record_simps])
414 lemma (in abelian_subgroup) a_rcos_self:
415   shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
416 by (rule group.rcos_self [OF a_group a_subgroup,
417     folded a_r_coset_def, simplified monoid_record_simps])
419 lemma (in abelian_subgroup) a_rcosets_part_G:
420   shows "\<Union>(a_rcosets H) = carrier G"
421 by (rule group.rcosets_part_G [OF a_group a_subgroup,
422     folded A_RCOSETS_def, simplified monoid_record_simps])
424 lemma (in abelian_subgroup) a_cosets_finite:
425      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
426 by (rule group.cosets_finite [OF a_group,
427     folded A_RCOSETS_def, simplified monoid_record_simps])
429 lemma (in abelian_group) a_card_cosets_equal:
430      "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
431       \<Longrightarrow> card c = card H"
432 by (rule group.card_cosets_equal [OF a_group,
433     folded A_RCOSETS_def, simplified monoid_record_simps])
435 lemma (in abelian_group) rcosets_subset_PowG:
436      "additive_subgroup H G  \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
437 by (rule group.rcosets_subset_PowG [OF a_group,
438     folded A_RCOSETS_def, simplified monoid_record_simps],
441 theorem (in abelian_group) a_lagrange:
442      "\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk>
443       \<Longrightarrow> card(a_rcosets H) * card(H) = order(G)"
444 by (rule group.lagrange [OF a_group,
445     folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
446     (fast intro!: additive_subgroup.a_subgroup)+
449 subsection {* Factorization *}
451 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
453 lemma A_FactGroup_def':
454   includes struct G
455   shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
456 unfolding A_FactGroup_defs
457 by (fold A_RCOSETS_def set_add_def)
460 lemma (in abelian_subgroup) a_setmult_closed:
461      "\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H"
462 by (rule normal.setmult_closed [OF a_normal,
463     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
465 lemma (in abelian_subgroup) a_setinv_closed:
466      "K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H"
467 by (rule normal.setinv_closed [OF a_normal,
468     folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])
470 lemma (in abelian_subgroup) a_rcosets_assoc:
471      "\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk>
472       \<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
473 by (rule normal.rcosets_assoc [OF a_normal,
474     folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
476 lemma (in abelian_subgroup) a_subgroup_in_rcosets:
477      "H \<in> a_rcosets H"
478 by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
479     folded A_RCOSETS_def, simplified monoid_record_simps])
481 lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
482      "M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H"
483 by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
484     folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])
486 theorem (in abelian_subgroup) a_factorgroup_is_group:
487   "group (G A_Mod H)"
488 by (rule normal.factorgroup_is_group [OF a_normal,
489     folded A_FactGroup_def, simplified monoid_record_simps])
491 text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in
492         a commutative group *}
493 theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
494   "comm_group (G A_Mod H)"
495 apply (intro comm_group.intro comm_monoid.intro) prefer 3
496   apply (rule a_factorgroup_is_group)
497  apply (rule group.axioms[OF a_factorgroup_is_group])
498 apply (rule comm_monoid_axioms.intro)
499 apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
500 apply (simp add: a_rcos_sum a_comm)
501 done
503 lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
506 lemma (in abelian_subgroup) a_inv_FactGroup:
507      "X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"
508 by (rule normal.inv_FactGroup [OF a_normal,
509     folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
511 text{*The coset map is a homomorphism from @{term G} to the quotient group
512   @{term "G Mod H"}*}
513 lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
514   "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
515 by (rule normal.r_coset_hom_Mod [OF a_normal,
516     folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
518 text {* The isomorphism theorems have been omitted from lifting, at
519   least for now *}
521 subsection{*The First Isomorphism Theorem*}
523 text{*The quotient by the kernel of a homomorphism is isomorphic to the
524   range of that homomorphism.*}
526 lemmas a_kernel_defs =
527   a_kernel_def kernel_def
529 lemma a_kernel_def':
530   "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
531 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
534 subsection {* Homomorphisms *}
536 lemma abelian_group_homI:
537   includes abelian_group G
538   includes abelian_group H
539   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
540                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
541   shows "abelian_group_hom G H h"
542 apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
543   apply (rule G.abelian_group_axioms)
544  apply (rule H.abelian_group_axioms)
545 apply (rule a_group_hom)
546 done
548 lemma (in abelian_group_hom) is_abelian_group_hom:
549   "abelian_group_hom G H h"
550 by (unfold_locales)
552 lemma (in abelian_group_hom) hom_add [simp]:
553   "[| x : carrier G; y : carrier G |]
554         ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
555 by (rule group_hom.hom_mult[OF a_group_hom,
556     simplified ring_record_simps])
558 lemma (in abelian_group_hom) hom_closed [simp]:
559   "x \<in> carrier G \<Longrightarrow> h x \<in> carrier H"
560 by (rule group_hom.hom_closed[OF a_group_hom,
561     simplified ring_record_simps])
563 lemma (in abelian_group_hom) zero_closed [simp]:
564   "h \<zero> \<in> carrier H"
565 by (rule group_hom.one_closed[OF a_group_hom,
566     simplified ring_record_simps])
568 lemma (in abelian_group_hom) hom_zero [simp]:
569   "h \<zero> = \<zero>\<^bsub>H\<^esub>"
570 by (rule group_hom.hom_one[OF a_group_hom,
571     simplified ring_record_simps])
573 lemma (in abelian_group_hom) a_inv_closed [simp]:
574   "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
575 by (rule group_hom.inv_closed[OF a_group_hom,
576     folded a_inv_def, simplified ring_record_simps])
578 lemma (in abelian_group_hom) hom_a_inv [simp]:
579   "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
580 by (rule group_hom.hom_inv[OF a_group_hom,
581     folded a_inv_def, simplified ring_record_simps])
583 lemma (in abelian_group_hom) additive_subgroup_a_kernel:
584   "additive_subgroup (a_kernel G H h) G"
585 apply (rule additive_subgroup.intro)
586 apply (rule group_hom.subgroup_kernel[OF a_group_hom,
587        folded a_kernel_def, simplified ring_record_simps])
588 done
590 text{*The kernel of a homomorphism is an abelian subgroup*}
591 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
592   "abelian_subgroup (a_kernel G H h) G"
593 apply (rule abelian_subgroupI)
594 apply (rule group_hom.normal_kernel[OF a_group_hom,
595        folded a_kernel_def, simplified ring_record_simps])
596 apply (simp add: G.a_comm)
597 done
599 lemma (in abelian_group_hom) A_FactGroup_nonempty:
600   assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
601   shows "X \<noteq> {}"
602 by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
603     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
605 lemma (in abelian_group_hom) FactGroup_contents_mem:
606   assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
607   shows "contents (hX) \<in> carrier H"
608 by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
609     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
611 lemma (in abelian_group_hom) A_FactGroup_hom:
612      "(\<lambda>X. contents (hX)) \<in> hom (G A_Mod (a_kernel G H h))
613           \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
614 by (rule group_hom.FactGroup_hom[OF a_group_hom,
615     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
617 lemma (in abelian_group_hom) A_FactGroup_inj_on:
618      "inj_on (\<lambda>X. contents (h  X)) (carrier (G A_Mod a_kernel G H h))"
619 by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
620     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
622 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
623 homomorphism from the quotient group*}
624 lemma (in abelian_group_hom) A_FactGroup_onto:
625   assumes h: "h  carrier G = carrier H"
626   shows "(\<lambda>X. contents (h  X))  carrier (G A_Mod a_kernel G H h) = carrier H"
627 by (rule group_hom.FactGroup_onto[OF a_group_hom,
628     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
630 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
631  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
632 theorem (in abelian_group_hom) A_FactGroup_iso:
633   "h  carrier G = carrier H
634    \<Longrightarrow> (\<lambda>X. contents (hX)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
635           (| carrier = carrier H, mult = add H, one = zero H |)"
636 by (rule group_hom.FactGroup_iso[OF a_group_hom,
637     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
639 section {* Lemmas Lifted from CosetExt.thy *}
641 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
643 subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
645 lemma (in additive_subgroup) a_Hcarr [simp]:
646   assumes hH: "h \<in> H"
647   shows "h \<in> carrier G"
648 by (rule subgroup.mem_carrier [OF a_subgroup,
649     simplified monoid_record_simps]) (rule hH)
652 subsection {* Lemmas for Right Cosets *}
654 lemma (in abelian_subgroup) a_elemrcos_carrier:
655   assumes acarr: "a \<in> carrier G"
656       and a': "a' \<in> H +> a"
657   shows "a' \<in> carrier G"
658 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
659     folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
661 lemma (in abelian_subgroup) a_rcos_const:
662   assumes hH: "h \<in> H"
663   shows "H +> h = H"
664 by (rule subgroup.rcos_const [OF a_subgroup a_group,
665     folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
667 lemma (in abelian_subgroup) a_rcos_module_imp:
668   assumes xcarr: "x \<in> carrier G"
669       and x'cos: "x' \<in> H +> x"
670   shows "(x' \<oplus> \<ominus>x) \<in> H"
671 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
672     folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
674 lemma (in abelian_subgroup) a_rcos_module_rev:
675   assumes "x \<in> carrier G" "x' \<in> carrier G"
676       and "(x' \<oplus> \<ominus>x) \<in> H"
677   shows "x' \<in> H +> x"
678 using assms
679 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
680     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
682 lemma (in abelian_subgroup) a_rcos_module:
683   assumes "x \<in> carrier G" "x' \<in> carrier G"
684   shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
685 using assms
686 by (rule subgroup.rcos_module [OF a_subgroup a_group,
687     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
689 --"variant"
690 lemma (in abelian_subgroup) a_rcos_module_minus:
691   includes ring G
692   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
693   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
694 proof -
695   from carr
696   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
697   with carr
698   show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
699     by (simp add: minus_eq)
700 qed
702 lemma (in abelian_subgroup) a_repr_independence':
703   assumes y: "y \<in> H +> x"
704       and xcarr: "x \<in> carrier G"
705   shows "H +> x = H +> y"
706   apply (rule a_repr_independence)
707     apply (rule y)
708    apply (rule xcarr)
709   apply (rule a_subgroup)
710   done
712 lemma (in abelian_subgroup) a_repr_independenceD:
713   assumes ycarr: "y \<in> carrier G"
714       and repr:  "H +> x = H +> y"
715   shows "y \<in> H +> x"
716 by (rule group.repr_independenceD [OF a_group a_subgroup,
717     folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
720 subsection {* Lemmas for the Set of Right Cosets *}
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])
729 subsection {* Addition of Subgroups *}
731 lemma (in abelian_monoid) set_add_closed:
732   assumes Acarr: "A \<subseteq> carrier G"
733       and Bcarr: "B \<subseteq> carrier G"
734   shows "A <+> B \<subseteq> carrier G"
735 by (rule monoid.set_mult_closed [OF a_monoid,
736     folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)