src/HOL/Algebra/Coset.thy
author paulson
Wed May 26 11:43:50 2004 +0200 (2004-05-26)
changeset 14803 f7557773cc87
parent 14761 28b5eb4a867f
child 14963 d584e32f7d46
permissions -rw-r--r--
more group isomorphisms
wenzelm@14706
     1
(*  Title:      HOL/Algebra/Coset.thy
paulson@13870
     2
    ID:         $Id$
paulson@13870
     3
    Author:     Florian Kammueller, with new proofs by L C Paulson
paulson@13870
     4
*)
paulson@13870
     5
paulson@14747
     6
header{*Cosets and Quotient Groups*}
paulson@13870
     7
paulson@13870
     8
theory Coset = Group + Exponent:
paulson@13870
     9
wenzelm@14666
    10
declare (in group) l_inv [simp] and r_inv [simp]
paulson@13870
    11
wenzelm@14651
    12
constdefs (structure G)
paulson@14747
    13
  r_coset    :: "[_, 'a set, 'a] => 'a set"    (infixl "#>\<index>" 60)
paulson@14747
    14
  "H #> a == (% x. x \<otimes> a) ` H"
paulson@13870
    15
paulson@14747
    16
  l_coset    :: "[_, 'a, 'a set] => 'a set"    (infixl "<#\<index>" 60)
paulson@14747
    17
  "a <# H == (% x. a \<otimes> x) ` H"
paulson@13870
    18
wenzelm@14651
    19
  rcosets  :: "[_, 'a set] => ('a set)set"
wenzelm@14666
    20
  "rcosets G H == r_coset G H ` (carrier G)"
paulson@13870
    21
paulson@14747
    22
  set_mult  :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)
paulson@14747
    23
  "H <#> K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
paulson@13870
    24
wenzelm@14651
    25
  set_inv   :: "[_,'a set] => 'a set"
wenzelm@14666
    26
  "set_inv G H == m_inv G ` H"
paulson@13870
    27
wenzelm@14651
    28
  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
wenzelm@14666
    29
  "normal H G == subgroup H G &
paulson@13870
    30
                  (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
paulson@13870
    31
paulson@13870
    32
syntax (xsymbols)
paulson@14747
    33
  normal :: "['a set, ('a,'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)
paulson@13870
    34
paulson@13870
    35
paulson@14803
    36
subsection {*Basic Properties of Cosets*}
paulson@13870
    37
paulson@14747
    38
lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
paulson@14747
    39
by (auto simp add: r_coset_def)
paulson@13870
    40
paulson@14747
    41
lemma (in group) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
paulson@14747
    42
by (auto simp add: l_coset_def)
paulson@13870
    43
paulson@14747
    44
lemma (in group) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
paulson@14747
    45
by (auto simp add: rcosets_def)
paulson@13870
    46
paulson@14747
    47
lemma (in group) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
paulson@14747
    48
by (simp add: set_mult_def image_def)
paulson@13870
    49
paulson@14747
    50
lemma (in group) coset_mult_assoc:
paulson@14747
    51
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
paulson@13870
    52
      ==> (M #> g) #> h = M #> (g \<otimes> h)"
paulson@14747
    53
by (force simp add: r_coset_def m_assoc)
paulson@13870
    54
paulson@14747
    55
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
paulson@14747
    56
by (force simp add: r_coset_def)
paulson@13870
    57
paulson@14747
    58
lemma (in group) coset_mult_inv1:
wenzelm@14666
    59
     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
paulson@14747
    60
         M \<subseteq> carrier G |] ==> M #> x = M #> y"
paulson@13870
    61
apply (erule subst [of concl: "%z. M #> x = z #> y"])
paulson@13870
    62
apply (simp add: coset_mult_assoc m_assoc)
paulson@13870
    63
done
paulson@13870
    64
paulson@14747
    65
lemma (in group) coset_mult_inv2:
paulson@14747
    66
     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
paulson@13870
    67
      ==> M #> (x \<otimes> (inv y)) = M "
paulson@13870
    68
apply (simp add: coset_mult_assoc [symmetric])
paulson@13870
    69
apply (simp add: coset_mult_assoc)
paulson@13870
    70
done
paulson@13870
    71
paulson@14747
    72
lemma (in group) coset_join1:
paulson@14747
    73
     "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
paulson@13870
    74
apply (erule subst)
paulson@13870
    75
apply (simp add: r_coset_eq)
paulson@13870
    76
apply (blast intro: l_one subgroup.one_closed)
paulson@13870
    77
done
paulson@13870
    78
paulson@14747
    79
lemma (in group) solve_equation:
paulson@13870
    80
    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
paulson@13870
    81
apply (rule bexI [of _ "y \<otimes> (inv x)"])
wenzelm@14666
    82
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
paulson@13870
    83
                      subgroup.subset [THEN subsetD])
