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