src/HOL/Algebra/AbelCoset.thy
 author wenzelm Mon Mar 17 22:34:23 2008 +0100 (2008-03-17) changeset 26310 f8a7fac36e13 parent 26203 9625f3579b48 child 27192 005d4b953fdc permissions -rw-r--r--
only one version of group.rcos_self;
     1 (*

     2   Title:     HOL/Algebra/AbelCoset.thy

     3   Id:        $Id$

     4   Author:    Stephan Hohe, TU Muenchen

     5 *)

     6

     7 theory AbelCoset

     8 imports Coset Ring

     9 begin

    10

    11

    12 section {* More Lifting from Groups to Abelian Groups *}

    13

    14 subsection {* Definitions *}

    15

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

    17   up with better syntax here *}

    18

    19 hide const Plus

    20

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

    24

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

    27

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

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

    30

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

    33

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

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

    36

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

    41

    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"

    47

    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"

    54

    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"

    58

    59 lemmas a_r_coset_defs =

    60   a_r_coset_def r_coset_def

    61

    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

    67

    68 lemmas a_l_coset_defs =

    69   a_l_coset_def l_coset_def

    70

    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

    76

    77 lemmas A_RCOSETS_defs =

    78   A_RCOSETS_def RCOSETS_def

    79

    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)

    85

    86 lemmas set_add_defs =

    87   set_add_def set_mult_def

    88

    89 lemma set_add_def':

    90   includes struct G

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

    92 unfolding set_add_defs

    93 by simp

    94

    95 lemmas A_SET_INV_defs =

    96   A_SET_INV_def SET_INV_def

    97

    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)

   103

   104

   105 subsection {* Cosets *}

   106

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

   112

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

   117

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

   123

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

   129

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

   134

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

   139

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

   144

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

   149

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

   154

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

   159

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

   164

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

   171

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

   179

   180

   181 subsection {* Subgroups *}

   182

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

   185

   186 lemma (in additive_subgroup) is_additive_subgroup:

   187   shows "additive_subgroup H G"

   188 by (rule additive_subgroup_axioms)

   189

   190 lemma additive_subgroupI:

   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)

   195

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

   200

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

   205

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

   210

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

   215

   216

   217 subsection {* Normal additive subgroups *}

   218

   219 subsubsection {* Definition of @{text "abelian_subgroup"} *}

   220

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

   222

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

   225

   226 lemma (in abelian_subgroup) is_abelian_subgroup:

   227   shows "abelian_subgroup H G"

   228 by (rule abelian_subgroup_axioms)

   229

   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)

   237

   238   show "abelian_subgroup H G"

   239   by (unfold_locales, simp add: a_comm)

   240 qed

   241

   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)

   252

   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

   266

   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

   276

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

   281

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

   286

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

   291

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

   299

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

   305

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

   310

   311

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

   316

   317

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

   322

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

   327

   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

   337

   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

   347

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

   352

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

   356

   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)

   362

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

   368

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

   374

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

   380

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

   386

   387

   388 subsection {* Congruence Relation *}

   389

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

   394

   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)

   400

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

   408

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

   413

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

   418

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

   423

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

   428

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

   434

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

   439     rule additive_subgroup.a_subgroup)

   440

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

   447

   448

   449 subsection {* Factorization *}

   450

   451 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def

   452

   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)

   458

   459

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

   464

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

   469

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

   475

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

   480

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

   485

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

   490

   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

   502

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

   504 by (simp add: A_FactGroup_def set_add_def)

   505

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

   510

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

   517

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

   519   least for now *}

   520

   521 subsection{*The First Isomorphism Theorem*}

   522

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

   524   range of that homomorphism.*}

   525

   526 lemmas a_kernel_defs =

   527   a_kernel_def kernel_def

   528

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

   532

   533

   534 subsection {* Homomorphisms *}

   535

   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

   547

   548 lemma (in abelian_group_hom) is_abelian_group_hom:

   549   "abelian_group_hom G H h"

   550 by (unfold_locales)

   551

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

   557

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

   562

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

   567

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

   572

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

   577

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

   582

   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

   589

   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

   598

   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)

   604

   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)

   610

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

   616

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

   621

   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)

   629

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

   638

   639 section {* Lemmas Lifted from CosetExt.thy *}

   640

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

   642

   643 subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}

   644

   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)

   650

   651

   652 subsection {* Lemmas for Right Cosets *}

   653

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

   660

   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)

   666

   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)

   673

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

   681

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

   688

   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

   701

   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

   711

   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)

   718

   719

   720 subsection {* Lemmas for the Set of Right Cosets *}

   721

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

   726

   727

   728

   729 subsection {* Addition of Subgroups *}

   730

   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)

   737

   738 lemma (in abelian_group) add_additive_subgroups:

   739   assumes subH: "additive_subgroup H G"

   740       and subK: "additive_subgroup K G"

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

   742 apply (rule additive_subgroup.intro)

   743 apply (unfold set_add_def)

   744 apply (intro comm_group.mult_subgroups)

   745   apply (rule a_comm_group)

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

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

   748 done

   749

   750 end