48 lemma r_coset_eq_set_mult: |
48 lemma r_coset_eq_set_mult: |
49 fixes G (structure) |
49 fixes G (structure) |
50 shows "H #> x = H <#> {x}" |
50 shows "H #> x = H <#> {x}" |
51 unfolding r_coset_def set_mult_def by simp |
51 unfolding r_coset_def set_mult_def by simp |
52 |
52 |
53 (* ************************************************************************** *) |
|
54 |
|
55 |
|
56 (* ************************************************************************** *) |
|
57 (* Next five lemmas contributed by Paulo Emílio de Vilhena. *) |
53 (* Next five lemmas contributed by Paulo Emílio de Vilhena. *) |
58 |
54 |
59 lemma (in subgroup) rcosets_not_empty: |
55 lemma (in subgroup) rcosets_non_empty: |
60 assumes "R \<in> rcosets H" |
56 assumes "R \<in> rcosets H" |
61 shows "R \<noteq> {}" |
57 shows "R \<noteq> {}" |
62 proof - |
58 proof - |
63 obtain g where "g \<in> carrier G" "R = H #> g" |
59 obtain g where "g \<in> carrier G" "R = H #> g" |
64 using assms unfolding RCOSETS_def by blast |
60 using assms unfolding RCOSETS_def by blast |
85 finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2" |
81 finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2" |
86 using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce |
82 using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce |
87 thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def) |
83 thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def) |
88 qed |
84 qed |
89 |
85 |
|
86 lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'" |
|
87 unfolding set_mult_def by (simp add: UN_mono) |
|
88 |
90 |
89 |
91 subsection \<open>Stable Operations for Subgroups\<close> |
90 subsection \<open>Stable Operations for Subgroups\<close> |
92 |
91 |
93 lemma (in group) subgroup_set_mult_equality[simp]: |
92 lemma (in group) subgroup_set_mult_equality[simp]: |
94 assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H" |
93 assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H" |
103 lemma (in group) subgroup_lcos_equality[simp]: |
102 lemma (in group) subgroup_lcos_equality[simp]: |
104 assumes "subgroup H G" "I \<subseteq> H" "h \<in> H" |
103 assumes "subgroup H G" "I \<subseteq> H" "h \<in> H" |
105 shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I" |
104 shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I" |
106 using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms) |
105 using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms) |
107 |
106 |
108 |
107 lemma set_mult_consistent [simp]: |
|
108 "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K" |
|
109 unfolding set_mult_def by simp |
|
110 |
|
111 lemma r_coset_consistent [simp]: |
|
112 "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h" |
|
113 unfolding r_coset_def by simp |
|
114 |
|
115 lemma l_coset_consistent [simp]: |
|
116 "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I" |
|
117 unfolding l_coset_def by simp |
109 |
118 |
110 subsection \<open>Basic Properties of set multiplication\<close> |
119 subsection \<open>Basic Properties of set multiplication\<close> |
111 |
120 |
112 lemma (in group) setmult_subset_G: |
121 lemma (in group) setmult_subset_G: |
113 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
122 assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G" |
1121 proof- |
1130 proof- |
1122 have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)" |
1131 have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)" |
1123 unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast |
1132 unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast |
1124 moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H). |
1133 moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H). |
1125 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) = x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)" |
1134 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) = x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)" |
1126 unfolding set_mult_def apply auto apply blast+. |
1135 unfolding set_mult_def by force |
1127 moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H). |
1136 moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H). |
1128 \<forall>ya\<in>carrier (K Mod N). x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)" |
1137 \<forall>ya\<in>carrier (K Mod N). x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)" |
1129 unfolding FactGroup_def using times_eq_iff subgroup.rcosets_not_empty |
1138 unfolding FactGroup_def using times_eq_iff subgroup.rcosets_non_empty |
1130 by (metis assms(2) assms(3) normal_def partial_object.select_convs(1)) |
1139 by (metis assms(2) assms(3) normal_def partial_object.select_convs(1)) |
1131 moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = |
1140 moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = |
1132 carrier (G \<times>\<times> K Mod H \<times> N)" |
1141 carrier (G \<times>\<times> K Mod H \<times> N)" |
1133 unfolding image_def apply auto using R apply force |
1142 unfolding image_def apply auto using R apply force |
1134 unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def apply auto apply force. |
1143 unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force |
1135 ultimately show ?thesis |
1144 ultimately show ?thesis |
1136 unfolding iso_def hom_def bij_betw_def inj_on_def by simp |
1145 unfolding iso_def hom_def bij_betw_def inj_on_def by simp |
1137 qed |
1146 qed |
1138 |
1147 |
1139 corollary (in group) FactGroup_DirProd_multiplication_iso_1 : |
1148 corollary (in group) FactGroup_DirProd_multiplication_iso_1 : |