paulson@13870
    84
done
paulson@13870
    85
paulson@14747
    86
lemma (in group) coset_join2:
paulson@13870
    87
     "[| x \<in> carrier G;  subgroup H G;  x\<in>H |] ==> H #> x = H"
paulson@13870
    88
by (force simp add: subgroup.m_closed r_coset_eq solve_equation)
paulson@13870
    89
paulson@14747
    90
lemma (in group) r_coset_subset_G:
paulson@14747
    91
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
paulson@14747
    92
by (auto simp add: r_coset_def)
paulson@13870
    93
paulson@14747
    94
lemma (in group) rcosI:
paulson@14747
    95
     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
paulson@14747
    96
by (auto simp add: r_coset_def)
paulson@13870
    97
paulson@14747
    98
lemma (in group) setrcosI:
paulson@14747
    99
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
paulson@13870
   100
by (auto simp add: setrcos_eq)
paulson@13870
   101
paulson@13870
   102
paulson@13870
   103
text{*Really needed?*}
paulson@14747
   104
lemma (in group) transpose_inv:
wenzelm@14666
   105
     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
paulson@13870
   106
      ==> (inv x) \<otimes> z = y"
paulson@13870
   107
by (force simp add: m_assoc [symmetric])
paulson@13870
   108
paulson@14747
   109
lemma (in group) repr_independence:
paulson@13870
   110
     "[| y \<in> H #> x;  x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
wenzelm@14666
   111
by (auto simp add: r_coset_eq m_assoc [symmetric]
paulson@13870
   112
                   subgroup.subset [THEN subsetD]
paulson@13870
   113
                   subgroup.m_closed solve_equation)
paulson@13870
   114
paulson@14747
   115
lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
paulson@13870
   116
apply (simp add: r_coset_eq)
wenzelm@14666
   117
apply (blast intro: l_one subgroup.subset [THEN subsetD]
paulson@13870
   118
                    subgroup.one_closed)
paulson@13870
   119
done
paulson@13870
   120
paulson@13870
   121
wenzelm@14666
   122
subsection {* Normal subgroups *}
paulson@13870
   123
paulson@13870
   124
lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
paulson@13870
   125
by (simp add: normal_def)
paulson@13870
   126
paulson@14747
   127
lemma (in group) normal_inv_op_closed1:
paulson@13870
   128
     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
paulson@14747
   129
apply (auto simp add: l_coset_def r_coset_def normal_def)
wenzelm@14666
   130
apply (drule bspec, assumption)
paulson@13870
   131
apply (drule equalityD1 [THEN subsetD], blast, clarify)
paulson@13870
   132
