|
1 (* Title: Vector_Spaces.thy |
|
2 Author: Amine Chaieb, University of Cambridge |
|
3 Author: Jose Divasón <jose.divasonm at unirioja.es> |
|
4 Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> |
|
5 Author: Johannes Hölzl, VU Amsterdam |
|
6 Author: Fabian Immler, TUM |
|
7 *) |
|
8 |
|
9 section \<open>Vector Spaces\<close> |
|
10 |
|
11 theory Vector_Spaces |
|
12 imports Modules FuncSet |
|
13 begin |
|
14 |
|
15 lemma isomorphism_expand: |
|
16 "f \<circ> g = id \<and> g \<circ> f = id \<longleftrightarrow> (\<forall>x. f (g x) = x) \<and> (\<forall>x. g (f x) = x)" |
|
17 by (simp add: fun_eq_iff o_def id_def) |
|
18 |
|
19 lemma left_right_inverse_eq: |
|
20 assumes fg: "f \<circ> g = id" |
|
21 and gh: "g \<circ> h = id" |
|
22 shows "f = h" |
|
23 proof - |
|
24 have "f = f \<circ> (g \<circ> h)" |
|
25 unfolding gh by simp |
|
26 also have "\<dots> = (f \<circ> g) \<circ> h" |
|
27 by (simp add: o_assoc) |
|
28 finally show "f = h" |
|
29 unfolding fg by simp |
|
30 qed |
|
31 |
|
32 lemma ordLeq3_finite_infinite: |
|
33 assumes A: "finite A" and B: "infinite B" shows "ordLeq3 (card_of A) (card_of B)" |
|
34 proof - |
|
35 have \<open>ordLeq3 (card_of A) (card_of B) \<or> ordLeq3 (card_of B) (card_of A)\<close> |
|
36 by (intro ordLeq_total card_of_Well_order) |
|
37 moreover have "\<not> ordLeq3 (card_of B) (card_of A)" |
|
38 using B A card_of_ordLeq_finite[of B A] by auto |
|
39 ultimately show ?thesis by auto |
|
40 qed |
|
41 |
|
42 locale vector_space = |
|
43 fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75) |
|
44 assumes vector_space_assms:\<comment>\<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close> |
|
45 allows us to rewrite in the sublocale.\<close> |
|
46 "a *s (x + y) = a *s x + a *s y" |
|
47 "(a + b) *s x = a *s x + b *s x" |
|
48 "a *s (b *s x) = (a * b) *s x" |
|
49 "1 *s x = x" |
|
50 |
|
51 lemma module_iff_vector_space: "module s \<longleftrightarrow> vector_space s" |
|
52 unfolding module_def vector_space_def .. |
|
53 |
|
54 locale linear = vs1: vector_space s1 + vs2: vector_space s2 + module_hom s1 s2 f |
|
55 for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75) |
|
56 and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) |
|
57 and f :: "'b \<Rightarrow> 'c" |
|
58 |
|
59 lemma module_hom_iff_linear: "module_hom s1 s2 f \<longleftrightarrow> linear s1 s2 f" |
|
60 unfolding module_hom_def linear_def module_iff_vector_space by auto |
|
61 lemmas module_hom_eq_linear = module_hom_iff_linear[abs_def, THEN meta_eq_to_obj_eq] |
|
62 lemmas linear_iff_module_hom = module_hom_iff_linear[symmetric] |
|
63 lemmas linear_module_homI = module_hom_iff_linear[THEN iffD1] |
|
64 and module_hom_linearI = module_hom_iff_linear[THEN iffD2] |
|
65 |
|
66 context vector_space begin |
|
67 |
|
68 sublocale module scale rewrites "module_hom = linear" |
|
69 by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+ |
|
70 |
|
71 lemmas\<comment>\<open>from \<open>module\<close>\<close> |
|
72 linear_id = module_hom_id |
|
73 and linear_ident = module_hom_ident |
|
74 and linear_scale_self = module_hom_scale_self |
|
75 and linear_scale_left = module_hom_scale_left |
|
76 and linear_uminus = module_hom_uminus |
|
77 |
|
78 lemma linear_imp_scale: |
|
79 fixes D::"'a \<Rightarrow> 'b" |
|
80 assumes "linear ( *) scale D" |
|
81 obtains d where "D = (\<lambda>x. scale x d)" |
|
82 proof - |
|
83 interpret linear "( *)" scale D by fact |
|
84 show ?thesis |
|
85 by (metis mult.commute mult.left_neutral scale that) |
|
86 qed |
|
87 |
|
88 lemma scale_eq_0_iff [simp]: "scale a x = 0 \<longleftrightarrow> a = 0 \<or> x = 0" |
|
89 by (metis scale_left_commute right_inverse scale_one scale_scale scale_zero_left) |
|
90 |
|
91 lemma scale_left_imp_eq: |
|
92 assumes nonzero: "a \<noteq> 0" |
|
93 and scale: "scale a x = scale a y" |
|
94 shows "x = y" |
|
95 proof - |
|
96 from scale have "scale a (x - y) = 0" |
|
97 by (simp add: scale_right_diff_distrib) |
|
98 with nonzero have "x - y = 0" by simp |
|
99 then show "x = y" by (simp only: right_minus_eq) |
|
100 qed |
|
101 |
|
102 lemma scale_right_imp_eq: |
|
103 assumes nonzero: "x \<noteq> 0" |
|
104 and scale: "scale a x = scale b x" |
|
105 shows "a = b" |
|
106 proof - |
|
107 from scale have "scale (a - b) x = 0" |
|
108 by (simp add: scale_left_diff_distrib) |
|
109 with nonzero have "a - b = 0" by simp |
|
110 then show "a = b" by (simp only: right_minus_eq) |
|
111 qed |
|
112 |
|
113 lemma scale_cancel_left [simp]: "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0" |
|
114 by (auto intro: scale_left_imp_eq) |
|
115 |
|
116 lemma scale_cancel_right [simp]: "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0" |
|
117 by (auto intro: scale_right_imp_eq) |
|
118 |
|
119 lemma injective_scale: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x. scale c x)" |
|
120 by (simp add: inj_on_def) |
|
121 |
|
122 lemma dependent_def: "dependent P \<longleftrightarrow> (\<exists>a \<in> P. a \<in> span (P - {a}))" |
|
123 unfolding dependent_explicit |
|
124 proof safe |
|
125 fix a assume aP: "a \<in> P" and "a \<in> span (P - {a})" |
|
126 then obtain a S u |
|
127 where aP: "a \<in> P" and fS: "finite S" and SP: "S \<subseteq> P" "a \<notin> S" and ua: "(\<Sum>v\<in>S. u v *s v) = a" |
|
128 unfolding span_explicit by blast |
|
129 let ?S = "insert a S" |
|
130 let ?u = "\<lambda>y. if y = a then - 1 else u y" |
|
131 from fS SP have "(\<Sum>v\<in>?S. ?u v *s v) = 0" |
|
132 by (simp add: if_distrib[of "\<lambda>r. r *s a" for a] sum.If_cases field_simps Diff_eq[symmetric] ua) |
|
133 moreover have "finite ?S" "?S \<subseteq> P" "a \<in> ?S" "?u a \<noteq> 0" |
|
134 using fS SP aP by auto |
|
135 ultimately show "\<exists>t u. finite t \<and> t \<subseteq> P \<and> (\<Sum>v\<in>t. u v *s v) = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0)" by fast |
|
136 next |
|
137 fix S u v |
|
138 assume fS: "finite S" and SP: "S \<subseteq> P" and vS: "v \<in> S" |
|
139 and uv: "u v \<noteq> 0" and u: "(\<Sum>v\<in>S. u v *s v) = 0" |
|
140 let ?a = v |
|
141 let ?S = "S - {v}" |
|
142 let ?u = "\<lambda>i. (- u i) / u v" |
|
143 have th0: "?a \<in> P" "finite ?S" "?S \<subseteq> P" |
|
144 using fS SP vS by auto |
|
145 have "(\<Sum>v\<in>?S. ?u v *s v) = (\<Sum>v\<in>S. (- (inverse (u ?a))) *s (u v *s v)) - ?u v *s v" |
|
146 using fS vS uv by (simp add: sum_diff1 field_simps) |
|
147 also have "\<dots> = ?a" |
|
148 unfolding scale_sum_right[symmetric] u using uv by simp |
|
149 finally have "(\<Sum>v\<in>?S. ?u v *s v) = ?a" . |
|
150 with th0 show "\<exists>a \<in> P. a \<in> span (P - {a})" |
|
151 unfolding span_explicit by (auto intro!: bexI[where x="?a"] exI[where x="?S"] exI[where x="?u"]) |
|
152 qed |
|
153 |
|
154 lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0" |
|
155 unfolding dependent_def by auto |
|
156 |
|
157 lemma in_span_insert: |
|
158 assumes a: "a \<in> span (insert b S)" |
|
159 and na: "a \<notin> span S" |
|
160 shows "b \<in> span (insert a S)" |
|
161 proof - |
|
162 from span_breakdown[of b "insert b S" a, OF insertI1 a] |
|
163 obtain k where k: "a - k *s b \<in> span (S - {b})" by auto |
|
164 have "k \<noteq> 0" |
|
165 proof |
|
166 assume "k = 0" |
|
167 with k span_mono[of "S - {b}" S] have "a \<in> span S" by auto |
|
168 with na show False by blast |
|
169 qed |
|
170 then have eq: "b = (1/k) *s a - (1/k) *s (a - k *s b)" |
|
171 by (simp add: algebra_simps) |
|
172 |
|
173 from k have "(1/k) *s (a - k *s b) \<in> span (S - {b})" |
|
174 by (rule span_scale) |
|
175 also have "... \<subseteq> span (insert a S)" |
|
176 by (rule span_mono) auto |
|
177 finally show ?thesis |
|
178 using k by (subst eq) (blast intro: span_diff span_scale span_base) |
|
179 qed |
|
180 |
|
181 lemma dependent_insertD: assumes a: "a \<notin> span S" and S: "dependent (insert a S)" shows "dependent S" |
|
182 proof - |
|
183 have "a \<notin> S" using a by (auto dest: span_base) |
|
184 obtain b where b: "b = a \<or> b \<in> S" "b \<in> span (insert a S - {b})" |
|
185 using S unfolding dependent_def by blast |
|
186 have "b \<noteq> a" "b \<in> S" |
|
187 using b \<open>a \<notin> S\<close> a by auto |
|
188 with b have *: "b \<in> span (insert a (S - {b}))" |
|
189 by (auto simp: insert_Diff_if) |
|
190 show "dependent S" |
|
191 proof cases |
|
192 assume "b \<in> span (S - {b})" with \<open>b \<in> S\<close> show ?thesis |
|
193 by (auto simp add: dependent_def) |
|
194 next |
|
195 assume "b \<notin> span (S - {b})" |
|
196 with * have "a \<in> span (insert b (S - {b}))" by (rule in_span_insert) |
|
197 with a show ?thesis |
|
198 using \<open>b \<in> S\<close> by (auto simp: insert_absorb) |
|
199 qed |
|
200 qed |
|
201 |
|
202 lemma independent_insertI: "a \<notin> span S \<Longrightarrow> independent S \<Longrightarrow> independent (insert a S)" |
|
203 by (auto dest: dependent_insertD) |
|
204 |
|
205 lemma independent_insert: |
|
206 "independent (insert a S) \<longleftrightarrow> (if a \<in> S then independent S else independent S \<and> a \<notin> span S)" |
|
207 proof - |
|
208 have "a \<notin> S \<Longrightarrow> a \<in> span S \<Longrightarrow> dependent (insert a S)" |
|
209 by (auto simp: dependent_def) |
|
210 then show ?thesis |
|
211 by (auto intro: dependent_mono simp: independent_insertI) |
|
212 qed |
|
213 |
|
214 lemma maximal_independent_subset_extend: |
|
215 assumes "S \<subseteq> V" "independent S" |
|
216 shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B" |
|
217 proof - |
|
218 let ?C = "{B. S \<subseteq> B \<and> independent B \<and> B \<subseteq> V}" |
|
219 have "\<exists>M\<in>?C. \<forall>X\<in>?C. M \<subseteq> X \<longrightarrow> X = M" |
|
220 proof (rule subset_Zorn) |
|
221 fix C :: "'b set set" assume "subset.chain ?C C" |
|
222 then have C: "\<And>c. c \<in> C \<Longrightarrow> c \<subseteq> V" "\<And>c. c \<in> C \<Longrightarrow> S \<subseteq> c" "\<And>c. c \<in> C \<Longrightarrow> independent c" |
|
223 "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c" |
|
224 unfolding subset.chain_def by blast+ |
|
225 |
|
226 show "\<exists>U\<in>?C. \<forall>X\<in>C. X \<subseteq> U" |
|
227 proof cases |
|
228 assume "C = {}" with assms show ?thesis |
|
229 by (auto intro!: exI[of _ S]) |
|
230 next |
|
231 assume "C \<noteq> {}" |
|
232 with C(2) have "S \<subseteq> \<Union>C" |
|
233 by auto |
|
234 moreover have "independent (\<Union>C)" |
|
235 by (intro independent_Union_directed C) |
|
236 moreover have "\<Union>C \<subseteq> V" |
|
237 using C by auto |
|
238 ultimately show ?thesis |
|
239 by auto |
|
240 qed |
|
241 qed |
|
242 then obtain B where B: "independent B" "B \<subseteq> V" "S \<subseteq> B" |
|
243 and max: "\<And>S. independent S \<Longrightarrow> S \<subseteq> V \<Longrightarrow> B \<subseteq> S \<Longrightarrow> S = B" |
|
244 by auto |
|
245 moreover |
|
246 { assume "\<not> V \<subseteq> span B" |
|
247 then obtain v where "v \<in> V" "v \<notin> span B" |
|
248 by auto |
|
249 with B have "independent (insert v B)" by (auto intro: dependent_insertD) |
|
250 from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close> |
|
251 have "v \<in> B" |
|
252 by auto |
|
253 with \<open>v \<notin> span B\<close> have False |
|
254 by (auto intro: span_base) } |
|
255 ultimately show ?thesis |
|
256 by (auto intro!: exI[of _ B]) |
|
257 qed |
|
258 |
|
259 lemma maximal_independent_subset: "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B" |
|
260 by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty) |
|
261 |
|
262 text \<open>Extends a basis from B to a basis of the entire space.\<close> |
|
263 definition extend_basis :: "'b set \<Rightarrow> 'b set" |
|
264 where "extend_basis B = (SOME B'. B \<subseteq> B' \<and> independent B' \<and> span B' = UNIV)" |
|
265 |
|
266 lemma |
|
267 assumes B: "independent B" |
|
268 shows extend_basis_superset: "B \<subseteq> extend_basis B" |
|
269 and independent_extend_basis: "independent (extend_basis B)" |
|
270 and span_extend_basis[simp]: "span (extend_basis B) = UNIV" |
|
271 proof - |
|
272 define p where "p B' \<equiv> B \<subseteq> B' \<and> independent B' \<and> span B' = UNIV" for B' |
|
273 obtain B' where "p B'" |
|
274 using maximal_independent_subset_extend[OF subset_UNIV B] by (auto simp: p_def) |
|
275 then have "p (extend_basis B)" |
|
276 unfolding extend_basis_def p_def[symmetric] by (rule someI) |
|
277 then show "B \<subseteq> extend_basis B" "independent (extend_basis B)" "span (extend_basis B) = UNIV" |
|
278 by (auto simp: p_def) |
|
279 qed |
|
280 |
|
281 lemma in_span_delete: |
|
282 assumes a: "a \<in> span S" |
|
283 and na: "a \<notin> span (S - {b})" |
|
284 shows "b \<in> span (insert a (S - {b}))" |
|
285 apply (rule in_span_insert) |
|
286 apply (rule set_rev_mp) |
|
287 apply (rule a) |
|
288 apply (rule span_mono) |
|
289 apply blast |
|
290 apply (rule na) |
|
291 done |
|
292 |
|
293 lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S" |
|
294 unfolding span_def by (rule hull_redundant) |
|
295 |
|
296 lemma span_trans: "x \<in> span S \<Longrightarrow> y \<in> span (insert x S) \<Longrightarrow> y \<in> span S" |
|
297 by (simp only: span_redundant) |
|
298 |
|
299 lemma span_insert_0[simp]: "span (insert 0 S) = span S" |
|
300 by (metis span_zero span_redundant) |
|
301 |
|
302 lemma span_delete_0 [simp]: "span(S - {0}) = span S" |
|
303 proof |
|
304 show "span (S - {0}) \<subseteq> span S" |
|
305 by (blast intro!: span_mono) |
|
306 next |
|
307 have "span S \<subseteq> span(insert 0 (S - {0}))" |
|
308 by (blast intro!: span_mono) |
|
309 also have "... \<subseteq> span(S - {0})" |
|
310 using span_insert_0 by blast |
|
311 finally show "span S \<subseteq> span (S - {0})" . |
|
312 qed |
|
313 |
|
314 lemma span_image_scale: |
|
315 assumes "finite S" and nz: "\<And>x. x \<in> S \<Longrightarrow> c x \<noteq> 0" |
|
316 shows "span ((\<lambda>x. c x *s x) ` S) = span S" |
|
317 using assms |
|
318 proof (induction S arbitrary: c) |
|
319 case (empty c) show ?case by simp |
|
320 next |
|
321 case (insert x F c) |
|
322 show ?case |
|
323 proof (intro set_eqI iffI) |
|
324 fix y |
|
325 assume "y \<in> span ((\<lambda>x. c x *s x) ` insert x F)" |
|
326 then show "y \<in> span (insert x F)" |
|
327 using insert by (force simp: span_breakdown_eq) |
|
328 next |
|
329 fix y |
|
330 assume "y \<in> span (insert x F)" |
|
331 then show "y \<in> span ((\<lambda>x. c x *s x) ` insert x F)" |
|
332 using insert |
|
333 apply (clarsimp simp: span_breakdown_eq) |
|
334 apply (rule_tac x="k / c x" in exI) |
|
335 by simp |
|
336 qed |
|
337 qed |
|
338 |
|
339 lemma exchange_lemma: |
|
340 assumes f: "finite t" |
|
341 and i: "independent s" |
|
342 and sp: "s \<subseteq> span t" |
|
343 shows "\<exists>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'" |
|
344 using f i sp |
|
345 proof (induct "card (t - s)" arbitrary: s t rule: less_induct) |
|
346 case less |
|
347 note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t` |
|
348 let ?P = "\<lambda>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'" |
|
349 let ?ths = "\<exists>t'. ?P t'" |
|
350 |
|
351 { |
|
352 assume st: "t \<subseteq> s" |
|
353 from spanning_subset_independent[OF st s sp] st ft span_mono[OF st] |
|
354 have ?ths by (auto intro: span_base) |
|
355 } |
|
356 moreover |
|
357 { |
|
358 assume st:"\<not> t \<subseteq> s" |
|
359 from st obtain b where b: "b \<in> t" "b \<notin> s" |
|
360 by blast |
|
361 from b have "t - {b} - s \<subset> t - s" |
|
362 by blast |
|
363 then have cardlt: "card (t - {b} - s) < card (t - s)" |
|
364 using ft by (auto intro: psubset_card_mono) |
|
365 from b ft have ct0: "card t \<noteq> 0" |
|
366 by auto |
|
367 have ?ths |
|
368 proof cases |
|
369 assume stb: "s \<subseteq> span (t - {b})" |
|
370 from ft have ftb: "finite (t - {b})" |
|
371 by auto |
|
372 from less(1)[OF cardlt ftb s stb] |
|
373 obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" |
|
374 and fu: "finite u" by blast |
|
375 let ?w = "insert b u" |
|
376 have th0: "s \<subseteq> insert b u" |
|
377 using u by blast |
|
378 from u(3) b have "u \<subseteq> s \<union> t" |
|
379 by blast |
|
380 then have th1: "insert b u \<subseteq> s \<union> t" |
|
381 using u b by blast |
|
382 have bu: "b \<notin> u" |
|
383 using b u by blast |
|
384 from u(1) ft b have "card u = (card t - 1)" |
|
385 by auto |
|
386 then have th2: "card (insert b u) = card t" |
|
387 using card_insert_disjoint[OF fu bu] ct0 by auto |
|
388 from u(4) have "s \<subseteq> span u" . |
|
389 also have "\<dots> \<subseteq> span (insert b u)" |
|
390 by (rule span_mono) blast |
|
391 finally have th3: "s \<subseteq> span (insert b u)" . |
|
392 from th0 th1 th2 th3 fu have th: "?P ?w" |
|
393 by blast |
|
394 from th show ?thesis by blast |
|
395 next |
|
396 assume stb: "\<not> s \<subseteq> span (t - {b})" |
|
397 from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})" |
|
398 by blast |
|
399 have ab: "a \<noteq> b" |
|
400 using a b by blast |
|
401 have at: "a \<notin> t" |
|
402 using a ab span_base[of a "t- {b}"] by auto |
|
403 have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" |
|
404 using cardlt ft a b by auto |
|
405 have ft': "finite (insert a (t - {b}))" |
|
406 using ft by auto |
|
407 { |
|
408 fix x |
|
409 assume xs: "x \<in> s" |
|
410 have t: "t \<subseteq> insert b (insert a (t - {b}))" |
|
411 using b by auto |
|
412 have bs: "b \<in> span (insert a (t - {b}))" |
|
413 apply (rule in_span_delete) |
|
414 using a sp unfolding subset_eq |
|
415 apply auto |
|
416 done |
|
417 from xs sp have "x \<in> span t" |
|
418 by blast |
|
419 with span_mono[OF t] have x: "x \<in> span (insert b (insert a (t - {b})))" .. |
|
420 from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" . |
|
421 } |
|
422 then have sp': "s \<subseteq> span (insert a (t - {b}))" |
|
423 by blast |
|
424 from less(1)[OF mlt ft' s sp'] obtain u where u: |
|
425 "card u = card (insert a (t - {b}))" |
|
426 "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})" |
|
427 "s \<subseteq> span u" by blast |
|
428 from u a b ft at ct0 have "?P u" |
|
429 by auto |
|
430 then show ?thesis by blast |
|
431 qed |
|
432 } |
|
433 ultimately show ?ths by blast |
|
434 qed |
|
435 |
|
436 lemma independent_span_bound: |
|
437 assumes f: "finite t" |
|
438 and i: "independent s" |
|
439 and sp: "s \<subseteq> span t" |
|
440 shows "finite s \<and> card s \<le> card t" |
|
441 by (metis exchange_lemma[OF f i sp] finite_subset card_mono) |
|
442 |
|
443 lemma independent_explicit_finite_subsets: |
|
444 "independent A \<longleftrightarrow> (\<forall>S \<subseteq> A. finite S \<longrightarrow> (\<forall>u. (\<Sum>v\<in>S. u v *s v) = 0 \<longrightarrow> (\<forall>v\<in>S. u v = 0)))" |
|
445 unfolding dependent_explicit [of A] by (simp add: disj_not2) |
|
446 |
|
447 lemma independent_if_scalars_zero: |
|
448 assumes fin_A: "finite A" |
|
449 and sum: "\<And>f x. (\<Sum>x\<in>A. f x *s x) = 0 \<Longrightarrow> x \<in> A \<Longrightarrow> f x = 0" |
|
450 shows "independent A" |
|
451 proof (unfold independent_explicit_finite_subsets, clarify) |
|
452 fix S v and u :: "'b \<Rightarrow> 'a" |
|
453 assume S: "S \<subseteq> A" and v: "v \<in> S" |
|
454 let ?g = "\<lambda>x. if x \<in> S then u x else 0" |
|
455 have "(\<Sum>v\<in>A. ?g v *s v) = (\<Sum>v\<in>S. u v *s v)" |
|
456 using S fin_A by (auto intro!: sum.mono_neutral_cong_right) |
|
457 also assume "(\<Sum>v\<in>S. u v *s v) = 0" |
|
458 finally have "?g v = 0" using v S sum by force |
|
459 thus "u v = 0" unfolding if_P[OF v] . |
|
460 qed |
|
461 |
|
462 lemma bij_if_span_eq_span_bases: |
|
463 assumes B: "independent B" and C: "independent C" |
|
464 and eq: "span B = span C" |
|
465 shows "\<exists>f. bij_betw f B C" |
|
466 proof cases |
|
467 assume "finite B \<or> finite C" |
|
468 then have "finite B \<and> finite C \<and> card C = card B" |
|
469 using independent_span_bound[of B C] independent_span_bound[of C B] assms |
|
470 span_superset[of B] span_superset[of C] |
|
471 by auto |
|
472 then show ?thesis |
|
473 by (auto intro!: finite_same_card_bij) |
|
474 next |
|
475 assume "\<not> (finite B \<or> finite C)" |
|
476 then have "infinite B" "infinite C" by auto |
|
477 { fix B C assume B: "independent B" and C: "independent C" and "infinite B" "infinite C" and eq: "span B = span C" |
|
478 let ?R = "representation B" and ?R' = "representation C" let ?U = "\<lambda>c. {v. ?R c v \<noteq> 0}" |
|
479 have in_span_C [simp, intro]: \<open>b \<in> B \<Longrightarrow> b \<in> span C\<close> for b unfolding eq[symmetric] by (rule span_base) |
|
480 have in_span_B [simp, intro]: \<open>c \<in> C \<Longrightarrow> c \<in> span B\<close> for c unfolding eq by (rule span_base) |
|
481 have \<open>B \<subseteq> (\<Union>c\<in>C. ?U c)\<close> |
|
482 proof |
|
483 fix b assume \<open>b \<in> B\<close> |
|
484 have \<open>b \<in> span C\<close> |
|
485 using \<open>b \<in> B\<close> unfolding eq[symmetric] by (rule span_base) |
|
486 have \<open>(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) = |
|
487 (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close> |
|
488 by (simp add: scale_sum_right) |
|
489 also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s v)\<close> |
|
490 by (auto simp: sum_nonzero_representation_eq B eq span_base representation_ne_zero) |
|
491 also have \<open>\<dots> = b\<close> |
|
492 by (rule sum_nonzero_representation_eq[OF C \<open>b \<in> span C\<close>]) |
|
493 finally have "?R b b = ?R (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) b" |
|
494 by simp |
|
495 also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b)\<close> |
|
496 using B \<open>b \<in> B\<close> |
|
497 apply (subst representation_sum[OF B]) |
|
498 apply (fastforce intro: span_sum span_scale span_base representation_ne_zero) |
|
499 apply (rule sum.cong[OF refl]) |
|
500 apply (subst representation_sum[OF B]) |
|
501 apply (simp add: span_sum span_scale span_base representation_ne_zero) |
|
502 apply (simp add: representation_scale[OF B] span_base representation_ne_zero) |
|
503 done |
|
504 finally have "(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b) \<noteq> 0" |
|
505 using representation_basis[OF B \<open>b \<in> B\<close>] by auto |
|
506 then obtain v w where bv: "?R' b v \<noteq> 0" and vw: "?R v w \<noteq> 0" and "?R' b v * ?R v w * ?R w b \<noteq> 0" |
|
507 by (blast elim: sum.not_neutral_contains_not_neutral) |
|
508 with representation_basis[OF B, of w] vw[THEN representation_ne_zero] |
|
509 have \<open>?R' b v \<noteq> 0\<close> \<open>?R v b \<noteq> 0\<close> by (auto split: if_splits) |
|
510 then show \<open>b \<in> (\<Union>c\<in>C. ?U c)\<close> |
|
511 by (auto dest: representation_ne_zero) |
|
512 qed |
|
513 then have B_eq: \<open>B = (\<Union>c\<in>C. ?U c)\<close> |
|
514 by (auto intro: span_base representation_ne_zero eq) |
|
515 have "ordLeq3 (card_of B) (card_of C)" |
|
516 proof (subst B_eq, rule card_of_UNION_ordLeq_infinite[OF \<open>infinite C\<close>]) |
|
517 show "ordLeq3 (card_of C) (card_of C)" |
|
518 by (intro ordLeq_refl card_of_Card_order) |
|
519 show "\<forall>c\<in>C. ordLeq3 (card_of {v. representation B c v \<noteq> 0}) (card_of C)" |
|
520 by (intro ballI ordLeq3_finite_infinite \<open>infinite C\<close> finite_representation) |
|
521 qed } |
|
522 from this[of B C] this[of C B] B C eq \<open>infinite C\<close> \<open>infinite B\<close> |
|
523 show ?thesis by (auto simp add: ordIso_iff_ordLeq card_of_ordIso) |
|
524 qed |
|
525 |
|
526 definition dim :: "'b set \<Rightarrow> nat" |
|
527 where "dim V = card (SOME b. independent b \<and> span b = span V)" |
|
528 |
|
529 lemma dim_eq_card: |
|
530 assumes BV: "span B = span V" and B: "independent B" |
|
531 shows "dim V = card B" |
|
532 proof - |
|
533 define p where "p b \<equiv> independent b \<and> span b = span V" for b |
|
534 have "p (SOME B. p B)" |
|
535 using assms by (intro someI[of p B]) (auto simp: p_def) |
|
536 then have "\<exists>f. bij_betw f B (SOME B. p B)" |
|
537 by (subst (asm) p_def, intro bij_if_span_eq_span_bases[OF B]) (simp_all add: BV) |
|
538 then have "card B = card (SOME B. p B)" |
|
539 by (auto intro: bij_betw_same_card) |
|
540 then show ?thesis |
|
541 by (simp add: dim_def p_def) |
|
542 qed |
|
543 |
|
544 lemma basis_card_eq_dim: "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = dim V" |
|
545 using dim_eq_card[of B V] span_mono[of B V] span_minimal[OF _ subspace_span, of V B] by auto |
|
546 |
|
547 lemma basis_exists: "\<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> card B = dim V" |
|
548 by (meson basis_card_eq_dim empty_subsetI independent_empty maximal_independent_subset_extend) |
|
549 |
|
550 lemma dim_eq_card_independent: "independent B \<Longrightarrow> dim B = card B" |
|
551 by (rule dim_eq_card[OF refl]) |
|
552 |
|
553 lemma dim_span[simp]: "dim (span S) = dim S" |
|
554 by (simp add: dim_def span_span) |
|
555 |
|
556 lemma dim_span_eq_card_independent: "independent B \<Longrightarrow> dim (span B) = card B" |
|
557 by (simp add: dim_span dim_eq_card) |
|
558 |
|
559 lemma dim_le_card: assumes "V \<subseteq> span W" "finite W" shows "dim V \<le> card W" |
|
560 proof - |
|
561 obtain A where "independent A" "A \<subseteq> V" "V \<subseteq> span A" |
|
562 using maximal_independent_subset[of V] by auto |
|
563 with assms independent_span_bound[of W A] basis_card_eq_dim[of A V] |
|
564 show ?thesis by auto |
|
565 qed |
|
566 |
|
567 lemma span_eq_dim: "span S = span T \<Longrightarrow> dim S = dim T" |
|
568 by (metis dim_span) |
|
569 |
|
570 corollary dim_le_card': |
|
571 "finite s \<Longrightarrow> dim s \<le> card s" |
|
572 by (metis basis_exists card_mono) |
|
573 |
|
574 lemma span_card_ge_dim: |
|
575 "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B" |
|
576 by (simp add: dim_le_card) |
|
577 |
|
578 lemma dim_unique: |
|
579 "B \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n" |
|
580 by (metis basis_card_eq_dim) |
|
581 |
|
582 lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}" |
|
583 apply (simp add: subspace_def) |
|
584 apply (intro conjI impI allI) |
|
585 using add.right_neutral apply blast |
|
586 apply clarify |
|
587 apply (metis add.assoc add.left_commute) |
|
588 using scale_right_distrib by blast |
|
589 |
|
590 end |
|
591 |
|
592 lemma linear_iff: "linear s1 s2 f \<longleftrightarrow> |
|
593 (vector_space s1 \<and> vector_space s2 \<and> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (s1 c x) = s2 c (f x)))" |
|
594 unfolding linear_def module_hom_iff vector_space_def module_def by auto |
|
595 |
|
596 context begin |
|
597 qualified lemma linear_compose: "linear s1 s2 f \<Longrightarrow> linear s2 s3 g \<Longrightarrow> linear s1 s3 (g o f)" |
|
598 unfolding module_hom_iff_linear[symmetric] |
|
599 by (rule module_hom_compose) |
|
600 end |
|
601 |
|
602 locale vector_space_pair = vs1: vector_space s1 + vs2: vector_space s2 |
|
603 for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75) |
|
604 and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) |
|
605 begin |
|
606 |
|
607 context fixes f assumes "linear s1 s2 f" begin |
|
608 interpretation linear s1 s2 f by fact |
|
609 lemmas\<comment>\<open>from locale \<open>module_hom\<close>\<close> |
|
610 linear_0 = zero |
|
611 and linear_add = add |
|
612 and linear_scale = scale |
|
613 and linear_neg = neg |
|
614 and linear_diff = diff |
|
615 and linear_sum = sum |
|
616 and linear_inj_on_iff_eq_0 = inj_on_iff_eq_0 |
|
617 and linear_inj_iff_eq_0 = inj_iff_eq_0 |
|
618 and linear_subspace_image = subspace_image |
|
619 and linear_subspace_vimage = subspace_vimage |
|
620 and linear_subspace_kernel = subspace_kernel |
|
621 and linear_span_image = span_image |
|
622 and linear_dependent_inj_imageD = dependent_inj_imageD |
|
623 and linear_eq_0_on_span = eq_0_on_span |
|
624 and linear_independent_injective_image = independent_injective_image |
|
625 and linear_inj_on_span_independent_image = inj_on_span_independent_image |
|
626 and linear_inj_on_span_iff_independent_image = inj_on_span_iff_independent_image |
|
627 and linear_subspace_linear_preimage = subspace_linear_preimage |
|
628 and linear_spans_image = spans_image |
|
629 and linear_spanning_surjective_image = spanning_surjective_image |
|
630 end |
|
631 |
|
632 sublocale module_pair |
|
633 rewrites "module_hom = linear" |
|
634 by unfold_locales (fact module_hom_eq_linear) |
|
635 |
|
636 lemmas\<comment>\<open>from locale \<open>module_pair\<close>\<close> |
|
637 linear_eq_on_span = module_hom_eq_on_span |
|
638 and linear_compose_scale_right = module_hom_scale |
|
639 and linear_compose_add = module_hom_add |
|
640 and linear_zero = module_hom_zero |
|
641 and linear_compose_sub = module_hom_sub |
|
642 and linear_compose_neg = module_hom_neg |
|
643 and linear_compose_scale = module_hom_compose_scale |
|
644 |
|
645 lemma linear_indep_image_lemma: |
|
646 assumes lf: "linear s1 s2 f" |
|
647 and fB: "finite B" |
|
648 and ifB: "vs2.independent (f ` B)" |
|
649 and fi: "inj_on f B" |
|
650 and xsB: "x \<in> vs1.span B" |
|
651 and fx: "f x = 0" |
|
652 shows "x = 0" |
|
653 using fB ifB fi xsB fx |
|
654 proof (induct arbitrary: x rule: finite_induct[OF fB]) |
|
655 case 1 |
|
656 then show ?case by auto |
|
657 next |
|
658 case (2 a b x) |
|
659 have fb: "finite b" using "2.prems" by simp |
|
660 have th0: "f ` b \<subseteq> f ` (insert a b)" |
|
661 apply (rule image_mono) |
|
662 apply blast |
|
663 done |
|
664 from vs2.independent_mono[ OF "2.prems"(2) th0] |
|
665 have ifb: "vs2.independent (f ` b)" . |
|
666 have fib: "inj_on f b" |
|
667 apply (rule subset_inj_on [OF "2.prems"(3)]) |
|
668 apply blast |
|
669 done |
|
670 from vs1.span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] |
|
671 obtain k where k: "x - k *a a \<in> vs1.span (b - {a})" |
|
672 by blast |
|
673 have "f (x - k *a a) \<in> vs2.span (f ` b)" |
|
674 unfolding linear_span_image[OF lf] |
|
675 apply (rule imageI) |
|
676 using k vs1.span_mono[of "b - {a}" b] |
|
677 apply blast |
|
678 done |
|
679 then have "f x - k *b f a \<in> vs2.span (f ` b)" |
|
680 by (simp add: linear_diff linear_scale lf) |
|
681 then have th: "-k *b f a \<in> vs2.span (f ` b)" |
|
682 using "2.prems"(5) by simp |
|
683 have xsb: "x \<in> vs1.span b" |
|
684 proof (cases "k = 0") |
|
685 case True |
|
686 with k have "x \<in> vs1.span (b - {a})" by simp |
|
687 then show ?thesis using vs1.span_mono[of "b - {a}" b] |
|
688 by blast |
|
689 next |
|
690 case False |
|
691 with vs2.span_scale[OF th, of "- 1/ k"] |
|
692 have th1: "f a \<in> vs2.span (f ` b)" |
|
693 by auto |
|
694 from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] |
|
695 have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast |
|
696 from "2.prems"(2) [unfolded vs2.dependent_def bex_simps(8), rule_format, of "f a"] |
|
697 have "f a \<notin> vs2.span (f ` b)" using tha |
|
698 using "2.hyps"(2) |
|
699 "2.prems"(3) by auto |
|
700 with th1 have False by blast |
|
701 then show ?thesis by blast |
|
702 qed |
|
703 from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" . |
|
704 qed |
|
705 |
|
706 lemma linear_eq_on: |
|
707 assumes l: "linear s1 s2 f" "linear s1 s2 g" |
|
708 assumes x: "x \<in> vs1.span B" and eq: "\<And>b. b \<in> B \<Longrightarrow> f b = g b" |
|
709 shows "f x = g x" |
|
710 proof - |
|
711 interpret d: linear s1 s2 "\<lambda>x. f x - g x" |
|
712 using l by (intro linear_compose_sub) (auto simp: module_hom_iff_linear) |
|
713 have "f x - g x = 0" |
|
714 by (rule d.eq_0_on_span[OF _ x]) (auto simp: eq) |
|
715 then show ?thesis by auto |
|
716 qed |
|
717 |
|
718 definition construct :: "'b set \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" |
|
719 where "construct B g v = (\<Sum>b | vs1.representation (vs1.extend_basis B) v b \<noteq> 0. |
|
720 vs1.representation (vs1.extend_basis B) v b *b (if b \<in> B then g b else 0))" |
|
721 |
|
722 lemma construct_cong: "(\<And>b. b \<in> B \<Longrightarrow> f b = g b) \<Longrightarrow> construct B f = construct B g" |
|
723 unfolding construct_def by (rule ext, auto intro!: sum.cong) |
|
724 |
|
725 lemma linear_construct: |
|
726 assumes B[simp]: "vs1.independent B" |
|
727 shows "linear s1 s2 (construct B f)" |
|
728 unfolding module_hom_iff_linear linear_iff |
|
729 proof safe |
|
730 have eB[simp]: "vs1.independent (vs1.extend_basis B)" |
|
731 using vs1.independent_extend_basis[OF B] . |
|
732 let ?R = "vs1.representation (vs1.extend_basis B)" |
|
733 fix c x y |
|
734 have "construct B f (x + y) = |
|
735 (\<Sum>b\<in>{b. ?R x b \<noteq> 0} \<union> {b. ?R y b \<noteq> 0}. ?R (x + y) b *b (if b \<in> B then f b else 0))" |
|
736 by (auto intro!: sum.mono_neutral_cong_left simp: vs1.finite_representation vs1.representation_add construct_def) |
|
737 also have "\<dots> = construct B f x + construct B f y" |
|
738 by (auto simp: construct_def vs1.representation_add vs2.scale_left_distrib sum.distrib |
|
739 intro!: arg_cong2[where f="(+)"] sum.mono_neutral_cong_right vs1.finite_representation) |
|
740 finally show "construct B f (x + y) = construct B f x + construct B f y" . |
|
741 |
|
742 show "construct B f (c *a x) = c *b construct B f x" |
|
743 by (auto simp del: vs2.scale_scale intro!: sum.mono_neutral_cong_left vs1.finite_representation |
|
744 simp add: construct_def vs2.scale_scale[symmetric] vs1.representation_scale vs2.scale_sum_right) |
|
745 qed intro_locales |
|
746 |
|
747 lemma construct_basis: |
|
748 assumes B[simp]: "vs1.independent B" and b: "b \<in> B" |
|
749 shows "construct B f b = f b" |
|
750 proof - |
|
751 have *: "vs1.representation (vs1.extend_basis B) b = (\<lambda>v. if v = b then 1 else 0)" |
|
752 using vs1.extend_basis_superset[OF B] b |
|
753 by (intro vs1.representation_basis vs1.independent_extend_basis) auto |
|
754 then have "{v. vs1.representation (vs1.extend_basis B) b v \<noteq> 0} = {b}" |
|
755 by auto |
|
756 then show ?thesis |
|
757 unfolding construct_def by (simp add: * b) |
|
758 qed |
|
759 |
|
760 lemma construct_outside: |
|
761 assumes B: "vs1.independent B" and v: "v \<in> vs1.span (vs1.extend_basis B - B)" |
|
762 shows "construct B f v = 0" |
|
763 unfolding construct_def |
|
764 proof (clarsimp intro!: sum.neutral simp del: vs2.scale_eq_0_iff) |
|
765 fix b assume "b \<in> B" |
|
766 then have "vs1.representation (vs1.extend_basis B - B) v b = 0" |
|
767 using vs1.representation_ne_zero[of "vs1.extend_basis B - B" v b] by auto |
|
768 moreover have "vs1.representation (vs1.extend_basis B) v = vs1.representation (vs1.extend_basis B - B) v" |
|
769 using vs1.representation_extend[OF vs1.independent_extend_basis[OF B] v] by auto |
|
770 ultimately show "vs1.representation (vs1.extend_basis B) v b *b f b = 0" |
|
771 by simp |
|
772 qed |
|
773 |
|
774 lemma construct_add: |
|
775 assumes B[simp]: "vs1.independent B" |
|
776 shows "construct B (\<lambda>x. f x + g x) v = construct B f v + construct B g v" |
|
777 proof (rule linear_eq_on) |
|
778 show "v \<in> vs1.span (vs1.extend_basis B)" by simp |
|
779 show "b \<in> vs1.extend_basis B \<Longrightarrow> construct B (\<lambda>x. f x + g x) b = construct B f b + construct B g b" for b |
|
780 using construct_outside[OF B vs1.span_base, of b] by (cases "b \<in> B") (auto simp: construct_basis) |
|
781 qed (intro linear_compose_add linear_construct B)+ |
|
782 |
|
783 lemma construct_scale: |
|
784 assumes B[simp]: "vs1.independent B" |
|
785 shows "construct B (\<lambda>x. c *b f x) v = c *b construct B f v" |
|
786 proof (rule linear_eq_on) |
|
787 show "v \<in> vs1.span (vs1.extend_basis B)" by simp |
|
788 show "b \<in> vs1.extend_basis B \<Longrightarrow> construct B (\<lambda>x. c *b f x) b = c *b construct B f b" for b |
|
789 using construct_outside[OF B vs1.span_base, of b] by (cases "b \<in> B") (auto simp: construct_basis) |
|
790 qed (intro linear_construct module_hom_scale B)+ |
|
791 |
|
792 lemma construct_in_span: |
|
793 assumes B[simp]: "vs1.independent B" |
|
794 shows "construct B f v \<in> vs2.span (f ` B)" |
|
795 proof - |
|
796 interpret c: linear s1 s2 "construct B f" by (rule linear_construct) fact |
|
797 let ?R = "vs1.representation B" |
|
798 have "v \<in> vs1.span ((vs1.extend_basis B - B) \<union> B)" |
|
799 by (auto simp: Un_absorb2 vs1.extend_basis_superset) |
|
800 then obtain x y where "v = x + y" "x \<in> vs1.span (vs1.extend_basis B - B)" "y \<in> vs1.span B" |
|
801 unfolding vs1.span_Un by auto |
|
802 moreover have "construct B f (\<Sum>b | ?R y b \<noteq> 0. ?R y b *a b) \<in> vs2.span (f ` B)" |
|
803 by (auto simp add: c.sum c.scale construct_basis vs1.representation_ne_zero |
|
804 intro!: vs2.span_sum vs2.span_scale intro: vs2.span_base ) |
|
805 ultimately show "construct B f v \<in> vs2.span (f ` B)" |
|
806 by (auto simp add: c.add construct_outside vs1.sum_nonzero_representation_eq) |
|
807 qed |
|
808 |
|
809 lemma linear_compose_sum: |
|
810 assumes lS: "\<forall>a \<in> S. linear s1 s2 (f a)" |
|
811 shows "linear s1 s2 (\<lambda>x. sum (\<lambda>a. f a x) S)" |
|
812 proof (cases "finite S") |
|
813 case True |
|
814 then show ?thesis |
|
815 using lS by induct (simp_all add: linear_zero linear_compose_add) |
|
816 next |
|
817 case False |
|
818 then show ?thesis |
|
819 by (simp add: linear_zero) |
|
820 qed |
|
821 |
|
822 lemma in_span_in_range_construct: |
|
823 "x \<in> range (construct B f)" if i: "vs1.independent B" and x: "x \<in> vs2.span (f ` B)" |
|
824 proof - |
|
825 interpret linear "( *a)" "( *b)" "construct B f" |
|
826 using i by (rule linear_construct) |
|
827 obtain bb :: "('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'b set \<Rightarrow> 'b" where |
|
828 "\<forall>x0 x1 x2. (\<exists>v4. v4 \<in> x2 \<and> x1 v4 \<noteq> x0 v4) = (bb x0 x1 x2 \<in> x2 \<and> x1 (bb x0 x1 x2) \<noteq> x0 (bb x0 x1 x2))" |
|
829 by moura |
|
830 then have f2: "\<forall>B Ba f fa. (B \<noteq> Ba \<or> bb fa f Ba \<in> Ba \<and> f (bb fa f Ba) \<noteq> fa (bb fa f Ba)) \<or> f ` B = fa ` Ba" |
|
831 by (meson image_cong) |
|
832 have "vs1.span B \<subseteq> vs1.span (vs1.extend_basis B)" |
|
833 by (simp add: vs1.extend_basis_superset[OF i] vs1.span_mono) |
|
834 then show "x \<in> range (construct B f)" |
|
835 using f2 x by (metis (no_types) construct_basis[OF i, of _ f] |
|
836 vs1.span_extend_basis[OF i] set_mp span_image spans_image) |
|
837 qed |
|
838 |
|
839 lemma range_construct_eq_span: |
|
840 "range (construct B f) = vs2.span (f ` B)" |
|
841 if "vs1.independent B" |
|
842 by (auto simp: that construct_in_span in_span_in_range_construct) |
|
843 |
|
844 lemma linear_independent_extend_subspace: |
|
845 \<comment>\<open>legacy: use @{term construct} instead\<close> |
|
846 assumes "vs1.independent B" |
|
847 shows "\<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x) \<and> range g = vs2.span (f`B)" |
|
848 by (rule exI[where x="construct B f"]) |
|
849 (auto simp: linear_construct assms construct_basis range_construct_eq_span) |
|
850 |
|
851 lemma linear_independent_extend: |
|
852 "vs1.independent B \<Longrightarrow> \<exists>g. linear s1 s2 g \<and> (\<forall>x\<in>B. g x = f x)" |
|
853 using linear_independent_extend_subspace[of B f] by auto |
|
854 |
|
855 lemma linear_exists_left_inverse_on: |
|
856 assumes lf: "linear s1 s2 f" |
|
857 assumes V: "vs1.subspace V" and f: "inj_on f V" |
|
858 shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>V. g (f v) = v)" |
|
859 proof - |
|
860 interpret linear s1 s2 f by fact |
|
861 obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B" |
|
862 using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto |
|
863 have f: "inj_on f (vs1.span B)" |
|
864 using f unfolding V_eq . |
|
865 show ?thesis |
|
866 proof (intro bexI ballI conjI) |
|
867 interpret p: vector_space_pair s2 s1 by unfold_locales |
|
868 have fB: "vs2.independent (f ` B)" |
|
869 using independent_injective_image[OF B f] . |
|
870 let ?g = "p.construct (f ` B) (the_inv_into B f)" |
|
871 show "linear ( *b) ( *a) ?g" |
|
872 by (rule p.linear_construct[OF fB]) |
|
873 have "?g b \<in> vs1.span (the_inv_into B f ` f ` B)" for b |
|
874 by (intro p.construct_in_span fB) |
|
875 moreover have "the_inv_into B f ` f ` B = B" |
|
876 by (auto simp: image_comp comp_def the_inv_into_f_f inj_on_subset[OF f vs1.span_superset] |
|
877 cong: image_cong) |
|
878 ultimately show "?g \<in> UNIV \<rightarrow> V" |
|
879 by (auto simp: V_eq) |
|
880 have "(?g \<circ> f) v = id v" if "v \<in> vs1.span B" for v |
|
881 proof (rule vector_space_pair.linear_eq_on[where x=v]) |
|
882 show "vector_space_pair ( *a) ( *a)" by unfold_locales |
|
883 show "linear ( *a) ( *a) (?g \<circ> f)" |
|
884 apply (rule Vector_Spaces.linear_compose[of _ "( *b)"]) |
|
885 subgoal by unfold_locales |
|
886 apply fact |
|
887 done |
|
888 show "linear ( *a) ( *a) id" by (rule vs1.linear_id) |
|
889 show "v \<in> vs1.span B" by fact |
|
890 show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b |
|
891 by (simp add: p.construct_basis fB the_inv_into_f_f inj_on_subset[OF f vs1.span_superset]) |
|
892 qed |
|
893 then show "v \<in> V \<Longrightarrow> ?g (f v) = v" for v by (auto simp: comp_def id_def V_eq) |
|
894 qed |
|
895 qed |
|
896 |
|
897 lemma linear_exists_right_inverse_on: |
|
898 assumes lf: "linear s1 s2 f" |
|
899 assumes "vs1.subspace V" |
|
900 shows "\<exists>g\<in>UNIV \<rightarrow> V. linear s2 s1 g \<and> (\<forall>v\<in>f ` V. f (g v) = v)" |
|
901 proof - |
|
902 obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B" |
|
903 using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>] by auto |
|
904 obtain C where C: "vs2.independent C" and fB_C: "f ` B \<subseteq> vs2.span C" "C \<subseteq> f ` B" |
|
905 using vs2.maximal_independent_subset[of "f ` B"] by auto |
|
906 then have "\<forall>v\<in>C. \<exists>b\<in>B. v = f b" by auto |
|
907 then obtain g where g: "\<And>v. v \<in> C \<Longrightarrow> g v \<in> B" "\<And>v. v \<in> C \<Longrightarrow> f (g v) = v" by metis |
|
908 show ?thesis |
|
909 proof (intro bexI ballI conjI) |
|
910 interpret p: vector_space_pair s2 s1 by unfold_locales |
|
911 let ?g = "p.construct C g" |
|
912 show "linear ( *b) ( *a) ?g" |
|
913 by (rule p.linear_construct[OF C]) |
|
914 have "?g v \<in> vs1.span (g ` C)" for v |
|
915 by (rule p.construct_in_span[OF C]) |
|
916 also have "\<dots> \<subseteq> V" unfolding V_eq using g by (intro vs1.span_mono) auto |
|
917 finally show "?g \<in> UNIV \<rightarrow> V" by auto |
|
918 have "(f \<circ> ?g) v = id v" if v: "v \<in> f ` V" for v |
|
919 proof (rule vector_space_pair.linear_eq_on[where x=v]) |
|
920 show "vector_space_pair ( *b) ( *b)" by unfold_locales |
|
921 show "linear ( *b) ( *b) (f \<circ> ?g)" |
|
922 apply (rule Vector_Spaces.linear_compose[of _ "( *a)"]) |
|
923 apply fact |
|
924 subgoal by fact |
|
925 done |
|
926 show "linear ( *b) ( *b) id" by (rule vs2.linear_id) |
|
927 have "vs2.span (f ` B) = vs2.span C" |
|
928 using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"] by (auto simp: vs2.subspace_span) |
|
929 then show "v \<in> vs2.span C" |
|
930 using v linear_span_image[OF lf, of B] by (simp add: V_eq) |
|
931 show "(f \<circ> p.construct C g) b = id b" if b: "b \<in> C" for b |
|
932 by (auto simp: p.construct_basis g C b) |
|
933 qed |
|
934 then show "v \<in> f ` V \<Longrightarrow> f (?g v) = v" for v by (auto simp: comp_def id_def) |
|
935 qed |
|
936 qed |
|
937 |
|
938 lemma linear_inj_on_left_inverse: |
|
939 assumes lf: "linear s1 s2 f" |
|
940 assumes fi: "inj_on f (vs1.span S)" |
|
941 shows "\<exists>g. range g \<subseteq> vs1.span S \<and> linear s2 s1 g \<and> (\<forall>x\<in>vs1.span S. g (f x) = x)" |
|
942 using linear_exists_left_inverse_on[OF lf vs1.subspace_span fi] |
|
943 by (auto simp: linear_iff_module_hom) |
|
944 |
|
945 lemma linear_injective_left_inverse: "linear s1 s2 f \<Longrightarrow> inj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> g \<circ> f = id" |
|
946 using linear_inj_on_left_inverse[of f UNIV] by (auto simp: fun_eq_iff vs1.span_UNIV) |
|
947 |
|
948 lemma linear_surj_right_inverse: |
|
949 assumes lf: "linear s1 s2 f" |
|
950 assumes sf: "vs2.span T \<subseteq> f`vs1.span S" |
|
951 shows "\<exists>g. range g \<subseteq> vs1.span S \<and> linear s2 s1 g \<and> (\<forall>x\<in>vs2.span T. f (g x) = x)" |
|
952 using linear_exists_right_inverse_on[OF lf vs1.subspace_span, of S] sf |
|
953 by (auto simp: linear_iff_module_hom) |
|
954 |
|
955 lemma linear_surjective_right_inverse: "linear s1 s2 f \<Longrightarrow> surj f \<Longrightarrow> \<exists>g. linear s2 s1 g \<and> f \<circ> g = id" |
|
956 using linear_surj_right_inverse[of f UNIV UNIV] |
|
957 by (auto simp: vs1.span_UNIV vs2.span_UNIV fun_eq_iff) |
|
958 |
|
959 end |
|
960 |
|
961 lemma surjective_iff_injective_gen: |
|
962 assumes fS: "finite S" |
|
963 and fT: "finite T" |
|
964 and c: "card S = card T" |
|
965 and ST: "f ` S \<subseteq> T" |
|
966 shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S" |
|
967 (is "?lhs \<longleftrightarrow> ?rhs") |
|
968 proof |
|
969 assume h: "?lhs" |
|
970 { |
|
971 fix x y |
|
972 assume x: "x \<in> S" |
|
973 assume y: "y \<in> S" |
|
974 assume f: "f x = f y" |
|
975 from x fS have S0: "card S \<noteq> 0" |
|
976 by auto |
|
977 have "x = y" |
|
978 proof (rule ccontr) |
|
979 assume xy: "\<not> ?thesis" |
|
980 have th: "card S \<le> card (f ` (S - {y}))" |
|
981 unfolding c |
|
982 apply (rule card_mono) |
|
983 apply (rule finite_imageI) |
|
984 using fS apply simp |
|
985 using h xy x y f unfolding subset_eq image_iff |
|
986 apply auto |
|
987 apply (case_tac "xa = f x") |
|
988 apply (rule bexI[where x=x]) |
|
989 apply auto |
|
990 done |
|
991 also have " \<dots> \<le> card (S - {y})" |
|
992 apply (rule card_image_le) |
|
993 using fS by simp |
|
994 also have "\<dots> \<le> card S - 1" using y fS by simp |
|
995 finally show False using S0 by arith |
|
996 qed |
|
997 } |
|
998 then show ?rhs |
|
999 unfolding inj_on_def by blast |
|
1000 next |
|
1001 assume h: ?rhs |
|
1002 have "f ` S = T" |
|
1003 apply (rule card_subset_eq[OF fT ST]) |
|
1004 unfolding card_image[OF h] |
|
1005 apply (rule c) |
|
1006 done |
|
1007 then show ?lhs by blast |
|
1008 qed |
|
1009 |
|
1010 locale finite_dimensional_vector_space = vector_space + |
|
1011 fixes Basis :: "'b set" |
|
1012 assumes finite_Basis: "finite Basis" |
|
1013 and independent_Basis: "independent Basis" |
|
1014 and span_Basis: "span Basis = UNIV" |
|
1015 begin |
|
1016 |
|
1017 definition "dimension = card Basis" |
|
1018 |
|
1019 lemma finiteI_independent: "independent B \<Longrightarrow> finite B" |
|
1020 using independent_span_bound[OF finite_Basis, of B] by (auto simp: span_Basis) |
|
1021 |
|
1022 lemma dim_empty [simp]: "dim {} = 0" |
|
1023 by (rule dim_unique[OF order_refl]) (auto simp: dependent_def) |
|
1024 |
|
1025 lemma dim_insert: |
|
1026 "dim (insert x S) = (if x \<in> span S then dim S else dim S + 1)" |
|
1027 proof - |
|
1028 show ?thesis |
|
1029 proof (cases "x \<in> span S") |
|
1030 case True then show ?thesis |
|
1031 by (metis dim_span span_redundant) |
|
1032 next |
|
1033 case False |
|
1034 obtain B where B: "B \<subseteq> span S" "independent B" "span S \<subseteq> span B" "card B = dim (span S)" |
|
1035 using basis_exists [of "span S"] by blast |
|
1036 have 1: "insert x B \<subseteq> span (insert x S)" |
|
1037 by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI) |
|
1038 have 2: "span (insert x S) \<subseteq> span (insert x B)" |
|
1039 by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span) |
|
1040 have 3: "independent (insert x B)" |
|
1041 by (metis B independent_insert span_subspace subspace_span False) |
|
1042 have "dim (span (insert x S)) = Suc (dim S)" |
|
1043 apply (rule dim_unique [OF 1 2 3]) |
|
1044 by (metis B False card_insert_disjoint dim_span finiteI_independent span_base span_eq span_span) |
|
1045 then show ?thesis |
|
1046 by (metis False Suc_eq_plus1 dim_span) |
|
1047 qed |
|
1048 qed |
|
1049 |
|
1050 lemma dim_singleton [simp]: |
|
1051 "dim{x} = (if x = 0 then 0 else 1)" |
|
1052 by (simp add: dim_insert) |
|
1053 |
|
1054 proposition choose_subspace_of_subspace: |
|
1055 assumes "n \<le> dim S" |
|
1056 obtains T where "subspace T" "T \<subseteq> span S" "dim T = n" |
|
1057 proof - |
|
1058 have "\<exists>T. subspace T \<and> T \<subseteq> span S \<and> dim T = n" |
|
1059 using assms |
|
1060 proof (induction n) |
|
1061 case 0 then show ?case by (auto intro!: exI[where x="{0}"] span_zero) |
|
1062 next |
|
1063 case (Suc n) |
|
1064 then obtain T where "subspace T" "T \<subseteq> span S" "dim T = n" |
|
1065 by force |
|
1066 then show ?case |
|
1067 proof (cases "span S \<subseteq> span T") |
|
1068 case True |
|
1069 have "dim S = dim T" |
|
1070 apply (rule span_eq_dim [OF subset_antisym [OF True]]) |
|
1071 by (simp add: \<open>T \<subseteq> span S\<close> span_minimal subspace_span) |
|
1072 then show ?thesis |
|
1073 using Suc.prems \<open>dim T = n\<close> by linarith |
|
1074 next |
|
1075 case False |
|
1076 then obtain y where y: "y \<in> S" "y \<notin> T" |
|
1077 by (meson span_mono subsetI) |
|
1078 then have "span (insert y T) \<subseteq> span S" |
|
1079 by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span) |
|
1080 with \<open>dim T = n\<close> \<open>subspace T\<close> y show ?thesis |
|
1081 apply (rule_tac x="span(insert y T)" in exI) |
|
1082 apply (auto simp: dim_insert dim_span subspace_span) |
|
1083 using span_eq_iff by blast |
|
1084 qed |
|
1085 qed |
|
1086 with that show ?thesis by blast |
|
1087 qed |
|
1088 |
|
1089 lemma basis_subspace_exists: |
|
1090 "subspace S |
|
1091 \<Longrightarrow> \<exists>b. finite b \<and> b \<subseteq> S \<and> |
|
1092 independent b \<and> span b = S \<and> card b = dim S" |
|
1093 by (meson basis_exists finiteI_independent span_subspace) |
|
1094 |
|
1095 lemma dim_mono: assumes "V \<subseteq> span W" shows "dim V \<le> dim W" |
|
1096 proof - |
|
1097 obtain B where "independent B" "B \<subseteq> W" "W \<subseteq> span B" |
|
1098 using maximal_independent_subset[of W] by auto |
|
1099 with dim_le_card[of V B] assms independent_span_bound[of Basis B] basis_card_eq_dim[of B W] |
|
1100 span_mono[of B W] span_minimal[OF _ subspace_span, of W B] |
|
1101 show ?thesis |
|
1102 by (auto simp: finite_Basis span_Basis) |
|
1103 qed |
|
1104 |
|
1105 lemma dim_subset: "S \<subseteq> T \<Longrightarrow> dim S \<le> dim T" |
|
1106 using dim_mono[of S T] by (auto intro: span_base) |
|
1107 |
|
1108 lemma dim_eq_0 [simp]: |
|
1109 "dim S = 0 \<longleftrightarrow> S \<subseteq> {0}" |
|
1110 using basis_exists finiteI_independent |
|
1111 apply safe |
|
1112 subgoal by fastforce |
|
1113 by (metis dim_singleton dim_subset le_0_eq) |
|
1114 |
|
1115 lemma dim_UNIV[simp]: "dim UNIV = card Basis" |
|
1116 using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis span_UNIV) |
|
1117 |
|
1118 lemma independent_card_le_dim: assumes "B \<subseteq> V" and "independent B" shows "card B \<le> dim V" |
|
1119 by (subst dim_eq_card[symmetric, OF refl \<open>independent B\<close>]) (rule dim_subset[OF \<open>B \<subseteq> V\<close>]) |
|
1120 |
|
1121 lemma dim_subset_UNIV: "dim S \<le> dimension" |
|
1122 by (metis dim_subset subset_UNIV dim_UNIV dimension_def) |
|
1123 |
|
1124 lemma card_ge_dim_independent: |
|
1125 assumes BV: "B \<subseteq> V" |
|
1126 and iB: "independent B" |
|
1127 and dVB: "dim V \<le> card B" |
|
1128 shows "V \<subseteq> span B" |
|
1129 proof |
|
1130 fix a |
|
1131 assume aV: "a \<in> V" |
|
1132 { |
|
1133 assume aB: "a \<notin> span B" |
|
1134 then have iaB: "independent (insert a B)" |
|
1135 using iB aV BV by (simp add: independent_insert) |
|
1136 from aV BV have th0: "insert a B \<subseteq> V" |
|
1137 by blast |
|
1138 from aB have "a \<notin>B" |
|
1139 by (auto simp add: span_base) |
|
1140 with independent_card_le_dim[OF th0 iaB] dVB finiteI_independent[OF iB] |
|
1141 have False by auto |
|
1142 } |
|
1143 then show "a \<in> span B" by blast |
|
1144 qed |
|
1145 |
|
1146 lemma card_le_dim_spanning: |
|
1147 assumes BV: "B \<subseteq> V" |
|
1148 and VB: "V \<subseteq> span B" |
|
1149 and fB: "finite B" |
|
1150 and dVB: "dim V \<ge> card B" |
|
1151 shows "independent B" |
|
1152 proof - |
|
1153 { |
|
1154 fix a |
|
1155 assume a: "a \<in> B" "a \<in> span (B - {a})" |
|
1156 from a fB have c0: "card B \<noteq> 0" |
|
1157 by auto |
|
1158 from a fB have cb: "card (B - {a}) = card B - 1" |
|
1159 by auto |
|
1160 { |
|
1161 fix x |
|
1162 assume x: "x \<in> V" |
|
1163 from a have eq: "insert a (B - {a}) = B" |
|
1164 by blast |
|
1165 from x VB have x': "x \<in> span B" |
|
1166 by blast |
|
1167 from span_trans[OF a(2), unfolded eq, OF x'] |
|
1168 have "x \<in> span (B - {a})" . |
|
1169 } |
|
1170 then have th1: "V \<subseteq> span (B - {a})" |
|
1171 by blast |
|
1172 have th2: "finite (B - {a})" |
|
1173 using fB by auto |
|
1174 from dim_le_card[OF th1 th2] |
|
1175 have c: "dim V \<le> card (B - {a})" . |
|
1176 from c c0 dVB cb have False by simp |
|
1177 } |
|
1178 then show ?thesis |
|
1179 unfolding dependent_def by blast |
|
1180 qed |
|
1181 |
|
1182 lemma card_eq_dim: "B \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B" |
|
1183 by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent) |
|
1184 |
|
1185 lemma subspace_dim_equal: |
|
1186 assumes "subspace S" |
|
1187 and "subspace T" |
|
1188 and "S \<subseteq> T" |
|
1189 and "dim S \<ge> dim T" |
|
1190 shows "S = T" |
|
1191 proof - |
|
1192 obtain B where B: "B \<le> S" "independent B \<and> S \<subseteq> span B" "card B = dim S" |
|
1193 using basis_exists[of S] by auto |
|
1194 then have "span B \<subseteq> S" |
|
1195 using span_mono[of B S] span_eq_iff[of S] assms by metis |
|
1196 then have "span B = S" |
|
1197 using B by auto |
|
1198 have "dim S = dim T" |
|
1199 using assms dim_subset[of S T] by auto |
|
1200 then have "T \<subseteq> span B" |
|
1201 using card_eq_dim[of B T] B finiteI_independent assms by auto |
|
1202 then show ?thesis |
|
1203 using assms \<open>span B = S\<close> by auto |
|
1204 qed |
|
1205 |
|
1206 corollary dim_eq_span: |
|
1207 shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T" |
|
1208 by (simp add: dim_span span_mono subspace_dim_equal subspace_span) |
|
1209 |
|
1210 lemma dim_psubset: |
|
1211 "span S \<subset> span T \<Longrightarrow> dim S < dim T" |
|
1212 by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span) |
|
1213 |
|
1214 lemma dim_eq_full: |
|
1215 shows "dim S = dimension \<longleftrightarrow> span S = UNIV" |
|
1216 by (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV |
|
1217 dim_UNIV dim_span dimension_def) |
|
1218 |
|
1219 lemma indep_card_eq_dim_span: |
|
1220 assumes "independent B" |
|
1221 shows "finite B \<and> card B = dim (span B)" |
|
1222 using dim_span_eq_card_independent[OF assms] finiteI_independent[OF assms] by auto |
|
1223 |
|
1224 text \<open>More general size bound lemmas.\<close> |
|
1225 |
|
1226 lemma independent_bound_general: |
|
1227 "independent S \<Longrightarrow> finite S \<and> card S \<le> dim S" |
|
1228 by (simp add: dim_eq_card_independent finiteI_independent) |
|
1229 |
|
1230 lemma independent_explicit: |
|
1231 shows "independent B \<longleftrightarrow> finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *s v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))" |
|
1232 apply (cases "finite B") |
|
1233 apply (force simp: dependent_finite) |
|
1234 using independent_bound_general |
|
1235 apply auto |
|
1236 done |
|
1237 |
|
1238 proposition dim_sums_Int: |
|
1239 assumes "subspace S" "subspace T" |
|
1240 shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T" |
|
1241 proof - |
|
1242 obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B" |
|
1243 and indB: "independent B" |
|
1244 and cardB: "card B = dim (S \<inter> T)" |
|
1245 using basis_exists by blast |
|
1246 then obtain C D where "B \<subseteq> C" "C \<subseteq> S" "independent C" "S \<subseteq> span C" |
|
1247 and "B \<subseteq> D" "D \<subseteq> T" "independent D" "T \<subseteq> span D" |
|
1248 using maximal_independent_subset_extend |
|
1249 by (metis Int_subset_iff \<open>B \<subseteq> S \<inter> T\<close> indB) |
|
1250 then have "finite B" "finite C" "finite D" |
|
1251 by (simp_all add: finiteI_independent indB independent_bound_general) |
|
1252 have Beq: "B = C \<inter> D" |
|
1253 apply (rule sym) |
|
1254 apply (rule spanning_subset_independent) |
|
1255 using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast |
|
1256 apply (meson \<open>independent C\<close> independent_mono inf.cobounded1) |
|
1257 using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto |
|
1258 done |
|
1259 then have Deq: "D = B \<union> (D - C)" |
|
1260 by blast |
|
1261 have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}" |
|
1262 apply safe |
|
1263 apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_zero span_minimal) |
|
1264 apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_zero span_minimal) |
|
1265 done |
|
1266 have "a v = 0" if 0: "(\<Sum>v\<in>C. a v *s v) + (\<Sum>v\<in>D - C. a v *s v) = 0" |
|
1267 and v: "v \<in> C \<union> (D-C)" for a v |
|
1268 proof - |
|
1269 have eq: "(\<Sum>v\<in>D - C. a v *s v) = - (\<Sum>v\<in>C. a v *s v)" |
|
1270 using that add_eq_0_iff by blast |
|
1271 have "(\<Sum>v\<in>D - C. a v *s v) \<in> S" |
|
1272 apply (subst eq) |
|
1273 apply (rule subspace_neg [OF \<open>subspace S\<close>]) |
|
1274 apply (rule subspace_sum [OF \<open>subspace S\<close>]) |
|
1275 by (meson subsetCE subspace_scale \<open>C \<subseteq> S\<close> \<open>subspace S\<close>) |
|
1276 moreover have "(\<Sum>v\<in>D - C. a v *s v) \<in> T" |
|
1277 apply (rule subspace_sum [OF \<open>subspace T\<close>]) |
|
1278 by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def) |
|
1279 ultimately have "(\<Sum>v \<in> D-C. a v *s v) \<in> span B" |
|
1280 using B by blast |
|
1281 then obtain e where e: "(\<Sum>v\<in>B. e v *s v) = (\<Sum>v \<in> D-C. a v *s v)" |
|
1282 using span_finite [OF \<open>finite B\<close>] by force |
|
1283 have "\<And>c v. \<lbrakk>(\<Sum>v\<in>C. c v *s v) = 0; v \<in> C\<rbrakk> \<Longrightarrow> c v = 0" |
|
1284 using \<open>finite C\<close> \<open>independent C\<close> independentD by blast |
|
1285 define cc where "cc x = (if x \<in> B then a x + e x else a x)" for x |
|
1286 have [simp]: "C \<inter> B = B" "D \<inter> B = B" "C \<inter> - B = C-D" "B \<inter> (D - C) = {}" |
|
1287 using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+ |
|
1288 have f2: "(\<Sum>v\<in>C \<inter> D. e v *s v) = (\<Sum>v\<in>D - C. a v *s v)" |
|
1289 using Beq e by presburger |
|
1290 have f3: "(\<Sum>v\<in>C \<union> D. a v *s v) = (\<Sum>v\<in>C - D. a v *s v) + (\<Sum>v\<in>D - C. a v *s v) + (\<Sum>v\<in>C \<inter> D. a v *s v)" |
|
1291 using \<open>finite C\<close> \<open>finite D\<close> sum.union_diff2 by blast |
|
1292 have f4: "(\<Sum>v\<in>C \<union> (D - C). a v *s v) = (\<Sum>v\<in>C. a v *s v) + (\<Sum>v\<in>D - C. a v *s v)" |
|
1293 by (meson Diff_disjoint \<open>finite C\<close> \<open>finite D\<close> finite_Diff sum.union_disjoint) |
|
1294 have "(\<Sum>v\<in>C. cc v *s v) = 0" |
|
1295 using 0 f2 f3 f4 |
|
1296 apply (simp add: cc_def Beq \<open>finite C\<close> sum.If_cases algebra_simps sum.distrib |
|
1297 if_distrib if_distribR) |
|
1298 apply (simp add: add.commute add.left_commute diff_eq) |
|
1299 done |
|
1300 then have "\<And>v. v \<in> C \<Longrightarrow> cc v = 0" |
|
1301 using independent_explicit \<open>independent C\<close> \<open>finite C\<close> by blast |
|
1302 then have C0: "\<And>v. v \<in> C - B \<Longrightarrow> a v = 0" |
|
1303 by (simp add: cc_def Beq) meson |
|
1304 then have [simp]: "(\<Sum>x\<in>C - B. a x *s x) = 0" |
|
1305 by simp |
|
1306 have "(\<Sum>x\<in>C. a x *s x) = (\<Sum>x\<in>B. a x *s x)" |
|
1307 proof - |
|
1308 have "C - D = C - B" |
|
1309 using Beq by blast |
|
1310 then show ?thesis |
|
1311 using Beq \<open>(\<Sum>x\<in>C - B. a x *s x) = 0\<close> f3 f4 by auto |
|
1312 qed |
|
1313 with 0 have Dcc0: "(\<Sum>v\<in>D. a v *s v) = 0" |
|
1314 apply (subst Deq) |
|
1315 by (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un) |
|
1316 then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0" |
|
1317 using independent_explicit \<open>independent D\<close> \<open>finite D\<close> by blast |
|
1318 show ?thesis |
|
1319 using v C0 D0 Beq by blast |
|
1320 qed |
|
1321 then have "independent (C \<union> (D - C))" |
|
1322 unfolding independent_explicit |
|
1323 using independent_explicit |
|
1324 by (simp add: independent_explicit \<open>finite C\<close> \<open>finite D\<close> sum_Un del: Un_Diff_cancel) |
|
1325 then have indCUD: "independent (C \<union> D)" by simp |
|
1326 have "dim (S \<inter> T) = card B" |
|
1327 by (rule dim_unique [OF B indB refl]) |
|
1328 moreover have "dim S = card C" |
|
1329 by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim) |
|
1330 moreover have "dim T = card D" |
|
1331 by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim) |
|
1332 moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)" |
|
1333 apply (rule dim_unique [OF CUD _ indCUD refl], clarify) |
|
1334 apply (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_superset span_minimal subsetCE subspace_span sup.bounded_iff) |
|
1335 done |
|
1336 ultimately show ?thesis |
|
1337 using \<open>B = C \<inter> D\<close> [symmetric] |
|
1338 by (simp add: \<open>independent C\<close> \<open>independent D\<close> card_Un_Int finiteI_independent) |
|
1339 qed |
|
1340 |
|
1341 lemma dependent_biggerset_general: |
|
1342 "(finite S \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S" |
|
1343 using independent_bound_general[of S] by (metis linorder_not_le) |
|
1344 |
|
1345 lemma subset_le_dim: |
|
1346 "S \<subseteq> span T \<Longrightarrow> dim S \<le> dim T" |
|
1347 by (metis dim_span dim_subset) |
|
1348 |
|
1349 lemma linear_inj_imp_surj: |
|
1350 assumes lf: "linear scale scale f" |
|
1351 and fi: "inj f" |
|
1352 shows "surj f" |
|
1353 proof - |
|
1354 interpret lf: linear scale scale f by fact |
|
1355 from basis_exists[of UNIV] obtain B |
|
1356 where B: "B \<subseteq> UNIV" "independent B" "UNIV \<subseteq> span B" "card B = dim UNIV" |
|
1357 by blast |
|
1358 from B(4) have d: "dim UNIV = card B" |
|
1359 by simp |
|
1360 have th: "UNIV \<subseteq> span (f ` B)" |
|
1361 apply (rule card_ge_dim_independent) |
|
1362 apply blast |
|
1363 using B(2) inj_on_subset[OF fi] |
|
1364 apply (rule lf.independent_inj_on_image) |
|
1365 apply blast |
|
1366 apply (rule order_eq_refl) |
|
1367 apply (rule sym) |
|
1368 unfolding d |
|
1369 apply (rule card_image) |
|
1370 apply (rule subset_inj_on[OF fi]) |
|
1371 apply blast |
|
1372 done |
|
1373 from th show ?thesis |
|
1374 unfolding lf.span_image surj_def |
|
1375 using B(3) by blast |
|
1376 qed |
|
1377 |
|
1378 end |
|
1379 |
|
1380 locale finite_dimensional_vector_space_pair = |
|
1381 vs1: finite_dimensional_vector_space s1 B1 + vs2: finite_dimensional_vector_space s2 B2 |
|
1382 for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75) |
|
1383 and B1 :: "'b set" |
|
1384 and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) |
|
1385 and B2 :: "'c set" |
|
1386 begin |
|
1387 |
|
1388 sublocale vector_space_pair s1 s2 by unfold_locales |
|
1389 |
|
1390 lemma linear_surjective_imp_injective: |
|
1391 assumes lf: "linear s1 s2 f" and sf: "surj f" and eq: "vs2.dim UNIV = vs1.dim UNIV" |
|
1392 shows "inj f" |
|
1393 proof - |
|
1394 interpret linear s1 s2 f by fact |
|
1395 have *: "card (f ` B1) \<le> vs2.dim UNIV" |
|
1396 using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf |
|
1397 by (auto simp: vs1.span_Basis vs1.span_UNIV vs1.independent_Basis eq |
|
1398 simp del: vs2.dim_UNIV |
|
1399 intro!: card_image_le) |
|
1400 have indep_fB: "vs2.independent (f ` B1)" |
|
1401 using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf * |
|
1402 by (intro vs2.card_le_dim_spanning[of "f ` B1" UNIV]) (auto simp: span_image vs1.span_Basis ) |
|
1403 have "vs2.dim UNIV \<le> card (f ` B1)" |
|
1404 unfolding eq sf[symmetric] vs2.dim_span_eq_card_independent[symmetric, OF indep_fB] |
|
1405 vs2.dim_span |
|
1406 by (intro vs2.dim_mono) (auto simp: span_image vs1.span_Basis) |
|
1407 with * have "card (f ` B1) = vs2.dim UNIV" by auto |
|
1408 also have "... = card B1" |
|
1409 unfolding eq vs1.dim_UNIV .. |
|
1410 finally have "inj_on f B1" |
|
1411 by (subst inj_on_iff_eq_card[OF vs1.finite_Basis]) |
|
1412 then show "inj f" |
|
1413 using inj_on_span_iff_independent_image[OF indep_fB] vs1.span_Basis by auto |
|
1414 qed |
|
1415 |
|
1416 lemma linear_injective_imp_surjective: |
|
1417 assumes lf: "linear s1 s2 f" and sf: "inj f" and eq: "vs2.dim UNIV = vs1.dim UNIV" |
|
1418 shows "surj f" |
|
1419 proof - |
|
1420 interpret linear s1 s2 f by fact |
|
1421 have *: False if b: "b \<notin> vs2.span (f ` B1)" for b |
|
1422 proof - |
|
1423 have *: "vs2.independent (f ` B1)" |
|
1424 using vs1.independent_Basis by (intro independent_injective_image inj_on_subset[OF sf]) auto |
|
1425 have **: "vs2.independent (insert b (f ` B1))" |
|
1426 using b * by (rule vs2.independent_insertI) |
|
1427 |
|
1428 have "b \<notin> f ` B1" using vs2.span_base[of b "f ` B1"] b by auto |
|
1429 then have "Suc (card B1) = card (insert b (f ` B1))" |
|
1430 using sf[THEN inj_on_subset, of B1] by (subst card_insert) (auto intro: vs1.finite_Basis simp: card_image) |
|
1431 also have "\<dots> = vs2.dim (insert b (f ` B1))" |
|
1432 using vs2.dim_eq_card_independent[OF **] by simp |
|
1433 also have "vs2.dim (insert b (f ` B1)) \<le> vs2.dim B2" |
|
1434 by (rule vs2.dim_mono) (auto simp: vs2.span_Basis) |
|
1435 also have "\<dots> = card B1" |
|
1436 using vs1.dim_span[of B1] vs2.dim_span[of B2] unfolding vs1.span_Basis vs2.span_Basis eq |
|
1437 vs1.dim_eq_card_independent[OF vs1.independent_Basis] by simp |
|
1438 finally show False by simp |
|
1439 qed |
|
1440 have "f ` UNIV = f ` vs1.span B1" unfolding vs1.span_Basis .. |
|
1441 also have "\<dots> = vs2.span (f ` B1)" unfolding span_image .. |
|
1442 also have "\<dots> = UNIV" using * by blast |
|
1443 finally show ?thesis . |
|
1444 qed |
|
1445 |
|
1446 lemma linear_injective_isomorphism: |
|
1447 assumes lf: "linear s1 s2 f" |
|
1448 and fi: "inj f" |
|
1449 and dims: "vs2.dim UNIV = vs1.dim UNIV" |
|
1450 shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)" |
|
1451 proof - |
|
1452 show ?thesis |
|
1453 unfolding isomorphism_expand[symmetric] |
|
1454 using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV] |
|
1455 linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV fi] |
|
1456 apply (auto simp: module_hom_iff_linear) |
|
1457 subgoal for f' f'' |
|
1458 apply (rule exI[where x=f'']) |
|
1459 using linear_injective_imp_surjective[OF lf fi dims] |
|
1460 apply auto |
|
1461 by (metis comp_apply eq_id_iff surj_def) |
|
1462 done |
|
1463 qed |
|
1464 |
|
1465 lemma linear_surjective_isomorphism: |
|
1466 assumes lf: "linear s1 s2 f" |
|
1467 and sf: "surj f" |
|
1468 and dims: "vs2.dim UNIV = vs1.dim UNIV" |
|
1469 shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)" |
|
1470 proof - |
|
1471 show ?thesis |
|
1472 unfolding isomorphism_expand[symmetric] |
|
1473 using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV] |
|
1474 linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV] |
|
1475 using linear_surjective_imp_injective[OF lf sf dims] sf |
|
1476 apply (auto simp: module_hom_iff_linear) |
|
1477 subgoal for f' f'' |
|
1478 apply (rule exI[where x=f'']) |
|
1479 apply auto |
|
1480 by (metis isomorphism_expand) |
|
1481 done |
|
1482 qed |
|
1483 |
|
1484 lemma dim_image_eq: |
|
1485 assumes lf: "linear s1 s2 f" |
|
1486 and fi: "inj_on f (vs1.span S)" |
|
1487 shows "vs2.dim (f ` S) = vs1.dim S" |
|
1488 proof - |
|
1489 interpret lf: linear by fact |
|
1490 obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" |
|
1491 using vs1.basis_exists[of S] by auto |
|
1492 then have "vs1.span S = vs1.span B" |
|
1493 using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto |
|
1494 moreover have "card (f ` B) = card B" |
|
1495 using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto |
|
1496 moreover have "(f ` B) \<subseteq> (f ` S)" |
|
1497 using B by auto |
|
1498 ultimately show ?thesis |
|
1499 by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span) |
|
1500 qed |
|
1501 |
|
1502 lemma basis_to_basis_subspace_isomorphism: |
|
1503 assumes s: "vs1.subspace S" |
|
1504 and t: "vs2.subspace T" |
|
1505 and d: "vs1.dim S = vs2.dim T" |
|
1506 and B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" |
|
1507 and C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T" |
|
1508 shows "\<exists>f. linear s1 s2 f \<and> f ` B = C \<and> f ` S = T \<and> inj_on f S" |
|
1509 proof - |
|
1510 from B have fB: "finite B" |
|
1511 by (simp add: vs1.finiteI_independent) |
|
1512 from C have fC: "finite C" |
|
1513 by (simp add: vs2.finiteI_independent) |
|
1514 from B(4) C(4) card_le_inj[of B C] d obtain f where |
|
1515 f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto |
|
1516 from linear_independent_extend[OF B(2)] obtain g where |
|
1517 g: "linear s1 s2 g" "\<forall>x \<in> B. g x = f x" by blast |
|
1518 interpret g: linear s1 s2 g by fact |
|
1519 from inj_on_iff_eq_card[OF fB, of f] f(2) |
|
1520 have "card (f ` B) = card B" by simp |
|
1521 with B(4) C(4) have ceq: "card (f ` B) = card C" using d |
|
1522 by simp |
|
1523 have "g ` B = f ` B" using g(2) |
|
1524 by (auto simp add: image_iff) |
|
1525 also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] . |
|
1526 finally have gBC: "g ` B = C" . |
|
1527 have gi: "inj_on g B" using f(2) g(2) |
|
1528 by (auto simp add: inj_on_def) |
|
1529 note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] |
|
1530 { |
|
1531 fix x y |
|
1532 assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y" |
|
1533 from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B" |
|
1534 by blast+ |
|
1535 from gxy have th0: "g (x - y) = 0" |
|
1536 by (simp add: g.diff) |
|
1537 have th1: "x - y \<in> vs1.span B" using x' y' |
|
1538 by (metis vs1.span_diff) |
|
1539 have "x = y" using g0[OF th1 th0] by simp |
|
1540 } |
|
1541 then have giS: "inj_on g S" unfolding inj_on_def by blast |
|
1542 from vs1.span_subspace[OF B(1,3) s] |
|
1543 have "g ` S = vs2.span (g ` B)" |
|
1544 by (simp add: g.span_image) |
|
1545 also have "\<dots> = vs2.span C" |
|
1546 unfolding gBC .. |
|
1547 also have "\<dots> = T" |
|
1548 using vs2.span_subspace[OF C(1,3) t] . |
|
1549 finally have gS: "g ` S = T" . |
|
1550 from g(1) gS giS gBC show ?thesis |
|
1551 by blast |
|
1552 qed |
|
1553 |
|
1554 lemma dim_image_le: |
|
1555 assumes lf: "linear s1 s2 f" |
|
1556 shows "vs2.dim (f ` S) \<le> vs1.dim (S)" |
|
1557 proof - |
|
1558 from vs1.basis_exists[of S] obtain B where |
|
1559 B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" by blast |
|
1560 from B have fB: "finite B" "card B = vs1.dim S" |
|
1561 using vs1.independent_bound_general by blast+ |
|
1562 have "vs2.dim (f ` S) \<le> card (f ` B)" |
|
1563 apply (rule vs2.span_card_ge_dim) |
|
1564 using lf B fB |
|
1565 apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff |
|
1566 linear_iff_module_hom) |
|
1567 done |
|
1568 also have "\<dots> \<le> vs1.dim S" |
|
1569 using card_image_le[OF fB(1)] fB by simp |
|
1570 finally show ?thesis . |
|
1571 qed |
|
1572 |
|
1573 end |
|
1574 |
|
1575 context finite_dimensional_vector_space begin |
|
1576 |
|
1577 lemma linear_surj_imp_inj: |
|
1578 assumes lf: "linear scale scale f" |
|
1579 and sf: "surj f" |
|
1580 shows "inj f" |
|
1581 proof - |
|
1582 interpret finite_dimensional_vector_space_pair scale Basis scale Basis by unfold_locales |
|
1583 let ?U = "UNIV :: 'b set" |
|
1584 from basis_exists[of ?U] obtain B |
|
1585 where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U" |
|
1586 by blast |
|
1587 { |
|
1588 fix x |
|
1589 assume x: "x \<in> span B" |
|
1590 assume fx: "f x = 0" |
|
1591 from B(2) have fB: "finite B" |
|
1592 using finiteI_independent by auto |
|
1593 have fBi: "independent (f ` B)" |
|
1594 apply (rule card_le_dim_spanning[of "f ` B" ?U]) |
|
1595 apply blast |
|
1596 using sf B(3) |
|
1597 unfolding linear_span_image[OF lf] surj_def subset_eq image_iff |
|
1598 apply blast |
|
1599 using fB apply blast |
|
1600 unfolding d[symmetric] |
|
1601 apply (rule card_image_le) |
|
1602 apply (rule fB) |
|
1603 done |
|
1604 have th0: "dim ?U \<le> card (f ` B)" |
|
1605 apply (rule span_card_ge_dim) |
|
1606 apply blast |
|
1607 unfolding linear_span_image[OF lf] |
|
1608 apply (rule subset_trans[where B = "f ` UNIV"]) |
|
1609 using sf unfolding surj_def |
|
1610 apply blast |
|
1611 apply (rule image_mono) |
|
1612 apply (rule B(3)) |
|
1613 apply (metis finite_imageI fB) |
|
1614 done |
|
1615 moreover have "card (f ` B) \<le> card B" |
|
1616 by (rule card_image_le, rule fB) |
|
1617 ultimately have th1: "card B = card (f ` B)" |
|
1618 unfolding d by arith |
|
1619 have fiB: "inj_on f B" |
|
1620 unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] |
|
1621 by blast |
|
1622 from linear_indep_image_lemma[OF lf fB fBi fiB x] fx |
|
1623 have "x = 0" by blast |
|
1624 } |
|
1625 then show ?thesis |
|
1626 unfolding linear_inj_on_iff_eq_0[OF lf subspace_UNIV] |
|
1627 using B(3) |
|
1628 by blast |
|
1629 qed |
|
1630 |
|
1631 lemma linear_inverse_left: |
|
1632 assumes lf: "linear scale scale f" |
|
1633 and lf': "linear scale scale f'" |
|
1634 shows "f \<circ> f' = id \<longleftrightarrow> f' \<circ> f = id" |
|
1635 proof - |
|
1636 { |
|
1637 fix f f':: "'b \<Rightarrow> 'b" |
|
1638 assume lf: "linear scale scale f" "linear scale scale f'" |
|
1639 assume f: "f \<circ> f' = id" |
|
1640 from f have sf: "surj f" |
|
1641 apply (auto simp add: o_def id_def surj_def) |
|
1642 apply metis |
|
1643 done |
|
1644 interpret finite_dimensional_vector_space_pair scale Basis scale Basis by unfold_locales |
|
1645 from linear_surjective_isomorphism[OF lf(1) sf] lf f |
|
1646 have "f' \<circ> f = id" |
|
1647 unfolding fun_eq_iff o_def id_def by metis |
|
1648 } |
|
1649 then show ?thesis |
|
1650 using lf lf' by metis |
|
1651 qed |
|
1652 |
|
1653 lemma left_inverse_linear: |
|
1654 assumes lf: "linear scale scale f" |
|
1655 and gf: "g \<circ> f = id" |
|
1656 shows "linear scale scale g" |
|
1657 proof - |
|
1658 from gf have fi: "inj f" |
|
1659 apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) |
|
1660 apply metis |
|
1661 done |
|
1662 interpret finite_dimensional_vector_space_pair scale Basis scale Basis by unfold_locales |
|
1663 from linear_injective_isomorphism[OF lf fi] |
|
1664 obtain h :: "'b \<Rightarrow> 'b" where h: "linear scale scale h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" |
|
1665 by blast |
|
1666 have "h = g" |
|
1667 apply (rule ext) using gf h(2,3) |
|
1668 apply (simp add: o_def id_def fun_eq_iff) |
|
1669 apply metis |
|
1670 done |
|
1671 with h(1) show ?thesis by blast |
|
1672 qed |
|
1673 |
|
1674 lemma inj_linear_imp_inv_linear: |
|
1675 assumes "linear scale scale f" "inj f" shows "linear scale scale (inv f)" |
|
1676 using assms inj_iff left_inverse_linear by blast |
|
1677 |
|
1678 lemma right_inverse_linear: |
|
1679 assumes lf: "linear scale scale f" |
|
1680 and gf: "f \<circ> g = id" |
|
1681 shows "linear scale scale g" |
|
1682 proof - |
|
1683 from gf have fi: "surj f" |
|
1684 by (auto simp add: surj_def o_def id_def) metis |
|
1685 interpret finite_dimensional_vector_space_pair scale Basis scale Basis by unfold_locales |
|
1686 from linear_surjective_isomorphism[OF lf fi] |
|
1687 obtain h:: "'b \<Rightarrow> 'b" where h: "linear scale scale h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" |
|
1688 by blast |
|
1689 have "h = g" |
|
1690 apply (rule ext) |
|
1691 using gf h(2,3) |
|
1692 apply (simp add: o_def id_def fun_eq_iff) |
|
1693 apply metis |
|
1694 done |
|
1695 with h(1) show ?thesis by blast |
|
1696 qed |
|
1697 |
|
1698 end |
|
1699 |
|
1700 context finite_dimensional_vector_space_pair begin |
|
1701 |
|
1702 lemma subspace_isomorphism: |
|
1703 assumes s: "vs1.subspace S" |
|
1704 and t: "vs2.subspace T" |
|
1705 and d: "vs1.dim S = vs2.dim T" |
|
1706 shows "\<exists>f. linear s1 s2 f \<and> f ` S = T \<and> inj_on f S" |
|
1707 proof - |
|
1708 from vs1.basis_exists[of S] vs1.finiteI_independent |
|
1709 obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" and fB: "finite B" |
|
1710 by blast |
|
1711 from vs2.basis_exists[of T] vs2.finiteI_independent |
|
1712 obtain C where C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T" and fC: "finite C" |
|
1713 by blast |
|
1714 from B(4) C(4) card_le_inj[of B C] d |
|
1715 obtain f where f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> |
|
1716 by auto |
|
1717 from linear_independent_extend[OF B(2)] |
|
1718 obtain g where g: "linear s1 s2 g" "\<forall>x\<in> B. g x = f x" |
|
1719 by blast |
|
1720 interpret g: linear s1 s2 g by fact |
|
1721 from inj_on_iff_eq_card[OF fB, of f] f(2) have "card (f ` B) = card B" |
|
1722 by simp |
|
1723 with B(4) C(4) have ceq: "card (f ` B) = card C" |
|
1724 using d by simp |
|
1725 have "g ` B = f ` B" |
|
1726 using g(2) by (auto simp add: image_iff) |
|
1727 also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] . |
|
1728 finally have gBC: "g ` B = C" . |
|
1729 have gi: "inj_on g B" |
|
1730 using f(2) g(2) by (auto simp add: inj_on_def) |
|
1731 note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi] |
|
1732 { |
|
1733 fix x y |
|
1734 assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y" |
|
1735 from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B" |
|
1736 by blast+ |
|
1737 from gxy have th0: "g (x - y) = 0" |
|
1738 by (simp add: linear_diff g) |
|
1739 have th1: "x - y \<in> vs1.span B" |
|
1740 using x' y' by (metis vs1.span_diff) |
|
1741 have "x = y" |
|
1742 using g0[OF th1 th0] by simp |
|
1743 } |
|
1744 then have giS: "inj_on g S" |
|
1745 unfolding inj_on_def by blast |
|
1746 from vs1.span_subspace[OF B(1,3) s] have "g ` S = vs2.span (g ` B)" |
|
1747 by (simp add: module_hom.span_image[OF g(1)[unfolded linear_iff_module_hom]]) |
|
1748 also have "\<dots> = vs2.span C" unfolding gBC .. |
|
1749 also have "\<dots> = T" using vs2.span_subspace[OF C(1,3) t] . |
|
1750 finally have gS: "g ` S = T" . |
|
1751 from g(1) gS giS show ?thesis |
|
1752 by blast |
|
1753 qed |
|
1754 |
|
1755 end |
|
1756 |
|
1757 hide_const (open) linear |
|
1758 |
|
1759 end |