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