apply (simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@13870
   133
apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
paulson@13870
   134
done
paulson@13870
   135
paulson@14747
   136
lemma (in group) normal_inv_op_closed2:
paulson@13870
   137
     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
wenzelm@14666
   138
apply (drule normal_inv_op_closed1 [of H "(inv x)"])
paulson@13870
   139
apply auto
paulson@13870
   140
done
paulson@13870
   141
paulson@14747
   142
text{*Alternative characterization of normal subgroups*}
paulson@14747
   143
lemma (in group) normal_inv_iff:
paulson@14747
   144
     "(N \<lhd> G) = 
paulson@14747
   145
      (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
paulson@14747
   146
      (is "_ = ?rhs")
paulson@14747
   147
proof
paulson@14747
   148
  assume N: "N \<lhd> G"
paulson@14747
   149
  show ?rhs
paulson@14747
   150
    by (blast intro: N normal_imp_subgroup normal_inv_op_closed2) 
paulson@14747
   151
next
paulson@14747
   152
  assume ?rhs
paulson@14747
   153
  hence sg: "subgroup N G" 
paulson@14747
   154
    and closed: "!!x. x\<in>carrier G ==> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
paulson@14747
   155
  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
paulson@14747
   156
  show "N \<lhd> G"
paulson@14747
   157
  proof (simp add: sg normal_def l_coset_def r_coset_def, clarify)
paulson@14747
   158
    fix x
paulson@14747
   159
    assume x: "x \<in> carrier G"
paulson@14747
   160
    show "(\<lambda>n. n \<otimes> x) ` N = op \<otimes> x ` N"
paulson@14747
   161
    proof
paulson@14747
   162
      show "(\<lambda>n. n \<otimes> x) ` N \<subseteq> op \<otimes> x ` N"
paulson@14747
   163
      proof clarify
paulson@14747
   164
        fix n
paulson@14747
   165
        assume n: "n \<in> N" 
paulson@14747
   166
        show "n \<otimes> x \<in> op \<otimes> x ` N"
paulson@14747
   167
        proof 
paulson@14747
   168
          show "n \<otimes> x = x \<otimes> (inv x \<otimes> n \<otimes> x)"
paulson@14747
   169
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
paulson@14747
   170
          with closed [of "inv x"]
paulson@14747
   171
          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
paulson@14747
   172
        qed
paulson@14747
   173
      qed
paulson@14747
   174
    next
paulson@14747
   175
      show "op \<otimes> x ` N \<subseteq> (\<lambda>n. n \<otimes> x) ` N" 
paulson@14747
   176
      proof clarify
paulson@14747
   177
        fix n
paulson@14747
   178
        assume n: "n \<in> N" 
paulson@14747
   179
        show "x \<otimes> n \<in> (\<lambda>n. n \<otimes> x) ` N"
paulson@14747
   180
        proof 
paulson@14747
   181
          show "x \<otimes> n = (x \<otimes> n \<otimes> inv x) \<otimes> x"
paulson@14747
   182
            by (simp add: x n m_assoc sb [THEN subsetD])
paulson@14747
   183
          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
paulson@14747
   184
        qed
paulson@14747
   185
      qed
paulson@14747
   186
    qed
paulson@14747
   187
  qed
paulson@14747
   188
qed
paulson@13870
   189
paulson@14803
   190
subsection{*More Properties of Cosets*}
paulson@14803
   191
paulson@14747
   192
lemma (in group) lcos_m_assoc:
paulson@14747
   193
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
paulson@14747
   194
      ==> g <# (h <# M) = (g \<otimes> h) <# M"
paulson@14747
   195
by (force simp add: l_coset_def m_assoc)
paulson@13870
   196
paulson@14747
   197
lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
paulson@14747
   198
by (force simp add: l_coset_def)
paulson@13870
   199
paulson@14747
   200
lemma (in group) l_coset_subset_G:
paulson@14747
   201
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
paulson@14747
   202
by (auto simp add: l_coset_def subsetD)
paulson@14747
   203
paulson@14747
   204
lemma (in group) l_coset_swap:
paulson@14530
   205
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
paulson@14530
   206
proof (simp add: l_coset_eq)
wenzelm@14666
   207
  assume "\<exists>h\<in>H. x \<otimes> h = y"
wenzelm@14666
   208
    and x: "x \<in> carrier G"
paulson@14530
   209
    and sb: "subgroup H G"
paulson@14530
   210
  then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
paulson@14530
   211
  show "\<exists>h\<in>H. y \<otimes> h = x"
paulson@14530
   212
  proof
paulson@14530
   213
    show "y \<otimes> inv h' = x" using h' x sb
paulson@14530
   214
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@14530
   215
    show "inv h' \<in> H" using h' sb
paulson@14530
   216
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
paulson@14530
   217
  qed
paulson@14530
   218
qed
paulson@14530
   219
paulson@14747
   220
lemma (in group) l_coset_carrier:
paulson@14530
   221
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
paulson@14747
   222
by (auto simp add: l_coset_def m_assoc
paulson@14530
   223
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   224
paulson@14747
   225
lemma (in group) l_repr_imp_subset:
wenzelm@14666
   226
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
paulson@14530
   227
  shows "y <# H \<subseteq> x <# H"
paulson@14530
   228
proof -
paulson@14530
   229
  from y
paulson@14747
   230
  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
paulson@14530
   231
  thus ?thesis using x sb
paulson@14747
   232
    by (auto simp add: l_coset_def m_assoc
paulson@14530
   233
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   234
qed
paulson@14530
   235
paulson@14747
   236
lemma (in group) l_repr_independence:
wenzelm@14666
   237
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
paulson@14530
   238
  shows "x <# H = y <# H"
wenzelm@14666
   239
proof
paulson@14530
   240
  show "x <# H \<subseteq> y <# H"
wenzelm@14666
   241
    by (rule l_repr_imp_subset,
paulson@14530
   242
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
wenzelm@14666
   243
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
paulson@14530
   244
qed
paulson@13870
   245
paulson@14747
   246
lemma (in group) setmult_subset_G:
paulson@14747
   247
     "[| H \<subseteq> carrier G; K \<subseteq> carrier G |] ==> H <#> K \<subseteq> carrier G"
paulson@13870
   248
by (auto simp add: set_mult_eq subsetD)
paulson@13870
   249
paulson@14747
   250
lemma (in group) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
paulson@13870
   251
apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
paulson@13870
   252
apply (rule_tac x = x in bexI)
paulson@13870
   253
apply (rule bexI [of _ "\<one>"])
wenzelm@14666
   254
apply (auto simp add: subgroup.m_closed subgroup.one_closed
paulson@13870
   255
                      r_one subgroup.subset [THEN subsetD])
paulson@13870
   256
done
paulson@13870
   257
paulson@13870
   258
paulson@14747
   259
subsubsection {* Set of inverses of an @{text r_coset}. *}
wenzelm@14666
   260
paulson@14747
   261
lemma (in group) rcos_inv:
paulson@13870
   262
  assumes normalHG: "H <| G"
paulson@14747
   263
      and x:     "x \<in> carrier G"
paulson@13870
   264
  shows "set_inv G (H #> x) = H #> (inv x)"
paulson@13870
   265
proof -
paulson@14747
   266
  have H_subset: "H \<subseteq> carrier G"
paulson@13870
   267
    by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
paulson@13870
   268
  show ?thesis
paulson@13870
   269
  proof (auto simp add: r_coset_eq image_def set_inv_def)
paulson@13870
   270
    fix h
paulson@13870
   271
    assume "h \<in> H"
paulson@13870
   272
      hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
paulson@14747
   273
        by (simp add: x m_assoc inv_mult_group H_subset [THEN subsetD])
wenzelm@14666
   274
      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
paulson@13870
   275
       using prems
wenzelm@14666
   276
        by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
wenzelm@14666
   277
                         subgroup.m_inv_closed)
paulson@13870
   278
  next
paulson@13870
   279
    fix h
paulson@13870
   280
    assume "h \<in> H"
paulson@13870
   281
      hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
paulson@14747
   282
        by (simp add: x m_assoc H_subset [THEN subsetD])
paulson@13870
   283
      hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
paulson@13870
   284
       using prems
wenzelm@14666
   285
        by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
wenzelm@14666
   286
            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
wenzelm@14666
   287
                         subgroup.m_inv_closed)
paulson@13870
   288
      thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
paulson@13870
   289
  qed
paulson@13870
   290
qed
paulson@13870
   291
paulson@14747
   292
lemma (in group) rcos_inv2:
paulson@13870
   293
     "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
paulson@13870
   294
apply (simp add: setrcos_eq, clarify)
paulson@13870
   295
apply (subgoal_tac "x : carrier G")
paulson@13870
   296
 prefer 2
wenzelm@14666
   297
 apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
paulson@13870
   298
apply (drule repr_independence)
paulson@13870
   299
  apply assumption
paulson@13870
   300
 apply (erule normal_imp_subgroup)
paulson@13870
   301
apply (simp add: rcos_inv)
paulson@13870
   302
done
paulson@13870
   303
paulson@13870
   304
paulson@14803
   305
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
wenzelm@14666
   306
paulson@14747
   307
lemma (in group) setmult_rcos_assoc:
paulson@14747
   308
     "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
paulson@13870
   309
      ==> H <#> (K #> x) = (H <#> K) #> x"
paulson@14747
   310
apply (auto simp add: r_coset_def set_mult_def)
paulson@13870
   311
apply (force simp add: m_assoc)+
paulson@13870
   312
done
paulson@13870
   313
paulson@14747
   314
lemma (in group) rcos_assoc_lcos:
paulson@14747
   315
     "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
paulson@13870
   316
      ==> (H #> x) <#> K = H <#> (x <# K)"
paulson@14747
   317
apply (auto simp add: r_coset_def l_coset_def set_mult_def Sigma_def image_def)
paulson@13870
   318
apply (force intro!: exI bexI simp add: m_assoc)+
paulson@13870
   319
done
paulson@13870
   320
paulson@14747
   321
lemma (in group) rcos_mult_step1:
wenzelm@14666
   322
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
paulson@13870
   323
      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
paulson@13870
   324
by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
paulson@13870
   325
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
paulson@13870
   326
paulson@14747
   327
lemma (in group) rcos_mult_step2:
wenzelm@14666
   328
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
paulson@13870
   329
      ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
paulson@14747
   330
by (simp add: normal_def)
paulson@13870
   331
paulson@14747
   332
lemma (in group) rcos_mult_step3:
wenzelm@14666
   333
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
paulson@13870
   334
      ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
paulson@13870
   335
by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
paulson@13870
   336
              setmult_subset_G  subgroup_mult_id
paulson@13870
   337
              subgroup.subset normal_imp_subgroup)
paulson@13870
   338
paulson@14747
   339
lemma (in group) rcos_sum:
wenzelm@14666
   340
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
paulson@13870
   341
      ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
paulson@13870
   342
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
paulson@13870
   343
paulson@14747
   344
lemma (in group) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
wenzelm@14666
   345
  -- {* generalizes @{text subgroup_mult_id} *}
wenzelm@14666
   346
  by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
wenzelm@14666
   347
    setmult_rcos_assoc subgroup_mult_id)
paulson@13870
   348
paulson@13870
   349
paulson@14803
   350
subsubsection{*Two distinct right cosets are disjoint*}
paulson@14803
   351
paulson@14803
   352
lemma (in group) rcos_equation:
paulson@14803
   353
     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
paulson@14803
   354
        h \<in> H;  ha \<in> H;  hb \<in> H|]
paulson@14803
   355
      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
paulson@14803
   356
apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
paulson@14803
   357
apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
paulson@14803
   358
apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
paulson@14803
   359
done
paulson@14803
   360
paulson@14803
   361
lemma (in group) rcos_disjoint:
paulson@14803
   362
     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
paulson@14803
   363
apply (simp add: setrcos_eq r_coset_eq)
paulson@14803
   364
apply (blast intro: rcos_equation sym)
paulson@14803
   365
done
paulson@14803
   366
paulson@14803
   367
paulson@14803
   368
subsection {*Order of a Group and Lagrange's Theorem*}
paulson@14803
   369
paulson@14803
   370
constdefs
paulson@14803
   371
  order :: "('a, 'b) semigroup_scheme => nat"
paulson@14803
   372
  "order S == card (carrier S)"
paulson@13870
   373
paulson@14747
   374
lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
paulson@13870
   375
apply (rule equalityI)
wenzelm@14666
   376
apply (force simp add: subgroup.subset [THEN subsetD]
paulson@14747
   377
                       setrcos_eq r_coset_def)
paulson@13870
   378
apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
paulson@13870
   379
done
paulson@13870
   380
paulson@14747
   381
lemma (in group) cosets_finite:
paulson@14747
   382
     "[| c \<in> rcosets G H;  H \<subseteq> carrier G;  finite (carrier G) |] ==> finite c"
paulson@13870
   383
apply (auto simp add: setrcos_eq)
paulson@13870
   384
apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   385
done
paulson@13870
   386
paulson@14747
   387
text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
paulson@14747
   388
lemma (in group) inj_on_f:
paulson@13870
   389
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
paulson@13870
   390
apply (rule inj_onI)
paulson@13870
   391
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
paulson@13870
   392
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
paulson@13870
   393
apply (simp add: subsetD)
paulson@13870
   394
done
paulson@13870
   395
paulson@14747
   396
lemma (in group) inj_on_g:
paulson@13870
   397
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
paulson@13870
   398
by (force simp add: inj_on_def subsetD)
paulson@13870
   399
paulson@14747
   400
lemma (in group) card_cosets_equal:
paulson@14747
   401
     "[| c \<in> rcosets G H;  H \<subseteq> carrier G; finite(carrier G) |]
paulson@13870
   402
      ==> card c = card H"
paulson@13870
   403
apply (auto simp add: setrcos_eq)
paulson@13870
   404
apply (rule card_bij_eq)
wenzelm@14666
   405
     apply (rule inj_on_f, assumption+)
paulson@14747
   406
    apply (force simp add: m_assoc subsetD r_coset_def)
wenzelm@14666
   407
   apply (rule inj_on_g, assumption+)
paulson@14747
   408
  apply (force simp add: m_assoc subsetD r_coset_def)
paulson@13870
   409
 txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
paulson@13870
   410
 apply (simp add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   411
apply (blast intro: finite_subset)
paulson@13870
   412
done
paulson@13870
   413
paulson@14747
   414
lemma (in group) setrcos_subset_PowG:
paulson@14747
   415
     "subgroup H G  ==> rcosets G H \<subseteq> Pow(carrier G)"
paulson@13870
   416
apply (simp add: setrcos_eq)
paulson@13870
   417
apply (blast dest: r_coset_subset_G subgroup.subset)
paulson@13870
   418
done
paulson@13870
   419
paulson@14803
   420
paulson@14803
   421
theorem (in group) lagrange:
paulson@14803
   422
     "[| finite(carrier G); subgroup H G |]
paulson@14803
   423
      ==> card(rcosets G H) * card(H) = order(G)"
paulson@14803
   424
apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
paulson@14803
   425
apply (subst mult_commute)
paulson@14803
   426
apply (rule card_partition)
paulson@14803
   427
   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
paulson@14803
   428
  apply (simp add: setrcos_part_G)
paulson@14803
   429
 apply (simp add: card_cosets_equal subgroup.subset)
paulson@14803
   430
apply (simp add: rcos_disjoint)
paulson@14803
   431
done
paulson@14803
   432
paulson@14803
   433
paulson@14747
   434
subsection {*Quotient Groups: Factorization of a Group*}
paulson@13870
   435
paulson@13870
   436
constdefs
ballarin@13936
   437
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
paulson@14803
   438
     (infixl "Mod" 65)
paulson@14747
   439
    --{*Actually defined for groups rather than monoids*}
wenzelm@14666
   440
  "FactGroup G H ==
paulson@14803
   441
    (| carrier = rcosets G H, mult = set_mult G, one = H |)"
paulson@14747
   442
paulson@14747
   443
lemma (in group) setmult_closed:
wenzelm@14666
   444
     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
paulson@13870
   445
      ==> K1 <#> K2 \<in> rcosets G H"
wenzelm@14666
   446
by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
paulson@13870
   447
                   rcos_sum setrcos_eq)
paulson@13870
   448
ballarin@13889
   449
lemma (in group) setinv_closed:
ballarin@13889
   450
     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
paulson@14747
   451
by (auto simp add: normal_imp_subgroup
paulson@14747
   452
                   subgroup.subset rcos_inv
paulson@14747
   453
                   setrcos_eq)
ballarin@13889
   454
paulson@14747
   455
lemma (in group) setrcos_assoc:
wenzelm@14666
   456
     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
paulson@13870
   457
      ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
wenzelm@14666
   458
by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
paulson@13870
   459
                   subgroup.subset m_assoc)
paulson@13870
   460
ballarin@13889
   461
lemma (in group) subgroup_in_rcosets:
ballarin@13889
   462
  "subgroup H G ==> H \<in> rcosets G H"
ballarin@13889
   463
proof -
ballarin@13889
   464
  assume sub: "subgroup H G"
ballarin@13889
   465
  have "r_coset G H \<one> = H"
paulson@14747
   466
    by (rule coset_join2)
paulson@14747
   467
       (auto intro: sub subgroup.one_closed)
ballarin@13889
   468
  then show ?thesis
paulson@14747
   469
    by (auto simp add: setrcos_eq)
ballarin@13889
   470
qed
ballarin@13889
   471
paulson@14747
   472
lemma (in group) setrcos_inv_mult_group_eq:
paulson@13870
   473
     "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
wenzelm@14666
   474
by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
paulson@13870
   475
                   subgroup.subset)
