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 *)

     5

     6 theory AbelCoset

     7 imports Coset Ring

     8 begin

     9

    10

    11 subsection {* More Lifting from Groups to Abelian Groups *}

    12

    13 subsubsection {* Definitions *}

    14

    15 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come

    16   up with better syntax here *}

    17

    18 no_notation Plus (infixr "<+>" 65)

    19

    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>"

    23

    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>"

    27

    28 definition

    29   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)

    30   where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"

    31

    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>"

    35

    36 definition

    37   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)

    38   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"

    39

    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>"

    43

    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"

    48

    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"

    55

    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"

    61

    62 lemmas a_r_coset_defs =

    63   a_r_coset_def r_coset_def

    64

    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

    70

    71 lemmas a_l_coset_defs =

    72   a_l_coset_def l_coset_def

    73

    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

    79

    80 lemmas A_RCOSETS_defs =

    81   A_RCOSETS_def RCOSETS_def

    82

    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)

    88

    89 lemmas set_add_defs =

    90   set_add_def set_mult_def

    91

    92 lemma set_add_def':

    93   fixes G (structure)

    94   shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"

    95 unfolding set_add_defs

    96 by simp

    97

    98 lemmas A_SET_INV_defs =

    99   A_SET_INV_def SET_INV_def

   100

   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)

   106

   107

   108 subsubsection {* Cosets *}

   109

   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])

   115

   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])

   120

   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])

   126

   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])

   132

   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])

   137

   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])

   142

   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])

   147

   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])

   152

   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])

   157

   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])

   162

   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])

   167

   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])

   174

   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 *)

   182

   183

   184 subsubsection {* Subgroups *}

   185

   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>"

   189

   190 lemma (in additive_subgroup) is_additive_subgroup:

   191   shows "additive_subgroup H G"

   192 by (rule additive_subgroup_axioms)

   193

   194 lemma additive_subgroupI:

   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)

   199

   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])

   204

   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])

   209

   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])

   214

   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])

   219

   220

   221 subsubsection {* Additive subgroups are normal *}

   222

   223 text {* Every subgroup of an @{text "abelian_group"} is normal *}

   224

   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>"

   227

   228 lemma (in abelian_subgroup) is_abelian_subgroup:

   229   shows "abelian_subgroup H G"

   230 by (rule abelian_subgroup_axioms)

   231

   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)

   239

   240   show "abelian_subgroup H G"

   241   proof qed (simp add: a_comm)

   242 qed

   243

   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)

   254

   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

   268

   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

   278

   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])

   283

   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])

   288

   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])

   293

   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])

   301

   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])

   307

   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])

   312

   313

   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])

   318

   319

   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])

   324

   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])

   329

   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

   339

   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

   349

   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])

   354

   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])

   358

   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)

   364

   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])

   370

   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])

   376

   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])

   382

   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])

   388

   389

   390 subsubsection {* Congruence Relation *}

   391

   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])

   396

   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)

   402

   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])

   410

   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])

   415

   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])

   420

   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])

   425

   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])

   430

   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])

   436

   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],

   441     rule additive_subgroup.a_subgroup)

   442

   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)+

   449

   450

   451 subsubsection {* Factorization *}

   452

   453 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def

   454

   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)

   460

   461

   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])

   466

   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])

   471

   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])

   477

   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])

   482

   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])

   487

   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])

   492

   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

   504

   505 lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"

   506 by (simp add: A_FactGroup_def set_add_def)

   507

   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])

   512

   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])

   519

   520 text {* The isomorphism theorems have been omitted from lifting, at

   521   least for now *}

   522

   523 subsubsection{*The First Isomorphism Theorem*}

   524

   525 text{*The quotient by the kernel of a homomorphism is isomorphic to the

   526   range of that homomorphism.*}

   527

   528 lemmas a_kernel_defs =

   529   a_kernel_def kernel_def

   530

   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])

   534

   535

   536 subsubsection {* Homomorphisms *}

   537

   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

   553

   554 lemma (in abelian_group_hom) is_abelian_group_hom:

   555   "abelian_group_hom G H h"

   556   ..

   557

   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])

   563

   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])

   568

   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])

   573

   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])

   578

   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])

   583

   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])

   588

   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

   595

   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

   604

   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)

   610

   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)

   616

   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])

   622

   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])

   627

   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)

   635

   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])

   644

   645 subsubsection {* Cosets *}

   646

   647 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}

   648

   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)

   654

   655

   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')

   662

   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)

   668

   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)

   675

   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])

   683

   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])

   690

   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

   704

   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

   714

   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)

   721

   722

   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])

   727

   728

   729

   730 subsubsection {* Addition of Subgroups *}

   731

   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)

   738

   739 lemma (in abelian_group) add_additive_subgroups:

   740   assumes subH: "additive_subgroup H G"

   741       and subK: "additive_subgroup K G"

   742   shows "additive_subgroup (H <+> K) G"

   743 apply (rule additive_subgroup.intro)

   744 apply (unfold set_add_def)

   745 apply (intro comm_group.mult_subgroups)

   746   apply (rule a_comm_group)

   747  apply (rule additive_subgroup.a_subgroup[OF subH])

   748 apply (rule additive_subgroup.a_subgroup[OF subK])

   749 done

   750

   751 end