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