ballarin@13940
   476
(*
ballarin@13889
   477
lemma (in group) factorgroup_is_magma:
ballarin@13889
   478
  "H <| G ==> magma (G Mod H)"
ballarin@13889
   479
  by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
ballarin@13889
   480
ballarin@13889
   481
lemma (in group) factorgroup_semigroup_axioms:
ballarin@13889
   482
  "H <| G ==> semigroup_axioms (G Mod H)"
ballarin@13889
   483
  by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
ballarin@13889
   484
    coset.setmult_closed [OF is_coset])
ballarin@13940
   485
*)
ballarin@13889
   486
theorem (in group) factorgroup_is_group:
ballarin@13889
   487
  "H <| G ==> group (G Mod H)"
wenzelm@14666
   488
apply (simp add: FactGroup_def)
ballarin@13936
   489
apply (rule groupI)
paulson@14747
   490
    apply (simp add: setmult_closed)
ballarin@13936
   491
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
paulson@14747
   492
  apply (simp add: restrictI setmult_closed setrcos_assoc)
ballarin@13889
   493
 apply (simp add: normal_imp_subgroup
paulson@14747
   494
                  subgroup_in_rcosets setrcos_mult_eq)
paulson@14747
   495
apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
ballarin@13889
   496
done
ballarin@13889
   497
