|
1 section\<open>Free Abelian Groups\<close> |
|
2 |
|
3 theory Free_Abelian_Groups |
|
4 imports |
|
5 Product_Groups "HOL-Cardinals.Cardinal_Arithmetic" |
|
6 "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence" |
|
7 |
|
8 begin |
|
9 |
|
10 (*Move? But where?*) |
|
11 lemma eqpoll_Fpow: |
|
12 assumes "infinite A" shows "Fpow A \<approx> A" |
|
13 unfolding eqpoll_iff_card_of_ordIso |
|
14 by (metis assms card_of_Fpow_infinite) |
|
15 |
|
16 lemma infinite_iff_card_of_countable: "\<lbrakk>countable B; infinite B\<rbrakk> \<Longrightarrow> infinite A \<longleftrightarrow> ( |B| \<le>o |A| )" |
|
17 unfolding infinite_iff_countable_subset card_of_ordLeq countable_def |
|
18 by (force intro: card_of_ordLeqI ordLeq_transitive) |
|
19 |
|
20 lemma iso_imp_eqpoll_carrier: "G \<cong> H \<Longrightarrow> carrier G \<approx> carrier H" |
|
21 by (auto simp: is_iso_def iso_def eqpoll_def) |
|
22 |
|
23 subsection\<open>Generalised finite product\<close> |
|
24 |
|
25 definition |
|
26 gfinprod :: "[('b, 'm) monoid_scheme, 'a \<Rightarrow> 'b, 'a set] \<Rightarrow> 'b" |
|
27 where "gfinprod G f A = |
|
28 (if finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} then finprod G f {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>} else \<one>\<^bsub>G\<^esub>)" |
|
29 |
|
30 context comm_monoid begin |
|
31 |
|
32 lemma gfinprod_closed [simp]: |
|
33 "f \<in> A \<rightarrow> carrier G \<Longrightarrow> gfinprod G f A \<in> carrier G" |
|
34 unfolding gfinprod_def |
|
35 by (auto simp: image_subset_iff_funcset intro: finprod_closed) |
|
36 |
|
37 lemma gfinprod_cong: |
|
38 "\<lbrakk>A = B; f \<in> B \<rightarrow> carrier G; |
|
39 \<And>i. i \<in> B =simp=> f i = g i\<rbrakk> \<Longrightarrow> gfinprod G f A = gfinprod G g B" |
|
40 unfolding gfinprod_def |
|
41 by (auto simp: simp_implies_def cong: conj_cong intro: finprod_cong) |
|
42 |
|
43 lemma gfinprod_eq_finprod [simp]: "\<lbrakk>finite A; f \<in> A \<rightarrow> carrier G\<rbrakk> \<Longrightarrow> gfinprod G f A = finprod G f A" |
|
44 by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_left) |
|
45 |
|
46 lemma gfinprod_insert [simp]: |
|
47 assumes "finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>}" "f \<in> A \<rightarrow> carrier G" "f i \<in> carrier G" |
|
48 shows "gfinprod G f (insert i A) = (if i \<in> A then gfinprod G f A else f i \<otimes> gfinprod G f A)" |
|
49 proof - |
|
50 have f: "f \<in> {x \<in> A. f x \<noteq> \<one>} \<rightarrow> carrier G" |
|
51 using assms by (auto simp: image_subset_iff_funcset) |
|
52 have "{x. x = i \<and> f x \<noteq> \<one> \<or> x \<in> A \<and> f x \<noteq> \<one>} = (if f i = \<one> then {x \<in> A. f x \<noteq> \<one>} else insert i {x \<in> A. f x \<noteq> \<one>})" |
|
53 by auto |
|
54 then show ?thesis |
|
55 using assms |
|
56 unfolding gfinprod_def by (simp add: conj_disj_distribR insert_absorb f split: if_split_asm) |
|
57 qed |
|
58 |
|
59 lemma gfinprod_distrib: |
|
60 assumes fin: "finite {x \<in> A. f x \<noteq> \<one>\<^bsub>G\<^esub>}" "finite {x \<in> A. g x \<noteq> \<one>\<^bsub>G\<^esub>}" |
|
61 and "f \<in> A \<rightarrow> carrier G" "g \<in> A \<rightarrow> carrier G" |
|
62 shows "gfinprod G (\<lambda>i. f i \<otimes> g i) A = gfinprod G f A \<otimes> gfinprod G g A" |
|
63 proof - |
|
64 have "finite {x \<in> A. f x \<otimes> g x \<noteq> \<one>}" |
|
65 by (auto intro: finite_subset [OF _ finite_UnI [OF fin]]) |
|
66 then have "gfinprod G (\<lambda>i. f i \<otimes> g i) A = gfinprod G (\<lambda>i. f i \<otimes> g i) ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>})" |
|
67 unfolding gfinprod_def |
|
68 using assms by (force intro: finprod_mono_neutral_cong) |
|
69 also have "\<dots> = gfinprod G f A \<otimes> gfinprod G g A" |
|
70 proof - |
|
71 have "finprod G f ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>}) = gfinprod G f A" |
|
72 "finprod G g ({i \<in> A. f i \<noteq> \<one>\<^bsub>G\<^esub>} \<union> {i \<in> A. g i \<noteq> \<one>\<^bsub>G\<^esub>}) = gfinprod G g A" |
|
73 using assms by (auto simp: gfinprod_def intro: finprod_mono_neutral_cong_right) |
|
74 moreover have "(\<lambda>i. f i \<otimes> g i) \<in> {i \<in> A. f i \<noteq> \<one>} \<union> {i \<in> A. g i \<noteq> \<one>} \<rightarrow> carrier G" |
|
75 using assms by (force simp: image_subset_iff_funcset) |
|
76 ultimately show ?thesis |
|
77 using assms |
|
78 apply simp |
|
79 apply (subst finprod_multf, auto) |
|
80 done |
|
81 qed |
|
82 finally show ?thesis . |
|
83 qed |
|
84 |
|
85 lemma gfinprod_mono_neutral_cong_left: |
|
86 assumes "A \<subseteq> B" |
|
87 and 1: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" |
|
88 and gh: "\<And>x. x \<in> A \<Longrightarrow> g x = h x" |
|
89 and h: "h \<in> B \<rightarrow> carrier G" |
|
90 shows "gfinprod G g A = gfinprod G h B" |
|
91 proof (cases "finite {x \<in> B. h x \<noteq> \<one>}") |
|
92 case True |
|
93 then have "finite {x \<in> A. h x \<noteq> \<one>}" |
|
94 apply (rule rev_finite_subset) |
|
95 using \<open>A \<subseteq> B\<close> by auto |
|
96 with True assms show ?thesis |
|
97 apply (simp add: gfinprod_def cong: conj_cong) |
|
98 apply (auto intro!: finprod_mono_neutral_cong_left) |
|
99 done |
|
100 next |
|
101 case False |
|
102 have "{x \<in> B. h x \<noteq> \<one>} \<subseteq> {x \<in> A. h x \<noteq> \<one>}" |
|
103 using 1 by auto |
|
104 with False have "infinite {x \<in> A. h x \<noteq> \<one>}" |
|
105 using infinite_super by blast |
|
106 with False assms show ?thesis |
|
107 by (simp add: gfinprod_def cong: conj_cong) |
|
108 qed |
|
109 |
|
110 lemma gfinprod_mono_neutral_cong_right: |
|
111 assumes "A \<subseteq> B" "\<And>i. i \<in> B - A \<Longrightarrow> g i = \<one>" "\<And>x. x \<in> A \<Longrightarrow> g x = h x" "g \<in> B \<rightarrow> carrier G" |
|
112 shows "gfinprod G g B = gfinprod G h A" |
|
113 using assms by (auto intro!: gfinprod_mono_neutral_cong_left [symmetric]) |
|
114 |
|
115 lemma gfinprod_mono_neutral_cong: |
|
116 assumes [simp]: "finite B" "finite A" |
|
117 and *: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" "\<And>i. i \<in> A - B \<Longrightarrow> g i = \<one>" |
|
118 and gh: "\<And>x. x \<in> A \<inter> B \<Longrightarrow> g x = h x" |
|
119 and g: "g \<in> A \<rightarrow> carrier G" |
|
120 and h: "h \<in> B \<rightarrow> carrier G" |
|
121 shows "gfinprod G g A = gfinprod G h B" |
|
122 proof- |
|
123 have "gfinprod G g A = gfinprod G g (A \<inter> B)" |
|
124 by (rule gfinprod_mono_neutral_cong_right) (use assms in auto) |
|
125 also have "\<dots> = gfinprod G h (A \<inter> B)" |
|
126 by (rule gfinprod_cong) (use assms in auto) |
|
127 also have "\<dots> = gfinprod G h B" |
|
128 by (rule gfinprod_mono_neutral_cong_left) (use assms in auto) |
|
129 finally show ?thesis . |
|
130 qed |
|
131 |
|
132 end |
|
133 |
|
134 lemma (in comm_group) hom_group_sum: |
|
135 assumes hom: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> hom (A i) G" and grp: "\<And>i. i \<in> I \<Longrightarrow> group (A i)" |
|
136 shows "(\<lambda>x. gfinprod G (\<lambda>i. (f i) (x i)) I) \<in> hom (sum_group I A) G" |
|
137 unfolding hom_def |
|
138 proof (intro CollectI conjI ballI) |
|
139 show "(\<lambda>x. gfinprod G (\<lambda>i. f i (x i)) I) \<in> carrier (sum_group I A) \<rightarrow> carrier G" |
|
140 using assms |
|
141 by (force simp: hom_def carrier_sum_group intro: gfinprod_closed simp flip: image_subset_iff_funcset) |
|
142 next |
|
143 fix x y |
|
144 assume x: "x \<in> carrier (sum_group I A)" and y: "y \<in> carrier (sum_group I A)" |
|
145 then have finx: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>A i\<^esub>}" and finy: "finite {i \<in> I. y i \<noteq> \<one>\<^bsub>A i\<^esub>}" |
|
146 using assms by (auto simp: carrier_sum_group) |
|
147 have finfx: "finite {i \<in> I. f i (x i) \<noteq> \<one>}" |
|
148 using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finx]) |
|
149 have finfy: "finite {i \<in> I. f i (y i) \<noteq> \<one>}" |
|
150 using assms by (auto simp: is_group hom_one [OF hom] intro: finite_subset [OF _ finy]) |
|
151 have carr: "f i (x i) \<in> carrier G" "f i (y i) \<in> carrier G" if "i \<in> I" for i |
|
152 using hom_carrier [OF hom] that x y assms |
|
153 by (fastforce simp add: carrier_sum_group)+ |
|
154 have lam: "(\<lambda>i. f i ( x i \<otimes>\<^bsub>A i\<^esub> y i)) \<in> I \<rightarrow> carrier G" |
|
155 using x y assms by (auto simp: hom_def carrier_sum_group PiE_def Pi_def) |
|
156 have lam': "(\<lambda>i. f i (if i \<in> I then x i \<otimes>\<^bsub>A i\<^esub> y i else undefined)) \<in> I \<rightarrow> carrier G" |
|
157 by (simp add: lam Pi_cong) |
|
158 with lam x y assms |
|
159 show "gfinprod G (\<lambda>i. f i ((x \<otimes>\<^bsub>sum_group I A\<^esub> y) i)) I |
|
160 = gfinprod G (\<lambda>i. f i (x i)) I \<otimes> gfinprod G (\<lambda>i. f i (y i)) I" |
|
161 by (simp add: carrier_sum_group PiE_def Pi_def hom_mult [OF hom] |
|
162 gfinprod_distrib finfx finfy carr cong: gfinprod_cong) |
|
163 qed |
|
164 |
|
165 subsection\<open>Free Abelian groups on a set, using the "frag" type constructor. \<close> |
|
166 |
|
167 definition free_Abelian_group :: "'a set \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) monoid" |
|
168 where "free_Abelian_group S = \<lparr>carrier = {c. Poly_Mapping.keys c \<subseteq> S}, monoid.mult = (+), one = 0\<rparr>" |
|
169 |
|
170 lemma group_free_Abelian_group [simp]: "group (free_Abelian_group S)" |
|
171 proof - |
|
172 have "\<And>x. Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> x \<in> Units (free_Abelian_group S)" |
|
173 unfolding free_Abelian_group_def Units_def |
|
174 by clarsimp (metis eq_neg_iff_add_eq_0 neg_eq_iff_add_eq_0 keys_minus) |
|
175 then show ?thesis |
|
176 unfolding free_Abelian_group_def |
|
177 by unfold_locales (auto simp: dest: subsetD [OF keys_add]) |
|
178 qed |
|
179 |
|
180 lemma carrier_free_Abelian_group_iff [simp]: |
|
181 shows "x \<in> carrier (free_Abelian_group S) \<longleftrightarrow> Poly_Mapping.keys x \<subseteq> S" |
|
182 by (auto simp: free_Abelian_group_def) |
|
183 |
|
184 lemma one_free_Abelian_group [simp]: "\<one>\<^bsub>free_Abelian_group S\<^esub> = 0" |
|
185 by (auto simp: free_Abelian_group_def) |
|
186 |
|
187 lemma mult_free_Abelian_group [simp]: "x \<otimes>\<^bsub>free_Abelian_group S\<^esub> y = x + y" |
|
188 by (auto simp: free_Abelian_group_def) |
|
189 |
|
190 lemma inv_free_Abelian_group [simp]: "Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> inv\<^bsub>free_Abelian_group S\<^esub> x = -x" |
|
191 by (rule group.inv_equality [OF group_free_Abelian_group]) auto |
|
192 |
|
193 lemma abelian_free_Abelian_group: "comm_group(free_Abelian_group S)" |
|
194 apply (rule group.group_comm_groupI [OF group_free_Abelian_group]) |
|
195 by (simp add: free_Abelian_group_def) |
|
196 |
|
197 lemma pow_free_Abelian_group [simp]: |
|
198 fixes n::nat |
|
199 shows "Group.pow (free_Abelian_group S) x n = frag_cmul (int n) x" |
|
200 by (induction n) (auto simp: nat_pow_def free_Abelian_group_def frag_cmul_distrib) |
|
201 |
|
202 lemma int_pow_free_Abelian_group [simp]: |
|
203 fixes n::int |
|
204 assumes "Poly_Mapping.keys x \<subseteq> S" |
|
205 shows "Group.pow (free_Abelian_group S) x n = frag_cmul n x" |
|
206 proof (induction n) |
|
207 case (nonneg n) |
|
208 then show ?case |
|
209 by (simp add: int_pow_int) |
|
210 next |
|
211 case (neg n) |
|
212 have "x [^]\<^bsub>free_Abelian_group S\<^esub> - int (Suc n) |
|
213 = inv\<^bsub>free_Abelian_group S\<^esub> (x [^]\<^bsub>free_Abelian_group S\<^esub> int (Suc n))" |
|
214 by (rule group.int_pow_neg [OF group_free_Abelian_group]) (use assms in \<open>simp add: free_Abelian_group_def\<close>) |
|
215 also have "\<dots> = frag_cmul (- int (Suc n)) x" |
|
216 by (metis assms inv_free_Abelian_group pow_free_Abelian_group int_pow_int minus_frag_cmul |
|
217 order_trans keys_cmul) |
|
218 finally show ?case . |
|
219 qed |
|
220 |
|
221 lemma frag_of_in_free_Abelian_group [simp]: |
|
222 "frag_of x \<in> carrier(free_Abelian_group S) \<longleftrightarrow> x \<in> S" |
|
223 by simp |
|
224 |
|
225 lemma free_Abelian_group_induct: |
|
226 assumes major: "Poly_Mapping.keys x \<subseteq> S" |
|
227 and minor: "P(0)" |
|
228 "\<And>x y. \<lbrakk>Poly_Mapping.keys x \<subseteq> S; Poly_Mapping.keys y \<subseteq> S; P x; P y\<rbrakk> \<Longrightarrow> P(x-y)" |
|
229 "\<And>a. a \<in> S \<Longrightarrow> P(frag_of a)" |
|
230 shows "P x" |
|
231 proof - |
|
232 have "Poly_Mapping.keys x \<subseteq> S \<and> P x" |
|
233 using major |
|
234 proof (induction x rule: frag_induction) |
|
235 case (diff a b) |
|
236 then show ?case |
|
237 by (meson Un_least minor(2) order.trans keys_diff) |
|
238 qed (auto intro: minor) |
|
239 then show ?thesis .. |
|
240 qed |
|
241 |
|
242 lemma sum_closed_free_Abelian_group: |
|
243 "(\<And>i. i \<in> I \<Longrightarrow> x i \<in> carrier (free_Abelian_group S)) \<Longrightarrow> sum x I \<in> carrier (free_Abelian_group S)" |
|
244 apply (induction I rule: infinite_finite_induct, auto) |
|
245 by (metis (no_types, hide_lams) UnE subsetCE keys_add) |
|
246 |
|
247 |
|
248 lemma (in comm_group) free_Abelian_group_universal: |
|
249 fixes f :: "'c \<Rightarrow> 'a" |
|
250 assumes "f ` S \<subseteq> carrier G" |
|
251 obtains h where "h \<in> hom (free_Abelian_group S) G" "\<And>x. x \<in> S \<Longrightarrow> h(frag_of x) = f x" |
|
252 proof |
|
253 have fin: "Poly_Mapping.keys u \<subseteq> S \<Longrightarrow> finite {x \<in> S. f x [^] poly_mapping.lookup u x \<noteq> \<one>}" for u :: "'c \<Rightarrow>\<^sub>0 int" |
|
254 apply (rule finite_subset [OF _ finite_keys [of u]]) |
|
255 unfolding keys.rep_eq by force |
|
256 define h :: "('c \<Rightarrow>\<^sub>0 int) \<Rightarrow> 'a" |
|
257 where "h \<equiv> \<lambda>x. gfinprod G (\<lambda>a. f a [^] poly_mapping.lookup x a) S" |
|
258 show "h \<in> hom (free_Abelian_group S) G" |
|
259 proof (rule homI) |
|
260 fix x y |
|
261 assume xy: "x \<in> carrier (free_Abelian_group S)" "y \<in> carrier (free_Abelian_group S)" |
|
262 then show "h (x \<otimes>\<^bsub>free_Abelian_group S\<^esub> y) = h x \<otimes> h y" |
|
263 using assms unfolding h_def free_Abelian_group_def |
|
264 by (simp add: fin gfinprod_distrib image_subset_iff Poly_Mapping.lookup_add int_pow_mult cong: gfinprod_cong) |
|
265 qed (use assms in \<open>force simp: free_Abelian_group_def h_def intro: gfinprod_closed\<close>) |
|
266 show "h(frag_of x) = f x" if "x \<in> S" for x |
|
267 proof - |
|
268 have fin: "(\<lambda>a. f x [^] (1::int)) \<in> {x} \<rightarrow> carrier G" "f x [^] (1::int) \<in> carrier G" |
|
269 using assms that by force+ |
|
270 show ?thesis |
|
271 by (cases " f x [^] (1::int) = \<one>") (use assms that in \<open>auto simp: h_def gfinprod_def finprod_singleton\<close>) |
|
272 qed |
|
273 qed |
|
274 |
|
275 lemma eqpoll_free_Abelian_group_infinite: |
|
276 assumes "infinite A" shows "carrier(free_Abelian_group A) \<approx> A" |
|
277 proof (rule lepoll_antisym) |
|
278 have "carrier (free_Abelian_group A) \<lesssim> {f::'a\<Rightarrow>int. f ` A \<subseteq> UNIV \<and> {x. f x \<noteq> 0} \<subseteq> A \<and> finite {x. f x \<noteq> 0}}" |
|
279 unfolding lepoll_def |
|
280 by (rule_tac x="Poly_Mapping.lookup" in exI) (auto simp: poly_mapping_eqI lookup_not_eq_zero_eq_in_keys inj_onI) |
|
281 also have "\<dots> \<lesssim> Fpow (A \<times> (UNIV::int set))" |
|
282 by (rule lepoll_restricted_funspace) |
|
283 also have "\<dots> \<approx> A \<times> (UNIV::int set)" |
|
284 proof (rule eqpoll_Fpow) |
|
285 show "infinite (A \<times> (UNIV::int set))" |
|
286 using assms finite_cartesian_productD1 by fastforce |
|
287 qed |
|
288 also have "\<dots> \<approx> A" |
|
289 unfolding eqpoll_iff_card_of_ordIso |
|
290 proof - |
|
291 have "|A \<times> (UNIV::int set)| <=o |A|" |
|
292 by (simp add: assms card_of_Times_ordLeq_infinite flip: infinite_iff_card_of_countable) |
|
293 moreover have "|A| \<le>o |A \<times> (UNIV::int set)|" |
|
294 by simp |
|
295 ultimately have "|A| *c |(UNIV::int set)| =o |A|" |
|
296 by (simp add: cprod_def ordIso_iff_ordLeq) |
|
297 then show "|A \<times> (UNIV::int set)| =o |A|" |
|
298 by (metis Times_cprod ordIso_transitive) |
|
299 qed |
|
300 finally show "carrier (free_Abelian_group A) \<lesssim> A" . |
|
301 have "inj_on frag_of A" |
|
302 by (simp add: frag_of_eq inj_on_def) |
|
303 moreover have "frag_of ` A \<subseteq> carrier (free_Abelian_group A)" |
|
304 by (simp add: image_subsetI) |
|
305 ultimately show "A \<lesssim> carrier (free_Abelian_group A)" |
|
306 by (force simp: lepoll_def) |
|
307 qed |
|
308 |
|
309 proposition (in comm_group) eqpoll_homomorphisms_from_free_Abelian_group: |
|
310 "{f. f \<in> extensional (carrier(free_Abelian_group S)) \<and> f \<in> hom (free_Abelian_group S) G} |
|
311 \<approx> (S \<rightarrow>\<^sub>E carrier G)" (is "?lhs \<approx> ?rhs") |
|
312 unfolding eqpoll_def bij_betw_def |
|
313 proof (intro exI conjI) |
|
314 let ?f = "\<lambda>f. restrict (f \<circ> frag_of) S" |
|
315 show "inj_on ?f ?lhs" |
|
316 proof (clarsimp simp: inj_on_def) |
|
317 fix g h |
|
318 assume |
|
319 g: "g \<in> extensional (carrier (free_Abelian_group S))" "g \<in> hom (free_Abelian_group S) G" |
|
320 and h: "h \<in> extensional (carrier (free_Abelian_group S))" "h \<in> hom (free_Abelian_group S) G" |
|
321 and eq: "restrict (g \<circ> frag_of) S = restrict (h \<circ> frag_of) S" |
|
322 have 0: "0 \<in> carrier (free_Abelian_group S)" |
|
323 by simp |
|
324 interpret hom_g: group_hom "free_Abelian_group S" G g |
|
325 using g by (auto simp: group_hom_def group_hom_axioms_def is_group) |
|
326 interpret hom_h: group_hom "free_Abelian_group S" G h |
|
327 using h by (auto simp: group_hom_def group_hom_axioms_def is_group) |
|
328 have "Poly_Mapping.keys c \<subseteq> S \<Longrightarrow> Poly_Mapping.keys c \<subseteq> S \<and> g c = h c" for c |
|
329 proof (induction c rule: frag_induction) |
|
330 case zero |
|
331 show ?case |
|
332 using hom_g.hom_one hom_h.hom_one by auto |
|
333 next |
|
334 case (one x) |
|
335 then show ?case |
|
336 using eq by (simp add: fun_eq_iff) (metis comp_def) |
|
337 next |
|
338 case (diff a b) |
|
339 then show ?case |
|
340 using hom_g.hom_mult hom_h.hom_mult hom_g.hom_inv hom_h.hom_inv |
|
341 apply (auto simp: dest: subsetD [OF keys_diff]) |
|
342 by (metis keys_minus uminus_add_conv_diff) |
|
343 qed |
|
344 then show "g = h" |
|
345 by (meson g h carrier_free_Abelian_group_iff extensionalityI) |
|
346 qed |
|
347 have "f \<in> (\<lambda>f. restrict (f \<circ> frag_of) S) ` |
|
348 {f \<in> extensional (carrier (free_Abelian_group S)). f \<in> hom (free_Abelian_group S) G}" |
|
349 if f: "f \<in> S \<rightarrow>\<^sub>E carrier G" |
|
350 for f :: "'c \<Rightarrow> 'a" |
|
351 proof - |
|
352 obtain h where h: "h \<in> hom (free_Abelian_group S) G" "\<And>x. x \<in> S \<Longrightarrow> h(frag_of x) = f x" |
|
353 proof (rule free_Abelian_group_universal) |
|
354 show "f ` S \<subseteq> carrier G" |
|
355 using f by blast |
|
356 qed auto |
|
357 let ?h = "restrict h (carrier (free_Abelian_group S))" |
|
358 show ?thesis |
|
359 proof |
|
360 show "f = restrict (?h \<circ> frag_of) S" |
|
361 using f by (force simp: h) |
|
362 show "?h \<in> {f \<in> extensional (carrier (free_Abelian_group S)). f \<in> hom (free_Abelian_group S) G}" |
|
363 using h by (auto simp: hom_def dest!: subsetD [OF keys_add]) |
|
364 qed |
|
365 qed |
|
366 then show "?f ` ?lhs = S \<rightarrow>\<^sub>E carrier G" |
|
367 by (auto simp: hom_def Ball_def Pi_def) |
|
368 qed |
|
369 |
|
370 lemma hom_frag_minus: |
|
371 assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S" |
|
372 shows "h (-a) = - (h a)" |
|
373 proof - |
|
374 have "Poly_Mapping.keys (h a) \<subseteq> T" |
|
375 by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) |
|
376 then show ?thesis |
|
377 by (metis (no_types) assms carrier_free_Abelian_group_iff group_free_Abelian_group group_hom.hom_inv group_hom_axioms_def group_hom_def inv_free_Abelian_group) |
|
378 qed |
|
379 |
|
380 lemma hom_frag_add: |
|
381 assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S" "Poly_Mapping.keys b \<subseteq> S" |
|
382 shows "h (a+b) = h a + h b" |
|
383 proof - |
|
384 have "Poly_Mapping.keys (h a) \<subseteq> T" |
|
385 by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) |
|
386 moreover |
|
387 have "Poly_Mapping.keys (h b) \<subseteq> T" |
|
388 by (meson assms carrier_free_Abelian_group_iff hom_in_carrier) |
|
389 ultimately show ?thesis |
|
390 using assms hom_mult by fastforce |
|
391 qed |
|
392 |
|
393 lemma hom_frag_diff: |
|
394 assumes "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" "Poly_Mapping.keys a \<subseteq> S" "Poly_Mapping.keys b \<subseteq> S" |
|
395 shows "h (a-b) = h a - h b" |
|
396 by (metis (no_types, lifting) assms diff_conv_add_uminus hom_frag_add hom_frag_minus keys_minus) |
|
397 |
|
398 |
|
399 proposition isomorphic_free_Abelian_groups: |
|
400 "free_Abelian_group S \<cong> free_Abelian_group T \<longleftrightarrow> S \<approx> T" (is "(?FS \<cong> ?FT) = ?rhs") |
|
401 proof |
|
402 interpret S: group "?FS" |
|
403 by simp |
|
404 interpret T: group "?FT" |
|
405 by simp |
|
406 interpret G2: comm_group "integer_mod_group 2" |
|
407 by (rule abelian_integer_mod_group) |
|
408 let ?Two = "{0..<2::int}" |
|
409 have [simp]: "\<not> ?Two \<subseteq> {a}" for a |
|
410 by (simp add: subset_iff) presburger |
|
411 assume L: "?FS \<cong> ?FT" |
|
412 let ?HS = "{h \<in> extensional (carrier ?FS). h \<in> hom ?FS (integer_mod_group 2)}" |
|
413 let ?HT = "{h \<in> extensional (carrier ?FT). h \<in> hom ?FT (integer_mod_group 2)}" |
|
414 have "S \<rightarrow>\<^sub>E ?Two \<approx> ?HS" |
|
415 apply (rule eqpoll_sym) |
|
416 using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group) |
|
417 also have "\<dots> \<approx> ?HT" |
|
418 proof - |
|
419 obtain f g where "group_isomorphisms ?FS ?FT f g" |
|
420 using L S.iso_iff_group_isomorphisms by (force simp: is_iso_def) |
|
421 then have f: "f \<in> hom ?FS ?FT" |
|
422 and g: "g \<in> hom ?FT ?FS" |
|
423 and gf: "\<forall>x \<in> carrier ?FS. g(f x) = x" |
|
424 and fg: "\<forall>y \<in> carrier ?FT. f(g y) = y" |
|
425 by (auto simp: group_isomorphisms_def) |
|
426 let ?f = "\<lambda>h. restrict (h \<circ> g) (carrier ?FT)" |
|
427 let ?g = "\<lambda>h. restrict (h \<circ> f) (carrier ?FS)" |
|
428 show ?thesis |
|
429 proof (rule lepoll_antisym) |
|
430 show "?HS \<lesssim> ?HT" |
|
431 unfolding lepoll_def |
|
432 proof (intro exI conjI) |
|
433 show "inj_on ?f ?HS" |
|
434 apply (rule inj_on_inverseI [where g = ?g]) |
|
435 using hom_in_carrier [OF f] |
|
436 by (auto simp: gf fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def) |
|
437 show "?f ` ?HS \<subseteq> ?HT" |
|
438 proof clarsimp |
|
439 fix h |
|
440 assume h: "h \<in> hom ?FS (integer_mod_group 2)" |
|
441 have "h \<circ> g \<in> hom ?FT (integer_mod_group 2)" |
|
442 by (rule hom_compose [OF g h]) |
|
443 moreover have "restrict (h \<circ> g) (carrier ?FT) x = (h \<circ> g) x" if "x \<in> carrier ?FT" for x |
|
444 using g that by (simp add: hom_def) |
|
445 ultimately show "restrict (h \<circ> g) (carrier ?FT) \<in> hom ?FT (integer_mod_group 2)" |
|
446 using T.hom_restrict by fastforce |
|
447 qed |
|
448 qed |
|
449 next |
|
450 show "?HT \<lesssim> ?HS" |
|
451 unfolding lepoll_def |
|
452 proof (intro exI conjI) |
|
453 show "inj_on ?g ?HT" |
|
454 apply (rule inj_on_inverseI [where g = ?f]) |
|
455 using hom_in_carrier [OF g] |
|
456 by (auto simp: fg fun_eq_iff carrier_integer_mod_group Ball_def Pi_def extensional_def) |
|
457 show "?g ` ?HT \<subseteq> ?HS" |
|
458 proof clarsimp |
|
459 fix k |
|
460 assume k: "k \<in> hom ?FT (integer_mod_group 2)" |
|
461 have "k \<circ> f \<in> hom ?FS (integer_mod_group 2)" |
|
462 by (rule hom_compose [OF f k]) |
|
463 moreover have "restrict (k \<circ> f) (carrier ?FS) x = (k \<circ> f) x" if "x \<in> carrier ?FS" for x |
|
464 using f that by (simp add: hom_def) |
|
465 ultimately show "restrict (k \<circ> f) (carrier ?FS) \<in> hom ?FS (integer_mod_group 2)" |
|
466 using S.hom_restrict by fastforce |
|
467 qed |
|
468 qed |
|
469 qed |
|
470 qed |
|
471 also have "\<dots> \<approx> T \<rightarrow>\<^sub>E ?Two" |
|
472 using G2.eqpoll_homomorphisms_from_free_Abelian_group by (simp add: carrier_integer_mod_group) |
|
473 finally have *: "S \<rightarrow>\<^sub>E ?Two \<approx> T \<rightarrow>\<^sub>E ?Two" . |
|
474 then have "finite (S \<rightarrow>\<^sub>E ?Two) \<longleftrightarrow> finite (T \<rightarrow>\<^sub>E ?Two)" |
|
475 by (rule eqpoll_finite_iff) |
|
476 then have "finite S \<longleftrightarrow> finite T" |
|
477 by (auto simp: finite_funcset_iff) |
|
478 then consider "finite S" "finite T" | "~ finite S" "~ finite T" |
|
479 by blast |
|
480 then show ?rhs |
|
481 proof cases |
|
482 case 1 |
|
483 with * have "2 ^ card S = (2::nat) ^ card T" |
|
484 by (simp add: card_PiE finite_PiE eqpoll_iff_card) |
|
485 then have "card S = card T" |
|
486 by auto |
|
487 then show ?thesis |
|
488 using eqpoll_iff_card 1 by blast |
|
489 next |
|
490 case 2 |
|
491 have "carrier (free_Abelian_group S) \<approx> carrier (free_Abelian_group T)" |
|
492 using L by (simp add: iso_imp_eqpoll_carrier) |
|
493 then show ?thesis |
|
494 using 2 eqpoll_free_Abelian_group_infinite eqpoll_sym eqpoll_trans by metis |
|
495 qed |
|
496 next |
|
497 assume ?rhs |
|
498 then obtain f g where f: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> T \<and> g(f x) = x" |
|
499 and g: "\<And>y. y \<in> T \<Longrightarrow> g y \<in> S \<and> f(g y) = y" |
|
500 using eqpoll_iff_bijections by metis |
|
501 interpret S: comm_group "?FS" |
|
502 by (simp add: abelian_free_Abelian_group) |
|
503 interpret T: comm_group "?FT" |
|
504 by (simp add: abelian_free_Abelian_group) |
|
505 have "(frag_of \<circ> f) ` S \<subseteq> carrier (free_Abelian_group T)" |
|
506 using f by auto |
|
507 then obtain h where h: "h \<in> hom (free_Abelian_group S) (free_Abelian_group T)" |
|
508 and h_frag: "\<And>x. x \<in> S \<Longrightarrow> h (frag_of x) = (frag_of \<circ> f) x" |
|
509 using T.free_Abelian_group_universal [of "frag_of \<circ> f" S] by blast |
|
510 interpret hhom: group_hom "free_Abelian_group S" "free_Abelian_group T" h |
|
511 by (simp add: h group_hom_axioms_def group_hom_def) |
|
512 have "(frag_of \<circ> g) ` T \<subseteq> carrier (free_Abelian_group S)" |
|
513 using g by auto |
|
514 then obtain k where k: "k \<in> hom (free_Abelian_group T) (free_Abelian_group S)" |
|
515 and k_frag: "\<And>x. x \<in> T \<Longrightarrow> k (frag_of x) = (frag_of \<circ> g) x" |
|
516 using S.free_Abelian_group_universal [of "frag_of \<circ> g" T] by blast |
|
517 interpret khom: group_hom "free_Abelian_group T" "free_Abelian_group S" k |
|
518 by (simp add: k group_hom_axioms_def group_hom_def) |
|
519 have kh: "Poly_Mapping.keys x \<subseteq> S \<Longrightarrow> Poly_Mapping.keys x \<subseteq> S \<and> k (h x) = x" for x |
|
520 proof (induction rule: frag_induction) |
|
521 case zero |
|
522 then show ?case |
|
523 apply auto |
|
524 by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group) |
|
525 next |
|
526 case (one x) |
|
527 then show ?case |
|
528 by (auto simp: h_frag k_frag f) |
|
529 next |
|
530 case (diff a b) |
|
531 with keys_diff have "Poly_Mapping.keys (a - b) \<subseteq> S" |
|
532 by (metis Un_least order_trans) |
|
533 with diff hhom.hom_closed show ?case |
|
534 by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k]) |
|
535 qed |
|
536 have hk: "Poly_Mapping.keys y \<subseteq> T \<Longrightarrow> Poly_Mapping.keys y \<subseteq> T \<and> h (k y) = y" for y |
|
537 proof (induction rule: frag_induction) |
|
538 case zero |
|
539 then show ?case |
|
540 apply auto |
|
541 by (metis group_free_Abelian_group h hom_one k one_free_Abelian_group) |
|
542 next |
|
543 case (one y) |
|
544 then show ?case |
|
545 by (auto simp: h_frag k_frag g) |
|
546 next |
|
547 case (diff a b) |
|
548 with keys_diff have "Poly_Mapping.keys (a - b) \<subseteq> T" |
|
549 by (metis Un_least order_trans) |
|
550 with diff khom.hom_closed show ?case |
|
551 by (simp add: hom_frag_diff [OF h] hom_frag_diff [OF k]) |
|
552 qed |
|
553 have "h \<in> iso ?FS ?FT" |
|
554 unfolding iso_def bij_betw_iff_bijections mem_Collect_eq |
|
555 proof (intro conjI exI ballI h) |
|
556 fix x |
|
557 assume x: "x \<in> carrier (free_Abelian_group S)" |
|
558 show "h x \<in> carrier (free_Abelian_group T)" |
|
559 by (meson x h hom_in_carrier) |
|
560 show "k (h x) = x" |
|
561 using x by (simp add: kh) |
|
562 next |
|
563 fix y |
|
564 assume y: "y \<in> carrier (free_Abelian_group T)" |
|
565 show "k y \<in> carrier (free_Abelian_group S)" |
|
566 by (meson y k hom_in_carrier) |
|
567 show "h (k y) = y" |
|
568 using y by (simp add: hk) |
|
569 qed |
|
570 then show "?FS \<cong> ?FT" |
|
571 by (auto simp: is_iso_def) |
|
572 qed |
|
573 |
|
574 lemma isomorphic_group_integer_free_Abelian_group_singleton: |
|
575 "integer_group \<cong> free_Abelian_group {x}" |
|
576 proof - |
|
577 have "(\<lambda>n. frag_cmul n (frag_of x)) \<in> iso integer_group (free_Abelian_group {x})" |
|
578 proof (rule isoI [OF homI]) |
|
579 show "bij_betw (\<lambda>n. frag_cmul n (frag_of x)) (carrier integer_group) (carrier (free_Abelian_group {x}))" |
|
580 apply (rule bij_betwI [where g = "\<lambda>y. Poly_Mapping.lookup y x"]) |
|
581 by (auto simp: integer_group_def in_keys_iff intro!: poly_mapping_eqI) |
|
582 qed (auto simp: frag_cmul_distrib) |
|
583 then show ?thesis |
|
584 unfolding is_iso_def |
|
585 by blast |
|
586 qed |
|
587 |
|
588 lemma group_hom_free_Abelian_groups_id: |
|
589 "id \<in> hom (free_Abelian_group S) (free_Abelian_group T) \<longleftrightarrow> S \<subseteq> T" |
|
590 proof - |
|
591 have "x \<in> T" if ST: "\<And>c:: 'a \<Rightarrow>\<^sub>0 int. Poly_Mapping.keys c \<subseteq> S \<longrightarrow> Poly_Mapping.keys c \<subseteq> T" and "x \<in> S" for x |
|
592 using ST [of "frag_of x"] \<open>x \<in> S\<close> by simp |
|
593 then show ?thesis |
|
594 by (auto simp: hom_def free_Abelian_group_def Pi_def) |
|
595 qed |
|
596 |
|
597 |
|
598 proposition iso_free_Abelian_group_sum: |
|
599 assumes "pairwise (\<lambda>i j. disjnt (S i) (S j)) I" |
|
600 shows "(\<lambda>f. sum' f I) \<in> iso (sum_group I (\<lambda>i. free_Abelian_group(S i))) (free_Abelian_group (\<Union>(S ` I)))" |
|
601 (is "?h \<in> iso ?G ?H") |
|
602 proof (rule isoI) |
|
603 show hom: "?h \<in> hom ?G ?H" |
|
604 proof (rule homI) |
|
605 show "?h c \<in> carrier ?H" if "c \<in> carrier ?G" for c |
|
606 using that |
|
607 apply (simp add: sum.G_def carrier_sum_group) |
|
608 apply (rule order_trans [OF keys_sum]) |
|
609 apply (auto simp: free_Abelian_group_def) |
|
610 done |
|
611 show "?h (x \<otimes>\<^bsub>?G\<^esub> y) = ?h x \<otimes>\<^bsub>?H\<^esub> ?h y" |
|
612 if "x \<in> carrier ?G" "y \<in> carrier ?G" for x y |
|
613 using that apply (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib') |
|
614 sorry |
|
615 qed |
|
616 interpret GH: group_hom "?G" "?H" "?h" |
|
617 using hom by (simp add: group_hom_def group_hom_axioms_def) |
|
618 show "bij_betw ?h (carrier ?G) (carrier ?H)" |
|
619 unfolding bij_betw_def |
|
620 proof (intro conjI subset_antisym) |
|
621 show "?h ` carrier ?G \<subseteq> carrier ?H" |
|
622 apply (clarsimp simp: sum.G_def carrier_sum_group simp del: carrier_free_Abelian_group_iff) |
|
623 by (force simp: PiE_def Pi_iff intro!: sum_closed_free_Abelian_group) |
|
624 have *: "poly_mapping.lookup (Abs_poly_mapping (\<lambda>j. if j \<in> S i then poly_mapping.lookup x j else 0)) k |
|
625 = (if k \<in> S i then poly_mapping.lookup x k else 0)" if "i \<in> I" for i k and x :: "'b \<Rightarrow>\<^sub>0 int" |
|
626 using that by (auto simp: conj_commute cong: conj_cong) |
|
627 have eq: "Abs_poly_mapping (\<lambda>j. if j \<in> S i then poly_mapping.lookup x j else 0) = 0 |
|
628 \<longleftrightarrow> (\<forall>c \<in> S i. poly_mapping.lookup x c = 0)" if "i \<in> I" for i and x :: "'b \<Rightarrow>\<^sub>0 int" |
|
629 apply (auto simp: poly_mapping_eq_iff fun_eq_iff) |
|
630 apply (simp add: * Abs_poly_mapping_inverse conj_commute cong: conj_cong) |
|
631 apply (force dest!: spec split: if_split_asm) |
|
632 done |
|
633 have "x \<in> ?h ` {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}" |
|
634 if x: "Poly_Mapping.keys x \<subseteq> \<Union> (S ` I)" for x :: "'b \<Rightarrow>\<^sub>0 int" |
|
635 proof - |
|
636 let ?f = "(\<lambda>i c. if c \<in> S i then Poly_Mapping.lookup x c else 0)" |
|
637 define J where "J \<equiv> {i \<in> I. \<exists>c\<in>S i. c \<in> Poly_Mapping.keys x}" |
|
638 have "J \<subseteq> (\<lambda>c. THE i. i \<in> I \<and> c \<in> S i) ` Poly_Mapping.keys x" |
|
639 proof (clarsimp simp: J_def) |
|
640 show "i \<in> (\<lambda>c. THE i. i \<in> I \<and> c \<in> S i) ` Poly_Mapping.keys x" |
|
641 if "i \<in> I" "c \<in> S i" "c \<in> Poly_Mapping.keys x" for i c |
|
642 proof |
|
643 show "i = (THE i. i \<in> I \<and> c \<in> S i)" |
|
644 using assms that by (auto simp: pairwise_def disjnt_def intro: the_equality [symmetric]) |
|
645 qed (simp add: that) |
|
646 qed |
|
647 then have fin: "finite J" |
|
648 using finite_subset finite_keys by blast |
|
649 have [simp]: "Poly_Mapping.keys (Abs_poly_mapping (?f i)) = {k. ?f i k \<noteq> 0}" if "i \<in> I" for i |
|
650 by (simp add: eq_onp_def keys.abs_eq conj_commute cong: conj_cong) |
|
651 have [simp]: "Poly_Mapping.lookup (Abs_poly_mapping (?f i)) c = ?f i c" if "i \<in> I" for i c |
|
652 by (auto simp: Abs_poly_mapping_inverse conj_commute cong: conj_cong) |
|
653 show ?thesis |
|
654 proof |
|
655 have "poly_mapping.lookup x c = poly_mapping.lookup (?h (\<lambda>i\<in>I. Abs_poly_mapping (?f i))) c" |
|
656 for c |
|
657 proof (cases "c \<in> Poly_Mapping.keys x") |
|
658 case True |
|
659 then obtain i where "i \<in> I" "c \<in> S i" "?f i c \<noteq> 0" |
|
660 using x by (auto simp: in_keys_iff) |
|
661 then have 1: "poly_mapping.lookup (sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})) c = 0" |
|
662 using assms |
|
663 apply (simp add: sum.G_def Poly_Mapping.lookup_sum pairwise_def disjnt_def) |
|
664 apply (force simp: eq split: if_split_asm intro!: comm_monoid_add_class.sum.neutral) |
|
665 done |
|
666 have 2: "poly_mapping.lookup x c = poly_mapping.lookup (Abs_poly_mapping (?f i)) c" |
|
667 by (auto simp: \<open>c \<in> S i\<close> Abs_poly_mapping_inverse conj_commute cong: conj_cong) |
|
668 have "finite {i \<in> I. Abs_poly_mapping (?f i) \<noteq> 0}" |
|
669 by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>) |
|
670 with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})" |
|
671 apply (simp add: sum_diff1') |
|
672 sorry |
|
673 then show ?thesis |
|
674 by (simp add: 1 2 Poly_Mapping.lookup_add) |
|
675 next |
|
676 case False |
|
677 then have "poly_mapping.lookup x c = 0" |
|
678 using keys.rep_eq by force |
|
679 then show ?thesis |
|
680 unfolding sum.G_def by (simp add: lookup_sum * comm_monoid_add_class.sum.neutral) |
|
681 qed |
|
682 then show "x = ?h (\<lambda>i\<in>I. Abs_poly_mapping (?f i))" |
|
683 by (rule poly_mapping_eqI) |
|
684 have "(\<lambda>i. Abs_poly_mapping (?f i)) \<in> (\<Pi> i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i})" |
|
685 by (auto simp: PiE_def Pi_def in_keys_iff) |
|
686 then show "(\<lambda>i\<in>I. Abs_poly_mapping (?f i)) |
|
687 \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}" |
|
688 using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong) |
|
689 qed |
|
690 qed |
|
691 then show "carrier ?H \<subseteq> ?h ` carrier ?G" |
|
692 by (simp add: carrier_sum_group) (auto simp: free_Abelian_group_def) |
|
693 show "inj_on ?h (carrier (sum_group I (\<lambda>i. free_Abelian_group (S i))))" |
|
694 unfolding GH.inj_on_one_iff |
|
695 proof clarify |
|
696 fix x |
|
697 assume "x \<in> carrier ?G" "?h x = \<one>\<^bsub>?H\<^esub>" |
|
698 then have eq0: "sum' x I = 0" |
|
699 and xs: "\<And>i. i \<in> I \<Longrightarrow> Poly_Mapping.keys (x i) \<subseteq> S i" and xext: "x \<in> extensional I" |
|
700 and fin: "finite {i \<in> I. x i \<noteq> 0}" |
|
701 by (simp_all add: carrier_sum_group PiE_def Pi_def) |
|
702 have "x i = 0" if "i \<in> I" for i |
|
703 proof - |
|
704 have "sum' x (insert i (I - {i})) = 0" |
|
705 using eq0 that by (simp add: insert_absorb) |
|
706 moreover have "Poly_Mapping.keys (sum' x (I - {i})) = {}" |
|
707 proof - |
|
708 have "x i = - sum' x (I - {i})" |
|
709 by (metis (mono_tags, lifting) diff_zero eq0 fin sum_diff1' minus_diff_eq that) |
|
710 then have "Poly_Mapping.keys (x i) = Poly_Mapping.keys (sum' x (I - {i}))" |
|
711 by simp |
|
712 then have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> S i" |
|
713 using that xs by metis |
|
714 moreover |
|
715 have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> (\<Union>j \<in> I - {i}. S j)" |
|
716 proof - |
|
717 have "Poly_Mapping.keys (sum' x (I - {i})) \<subseteq> (\<Union>i\<in>{j \<in> I. j \<noteq> i \<and> x j \<noteq> 0}. Poly_Mapping.keys (x i))" |
|
718 using keys_sum [of x "{j \<in> I. j \<noteq> i \<and> x j \<noteq> 0}"] by (simp add: sum.G_def) |
|
719 also have "\<dots> \<subseteq> \<Union> (S ` (I - {i}))" |
|
720 using xs by force |
|
721 finally show ?thesis . |
|
722 qed |
|
723 moreover have "A = {}" if "A \<subseteq> S i" "A \<subseteq> \<Union> (S ` (I - {i}))" for A |
|
724 using assms that \<open>i \<in> I\<close> |
|
725 by (force simp: pairwise_def disjnt_def image_def subset_iff) |
|
726 ultimately show ?thesis |
|
727 by metis |
|
728 qed |
|
729 then have [simp]: "sum' x (I - {i}) = 0" |
|
730 by (auto simp: sum.G_def) |
|
731 have "sum' x (insert i (I - {i})) = x i" |
|
732 by (subst sum.insert' [OF finite_subset [OF _ fin]]) auto |
|
733 ultimately show ?thesis |
|
734 by metis |
|
735 qed |
|
736 with xext [unfolded extensional_def] |
|
737 show "x = \<one>\<^bsub>sum_group I (\<lambda>i. free_Abelian_group (S i))\<^esub>" |
|
738 by (force simp: free_Abelian_group_def) |
|
739 qed |
|
740 qed |
|
741 qed |
|
742 |
|
743 lemma isomorphic_free_Abelian_group_Union: |
|
744 "pairwise disjnt I \<Longrightarrow> free_Abelian_group(\<Union> I) \<cong> sum_group I free_Abelian_group" |
|
745 using iso_free_Abelian_group_sum [of "\<lambda>X. X" I] |
|
746 by (metis SUP_identity_eq empty_iff group.iso_sym group_free_Abelian_group is_iso_def sum_group) |
|
747 |
|
748 lemma isomorphic_sum_integer_group: |
|
749 "sum_group I (\<lambda>i. integer_group) \<cong> free_Abelian_group I" |
|
750 proof - |
|
751 have "sum_group I (\<lambda>i. integer_group) \<cong> sum_group I (\<lambda>i. free_Abelian_group {i})" |
|
752 by (rule iso_sum_groupI) (auto simp: isomorphic_group_integer_free_Abelian_group_singleton) |
|
753 also have "\<dots> \<cong> free_Abelian_group I" |
|
754 using iso_free_Abelian_group_sum [of "\<lambda>x. {x}" I] by (auto simp: is_iso_def) |
|
755 finally show ?thesis . |
|
756 qed |
|
757 |
|
758 end |