src/HOL/Algebra/Coset.thy
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 32960 69916a850301
child 35416 d8d7d1b785af
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     1
(*  Title:      HOL/Algebra/Coset.thy
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
     2
    Author:     Florian Kammueller, with new proofs by L C Paulson, and
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
     3
                Stephan Hohe
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     4
*)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     5
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27698
diff changeset
     6
theory Coset imports Group begin
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     7
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
     8
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
     9
section {*Cosets and Quotient Groups*}
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    10
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14530
diff changeset
    11
constdefs (structure G)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    12
  r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    13
  "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    14
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    15
  l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    16
  "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    17
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    18
  RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    19
  "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    20
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    21
  set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    22
  "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    23
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    24
  SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    25
  "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    26
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    27
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    28
locale normal = subgroup + group +
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    29
  assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    30
19380
b808efaa5828 tuned syntax/abbreviations;
wenzelm
parents: 16417
diff changeset
    31
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20318
diff changeset
    32
  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
19380
b808efaa5828 tuned syntax/abbreviations;
wenzelm
parents: 16417
diff changeset
    33
  "H \<lhd> G \<equiv> normal H G"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    34
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    35
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
    36
subsection {*Basic Properties of Cosets*}
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    37
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    38
lemma (in group) coset_mult_assoc:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    39
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    40
      ==> (M #> g) #> h = M #> (g \<otimes> h)"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    41
by (force simp add: r_coset_def m_assoc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    42
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    43
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    44
by (force simp add: r_coset_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    45
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    46
lemma (in group) coset_mult_inv1:
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    47
     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    48
         M \<subseteq> carrier G |] ==> M #> x = M #> y"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    49
apply (erule subst [of concl: "%z. M #> x = z #> y"])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    50
apply (simp add: coset_mult_assoc m_assoc)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    51
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    52
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    53
lemma (in group) coset_mult_inv2:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    54
     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    55
      ==> M #> (x \<otimes> (inv y)) = M "
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    56
apply (simp add: coset_mult_assoc [symmetric])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    57
apply (simp add: coset_mult_assoc)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    58
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    59
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    60
lemma (in group) coset_join1:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    61
     "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    62
apply (erule subst)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    63
apply (simp add: r_coset_def)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    64
apply (blast intro: l_one subgroup.one_closed sym)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    65
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    66
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    67
lemma (in group) solve_equation:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    68
    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    69
apply (rule bexI [of _ "y \<otimes> (inv x)"])
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    70
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    71
                      subgroup.subset [THEN subsetD])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    72
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    73
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    74
lemma (in group) repr_independence:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    75
     "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    76
by (auto simp add: r_coset_def m_assoc [symmetric]
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    77
                   subgroup.subset [THEN subsetD]
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    78
                   subgroup.m_closed solve_equation)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    79
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    80
lemma (in group) coset_join2:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    81
     "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    82
  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    83
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    84
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
    85
lemma (in monoid) r_coset_subset_G:
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    86
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    87
by (auto simp add: r_coset_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    88
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    89
lemma (in group) rcosI:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    90
     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    91
by (auto simp add: r_coset_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    92
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    93
lemma (in group) rcosetsI:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    94
     "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
    95
by (auto simp add: RCOSETS_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    96
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    97
text{*Really needed?*}
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    98
lemma (in group) transpose_inv:
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    99
     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   100
      ==> (inv x) \<otimes> z = y"
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   101
by (force simp add: m_assoc [symmetric])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   102
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   103
lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   104
apply (simp add: r_coset_def)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   105
apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   106
                    subgroup.one_closed)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   107
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   108
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   109
text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   110
lemma (in group) repr_independenceD:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   111
  assumes "subgroup H G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   112
  assumes ycarr: "y \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   113
      and repr:  "H #> x = H #> y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   114
  shows "y \<in> H #> x"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   115
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   116
  interpret subgroup H G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   117
  show ?thesis  apply (subst repr)
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   118
  apply (intro rcos_self)
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   119
   apply (rule ycarr)
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   120
   apply (rule is_subgroup)
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   121
  done
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   122
qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   123
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   124
text {* Elements of a right coset are in the carrier *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   125
lemma (in subgroup) elemrcos_carrier:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   126
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   127
  assumes acarr: "a \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   128
    and a': "a' \<in> H #> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   129
  shows "a' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   130
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   131
  interpret group G by fact
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   132
  from subset and acarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   133
  have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   134
  from this and a'
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   135
  show "a' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   136
    by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   137
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   138
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   139
lemma (in subgroup) rcos_const:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   140
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   141
  assumes hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   142
  shows "H #> h = H"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   143
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   144
  interpret group G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   145
  show ?thesis apply (unfold r_coset_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   146
    apply rule
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   147
    apply rule
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   148
    apply clarsimp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   149
    apply (intro subgroup.m_closed)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   150
    apply (rule is_subgroup)
23463
9953ff53cc64 tuned proofs -- avoid implicit prems;
wenzelm
parents: 23350
diff changeset
   151
    apply assumption
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   152
    apply (rule hH)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   153
    apply rule
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   154
    apply simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   155
  proof -
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   156
    fix h'
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   157
    assume h'H: "h' \<in> H"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   158
    note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   159
    from carr
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   160
    have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   161
    from h'H hH
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   162
    have "h' \<otimes> inv h \<in> H" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   163
    from this and a
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   164
    show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   165
  qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   166
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   167
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   168
text {* Step one for lemma @{text "rcos_module"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   169
lemma (in subgroup) rcos_module_imp:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   170
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   171
  assumes xcarr: "x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   172
      and x'cos: "x' \<in> H #> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   173
  shows "(x' \<otimes> inv x) \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   174
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   175
  interpret group G by fact
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   176
  from xcarr x'cos
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   177
      have x'carr: "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   178
      by (rule elemrcos_carrier[OF is_group])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   179
  from xcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   180
      have ixcarr: "inv x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   181
      by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   182
  from x'cos
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   183
      have "\<exists>h\<in>H. x' = h \<otimes> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   184
      unfolding r_coset_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   185
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   186
  from this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   187
      obtain h
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   188
        where hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   189
        and x': "x' = h \<otimes> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   190
      by auto
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   191
  from hH and subset
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   192
      have hcarr: "h \<in> carrier G" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   193
  note carr = xcarr x'carr hcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   194
  from x' and carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   195
      have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   196
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   197
      have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   198
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   199
      have "\<dots> = h \<otimes> \<one>" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   200
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   201
      have "\<dots> = h" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   202
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   203
      have "x' \<otimes> (inv x) = h" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   204
  from hH this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   205
      show "x' \<otimes> (inv x) \<in> H" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   206
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   207
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   208
text {* Step two for lemma @{text "rcos_module"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   209
lemma (in subgroup) rcos_module_rev:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   210
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   211
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   212
      and xixH: "(x' \<otimes> inv x) \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   213
  shows "x' \<in> H #> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   214
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   215
  interpret group G by fact
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   216
  from xixH
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   217
      have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   218
  from this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   219
      obtain h
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   220
        where hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   221
        and hsym: "x' \<otimes> (inv x) = h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   222
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   223
  from hH subset have hcarr: "h \<in> carrier G" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   224
  note carr = carr hcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   225
  from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   226
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   227
      have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   228
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   229
      have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   230
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   231
      have "\<dots> = x'" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   232
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   233
      have "h \<otimes> x = x'" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   234
  from this[symmetric] and hH
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   235
      show "x' \<in> H #> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   236
      unfolding r_coset_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   237
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   238
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   239
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   240
text {* Module property of right cosets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   241
lemma (in subgroup) rcos_module:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   242
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   243
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   244
  shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   245
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   246
  interpret group G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   247
  show ?thesis proof  assume "x' \<in> H #> x"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   248
    from this and carr
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   249
    show "x' \<otimes> inv x \<in> H"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   250
      by (intro rcos_module_imp[OF is_group])
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   251
  next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   252
    assume "x' \<otimes> inv x \<in> H"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   253
    from this and carr
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   254
    show "x' \<in> H #> x"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   255
      by (intro rcos_module_rev[OF is_group])
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   256
  qed
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   257
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   258
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   259
text {* Right cosets are subsets of the carrier. *} 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   260
lemma (in subgroup) rcosets_carrier:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   261
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   262
  assumes XH: "X \<in> rcosets H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   263
  shows "X \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   264
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   265
  interpret group G by fact
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   266
  from XH have "\<exists>x\<in> carrier G. X = H #> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   267
      unfolding RCOSETS_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   268
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   269
  from this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   270
      obtain x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   271
        where xcarr: "x\<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   272
        and X: "X = H #> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   273
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   274
  from subset and xcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   275
      show "X \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   276
      unfolding X
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   277
      by (rule r_coset_subset_G)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   278
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   279
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   280
text {* Multiplication of general subsets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   281
lemma (in monoid) set_mult_closed:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   282
  assumes Acarr: "A \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   283
      and Bcarr: "B \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   284
  shows "A <#> B \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   285
apply rule apply (simp add: set_mult_def, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   286
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   287
  fix a b
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   288
  assume "a \<in> A"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   289
  from this and Acarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   290
      have acarr: "a \<in> carrier G" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   291
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   292
  assume "b \<in> B"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   293
  from this and Bcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   294
      have bcarr: "b \<in> carrier G" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   295
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   296
  from acarr bcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   297
      show "a \<otimes> b \<in> carrier G" by (rule m_closed)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   298
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   299
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   300
lemma (in comm_group) mult_subgroups:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   301
  assumes subH: "subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   302
      and subK: "subgroup K G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   303
  shows "subgroup (H <#> K) G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   304
apply (rule subgroup.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   305
   apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   306
  apply (simp add: set_mult_def) apply clarsimp defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   307
  apply (simp add: set_mult_def) defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   308
  apply (simp add: set_mult_def, clarsimp) defer 1
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   309
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   310
  fix ha hb ka kb
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   311
  assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   312
  note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   313
              kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   314
  from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   315
      have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   316
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   317
      have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   318
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   319
      have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   320
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   321
      have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   322
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   323
  from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   324
  from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   325
  
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   326
  from hH and kK and eq
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   327
      show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   328
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   329
  have "\<one> = \<one> \<otimes> \<one>" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   330
  from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   331
      show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   332
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   333
  fix h k
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   334
  assume hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   335
     and kK: "k \<in> K"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   336
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   337
  from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   338
      have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   339
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   340
  from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   341
      show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   342
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   343
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   344
lemma (in subgroup) lcos_module_rev:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   345
  assumes "group G"
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   346
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   347
      and xixH: "(inv x \<otimes> x') \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   348
  shows "x' \<in> x <# H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   349
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   350
  interpret group G by fact
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   351
  from xixH
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   352
      have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   353
  from this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   354
      obtain h
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   355
        where hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   356
        and hsym: "(inv x) \<otimes> x' = h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   357
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   358
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   359
  from hH subset have hcarr: "h \<in> carrier G" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   360
  note carr = carr hcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   361
  from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   362
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   363
      have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   364
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   365
      have "\<dots> = \<one> \<otimes> x'" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   366
  also from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   367
      have "\<dots> = x'" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   368
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   369
      have "x \<otimes> h = x'" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   370
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   371
  from this[symmetric] and hH
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   372
      show "x' \<in> x <# H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   373
      unfolding l_coset_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   374
      by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   375
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   376
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   377
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   378
subsection {* Normal subgroups *}
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   379
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   380
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   381
  by (simp add: normal_def subgroup_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   382
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   383
lemma (in group) normalI: 
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
   384
  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   385
  by (simp add: normal_def normal_axioms_def prems) 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   386
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   387
lemma (in normal) inv_op_closed1:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   388
     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   389
apply (insert coset_eq) 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   390
apply (auto simp add: l_coset_def r_coset_def)
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   391
apply (drule bspec, assumption)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   392
apply (drule equalityD1 [THEN subsetD], blast, clarify)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   393
apply (simp add: m_assoc)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   394
apply (simp add: m_assoc [symmetric])
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   395
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   396
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   397
lemma (in normal) inv_op_closed2:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   398
     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   399
apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
   400
apply (simp add: ) 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   401
apply (blast intro: inv_op_closed1) 
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   402
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   403
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   404
text{*Alternative characterization of normal subgroups*}
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   405
lemma (in group) normal_inv_iff:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   406
     "(N \<lhd> G) = 
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   407
      (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   408
      (is "_ = ?rhs")
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   409
proof
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   410
  assume N: "N \<lhd> G"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   411
  show ?rhs
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   412
    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   413
next
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   414
  assume ?rhs
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   415
  hence sg: "subgroup N G" 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   416
    and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   417
  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   418
  show "N \<lhd> G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   419
  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   420
    fix x
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   421
    assume x: "x \<in> carrier G"
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   422
    show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   423
    proof
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   424
      show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   425
      proof clarify
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   426
        fix n
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   427
        assume n: "n \<in> N" 
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   428
        show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   429
        proof 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   430
          from closed [of "inv x"]
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   431
          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   432
          show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   433
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   434
        qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   435
      qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   436
    next
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   437
      show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   438
      proof clarify
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   439
        fix n
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   440
        assume n: "n \<in> N" 
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   441
        show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   442
        proof 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   443
          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   444
          show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   445
            by (simp add: x n m_assoc sb [THEN subsetD])
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   446
        qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   447
      qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   448
    qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   449
  qed
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   450
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   451
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   452
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   453
subsection{*More Properties of Cosets*}
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   454
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   455
lemma (in group) lcos_m_assoc:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   456
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   457
      ==> g <# (h <# M) = (g \<otimes> h) <# M"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   458
by (force simp add: l_coset_def m_assoc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   459
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   460
lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   461
by (force simp add: l_coset_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   462
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   463
lemma (in group) l_coset_subset_G:
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   464
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   465
by (auto simp add: l_coset_def subsetD)
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   466
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   467
lemma (in group) l_coset_swap:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   468
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   469
proof (simp add: l_coset_def)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   470
  assume "\<exists>h\<in>H. y = x \<otimes> h"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   471
    and x: "x \<in> carrier G"
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   472
    and sb: "subgroup H G"
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   473
  then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   474
  show "\<exists>h\<in>H. x = y \<otimes> h"
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   475
  proof
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   476
    show "x = y \<otimes> inv h'" using h' x sb
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   477
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   478
    show "inv h' \<in> H" using h' sb
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   479
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   480
  qed
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   481
qed
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   482
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   483
lemma (in group) l_coset_carrier:
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   484
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   485
by (auto simp add: l_coset_def m_assoc
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   486
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   487
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   488
lemma (in group) l_repr_imp_subset:
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   489
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   490
  shows "y <# H \<subseteq> x <# H"
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   491
proof -
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   492
  from y
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   493
  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   494
  thus ?thesis using x sb
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   495
    by (auto simp add: l_coset_def m_assoc
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   496
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   497
qed
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   498
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   499
lemma (in group) l_repr_independence:
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   500
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   501
  shows "x <# H = y <# H"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   502
proof
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   503
  show "x <# H \<subseteq> y <# H"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   504
    by (rule l_repr_imp_subset,
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   505
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   506
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
14530
e94fd774ecf5 some (much longer) structured proofs
paulson
parents: 14254
diff changeset
   507
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   508
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   509
lemma (in group) setmult_subset_G:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   510
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   511
by (auto simp add: set_mult_def subsetD)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   512
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   513
lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   514
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   515
apply (rule_tac x = x in bexI)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   516
apply (rule bexI [of _ "\<one>"])
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   517
apply (auto simp add: subgroup.m_closed subgroup.one_closed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   518
                      r_one subgroup.subset [THEN subsetD])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   519
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   520
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   521
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   522
subsubsection {* Set of Inverses of an @{text r_coset}. *}
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   523
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   524
lemma (in normal) rcos_inv:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   525
  assumes x:     "x \<in> carrier G"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   526
  shows "set_inv (H #> x) = H #> (inv x)" 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   527
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   528
  fix h
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   529
  assume "h \<in> H"
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   530
  show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   531
  proof
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   532
    show "inv x \<otimes> inv h \<otimes> x \<in> H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   533
      by (simp add: inv_op_closed1 prems)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   534
    show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   535
      by (simp add: prems m_assoc)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   536
  qed
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   537
next
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   538
  fix h
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   539
  assume "h \<in> H"
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
   540
  show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   541
  proof
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   542
    show "x \<otimes> inv h \<otimes> inv x \<in> H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   543
      by (simp add: inv_op_closed2 prems)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   544
    show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   545
      by (simp add: prems m_assoc [symmetric] inv_mult_group)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   546
  qed
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   547
qed
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   548
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   549
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   550
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   551
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   552
lemma (in group) setmult_rcos_assoc:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   553
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   554
      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   555
by (force simp add: r_coset_def set_mult_def m_assoc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   556
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   557
lemma (in group) rcos_assoc_lcos:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   558
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   559
      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   560
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   561
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   562
lemma (in normal) rcos_mult_step1:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   563
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   564
      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   565
by (simp add: setmult_rcos_assoc subset
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   566
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   567
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   568
lemma (in normal) rcos_mult_step2:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   569
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   570
      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   571
by (insert coset_eq, simp add: normal_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   572
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   573
lemma (in normal) rcos_mult_step3:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   574
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   575
      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   576
by (simp add: setmult_rcos_assoc coset_mult_assoc
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19380
diff changeset
   577
              subgroup_mult_id normal.axioms subset prems)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   578
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   579
lemma (in normal) rcos_sum:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   580
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   581
      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   582
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   583
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   584
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   585
  -- {* generalizes @{text subgroup_mult_id} *}
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   586
  by (auto simp add: RCOSETS_def subset
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19380
diff changeset
   587
        setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   588
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   589
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   590
subsubsection{*An Equivalence Relation*}
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   591
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   592
constdefs (structure G)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   593
  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   594
                  ("rcong\<index> _")
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   595
   "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   596
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   597
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   598
lemma (in subgroup) equiv_rcong:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   599
   assumes "group G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   600
   shows "equiv (carrier G) (rcong H)"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   601
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   602
  interpret group G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   603
  show ?thesis
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   604
  proof (intro equiv.intro)
30198
922f944f03b2 name changes
nipkow
parents: 29237
diff changeset
   605
    show "refl_on (carrier G) (rcong H)"
922f944f03b2 name changes
nipkow
parents: 29237
diff changeset
   606
      by (auto simp add: r_congruent_def refl_on_def) 
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   607
  next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   608
    show "sym (rcong H)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   609
    proof (simp add: r_congruent_def sym_def, clarify)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   610
      fix x y
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   611
      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31727
diff changeset
   612
         and "inv x \<otimes> y \<in> H"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   613
      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   614
      thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   615
    qed
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   616
  next
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   617
    show "trans (rcong H)"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   618
    proof (simp add: r_congruent_def trans_def, clarify)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   619
      fix x y z
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   620
      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31727
diff changeset
   621
         and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   622
      hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
27698
197f0517f0bd Unit_inv_l, Unit_inv_r made [simp].
ballarin
parents: 27611
diff changeset
   623
      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31727
diff changeset
   624
        by (simp add: m_assoc del: r_inv Units_r_inv) 
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   625
      thus "inv x \<otimes> z \<in> H" by simp
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   626
    qed
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   627
  qed
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   628
qed
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   629
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   630
text{*Equivalence classes of @{text rcong} correspond to left cosets.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   631
  Was there a mistake in the definitions? I'd have expected them to
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   632
  correspond to right cosets.*}
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   633
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   634
(* CB: This is correct, but subtle.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   635
   We call H #> a the right coset of a relative to H.  According to
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   636
   Jacobson, this is what the majority of group theory literature does.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   637
   He then defines the notion of congruence relation ~ over monoids as
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   638
   equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   639
   Our notion of right congruence induced by K: rcong K appears only in
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   640
   the context where K is a normal subgroup.  Jacobson doesn't name it.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   641
   But in this context left and right cosets are identical.
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   642
*)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   643
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   644
lemma (in subgroup) l_coset_eq_rcong:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   645
  assumes "group G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   646
  assumes a: "a \<in> carrier G"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   647
  shows "a <# H = rcong H `` {a}"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   648
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   649
  interpret group G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   650
  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   651
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   652
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   653
subsubsection{*Two Distinct Right Cosets are Disjoint*}
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   654
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   655
lemma (in group) rcos_equation:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   656
  assumes "subgroup H G"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   657
  assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   658
  shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   659
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   660
  interpret subgroup H G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   661
  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   662
    apply (simp add: )
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   663
    apply (simp add: m_assoc transpose_inv)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   664
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   665
qed
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   666
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   667
lemma (in group) rcos_disjoint:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   668
  assumes "subgroup H G"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   669
  assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   670
  shows "a \<inter> b = {}"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   671
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   672
  interpret subgroup H G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   673
  from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   674
    apply (blast intro: rcos_equation prems sym)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   675
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   676
qed
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   677
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   678
subsection {* Further lemmas for @{text "r_congruent"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   679
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   680
text {* The relation is a congruence *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   681
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   682
lemma (in normal) congruent_rcong:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   683
  shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   684
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   685
  fix a b c
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   686
  assume abrcong: "(a, b) \<in> rcong H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   687
    and ccarr: "c \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   688
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   689
  from abrcong
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   690
      have acarr: "a \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   691
        and bcarr: "b \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   692
        and abH: "inv a \<otimes> b \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   693
      unfolding r_congruent_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   694
      by fast+
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   695
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   696
  note carr = acarr bcarr ccarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   697
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   698
  from ccarr and abH
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   699
      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   700
  moreover
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   701
      from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   702
      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   703
      by (force cong: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   704
  moreover 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   705
      from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   706
      have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   707
      by (simp add: inv_mult_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   708
  ultimately
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   709
      have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   710
  from carr and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   711
     have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   712
     by (simp add: lcos_module_rev[OF is_group])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   713
  from carr and this and is_subgroup
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   714
     show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   715
next
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   716
  fix a b c
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   717
  assume abrcong: "(a, b) \<in> rcong H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   718
    and ccarr: "c \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   719
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   720
  from ccarr have "c \<in> Units G" by (simp add: Units_eq)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   721
  hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   722
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   723
  from abrcong
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   724
      have acarr: "a \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   725
       and bcarr: "b \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   726
       and abH: "inv a \<otimes> b \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   727
      by (unfold r_congruent_def, fast+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   728
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   729
  note carr = acarr bcarr ccarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   730
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   731
  from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   732
     have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   733
  also from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   734
      have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   735
  also from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   736
      have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   737
  also from carr and inv_closed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   738
      have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   739
  finally
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   740
      have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   741
  from abH and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   742
      have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   743
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   744
  from carr and this
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   745
     have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   746
     by (simp add: lcos_module_rev[OF is_group])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   747
  from carr and this and is_subgroup
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   748
     show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   749
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 19931
diff changeset
   750
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   751
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   752
subsection {*Order of a Group and Lagrange's Theorem*}
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   753
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   754
constdefs
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   755
  order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   756
  "order S \<equiv> card (carrier S)"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   757
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   758
lemma (in group) rcosets_part_G:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   759
  assumes "subgroup H G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   760
  shows "\<Union>(rcosets H) = carrier G"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   761
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   762
  interpret subgroup H G by fact
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   763
  show ?thesis
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   764
    apply (rule equalityI)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   765
    apply (force simp add: RCOSETS_def r_coset_def)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   766
    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   767
    done
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   768
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   769
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   770
lemma (in group) cosets_finite:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   771
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   772
apply (auto simp add: RCOSETS_def)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   773
apply (simp add: r_coset_subset_G [THEN finite_subset])
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   774
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   775
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   776
text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   777
lemma (in group) inj_on_f:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   778
    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   779
apply (rule inj_onI)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   780
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   781
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   782
apply (simp add: subsetD)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   783
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   784
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   785
lemma (in group) inj_on_g:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   786
    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   787
by (force simp add: inj_on_def subsetD)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   788
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   789
lemma (in group) card_cosets_equal:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   790
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   791
      \<Longrightarrow> card c = card H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   792
apply (auto simp add: RCOSETS_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   793
apply (rule card_bij_eq)
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   794
     apply (rule inj_on_f, assumption+)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   795
    apply (force simp add: m_assoc subsetD r_coset_def)
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   796
   apply (rule inj_on_g, assumption+)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   797
  apply (force simp add: m_assoc subsetD r_coset_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   798
 txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   799
 apply (simp add: r_coset_subset_G [THEN finite_subset])
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   800
apply (blast intro: finite_subset)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   801
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   802
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   803
lemma (in group) rcosets_subset_PowG:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   804
     "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   805
apply (simp add: RCOSETS_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   806
apply (blast dest: r_coset_subset_G subgroup.subset)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   807
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   808
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   809
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   810
theorem (in group) lagrange:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   811
     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   812
      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   813
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   814
apply (subst mult_commute)
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   815
apply (rule card_partition)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   816
   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   817
  apply (simp add: rcosets_part_G)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   818
 apply (simp add: card_cosets_equal subgroup.subset)
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   819
apply (simp add: rcos_disjoint)
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   820
done
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   821
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   822
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   823
subsection {*Quotient Groups: Factorization of a Group*}
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   824
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   825
constdefs
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   826
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   827
     (infixl "Mod" 65)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   828
    --{*Actually defined for groups rather than monoids*}
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   829
  "FactGroup G H \<equiv>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   830
    \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   831
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   832
lemma (in normal) setmult_closed:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   833
     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   834
by (auto simp add: rcos_sum RCOSETS_def)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   835
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   836
lemma (in normal) setinv_closed:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   837
     "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   838
by (auto simp add: rcos_inv RCOSETS_def)
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   839
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   840
lemma (in normal) rcosets_assoc:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   841
     "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   842
      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   843
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   844
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   845
lemma (in subgroup) subgroup_in_rcosets:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 26310
diff changeset
   846
  assumes "group G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   847
  shows "H \<in> rcosets H"
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   848
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 27717
diff changeset
   849
  interpret group G by fact
26203
9625f3579b48 explicit referencing of background facts;
wenzelm
parents: 23463
diff changeset
   850
  from _ subgroup_axioms have "H #> \<one> = H"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   851
    by (rule coset_join2) auto
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   852
  then show ?thesis
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   853
    by (auto simp add: RCOSETS_def)
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   854
qed
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   855
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   856
lemma (in normal) rcosets_inv_mult_group_eq:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   857
     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19380
diff changeset
   858
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   859
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   860
theorem (in normal) factorgroup_is_group:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   861
  "group (G Mod H)"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   862
apply (simp add: FactGroup_def)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13889
diff changeset
   863
apply (rule groupI)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   864
    apply (simp add: setmult_closed)
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   865
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   866
  apply (simp add: restrictI setmult_closed rcosets_assoc)
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   867
 apply (simp add: normal_imp_subgroup
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   868
                  subgroup_in_rcosets rcosets_mult_eq)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   869
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
13889
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   870
done
6676ac2527fa Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents: 13870
diff changeset
   871
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   872
lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   873
  by (simp add: FactGroup_def) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   874
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   875
lemma (in normal) inv_FactGroup:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   876
     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   877
apply (rule group.inv_equality [OF factorgroup_is_group]) 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   878
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   879
done
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   880
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   881
text{*The coset map is a homomorphism from @{term G} to the quotient group
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   882
  @{term "G Mod H"}*}
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   883
lemma (in normal) r_coset_hom_Mod:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   884
  "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   885
  by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
14747
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   886
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   887
 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   888
subsection{*The First Isomorphism Theorem*}
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   889
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   890
text{*The quotient by the kernel of a homomorphism is isomorphic to the 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   891
  range of that homomorphism.*}
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   892
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   893
constdefs
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   894
  kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   895
             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   896
    --{*the kernel of a homomorphism*}
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
   897
  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   898
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   899
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   900
apply (rule subgroup.intro) 
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   901
apply (auto simp add: kernel_def group.intro prems) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   902
done
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   903
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   904
text{*The kernel of a homomorphism is a normal subgroup*}
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   905
lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19380
diff changeset
   906
apply (simp add: G.normal_inv_iff subgroup_kernel)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19380
diff changeset
   907
apply (simp add: kernel_def)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   908
done
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   909
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   910
lemma (in group_hom) FactGroup_nonempty:
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   911
  assumes X: "X \<in> carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   912
  shows "X \<noteq> {}"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   913
proof -
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   914
  from X
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   915
  obtain g where "g \<in> carrier G" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   916
             and "X = kernel G H h #> g"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   917
    by (auto simp add: FactGroup_def RCOSETS_def)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   918
  thus ?thesis 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   919
   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   920
qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   921
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   922
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   923
lemma (in group_hom) FactGroup_contents_mem:
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   924
  assumes X: "X \<in> carrier (G Mod (kernel G H h))"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   925
  shows "contents (h`X) \<in> carrier H"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   926
proof -
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   927
  from X
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   928
  obtain g where g: "g \<in> carrier G" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   929
             and "X = kernel G H h #> g"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   930
    by (auto simp add: FactGroup_def RCOSETS_def)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   931
  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   932
  thus ?thesis by (auto simp add: g)
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   933
qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   934
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   935
lemma (in group_hom) FactGroup_hom:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   936
     "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
31727
2621a957d417 Made Pi_I [simp]
nipkow
parents: 30198
diff changeset
   937
apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
2621a957d417 Made Pi_I [simp]
nipkow
parents: 30198
diff changeset
   938
proof (intro ballI)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   939
  fix X and X'
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   940
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   941
     and X': "X' \<in> carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   942
  then
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   943
  obtain g and g'
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   944
           where "g \<in> carrier G" and "g' \<in> carrier G" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   945
             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   946
    by (auto simp add: FactGroup_def RCOSETS_def)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   947
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   948
    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   949
    by (force simp add: kernel_def r_coset_def image_def)+
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   950
  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   951
    by (auto dest!: FactGroup_nonempty
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   952
             simp add: set_mult_def image_eq_UN 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   953
                       subsetD [OF Xsub] subsetD [OF X'sub]) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   954
  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
31727
2621a957d417 Made Pi_I [simp]
nipkow
parents: 30198
diff changeset
   955
    by (simp add: all image_eq_UN FactGroup_nonempty X X')
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   956
qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   957
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   958
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   959
text{*Lemma for the following injectivity result*}
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   960
lemma (in group_hom) FactGroup_subset:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   961
     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   962
      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
   963
apply (clarsimp simp add: kernel_def r_coset_def image_def)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   964
apply (rename_tac y)  
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   965
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
   966
apply (simp add: G.m_assoc) 
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   967
done
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   968
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   969
lemma (in group_hom) FactGroup_inj_on:
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   970
     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   971
proof (simp add: inj_on_def, clarify) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   972
  fix X and X'
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   973
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   974
     and X': "X' \<in> carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   975
  then
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   976
  obtain g and g'
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   977
           where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   978
              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   979
    by (auto simp add: FactGroup_def RCOSETS_def)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   980
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   981
    by (force simp add: kernel_def r_coset_def image_def)+
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   982
  assume "contents (h ` X) = contents (h ` X')"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   983
  hence h: "h g = h g'"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   984
    by (simp add: image_eq_UN all FactGroup_nonempty X X') 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   985
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   986
qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   987
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   988
text{*If the homomorphism @{term h} is onto @{term H}, then so is the
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   989
homomorphism from the quotient group*}
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   990
lemma (in group_hom) FactGroup_onto:
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   991
  assumes h: "h ` carrier G = carrier H"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   992
  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   993
proof
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   994
  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   995
    by (auto simp add: FactGroup_contents_mem)
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   996
  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   997
  proof
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   998
    fix y
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
   999
    assume y: "y \<in> carrier H"
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1000
    with h obtain g where g: "g \<in> carrier G" "h g = y"
26310
f8a7fac36e13 only one version of group.rcos_self;
wenzelm
parents: 26203
diff changeset
  1001
      by (blast elim: equalityE) 
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14963
diff changeset
  1002
    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1003
      by (auto simp add: y kernel_def r_coset_def) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1004
    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
  1005
      by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1006
  qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1007
qed
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1008
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1009
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1010
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1011
 quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1012
theorem (in group_hom) FactGroup_iso:
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1013
  "h ` carrier G = carrier H
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
  1014
   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
14803
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1015
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1016
              FactGroup_onto) 
f7557773cc87 more group isomorphisms
paulson
parents: 14761
diff changeset
  1017
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
  1018
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
  1019
end