paulson@14803
   498
lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
paulson@14803
   499
  by (simp add: FactGroup_def) 
paulson@14803
   500
paulson@14747
   501
lemma (in group) inv_FactGroup:
paulson@14747
   502
     "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
paulson@14747
   503
apply (rule group.inv_equality [OF factorgroup_is_group]) 
paulson@14761
   504
apply (simp_all add: FactGroup_def setinv_closed setrcos_inv_mult_group_eq)
paulson@14747
   505
done
paulson@14747
   506
paulson@14747
   507
text{*The coset map is a homomorphism from @{term G} to the quotient group
paulson@14747
   508
  @{term "G Mod N"}*}
paulson@14747
   509
lemma (in group) r_coset_hom_Mod:
paulson@14747
   510
  assumes N: "N <| G"
paulson@14747
   511
  shows "(r_coset G N) \<in> hom G (G Mod N)"
paulson@14761
   512
by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N) 
paulson@14747
   513
paulson@14803
   514
paulson@14803
   515
subsection{*Quotienting by the Kernel of a Homomorphism*}
paulson@14803
   516
paulson@14803
   517
constdefs
paulson@14803
   518
  kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme => 
paulson@14803
   519
             ('a => 'b) => 'a set" 
paulson@14803
   520
    --{*the kernel of a homomorphism*}
