more group isomorphisms
authorpaulson
Wed May 26 11:43:50 2004 +0200 (2004-05-26)
changeset 14803f7557773cc87
parent 14802 e05116289ff9
child 14804 8de39d3e8eb6
more group isomorphisms
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Sylow.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Mon May 24 18:35:34 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Wed May 26 11:43:50 2004 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4    normal :: "['a set, ('a,'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)
     1.5  
     1.6  
     1.7 -subsection {*Lemmas Using Locale Constants*}
     1.8 +subsection {*Basic Properties of Cosets*}
     1.9  
    1.10  lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
    1.11  by (auto simp add: r_coset_def)
    1.12 @@ -187,6 +187,8 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +subsection{*More Properties of Cosets*}
    1.17 +
    1.18  lemma (in group) lcos_m_assoc:
    1.19       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    1.20        ==> g <# (h <# M) = (g \<otimes> h) <# M"
    1.21 @@ -300,7 +302,7 @@
    1.22  done
    1.23  
    1.24  
    1.25 -subsubsection {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
    1.26 +subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
    1.27  
    1.28  lemma (in group) setmult_rcos_assoc:
    1.29       "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
    1.30 @@ -345,7 +347,29 @@
    1.31      setmult_rcos_assoc subgroup_mult_id)
    1.32  
    1.33  
    1.34 -subsection {*Lemmas Leading to Lagrange's Theorem *}
    1.35 +subsubsection{*Two distinct right cosets are disjoint*}
    1.36 +
    1.37 +lemma (in group) rcos_equation:
    1.38 +     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
    1.39 +        h \<in> H;  ha \<in> H;  hb \<in> H|]
    1.40 +      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
    1.41 +apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
    1.42 +apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
    1.43 +apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
    1.44 +done
    1.45 +
    1.46 +lemma (in group) rcos_disjoint:
    1.47 +     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
    1.48 +apply (simp add: setrcos_eq r_coset_eq)
    1.49 +apply (blast intro: rcos_equation sym)
    1.50 +done
    1.51 +
    1.52 +
    1.53 +subsection {*Order of a Group and Lagrange's Theorem*}
    1.54 +
    1.55 +constdefs
    1.56 +  order :: "('a, 'b) semigroup_scheme => nat"
    1.57 +  "order S == card (carrier S)"
    1.58  
    1.59  lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
    1.60  apply (rule equalityI)
    1.61 @@ -387,41 +411,34 @@
    1.62  apply (blast intro: finite_subset)
    1.63  done
    1.64  
    1.65 -
    1.66 -subsection{*Two distinct right cosets are disjoint*}
    1.67 -
    1.68 -lemma (in group) rcos_equation:
    1.69 -     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
    1.70 -        h \<in> H;  ha \<in> H;  hb \<in> H|]
    1.71 -      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
    1.72 -apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
    1.73 -apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
    1.74 -apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
    1.75 -done
    1.76 -
    1.77 -lemma (in group) rcos_disjoint:
    1.78 -     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
    1.79 -apply (simp add: setrcos_eq r_coset_eq)
    1.80 -apply (blast intro: rcos_equation sym)
    1.81 -done
    1.82 -
    1.83  lemma (in group) setrcos_subset_PowG:
    1.84       "subgroup H G  ==> rcosets G H \<subseteq> Pow(carrier G)"
    1.85  apply (simp add: setrcos_eq)
    1.86  apply (blast dest: r_coset_subset_G subgroup.subset)
    1.87  done
    1.88  
    1.89 +
    1.90 +theorem (in group) lagrange:
    1.91 +     "[| finite(carrier G); subgroup H G |]
    1.92 +      ==> card(rcosets G H) * card(H) = order(G)"
    1.93 +apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
    1.94 +apply (subst mult_commute)
    1.95 +apply (rule card_partition)
    1.96 +   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
    1.97 +  apply (simp add: setrcos_part_G)
    1.98 + apply (simp add: card_cosets_equal subgroup.subset)
    1.99 +apply (simp add: rcos_disjoint)
   1.100 +done
   1.101 +
   1.102 +
   1.103  subsection {*Quotient Groups: Factorization of a Group*}
   1.104  
   1.105  constdefs
   1.106    FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
   1.107 -     (infixl "Mod" 60)
   1.108 +     (infixl "Mod" 65)
   1.109      --{*Actually defined for groups rather than monoids*}
   1.110    "FactGroup G H ==
   1.111 -    (| carrier = rcosets G H,
   1.112 -       mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
   1.113 -       one = H |)"
   1.114 -
   1.115 +    (| carrier = rcosets G H, mult = set_mult G, one = H |)"
   1.116  
   1.117  lemma (in group) setmult_closed:
   1.118       "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
   1.119 @@ -435,15 +452,6 @@
   1.120                     subgroup.subset rcos_inv
   1.121                     setrcos_eq)
   1.122  
   1.123 -(*
   1.124 -The old version is no longer valid: "group G" has to be an explicit premise.
   1.125 -
   1.126 -lemma setinv_closed:
   1.127 -     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
   1.128 -by (auto simp add:  normal_imp_subgroup
   1.129 -                   subgroup.subset coset.rcos_inv coset.setrcos_eq)
   1.130 -*)
   1.131 -
   1.132  lemma (in group) setrcos_assoc:
   1.133       "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
   1.134        ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   1.135 @@ -461,18 +469,6 @@
   1.136      by (auto simp add: setrcos_eq)
   1.137  qed
   1.138  
   1.139 -(*
   1.140 -lemma subgroup_in_rcosets:
   1.141 -  "subgroup H G ==> H \<in> rcosets G H"
   1.142 -apply (frule subgroup_imp_coset)
   1.143 -apply (frule subgroup_imp_group)
   1.144 -apply (simp add: coset.setrcos_eq)
   1.145 -apply (blast del: equalityI
   1.146 -             intro!: group.subgroup.one_closed group.one_closed
   1.147 -                     coset.coset_join2 [symmetric])
   1.148 -done
   1.149 -*)
   1.150 -
   1.151  lemma (in group) setrcos_inv_mult_group_eq:
   1.152       "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
   1.153  by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
   1.154 @@ -499,6 +495,9 @@
   1.155  apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
   1.156  done
   1.157  
   1.158 +lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   1.159 +  by (simp add: FactGroup_def) 
   1.160 +
   1.161  lemma (in group) inv_FactGroup:
   1.162       "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
   1.163  apply (rule group.inv_equality [OF factorgroup_is_group]) 
   1.164 @@ -512,4 +511,130 @@
   1.165    shows "(r_coset G N) \<in> hom G (G Mod N)"
   1.166  by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N) 
   1.167  
   1.168 +
   1.169 +subsection{*Quotienting by the Kernel of a Homomorphism*}
   1.170 +
   1.171 +constdefs
   1.172 +  kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme => 
   1.173 +             ('a => 'b) => 'a set" 
   1.174 +    --{*the kernel of a homomorphism*}
   1.175 +  "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
   1.176 +
   1.177 +lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   1.178 +apply (rule group.subgroupI) 
   1.179 +apply (auto simp add: kernel_def group.intro prems) 
   1.180 +done
   1.181 +
   1.182 +text{*The kernel of a homomorphism is a normal subgroup*}
   1.183 +lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
   1.184 +apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
   1.185 +apply (simp add: kernel_def)  
   1.186 +done
   1.187 +
   1.188 +lemma (in group_hom) FactGroup_nonempty:
   1.189 +  assumes X: "X \<in> carrier (G Mod kernel G H h)"
   1.190 +  shows "X \<noteq> {}"
   1.191 +proof -
   1.192 +  from X
   1.193 +  obtain g where "g \<in> carrier G" 
   1.194 +             and "X = kernel G H h #> g"
   1.195 +    by (auto simp add: FactGroup_def rcosets_def)
   1.196 +  thus ?thesis 
   1.197 +   by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
   1.198 +qed
   1.199 +
   1.200 +
   1.201 +lemma (in group_hom) FactGroup_contents_mem:
   1.202 +  assumes X: "X \<in> carrier (G Mod (kernel G H h))"
   1.203 +  shows "contents (h`X) \<in> carrier H"
   1.204 +proof -
   1.205 +  from X
   1.206 +  obtain g where g: "g \<in> carrier G" 
   1.207 +             and "X = kernel G H h #> g"
   1.208 +    by (auto simp add: FactGroup_def rcosets_def)
   1.209 +  hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
   1.210 +  thus ?thesis by (auto simp add: g)
   1.211 +qed
   1.212 +
   1.213 +lemma (in group_hom) FactGroup_hom:
   1.214 +     "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   1.215 +proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
   1.216 +  fix X and X'
   1.217 +  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   1.218 +     and X': "X' \<in> carrier (G Mod kernel G H h)"
   1.219 +  then
   1.220 +  obtain g and g'
   1.221 +           where "g \<in> carrier G" and "g' \<in> carrier G" 
   1.222 +             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   1.223 +    by (auto simp add: FactGroup_def rcosets_def)
   1.224 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   1.225 +    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   1.226 +    by (force simp add: kernel_def r_coset_def image_def)+
   1.227 +  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   1.228 +    by (auto dest!: FactGroup_nonempty
   1.229 +             simp add: set_mult_def image_eq_UN 
   1.230 +                       subsetD [OF Xsub] subsetD [OF X'sub]) 
   1.231 +  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
   1.232 +    by (simp add: all image_eq_UN FactGroup_nonempty X X')  
   1.233 +qed
   1.234 +
   1.235 +text{*Lemma for the following injectivity result*}
   1.236 +lemma (in group_hom) FactGroup_subset:
   1.237 +     "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
   1.238 +      ==>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   1.239 +apply (clarsimp simp add: kernel_def r_coset_def image_def);
   1.240 +apply (rename_tac y)  
   1.241 +apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
   1.242 +apply (simp add: G.m_assoc); 
   1.243 +done
   1.244 +
   1.245 +lemma (in group_hom) FactGroup_inj_on:
   1.246 +     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
   1.247 +proof (simp add: inj_on_def, clarify) 
   1.248 +  fix X and X'
   1.249 +  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   1.250 +     and X': "X' \<in> carrier (G Mod kernel G H h)"
   1.251 +  then
   1.252 +  obtain g and g'
   1.253 +           where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
   1.254 +              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
   1.255 +    by (auto simp add: FactGroup_def rcosets_def)
   1.256 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   1.257 +    by (force simp add: kernel_def r_coset_def image_def)+
   1.258 +  assume "contents (h ` X) = contents (h ` X')"
   1.259 +  hence h: "h g = h g'"
   1.260 +    by (simp add: image_eq_UN all FactGroup_nonempty X X') 
   1.261 +  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
   1.262 +qed
   1.263 +
   1.264 +text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   1.265 +homomorphism from the quotient group*}
   1.266 +lemma (in group_hom) FactGroup_onto:
   1.267 +  assumes h: "h ` carrier G = carrier H"
   1.268 +  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
   1.269 +proof
   1.270 +  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
   1.271 +    by (auto simp add: FactGroup_contents_mem)
   1.272 +  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
   1.273 +  proof
   1.274 +    fix y
   1.275 +    assume y: "y \<in> carrier H"
   1.276 +    with h obtain g where g: "g \<in> carrier G" "h g = y"
   1.277 +      by (blast elim: equalityE); 
   1.278 +    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
   1.279 +      by (auto simp add: y kernel_def r_coset_def) 
   1.280 +    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
   1.281 +      by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
   1.282 +  qed
   1.283 +qed
   1.284 +
   1.285 +
   1.286 +text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   1.287 + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   1.288 +theorem (in group_hom) FactGroup_iso:
   1.289 +  "h ` carrier G = carrier H
   1.290 +   \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
   1.291 +by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
   1.292 +              FactGroup_onto) 
   1.293 +
   1.294  end
     2.1 --- a/src/HOL/Algebra/Group.thy	Mon May 24 18:35:34 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 26 11:43:50 2004 +0200
     2.3 @@ -593,15 +593,15 @@
     2.4  
     2.5  subsection {* Isomorphisms *}
     2.6  
     2.7 -constdefs (structure G and H)
     2.8 -  iso :: "_ => _ => ('a => 'b) set"
     2.9 -  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    2.10 +constdefs
    2.11 +  iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
    2.12 +  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    2.13  
    2.14 -lemma iso_refl: "(%x. x) \<in> iso G G"
    2.15 +lemma iso_refl: "(%x. x) \<in> G \<cong> G"
    2.16  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    2.17  
    2.18  lemma (in group) iso_sym:
    2.19 -     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
    2.20 +     "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
    2.21  apply (simp add: iso_def bij_betw_Inv) 
    2.22  apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    2.23   prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    2.24 @@ -609,15 +609,15 @@
    2.25  done
    2.26  
    2.27  lemma (in group) iso_trans: 
    2.28 -     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
    2.29 +     "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
    2.30  by (auto simp add: iso_def hom_compose bij_betw_compose)
    2.31  
    2.32  lemma DirProdGroup_commute_iso:
    2.33 -  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
    2.34 +  shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
    2.35  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    2.36  
    2.37  lemma DirProdGroup_assoc_iso:
    2.38 -  shows "(%(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<^sub>g H \<times>\<^sub>g I) (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
    2.39 +  shows "(%(x,y,z). (x,(y,z))) \<in> (G \<times>\<^sub>g H \<times>\<^sub>g I) \<cong> (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
    2.40  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
    2.41  
    2.42  
     3.1 --- a/src/HOL/Algebra/Sylow.thy	Mon May 24 18:35:34 2004 +0200
     3.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed May 26 11:43:50 2004 +0200
     3.3 @@ -11,25 +11,6 @@
     3.4    See also \cite{Kammueller-Paulson:1999}.
     3.5  *}
     3.6  
     3.7 -subsection {*Order of a Group and Lagrange's Theorem*}
     3.8 -
     3.9 -constdefs
    3.10 -  order :: "('a, 'b) semigroup_scheme => nat"
    3.11 -  "order S == card (carrier S)"
    3.12 -
    3.13 -theorem (in group) lagrange:
    3.14 -     "[| finite(carrier G); subgroup H G |]
    3.15 -      ==> card(rcosets G H) * card(H) = order(G)"
    3.16 -apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
    3.17 -apply (subst mult_commute)
    3.18 -apply (rule card_partition)
    3.19 -   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
    3.20 -  apply (simp add: setrcos_part_G)
    3.21 - apply (simp add: card_cosets_equal subgroup.subset)
    3.22 -apply (simp add: rcos_disjoint)
    3.23 -done
    3.24 -
    3.25 -
    3.26  text{*The combinatorial argument is in theory Exponent*}
    3.27  
    3.28  locale sylow = group +