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