paulson@14803
   521
  "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
paulson@14803
   522
paulson@14803
   523
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
paulson@14803
   524
apply (rule group.subgroupI) 
paulson@14803
   525
apply (auto simp add: kernel_def group.intro prems) 
paulson@14803
   526
done
paulson@14803
   527
paulson@14803
   528
text{*The kernel of a homomorphism is a normal subgroup*}
paulson@14803
   529
lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
paulson@14803
   530
apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
paulson@14803
   531
apply (simp add: kernel_def)  
paulson@14803
   532
done
paulson@14803
   533
paulson@14803
   534
lemma (in group_hom) FactGroup_nonempty:
paulson@14803
   535
  assumes X: "X \<in> carrier (G Mod kernel G H h)"
paulson@14803
   536
  shows "X \<noteq> {}"
paulson@14803
   537
proof -
paulson@14803
   538
  from X
paulson@14803
   539
  obtain g where "g \<in> carrier G" 
paulson@14803
   540
             and "X = kernel G H h #> g"
paulson@14803
   541
    by (auto simp add: FactGroup_def rcosets_def)
paulson@14803
   542
  thus ?thesis 
paulson@14803
   543
   by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
paulson@14803
   544
qed
paulson@14803
   545
paulson@14803
   546
paulson@14803
   547
