--- a/src/HOL/Algebra/Coset.thy Mon May 24 18:35:34 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy Wed May 26 11:43:50 2004 +0200
@@ -33,7 +33,7 @@
normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
-subsection {*Lemmas Using Locale Constants*}
+subsection {*Basic Properties of Cosets*}
lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
by (auto simp add: r_coset_def)
@@ -187,6 +187,8 @@
qed
qed
+subsection{*More Properties of Cosets*}
+
lemma (in group) lcos_m_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
==> g <# (h <# M) = (g \<otimes> h) <# M"
@@ -300,7 +302,7 @@
done
-subsubsection {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
+subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
lemma (in group) setmult_rcos_assoc:
"[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
@@ -345,7 +347,29 @@
setmult_rcos_assoc subgroup_mult_id)
-subsection {*Lemmas Leading to Lagrange's Theorem *}
+subsubsection{*Two distinct right cosets are disjoint*}
+
+lemma (in group) rcos_equation:
+ "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
+ h \<in> H; ha \<in> H; hb \<in> H|]
+ ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
+apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
+apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
+apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
+done
+
+lemma (in group) rcos_disjoint:
+ "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
+apply (simp add: setrcos_eq r_coset_eq)
+apply (blast intro: rcos_equation sym)
+done
+
+
+subsection {*Order of a Group and Lagrange's Theorem*}
+
+constdefs
+ order :: "('a, 'b) semigroup_scheme => nat"
+ "order S == card (carrier S)"
lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
apply (rule equalityI)
@@ -387,41 +411,34 @@
apply (blast intro: finite_subset)
done
-
-subsection{*Two distinct right cosets are disjoint*}
-
-lemma (in group) rcos_equation:
- "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
- h \<in> H; ha \<in> H; hb \<in> H|]
- ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
-apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
-apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
-apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
-done
-
-lemma (in group) rcos_disjoint:
- "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
-apply (simp add: setrcos_eq r_coset_eq)
-apply (blast intro: rcos_equation sym)
-done
-
lemma (in group) setrcos_subset_PowG:
"subgroup H G ==> rcosets G H \<subseteq> Pow(carrier G)"
apply (simp add: setrcos_eq)
apply (blast dest: r_coset_subset_G subgroup.subset)
done
+
+theorem (in group) lagrange:
+ "[| finite(carrier G); subgroup H G |]
+ ==> card(rcosets G H) * card(H) = order(G)"
+apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
+apply (subst mult_commute)
+apply (rule card_partition)
+ apply (simp add: setrcos_subset_PowG [THEN finite_subset])
+ apply (simp add: setrcos_part_G)
+ apply (simp add: card_cosets_equal subgroup.subset)
+apply (simp add: rcos_disjoint)
+done
+
+
subsection {*Quotient Groups: Factorization of a Group*}
constdefs
FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
- (infixl "Mod" 60)
+ (infixl "Mod" 65)
--{*Actually defined for groups rather than monoids*}
"FactGroup G H ==
- (| carrier = rcosets G H,
- mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
- one = H |)"
-
+ (| carrier = rcosets G H, mult = set_mult G, one = H |)"
lemma (in group) setmult_closed:
"[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
@@ -435,15 +452,6 @@
subgroup.subset rcos_inv
setrcos_eq)
-(*
-The old version is no longer valid: "group G" has to be an explicit premise.
-
-lemma setinv_closed:
- "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup
- subgroup.subset coset.rcos_inv coset.setrcos_eq)
-*)
-
lemma (in group) setrcos_assoc:
"[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
@@ -461,18 +469,6 @@
by (auto simp add: setrcos_eq)
qed
-(*
-lemma subgroup_in_rcosets:
- "subgroup H G ==> H \<in> rcosets G H"
-apply (frule subgroup_imp_coset)
-apply (frule subgroup_imp_group)
-apply (simp add: coset.setrcos_eq)
-apply (blast del: equalityI
- intro!: group.subgroup.one_closed group.one_closed
- coset.coset_join2 [symmetric])
-done
-*)
-
lemma (in group) setrcos_inv_mult_group_eq:
"[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
@@ -499,6 +495,9 @@
apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
done
+lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
+ by (simp add: FactGroup_def)
+
lemma (in group) inv_FactGroup:
"N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
apply (rule group.inv_equality [OF factorgroup_is_group])
@@ -512,4 +511,130 @@
shows "(r_coset G N) \<in> hom G (G Mod N)"
by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N)
+
+subsection{*Quotienting by the Kernel of a Homomorphism*}
+
+constdefs
+ kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme =>
+ ('a => 'b) => 'a set"
+ --{*the kernel of a homomorphism*}
+ "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
+
+lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
+apply (rule group.subgroupI)
+apply (auto simp add: kernel_def group.intro prems)
+done
+
+text{*The kernel of a homomorphism is a normal subgroup*}
+lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
+apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
+apply (simp add: kernel_def)
+done
+
+lemma (in group_hom) FactGroup_nonempty:
+ assumes X: "X \<in> carrier (G Mod kernel G H h)"
+ shows "X \<noteq> {}"
+proof -
+ from X
+ obtain g where "g \<in> carrier G"
+ and "X = kernel G H h #> g"
+ by (auto simp add: FactGroup_def rcosets_def)
+ thus ?thesis
+ by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
+qed
+
+
+lemma (in group_hom) FactGroup_contents_mem:
+ assumes X: "X \<in> carrier (G Mod (kernel G H h))"
+ shows "contents (h`X) \<in> carrier H"
+proof -
+ from X
+ obtain g where g: "g \<in> carrier G"
+ and "X = kernel G H h #> g"
+ by (auto simp add: FactGroup_def rcosets_def)
+ hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
+ thus ?thesis by (auto simp add: g)
+qed
+
+lemma (in group_hom) FactGroup_hom:
+ "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
+proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
+ fix X and X'
+ assume X: "X \<in> carrier (G Mod kernel G H h)"
+ and X': "X' \<in> carrier (G Mod kernel G H h)"
+ then
+ obtain g and g'
+ where "g \<in> carrier G" and "g' \<in> carrier G"
+ and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
+ by (auto simp add: FactGroup_def rcosets_def)
+ hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
+ and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
+ by (force simp add: kernel_def r_coset_def image_def)+
+ hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
+ by (auto dest!: FactGroup_nonempty
+ simp add: set_mult_def image_eq_UN
+ subsetD [OF Xsub] subsetD [OF X'sub])
+ thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
+ by (simp add: all image_eq_UN FactGroup_nonempty X X')
+qed
+
+text{*Lemma for the following injectivity result*}
+lemma (in group_hom) FactGroup_subset:
+ "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
+ ==> kernel G H h #> g \<subseteq> kernel G H h #> g'"
+apply (clarsimp simp add: kernel_def r_coset_def image_def);
+apply (rename_tac y)
+apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
+apply (simp add: G.m_assoc);
+done
+
+lemma (in group_hom) FactGroup_inj_on:
+ "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
+proof (simp add: inj_on_def, clarify)
+ fix X and X'
+ assume X: "X \<in> carrier (G Mod kernel G H h)"
+ and X': "X' \<in> carrier (G Mod kernel G H h)"
+ then
+ obtain g and g'
+ where gX: "g \<in> carrier G" "g' \<in> carrier G"
+ "X = kernel G H h #> g" "X' = kernel G H h #> g'"
+ by (auto simp add: FactGroup_def rcosets_def)
+ hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
+ by (force simp add: kernel_def r_coset_def image_def)+
+ assume "contents (h ` X) = contents (h ` X')"
+ hence h: "h g = h g'"
+ by (simp add: image_eq_UN all FactGroup_nonempty X X')
+ show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
+qed
+
+text{*If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group*}
+lemma (in group_hom) FactGroup_onto:
+ assumes h: "h ` carrier G = carrier H"
+ shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
+proof
+ show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
+ by (auto simp add: FactGroup_contents_mem)
+ show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ proof
+ fix y
+ assume y: "y \<in> carrier H"
+ with h obtain g where g: "g \<in> carrier G" "h g = y"
+ by (blast elim: equalityE);
+ hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}"
+ by (auto simp add: y kernel_def r_coset_def)
+ with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
+ qed
+qed
+
+
+text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+theorem (in group_hom) FactGroup_iso:
+ "h ` carrier G = carrier H
+ \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
+by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
+ FactGroup_onto)
+
end
--- a/src/HOL/Algebra/Group.thy Mon May 24 18:35:34 2004 +0200
+++ b/src/HOL/Algebra/Group.thy Wed May 26 11:43:50 2004 +0200
@@ -593,15 +593,15 @@
subsection {* Isomorphisms *}
-constdefs (structure G and H)
- iso :: "_ => _ => ('a => 'b) set"
- "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
+constdefs
+ iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
+ "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
-lemma iso_refl: "(%x. x) \<in> iso G G"
+lemma iso_refl: "(%x. x) \<in> G \<cong> G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
lemma (in group) iso_sym:
- "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
+ "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
apply (simp add: iso_def bij_betw_Inv)
apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
@@ -609,15 +609,15 @@
done
lemma (in group) iso_trans:
- "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
+ "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
by (auto simp add: iso_def hom_compose bij_betw_compose)
lemma DirProdGroup_commute_iso:
- shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
+ shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
lemma DirProdGroup_assoc_iso:
- 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))"
+ 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))"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
--- a/src/HOL/Algebra/Sylow.thy Mon May 24 18:35:34 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy Wed May 26 11:43:50 2004 +0200
@@ -11,25 +11,6 @@
See also \cite{Kammueller-Paulson:1999}.
*}
-subsection {*Order of a Group and Lagrange's Theorem*}
-
-constdefs
- order :: "('a, 'b) semigroup_scheme => nat"
- "order S == card (carrier S)"
-
-theorem (in group) lagrange:
- "[| finite(carrier G); subgroup H G |]
- ==> card(rcosets G H) * card(H) = order(G)"
-apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
-apply (subst mult_commute)
-apply (rule card_partition)
- apply (simp add: setrcos_subset_PowG [THEN finite_subset])
- apply (simp add: setrcos_part_G)
- apply (simp add: card_cosets_equal subgroup.subset)
-apply (simp add: rcos_disjoint)
-done
-
-
text{*The combinatorial argument is in theory Exponent*}
locale sylow = group +