lemma (in group_hom) FactGroup_contents_mem:
paulson@14803
   548
  assumes X: "X \<in> carrier (G Mod (kernel G H h))"
paulson@14803
   549
  shows "contents (h`X) \<in> carrier H"
paulson@14803
   550
proof -
paulson@14803
   551
  from X
paulson@14803
   552
  obtain g where g: "g \<in> carrier G" 
paulson@14803
   553
             and "X = kernel G H h #> g"
paulson@14803
   554
    by (auto simp add: FactGroup_def rcosets_def)
paulson@14803
   555
  hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
paulson@14803
   556
  thus ?thesis by (auto simp add: g)
paulson@14803
   557
qed
paulson@14803
   558
paulson@14803
   559
lemma (in group_hom) FactGroup_hom:
paulson@14803
   560
     "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
paulson@14803
   561
proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
paulson@14803
   562
  fix X and X'
paulson@14803
   563
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
paulson@14803
   564
     and X': "X' \<in> carrier (G Mod kernel G H h)"
paulson@14803
   565
  then
paulson@14803
   566
  obtain g and g'
paulson@14803
   567
           where "g \<in> carrier G" and "g' \<in> carrier G" 
paulson@14803
   568
             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
paulson@14803
   569
    by (auto simp add: FactGroup_def rcosets_def)
paulson@14803
   570
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
paulson@14803
   571
    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
paulson@14803
   572
    by (force simp add: kernel_def r_coset_def image_def)+
paulson@14803
   573
  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
paulson@14803
   574
    by (auto dest!: FactGroup_nonempty
paulson@14803
   575
             simp add: set_mult_def image_eq_UN 
paulson@14803
   576
                       subsetD [OF Xsub] subsetD [OF X'sub]) 
paulson@14803
   577
  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
paulson@14803
   578
    by (simp add: all image_eq_UN FactGroup_nonempty X X')  
paulson@14803
   579
qed
paulson@14803
   580
paulson@14803
   581
text{*Lemma for the following injectivity result*}
paulson@14803
   582
lemma (in group_hom) FactGroup_subset:
paulson@14803
   583
     "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
paulson@14803
   584
      ==>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
paulson@14803
   585
apply (clarsimp simp add: kernel_def r_coset_def image_def);
paulson@14803
   586
apply (rename_tac y)  
paulson@14803
   587
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
paulson@14803
   588
apply (simp add: G.m_assoc); 
paulson@14803
   589
done
paulson@14803
   590
paulson@14803
   591
lemma (in group_hom) FactGroup_inj_on:
paulson@14803
   592
     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
paulson@14803
   593
proof (simp add: inj_on_def, clarify) 
paulson@14803
   594
  fix X and X'
paulson@14803
   595
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
paulson@14803
   596
     and X': "X' \<in> carrier (G Mod kernel G H h)"
paulson@14803
   597
  then
paulson@14803
   598
  obtain g and g'
paulson@14803
   599
           where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
paulson@14803
   600
              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
paulson@14803
   601
    by (auto simp add: FactGroup_def rcosets_def)
paulson@14803
   602
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
paulson@14803
   603
    by (force simp add: kernel_def r_coset_def image_def)+
paulson@14803
   604
  assume "contents (h ` X) = contents (h ` X')"
paulson@14803
   605
  hence h: "h g = h g'"
paulson@14803
   606
    by (simp add: image_eq_UN all FactGroup_nonempty X X') 
paulson@14803
   607
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
paulson@14803
   608
qed
paulson@14803
   609
paulson@14803
   610
text{*If the homomorphism @{term h} is onto @{term H}, then so is the
paulson@14803
   611
homomorphism from the quotient group*}
paulson@14803
   612
lemma (in group_hom) FactGroup_onto:
paulson@14803
   613
  assumes h: "h ` carrier G = carrier H"
paulson@14803
   614
  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
paulson@14803
   615
proof
paulson@14803
   616
  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
paulson@14803
   617
    by (auto simp add: FactGroup_contents_mem)
paulson@14803
   618
  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
paulson@14803
   619
  proof
paulson@14803
   620
    fix y
paulson@14803
   621
    assume y: "y \<in> carrier H"
paulson@14803
   622
    with h obtain g where g: "g \<in> carrier G" "h g = y"
paulson@14803
   623
      by (blast elim: equalityE); 
paulson@14803
   624
    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
paulson@14803
   625
      by (auto simp add: y kernel_def r_coset_def) 
paulson@14803
   626
    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
paulson@14803
   627
      by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
paulson@14803
   628
  qed
paulson@14803
   629
qed
paulson@14803
   630
paulson@14803
   631
paulson@14803
   632
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
paulson@14803
   633
 quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
paulson@14803
   634
theorem (in group_hom) FactGroup_iso:
paulson@14803
   635
  "h ` carrier G = carrier H
paulson@14803
   636
   \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
paulson@14803
   637
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
paulson@14803
   638
              FactGroup_onto) 
paulson@14803
   639
paulson@13870
   640
end