1(* Title: HOL/Modules.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>Modules\<close> 10 11text \<open>Bases of a linear algebra based on modules (i.e. vector spaces of rings). \<close> 12 13theory Modules 14 imports Hull 15begin 16 17subsection \<open>Locale for additive functions\<close> 18 19locale additive = 20 fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add" 21 assumes add: "f (x + y) = f x + f y" 22begin 23 24lemma zero: "f 0 = 0" 25proof - 26 have "f 0 = f (0 + 0)" by simp 27 also have "\<dots> = f 0 + f 0" by (rule add) 28 finally show "f 0 = 0" by simp 29qed 30 31lemma minus: "f (- x) = - f x" 32proof - 33 have "f (- x) + f x = f (- x + x)" by (rule add [symmetric]) 34 also have "\<dots> = - f x + f x" by (simp add: zero) 35 finally show "f (- x) = - f x" by (rule add_right_imp_eq) 36qed 37 38lemma diff: "f (x - y) = f x - f y" 39 using add [of x "- y"] by (simp add: minus) 40 41lemma sum: "f (sum g A) = (\<Sum>x\<in>A. f (g x))" 42 by (induct A rule: infinite_finite_induct) (simp_all add: zero add) 43 44end 45 46 47text \<open>Modules form the central spaces in linear algebra. They are a generalization from vector 48spaces by replacing the scalar field by a scalar ring.\<close> 49locale module = 50 fixes scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75) 51 assumes scale_right_distrib [algebra_simps, algebra_split_simps]: 52 "a *s (x + y) = a *s x + a *s y" 53 and scale_left_distrib [algebra_simps, algebra_split_simps]: 54 "(a + b) *s x = a *s x + b *s x" 55 and scale_scale [simp]: "a *s (b *s x) = (a * b) *s x" 56 and scale_one [simp]: "1 *s x = x" 57begin 58 59lemma scale_left_commute: "a *s (b *s x) = b *s (a *s x)" 60 by (simp add: mult.commute) 61 62lemma scale_zero_left [simp]: "0 *s x = 0" 63 and scale_minus_left [simp]: "(- a) *s x = - (a *s x)" 64 and scale_left_diff_distrib [algebra_simps, algebra_split_simps]: 65 "(a - b) *s x = a *s x - b *s x" 66 and scale_sum_left: "(sum f A) *s x = (\<Sum>a\<in>A. (f a) *s x)" 67proof - 68 interpret s: additive "\<lambda>a. a *s x" 69 by standard (rule scale_left_distrib) 70 show "0 *s x = 0" by (rule s.zero) 71 show "(- a) *s x = - (a *s x)" by (rule s.minus) 72 show "(a - b) *s x = a *s x - b *s x" by (rule s.diff) 73 show "(sum f A) *s x = (\<Sum>a\<in>A. (f a) *s x)" by (rule s.sum) 74qed 75 76lemma scale_zero_right [simp]: "a *s 0 = 0" 77 and scale_minus_right [simp]: "a *s (- x) = - (a *s x)" 78 and scale_right_diff_distrib [algebra_simps, algebra_split_simps]: 79 "a *s (x - y) = a *s x - a *s y" 80 and scale_sum_right: "a *s (sum f A) = (\<Sum>x\<in>A. a *s (f x))" 81proof - 82 interpret s: additive "\<lambda>x. a *s x" 83 by standard (rule scale_right_distrib) 84 show "a *s 0 = 0" by (rule s.zero) 85 show "a *s (- x) = - (a *s x)" by (rule s.minus) 86 show "a *s (x - y) = a *s x - a *s y" by (rule s.diff) 87 show "a *s (sum f A) = (\<Sum>x\<in>A. a *s (f x))" by (rule s.sum) 88qed 89 90lemma sum_constant_scale: "(\<Sum>x\<in>A. y) = scale (of_nat (card A)) y" 91 by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) 92 93end 94 95setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close> 96 97context module 98begin 99 100lemma [field_simps, field_split_simps]: 101 shows scale_left_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) *s x = a *s x + b *s x" 102 and scale_right_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x + y) = a *s x + a *s y" 103 and scale_left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) *s x = a *s x - b *s x" 104 and scale_right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x - y) = a *s x - a *s y" 105 by (rule scale_left_distrib scale_right_distrib scale_left_diff_distrib scale_right_diff_distrib)+ 106 107end 108 109setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close> 110 111 112section \<open>Subspace\<close> 113 114context module 115begin 116 117definition subspace :: "'b set \<Rightarrow> bool" 118 where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in>S. \<forall>y\<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x\<in>S. c *s x \<in> S)" 119 120lemma subspaceI: 121 "0 \<in> S \<Longrightarrow> (\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S) \<Longrightarrow> (\<And>c x. x \<in> S \<Longrightarrow> c *s x \<in> S) \<Longrightarrow> subspace S" 122 by (auto simp: subspace_def) 123 124lemma subspace_UNIV[simp]: "subspace UNIV" 125 by (simp add: subspace_def) 126 127lemma subspace_single_0[simp]: "subspace {0}" 128 by (simp add: subspace_def) 129 130lemma subspace_0: "subspace S \<Longrightarrow> 0 \<in> S" 131 by (metis subspace_def) 132 133lemma subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S" 134 by (metis subspace_def) 135 136lemma subspace_scale: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *s x \<in> S" 137 by (metis subspace_def) 138 139lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S" 140 by (metis scale_minus_left scale_one subspace_scale) 141 142lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S" 143 by (metis diff_conv_add_uminus subspace_add subspace_neg) 144 145lemma subspace_sum: "subspace A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<in> A) \<Longrightarrow> sum f B \<in> A" 146 by (induct B rule: infinite_finite_induct) (auto simp add: subspace_add subspace_0) 147 148lemma subspace_Int: "(\<And>i. i \<in> I \<Longrightarrow> subspace (s i)) \<Longrightarrow> subspace (\<Inter>i\<in>I. s i)" 149 by (auto simp: subspace_def) 150 151lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)" 152 unfolding subspace_def by auto 153 154lemma subspace_inter: "subspace A \<Longrightarrow> subspace B \<Longrightarrow> subspace (A \<inter> B)" 155 by (simp add: subspace_def) 156 157 158section \<open>Span: subspace generated by a set\<close> 159 160definition span :: "'b set \<Rightarrow> 'b set" 161 where span_explicit: "span b = {(\<Sum>a\<in>t. r a *s a) | t r. finite t \<and> t \<subseteq> b}" 162 163lemma span_explicit': 164 "span b = {(\<Sum>v | f v \<noteq> 0. f v *s v) | f. finite {v. f v \<noteq> 0} \<and> (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)}" 165 unfolding span_explicit 166proof safe 167 fix t r assume "finite t" "t \<subseteq> b" 168 then show "\<exists>f. (\<Sum>a\<in>t. r a *s a) = (\<Sum>v | f v \<noteq> 0. f v *s v) \<and> finite {v. f v \<noteq> 0} \<and> (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)" 169 by (intro exI[of _ "\<lambda>v. if v \<in> t then r v else 0"]) (auto intro!: sum.mono_neutral_cong_right) 170next 171 fix f :: "'b \<Rightarrow> 'a" assume "finite {v. f v \<noteq> 0}" "(\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> b)" 172 then show "\<exists>t r. (\<Sum>v | f v \<noteq> 0. f v *s v) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> b" 173 by (intro exI[of _ "{v. f v \<noteq> 0}"] exI[of _ f]) auto 174qed 175 176lemma span_alt: 177 "span B = {(\<Sum>x | f x \<noteq> 0. f x *s x) | f. {x. f x \<noteq> 0} \<subseteq> B \<and> finite {x. f x \<noteq> 0}}" 178 unfolding span_explicit' by auto 179 180lemma span_finite: 181 assumes fS: "finite S" 182 shows "span S = range (\<lambda>u. \<Sum>v\<in>S. u v *s v)" 183 unfolding span_explicit 184proof safe 185 fix t r assume "t \<subseteq> S" then show "(\<Sum>a\<in>t. r a *s a) \<in> range (\<lambda>u. \<Sum>v\<in>S. u v *s v)" 186 by (intro image_eqI[of _ _ "\<lambda>a. if a \<in> t then r a else 0"]) 187 (auto simp: if_distrib[of "\<lambda>r. r *s a" for a] sum.If_cases fS Int_absorb1) 188next 189 show "\<exists>t r. (\<Sum>v\<in>S. u v *s v) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> S" for u 190 by (intro exI[of _ u] exI[of _ S]) (auto intro: fS) 191qed 192 193lemma span_induct_alt [consumes 1, case_names base step, induct set: span]: 194 assumes x: "x \<in> span S" 195 assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *s x + y)" 196 shows "h x" 197 using x unfolding span_explicit 198proof safe 199 fix t r assume "finite t" "t \<subseteq> S" then show "h (\<Sum>a\<in>t. r a *s a)" 200 by (induction t) (auto intro!: hS h0) 201qed 202 203lemma span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B" 204 by (auto simp: span_explicit) 205 206lemma span_base: "a \<in> S \<Longrightarrow> a \<in> span S" 207 by (auto simp: span_explicit intro!: exI[of _ "{a}"] exI[of _ "\<lambda>_. 1"]) 208 209lemma span_superset: "S \<subseteq> span S" 210 by (auto simp: span_base) 211 212lemma span_zero: "0 \<in> span S" 213 by (auto simp: span_explicit intro!: exI[of _ "{}"]) 214 215lemma span_UNIV[simp]: "span UNIV = UNIV" 216 by (auto intro: span_base) 217 218lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S" 219 unfolding span_explicit 220proof safe 221 fix tx ty rx ry assume *: "finite tx" "finite ty" "tx \<subseteq> S" "ty \<subseteq> S" 222 have [simp]: "(tx \<union> ty) \<inter> tx = tx" "(tx \<union> ty) \<inter> ty = ty" 223 by auto 224 show "\<exists>t r. (\<Sum>a\<in>tx. rx a *s a) + (\<Sum>a\<in>ty. ry a *s a) = (\<Sum>a\<in>t. r a *s a) \<and> finite t \<and> t \<subseteq> S" 225 apply (intro exI[of _ "tx \<union> ty"]) 226 apply (intro exI[of _ "\<lambda>a. (if a \<in> tx then rx a else 0) + (if a \<in> ty then ry a else 0)"]) 227 apply (auto simp: * scale_left_distrib sum.distrib if_distrib[of "\<lambda>r. r *s a" for a] sum.If_cases) 228 done 229qed 230 231lemma span_scale: "x \<in> span S \<Longrightarrow> c *s x \<in> span S" 232 unfolding span_explicit 233proof safe 234 fix t r assume *: "finite t" "t \<subseteq> S" 235 show "\<exists>t' r'. c *s (\<Sum>a\<in>t. r a *s a) = (\<Sum>a\<in>t'. r' a *s a) \<and> finite t' \<and> t' \<subseteq> S" 236 by (intro exI[of _ t] exI[of _ "\<lambda>a. c * r a"]) (auto simp: * scale_sum_right) 237qed 238 239lemma subspace_span [iff]: "subspace (span S)" 240 by (auto simp: subspace_def span_zero span_add span_scale) 241 242lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S" 243 by (metis subspace_neg subspace_span) 244 245lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S" 246 by (metis subspace_span subspace_diff) 247 248lemma span_sum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> sum f A \<in> span S" 249 by (rule subspace_sum, rule subspace_span) 250 251lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T" 252 by (auto simp: span_explicit intro!: subspace_sum subspace_scale) 253 254lemma span_def: "span S = subspace hull S" 255 by (intro hull_unique[symmetric] span_superset subspace_span span_minimal) 256 257lemma span_unique: 258 "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> (\<And>T'. S \<subseteq> T' \<Longrightarrow> subspace T' \<Longrightarrow> T \<subseteq> T') \<Longrightarrow> span S = T" 259 unfolding span_def by (rule hull_unique) 260 261lemma span_subspace_induct[consumes 2]: 262 assumes x: "x \<in> span S" 263 and P: "subspace P" 264 and SP: "\<And>x. x \<in> S \<Longrightarrow> x \<in> P" 265 shows "x \<in> P" 266proof - 267 from SP have SP': "S \<subseteq> P" 268 by (simp add: subset_eq) 269 from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]] 270 show "x \<in> P" 271 by (metis subset_eq) 272qed 273 274lemma (in module) span_induct[consumes 1, case_names base step, induct set: span]: 275 assumes x: "x \<in> span S" 276 and P: "subspace (Collect P)" 277 and SP: "\<And>x. x \<in> S \<Longrightarrow> P x" 278 shows "P x" 279 using P SP span_subspace_induct x by fastforce 280 281lemma span_empty[simp]: "span {} = {0}" 282 by (rule span_unique) (auto simp add: subspace_def) 283 284lemma span_subspace: "A \<subseteq> B \<Longrightarrow> B \<subseteq> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B" 285 by (metis order_antisym span_def hull_minimal) 286 287lemma span_span: "span (span A) = span A" 288 unfolding span_def hull_hull .. 289 290(* TODO: proof generally for subspace: *) 291lemma span_add_eq: assumes x: "x \<in> span S" shows "x + y \<in> span S \<longleftrightarrow> y \<in> span S" 292proof 293 assume *: "x + y \<in> span S" 294 have "(x + y) - x \<in> span S" using * x by (rule span_diff) 295 then show "y \<in> span S" by simp 296qed (intro span_add x) 297 298lemma span_add_eq2: assumes y: "y \<in> span S" shows "x + y \<in> span S \<longleftrightarrow> x \<in> span S" 299 using span_add_eq[of y S x] y by (auto simp: ac_simps) 300 301lemma span_singleton: "span {x} = range (\<lambda>k. k *s x)" 302 by (auto simp: span_finite) 303 304lemma span_Un: "span (S \<union> T) = {x + y | x y. x \<in> span S \<and> y \<in> span T}" 305proof safe 306 fix x assume "x \<in> span (S \<union> T)" 307 then obtain t r where t: "finite t" "t \<subseteq> S \<union> T" and x: "x = (\<Sum>a\<in>t. r a *s a)" 308 by (auto simp: span_explicit) 309 moreover have "t \<inter> S \<union> (t - S) = t" by auto 310 ultimately show "\<exists>xa y. x = xa + y \<and> xa \<in> span S \<and> y \<in> span T" 311 unfolding x 312 apply (rule_tac exI[of _ "\<Sum>a\<in>t \<inter> S. r a *s a"]) 313 apply (rule_tac exI[of _ "\<Sum>a\<in>t - S. r a *s a"]) 314 apply (subst sum.union_inter_neutral[symmetric]) 315 apply (auto intro!: span_sum span_scale intro: span_base) 316 done 317next 318 fix x y assume"x \<in> span S" "y \<in> span T" then show "x + y \<in> span (S \<union> T)" 319 using span_mono[of S "S \<union> T"] span_mono[of T "S \<union> T"] 320 by (auto intro!: span_add) 321qed 322 323lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *s a) \<in> span S}" 324proof - 325 have "span ({a} \<union> S) = {x. \<exists>k. (x - k *s a) \<in> span S}" 326 unfolding span_Un span_singleton 327 apply (auto simp add: set_eq_iff) 328 subgoal for y k by (auto intro!: exI[of _ "k"]) 329 subgoal for y k by (rule exI[of _ "k *s a"], rule exI[of _ "y - k *s a"]) auto 330 done 331 then show ?thesis by simp 332qed 333 334lemma span_breakdown: 335 assumes bS: "b \<in> S" 336 and aS: "a \<in> span S" 337 shows "\<exists>k. a - k *s b \<in> span (S - {b})" 338 using assms span_insert [of b "S - {b}"] 339 by (simp add: insert_absorb) 340 341lemma span_breakdown_eq: "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. x - k *s a \<in> span S)" 342 by (simp add: span_insert) 343 344lemmas span_clauses = span_base span_zero span_add span_scale 345 346lemma span_eq_iff[simp]: "span s = s \<longleftrightarrow> subspace s" 347 unfolding span_def by (rule hull_eq) (rule subspace_Inter) 348 349lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S" 350 by (metis span_minimal span_subspace span_superset subspace_span) 351 352lemma eq_span_insert_eq: 353 assumes "(x - y) \<in> span S" 354 shows "span(insert x S) = span(insert y S)" 355proof - 356 have *: "span(insert x S) \<subseteq> span(insert y S)" if "(x - y) \<in> span S" for x y 357 proof - 358 have 1: "(r *s x - r *s y) \<in> span S" for r 359 by (metis scale_right_diff_distrib span_scale that) 360 have 2: "(z - k *s y) - k *s (x - y) = z - k *s x" for z k 361 by (simp add: scale_right_diff_distrib) 362 show ?thesis 363 apply (clarsimp simp add: span_breakdown_eq) 364 by (metis 1 2 diff_add_cancel scale_right_diff_distrib span_add_eq) 365 qed 366 show ?thesis 367 apply (intro subset_antisym * assms) 368 using assms subspace_neg subspace_span minus_diff_eq by force 369qed 370 371 372section \<open>Dependent and independent sets\<close> 373 374definition dependent :: "'b set \<Rightarrow> bool" 375 where dependent_explicit: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (\<Sum>v\<in>t. u v *s v) = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0))" 376 377abbreviation "independent s \<equiv> \<not> dependent s" 378 379lemma dependent_mono: "dependent B \<Longrightarrow> B \<subseteq> A \<Longrightarrow> dependent A" 380 by (auto simp add: dependent_explicit) 381 382lemma independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B" 383 by (auto intro: dependent_mono) 384 385lemma dependent_zero: "0 \<in> A \<Longrightarrow> dependent A" 386 by (auto simp: dependent_explicit intro!: exI[of _ "\<lambda>i. 1"] exI[of _ "{0}"]) 387 388lemma independent_empty[intro]: "independent {}" 389 by (simp add: dependent_explicit) 390 391lemma independent_explicit_module: 392 "independent s \<longleftrightarrow> (\<forall>t u v. finite t \<longrightarrow> t \<subseteq> s \<longrightarrow> (\<Sum>v\<in>t. u v *s v) = 0 \<longrightarrow> v \<in> t \<longrightarrow> u v = 0)" 393 unfolding dependent_explicit by auto 394 395lemma independentD: "independent s \<Longrightarrow> finite t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (\<Sum>v\<in>t. u v *s v) = 0 \<Longrightarrow> v \<in> t \<Longrightarrow> u v = 0" 396 by (simp add: independent_explicit_module) 397 398lemma independent_Union_directed: 399 assumes directed: "\<And>c d. c \<in> C \<Longrightarrow> d \<in> C \<Longrightarrow> c \<subseteq> d \<or> d \<subseteq> c" 400 assumes indep: "\<And>c. c \<in> C \<Longrightarrow> independent c" 401 shows "independent (\<Union>C)" 402proof 403 assume "dependent (\<Union>C)" 404 then obtain u v S where S: "finite S" "S \<subseteq> \<Union>C" "v \<in> S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *s v) = 0" 405 by (auto simp: dependent_explicit) 406 407 have "S \<noteq> {}" 408 using \<open>v \<in> S\<close> by auto 409 have "\<exists>c\<in>C. S \<subseteq> c" 410 using \<open>finite S\<close> \<open>S \<noteq> {}\<close> \<open>S \<subseteq> \<Union>C\<close> 411 proof (induction rule: finite_ne_induct) 412 case (insert i I) 413 then obtain c d where cd: "c \<in> C" "d \<in> C" and iI: "I \<subseteq> c" "i \<in> d" 414 by blast 415 from directed[OF cd] cd have "c \<union> d \<in> C" 416 by (auto simp: sup.absorb1 sup.absorb2) 417 with iI show ?case 418 by (intro bexI[of _ "c \<union> d"]) auto 419 qed auto 420 then obtain c where "c \<in> C" "S \<subseteq> c" 421 by auto 422 have "dependent c" 423 unfolding dependent_explicit 424 by (intro exI[of _ S] exI[of _ u] bexI[of _ v] conjI) fact+ 425 with indep[OF \<open>c \<in> C\<close>] show False 426 by auto 427qed 428 429lemma dependent_finite: 430 assumes "finite S" 431 shows "dependent S \<longleftrightarrow> (\<exists>u. (\<exists>v \<in> S. u v \<noteq> 0) \<and> (\<Sum>v\<in>S. u v *s v) = 0)" 432 (is "?lhs = ?rhs") 433proof 434 assume ?lhs 435 then obtain T u v 436 where "finite T" "T \<subseteq> S" "v\<in>T" "u v \<noteq> 0" "(\<Sum>v\<in>T. u v *s v) = 0" 437 by (force simp: dependent_explicit) 438 with assms show ?rhs 439 apply (rule_tac x="\<lambda>v. if v \<in> T then u v else 0" in exI) 440 apply (auto simp: sum.mono_neutral_right) 441 done 442next 443 assume ?rhs with assms show ?lhs 444 by (fastforce simp add: dependent_explicit) 445qed 446 447lemma dependent_alt: 448 "dependent B \<longleftrightarrow> 449 (\<exists>X. finite {x. X x \<noteq> 0} \<and> {x. X x \<noteq> 0} \<subseteq> B \<and> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<and> (\<exists>x. X x \<noteq> 0))" 450 unfolding dependent_explicit 451 apply safe 452 subgoal for S u v 453 apply (intro exI[of _ "\<lambda>x. if x \<in> S then u x else 0"]) 454 apply (subst sum.mono_neutral_cong_left[where T=S]) 455 apply (auto intro!: sum.mono_neutral_cong_right cong: rev_conj_cong) 456 done 457 apply auto 458 done 459 460lemma independent_alt: 461 "independent B \<longleftrightarrow> 462 (\<forall>X. finite {x. X x \<noteq> 0} \<longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<longrightarrow> (\<forall>x. X x = 0))" 463 unfolding dependent_alt by auto 464 465lemma independentD_alt: 466 "independent B \<Longrightarrow> finite {x. X x \<noteq> 0} \<Longrightarrow> {x. X x \<noteq> 0} \<subseteq> B \<Longrightarrow> (\<Sum>x|X x \<noteq> 0. X x *s x) = 0 \<Longrightarrow> X x = 0" 467 unfolding independent_alt by blast 468 469lemma independentD_unique: 470 assumes B: "independent B" 471 and X: "finite {x. X x \<noteq> 0}" "{x. X x \<noteq> 0} \<subseteq> B" 472 and Y: "finite {x. Y x \<noteq> 0}" "{x. Y x \<noteq> 0} \<subseteq> B" 473 and "(\<Sum>x | X x \<noteq> 0. X x *s x) = (\<Sum>x| Y x \<noteq> 0. Y x *s x)" 474 shows "X = Y" 475proof - 476 have "X x - Y x = 0" for x 477 using B 478 proof (rule independentD_alt) 479 have "{x. X x - Y x \<noteq> 0} \<subseteq> {x. X x \<noteq> 0} \<union> {x. Y x \<noteq> 0}" 480 by auto 481 then show "finite {x. X x - Y x \<noteq> 0}" "{x. X x - Y x \<noteq> 0} \<subseteq> B" 482 using X Y by (auto dest: finite_subset) 483 then have "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *s x) = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. (X v - Y v) *s v)" 484 using X Y by (intro sum.mono_neutral_cong_left) auto 485 also have "\<dots> = (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *s v) - (\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *s v)" 486 by (simp add: scale_left_diff_distrib sum_subtractf assms) 487 also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. X v *s v) = (\<Sum>v\<in>{S. X S \<noteq> 0}. X v *s v)" 488 using X Y by (intro sum.mono_neutral_cong_right) auto 489 also have "(\<Sum>v\<in>{S. X S \<noteq> 0} \<union> {S. Y S \<noteq> 0}. Y v *s v) = (\<Sum>v\<in>{S. Y S \<noteq> 0}. Y v *s v)" 490 using X Y by (intro sum.mono_neutral_cong_right) auto 491 finally show "(\<Sum>x | X x - Y x \<noteq> 0. (X x - Y x) *s x) = 0" 492 using assms by simp 493 qed 494 then show ?thesis 495 by auto 496qed 497 498 499section \<open>Representation of a vector on a specific basis\<close> 500 501definition representation :: "'b set \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'a" 502 where "representation basis v = 503 (if independent basis \<and> v \<in> span basis then 504 SOME f. (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> basis) \<and> finite {v. f v \<noteq> 0} \<and> (\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = v 505 else (\<lambda>b. 0))" 506 507lemma unique_representation: 508 assumes basis: "independent basis" 509 and in_basis: "\<And>v. f v \<noteq> 0 \<Longrightarrow> v \<in> basis" "\<And>v. g v \<noteq> 0 \<Longrightarrow> v \<in> basis" 510 and [simp]: "finite {v. f v \<noteq> 0}" "finite {v. g v \<noteq> 0}" 511 and eq: "(\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = (\<Sum>v\<in>{v. g v \<noteq> 0}. g v *s v)" 512 shows "f = g" 513proof (rule ext, rule ccontr) 514 fix v assume ne: "f v \<noteq> g v" 515 have "dependent basis" 516 unfolding dependent_explicit 517 proof (intro exI conjI) 518 have *: "{v. f v - g v \<noteq> 0} \<subseteq> {v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}" 519 by auto 520 show "finite {v. f v - g v \<noteq> 0}" 521 by (rule finite_subset[OF *]) simp 522 show "\<exists>v\<in>{v. f v - g v \<noteq> 0}. f v - g v \<noteq> 0" 523 by (rule bexI[of _ v]) (auto simp: ne) 524 have "(\<Sum>v | f v - g v \<noteq> 0. (f v - g v) *s v) = 525 (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. (f v - g v) *s v)" 526 by (intro sum.mono_neutral_cong_left *) auto 527 also have "... = 528 (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. f v *s v) - (\<Sum>v\<in>{v. f v \<noteq> 0} \<union> {v. g v \<noteq> 0}. g v *s v)" 529 by (simp add: algebra_simps sum_subtractf) 530 also have "... = (\<Sum>v | f v \<noteq> 0. f v *s v) - (\<Sum>v | g v \<noteq> 0. g v *s v)" 531 by (intro arg_cong2[where f= "(-)"] sum.mono_neutral_cong_right) auto 532 finally show "(\<Sum>v | f v - g v \<noteq> 0. (f v - g v) *s v) = 0" 533 by (simp add: eq) 534 show "{v. f v - g v \<noteq> 0} \<subseteq> basis" 535 using in_basis * by auto 536 qed 537 with basis show False by auto 538qed 539 540lemma 541 shows representation_ne_zero: "\<And>b. representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis" 542 and finite_representation: "finite {b. representation basis v b \<noteq> 0}" 543 and sum_nonzero_representation_eq: 544 "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b) = v" 545proof - 546 { assume basis: "independent basis" and v: "v \<in> span basis" 547 define p where "p f \<longleftrightarrow> 548 (\<forall>v. f v \<noteq> 0 \<longrightarrow> v \<in> basis) \<and> finite {v. f v \<noteq> 0} \<and> (\<Sum>v\<in>{v. f v \<noteq> 0}. f v *s v) = v" for f 549 obtain t r where *: "finite t" "t \<subseteq> basis" "(\<Sum>b\<in>t. r b *s b) = v" 550 using \<open>v \<in> span basis\<close> by (auto simp: span_explicit) 551 define f where "f b = (if b \<in> t then r b else 0)" for b 552 have "p f" 553 using * by (auto simp: p_def f_def intro!: sum.mono_neutral_cong_left) 554 have *: "representation basis v = Eps p" by (simp add: p_def[abs_def] representation_def basis v) 555 from someI[of p f, OF \<open>p f\<close>] have "p (representation basis v)" 556 unfolding * . } 557 note * = this 558 559 show "representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b 560 using * by (cases "independent basis \<and> v \<in> span basis") (auto simp: representation_def) 561 562 show "finite {b. representation basis v b \<noteq> 0}" 563 using * by (cases "independent basis \<and> v \<in> span basis") (auto simp: representation_def) 564 565 show "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b) = v" 566 using * by auto 567qed 568 569lemma sum_representation_eq: 570 "(\<Sum>b\<in>B. representation basis v b *s b) = v" 571 if "independent basis" "v \<in> span basis" "finite B" "basis \<subseteq> B" 572proof - 573 have "(\<Sum>b\<in>B. representation basis v b *s b) = 574 (\<Sum>b | representation basis v b \<noteq> 0. representation basis v b *s b)" 575 apply (rule sum.mono_neutral_cong) 576 apply (rule finite_representation) 577 apply fact 578 subgoal for b 579 using that representation_ne_zero[of basis v b] 580 by auto 581 subgoal by auto 582 subgoal by simp 583 done 584 also have "\<dots> = v" 585 by (rule sum_nonzero_representation_eq; fact) 586 finally show ?thesis . 587qed 588 589lemma representation_eqI: 590 assumes basis: "independent basis" and b: "v \<in> span basis" 591 and ne_zero: "\<And>b. f b \<noteq> 0 \<Longrightarrow> b \<in> basis" 592 and finite: "finite {b. f b \<noteq> 0}" 593 and eq: "(\<Sum>b | f b \<noteq> 0. f b *s b) = v" 594 shows "representation basis v = f" 595 by (rule unique_representation[OF basis]) 596 (auto simp: representation_ne_zero finite_representation 597 sum_nonzero_representation_eq[OF basis b] ne_zero finite eq) 598 599lemma representation_basis: 600 assumes basis: "independent basis" and b: "b \<in> basis" 601 shows "representation basis b = (\<lambda>v. if v = b then 1 else 0)" 602proof (rule unique_representation[OF basis]) 603 show "representation basis b v \<noteq> 0 \<Longrightarrow> v \<in> basis" for v 604 using representation_ne_zero . 605 show "finite {v. representation basis b v \<noteq> 0}" 606 using finite_representation . 607 show "(if v = b then 1 else 0) \<noteq> 0 \<Longrightarrow> v \<in> basis" for v 608 by (cases "v = b") (auto simp: b) 609 have *: "{v. (if v = b then 1 else 0 :: 'a) \<noteq> 0} = {b}" 610 by auto 611 show "finite {v. (if v = b then 1 else 0) \<noteq> 0}" unfolding * by auto 612 show "(\<Sum>v | representation basis b v \<noteq> 0. representation basis b v *s v) = 613 (\<Sum>v | (if v = b then 1 else 0::'a) \<noteq> 0. (if v = b then 1 else 0) *s v)" 614 unfolding * sum_nonzero_representation_eq[OF basis span_base[OF b]] by auto 615qed 616 617lemma representation_zero: "representation basis 0 = (\<lambda>b. 0)" 618proof cases 619 assume basis: "independent basis" show ?thesis 620 by (rule representation_eqI[OF basis span_zero]) auto 621qed (simp add: representation_def) 622 623lemma representation_diff: 624 assumes basis: "independent basis" and v: "v \<in> span basis" and u: "u \<in> span basis" 625 shows "representation basis (u - v) = (\<lambda>b. representation basis u b - representation basis v b)" 626proof (rule representation_eqI[OF basis span_diff[OF u v]]) 627 let ?R = "representation basis" 628 note finite_representation[simp] u[simp] v[simp] 629 have *: "{b. ?R u b - ?R v b \<noteq> 0} \<subseteq> {b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}" 630 by auto 631 then show "?R u b - ?R v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b 632 by (auto dest: representation_ne_zero) 633 show "finite {b. ?R u b - ?R v b \<noteq> 0}" 634 by (intro finite_subset[OF *]) simp_all 635 have "(\<Sum>b | ?R u b - ?R v b \<noteq> 0. (?R u b - ?R v b) *s b) = 636 (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. (?R u b - ?R v b) *s b)" 637 by (intro sum.mono_neutral_cong_left *) auto 638 also have "... = 639 (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. ?R u b *s b) - (\<Sum>b\<in>{b. ?R u b \<noteq> 0} \<union> {b. ?R v b \<noteq> 0}. ?R v b *s b)" 640 by (simp add: algebra_simps sum_subtractf) 641 also have "... = (\<Sum>b | ?R u b \<noteq> 0. ?R u b *s b) - (\<Sum>b | ?R v b \<noteq> 0. ?R v b *s b)" 642 by (intro arg_cong2[where f= "(-)"] sum.mono_neutral_cong_right) auto 643 finally show "(\<Sum>b | ?R u b - ?R v b \<noteq> 0. (?R u b - ?R v b) *s b) = u - v" 644 by (simp add: sum_nonzero_representation_eq[OF basis]) 645qed 646 647lemma representation_neg: 648 "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> representation basis (- v) = (\<lambda>b. - representation basis v b)" 649 using representation_diff[of basis v 0] by (simp add: representation_zero span_zero) 650 651lemma representation_add: 652 "independent basis \<Longrightarrow> v \<in> span basis \<Longrightarrow> u \<in> span basis \<Longrightarrow> 653 representation basis (u + v) = (\<lambda>b. representation basis u b + representation basis v b)" 654 using representation_diff[of basis "-v" u] by (simp add: representation_neg representation_diff span_neg) 655 656lemma representation_sum: 657 "independent basis \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> v i \<in> span basis) \<Longrightarrow> 658 representation basis (sum v I) = (\<lambda>b. \<Sum>i\<in>I. representation basis (v i) b)" 659 by (induction I rule: infinite_finite_induct) 660 (auto simp: representation_zero representation_add span_sum) 661 662lemma representation_scale: 663 assumes basis: "independent basis" and v: "v \<in> span basis" 664 shows "representation basis (r *s v) = (\<lambda>b. r * representation basis v b)" 665proof (rule representation_eqI[OF basis span_scale[OF v]]) 666 let ?R = "representation basis" 667 note finite_representation[simp] v[simp] 668 have *: "{b. r * ?R v b \<noteq> 0} \<subseteq> {b. ?R v b \<noteq> 0}" 669 by auto 670 then show "r * representation basis v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b 671 using representation_ne_zero by auto 672 show "finite {b. r * ?R v b \<noteq> 0}" 673 by (intro finite_subset[OF *]) simp_all 674 have "(\<Sum>b | r * ?R v b \<noteq> 0. (r * ?R v b) *s b) = (\<Sum>b\<in>{b. ?R v b \<noteq> 0}. (r * ?R v b) *s b)" 675 by (intro sum.mono_neutral_cong_left *) auto 676 also have "... = r *s (\<Sum>b | ?R v b \<noteq> 0. ?R v b *s b)" 677 by (simp add: scale_scale[symmetric] scale_sum_right del: scale_scale) 678 finally show "(\<Sum>b | r * ?R v b \<noteq> 0. (r * ?R v b) *s b) = r *s v" 679 by (simp add: sum_nonzero_representation_eq[OF basis]) 680qed 681 682lemma representation_extend: 683 assumes basis: "independent basis" and v: "v \<in> span basis'" and basis': "basis' \<subseteq> basis" 684 shows "representation basis v = representation basis' v" 685proof (rule representation_eqI[OF basis]) 686 show v': "v \<in> span basis" using span_mono[OF basis'] v by auto 687 have *: "independent basis'" using basis' basis by (auto intro: dependent_mono) 688 show "representation basis' v b \<noteq> 0 \<Longrightarrow> b \<in> basis" for b 689 using representation_ne_zero basis' by auto 690 show "finite {b. representation basis' v b \<noteq> 0}" 691 using finite_representation . 692 show "(\<Sum>b | representation basis' v b \<noteq> 0. representation basis' v b *s b) = v" 693 using sum_nonzero_representation_eq[OF * v] . 694qed 695 696text \<open>The set \<open>B\<close> is the maximal independent set for \<open>span B\<close>, or \<open>A\<close> is the minimal spanning set\<close> 697lemma spanning_subset_independent: 698 assumes BA: "B \<subseteq> A" 699 and iA: "independent A" 700 and AsB: "A \<subseteq> span B" 701 shows "A = B" 702proof (intro antisym[OF _ BA] subsetI) 703 have iB: "independent B" using independent_mono [OF iA BA] . 704 fix v assume "v \<in> A" 705 with AsB have "v \<in> span B" by auto 706 let ?RB = "representation B v" and ?RA = "representation A v" 707 have "?RB v = 1" 708 unfolding representation_extend[OF iA \<open>v \<in> span B\<close> BA, symmetric] representation_basis[OF iA \<open>v \<in> A\<close>] by simp 709 then show "v \<in> B" 710 using representation_ne_zero[of B v v] by auto 711qed 712 713end 714 715(* We need to introduce more specific modules, where the ring structure gets more and more finer, 716 i.e. Bezout rings & domains, division rings, fields *) 717 718text \<open>A linear function is a mapping between two modules over the same ring.\<close> 719 720locale module_hom = m1: module s1 + m2: module s2 721 for s1 :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75) 722 and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) + 723 fixes f :: "'b \<Rightarrow> 'c" 724 assumes add: "f (b1 + b2) = f b1 + f b2" 725 and scale: "f (r *a b) = r *b f b" 726begin 727 728lemma zero[simp]: "f 0 = 0" 729 using scale[of 0 0] by simp 730 731lemma neg: "f (- x) = - f x" 732 using scale [where r="-1"] by (metis add add_eq_0_iff zero) 733 734lemma diff: "f (x - y) = f x - f y" 735 by (metis diff_conv_add_uminus add neg) 736 737lemma sum: "f (sum g S) = (\<Sum>a\<in>S. f (g a))" 738proof (induct S rule: infinite_finite_induct) 739 case (insert x F) 740 have "f (sum g (insert x F)) = f (g x + sum g F)" 741 using insert.hyps by simp 742 also have "\<dots> = f (g x) + f (sum g F)" 743 using add by simp 744 also have "\<dots> = (\<Sum>a\<in>insert x F. f (g a))" 745 using insert.hyps by simp 746 finally show ?case . 747qed simp_all 748 749lemma inj_on_iff_eq_0: 750 assumes s: "m1.subspace s" 751 shows "inj_on f s \<longleftrightarrow> (\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0)" 752proof - 753 have "inj_on f s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. f x - f y = 0 \<longrightarrow> x - y = 0)" 754 by (simp add: inj_on_def) 755 also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. f (x - y) = 0 \<longrightarrow> x - y = 0)" 756 by (simp add: diff) 757 also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0)" (is "?l = ?r")(* TODO: sledgehammer! *) 758 proof safe 759 fix x assume ?l assume "x \<in> s" "f x = 0" with \<open>?l\<close>[rule_format, of x 0] s show "x = 0" 760 by (auto simp: m1.subspace_0) 761 next 762 fix x y assume ?r assume "x \<in> s" "y \<in> s" "f (x - y) = 0" 763 with \<open>?r\<close>[rule_format, of "x - y"] s 764 show "x - y = 0" 765 by (auto simp: m1.subspace_diff) 766 qed 767 finally show ?thesis 768 by auto 769qed 770 771lemma inj_iff_eq_0: "inj f = (\<forall>x. f x = 0 \<longrightarrow> x = 0)" 772 by (rule inj_on_iff_eq_0[OF m1.subspace_UNIV, unfolded ball_UNIV]) 773 774lemma subspace_image: assumes S: "m1.subspace S" shows "m2.subspace (f ` S)" 775 unfolding m2.subspace_def 776proof safe 777 show "0 \<in> f ` S" 778 by (rule image_eqI[of _ _ 0]) (auto simp: S m1.subspace_0) 779 show "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x + f y \<in> f ` S" for x y 780 by (rule image_eqI[of _ _ "x + y"]) (auto simp: S m1.subspace_add add) 781 show "x \<in> S \<Longrightarrow> r *b f x \<in> f ` S" for r x 782 by (rule image_eqI[of _ _ "r *a x"]) (auto simp: S m1.subspace_scale scale) 783qed 784 785lemma subspace_vimage: "m2.subspace S \<Longrightarrow> m1.subspace (f -` S)" 786 by (simp add: vimage_def add scale m1.subspace_def m2.subspace_0 m2.subspace_add m2.subspace_scale) 787 788lemma subspace_kernel: "m1.subspace {x. f x = 0}" 789 using subspace_vimage[OF m2.subspace_single_0] by (simp add: vimage_def) 790 791lemma span_image: "m2.span (f ` S) = f ` (m1.span S)" 792proof (rule m2.span_unique) 793 show "f ` S \<subseteq> f ` m1.span S" 794 by (rule image_mono, rule m1.span_superset) 795 show "m2.subspace (f ` m1.span S)" 796 using m1.subspace_span by (rule subspace_image) 797next 798 fix T assume "f ` S \<subseteq> T" and "m2.subspace T" then show "f ` m1.span S \<subseteq> T" 799 unfolding image_subset_iff_subset_vimage by (metis subspace_vimage m1.span_minimal) 800qed 801 802lemma dependent_inj_imageD: 803 assumes d: "m2.dependent (f ` s)" and i: "inj_on f (m1.span s)" 804 shows "m1.dependent s" 805proof - 806 have [intro]: "inj_on f s" 807 using \<open>inj_on f (m1.span s)\<close> m1.span_superset by (rule inj_on_subset) 808 from d obtain s' r v where *: "finite s'" "s' \<subseteq> s" "(\<Sum>v\<in>f ` s'. r v *b v) = 0" "v \<in> s'" "r (f v) \<noteq> 0" 809 by (auto simp: m2.dependent_explicit subset_image_iff dest!: finite_imageD intro: inj_on_subset) 810 have "f (\<Sum>v\<in>s'. r (f v) *a v) = (\<Sum>v\<in>s'. r (f v) *b f v)" 811 by (simp add: sum scale) 812 also have "... = (\<Sum>v\<in>f ` s'. r v *b v)" 813 using \<open>s' \<subseteq> s\<close> by (subst sum.reindex) (auto dest!: finite_imageD intro: inj_on_subset) 814 finally have "f (\<Sum>v\<in>s'. r (f v) *a v) = 0" 815 by (simp add: *) 816 with \<open>s' \<subseteq> s\<close> have "(\<Sum>v\<in>s'. r (f v) *a v) = 0" 817 by (intro inj_onD[OF i] m1.span_zero m1.span_sum m1.span_scale) (auto intro: m1.span_base) 818 then show "m1.dependent s" 819 using \<open>finite s'\<close> \<open>s' \<subseteq> s\<close> \<open>v \<in> s'\<close> \<open>r (f v) \<noteq> 0\<close> by (force simp add: m1.dependent_explicit) 820qed 821 822lemma eq_0_on_span: 823 assumes f0: "\<And>x. x \<in> b \<Longrightarrow> f x = 0" and x: "x \<in> m1.span b" shows "f x = 0" 824 using m1.span_induct[OF x subspace_kernel] f0 by simp 825 826lemma independent_injective_image: "m1.independent s \<Longrightarrow> inj_on f (m1.span s) \<Longrightarrow> m2.independent (f ` s)" 827 using dependent_inj_imageD[of s] by auto 828 829lemma inj_on_span_independent_image: 830 assumes ifB: "m2.independent (f ` B)" and f: "inj_on f B" shows "inj_on f (m1.span B)" 831 unfolding inj_on_iff_eq_0[OF m1.subspace_span] unfolding m1.span_explicit' 832proof safe 833 fix r assume fr: "finite {v. r v \<noteq> 0}" and r: "\<forall>v. r v \<noteq> 0 \<longrightarrow> v \<in> B" 834 and eq0: "f (\<Sum>v | r v \<noteq> 0. r v *a v) = 0" 835 have "0 = (\<Sum>v | r v \<noteq> 0. r v *b f v)" 836 using eq0 by (simp add: sum scale) 837 also have "... = (\<Sum>v\<in>f ` {v. r v \<noteq> 0}. r (the_inv_into B f v) *b v)" 838 using r by (subst sum.reindex) (auto simp: the_inv_into_f_f[OF f] intro!: inj_on_subset[OF f] sum.cong) 839 finally have "r v \<noteq> 0 \<Longrightarrow> r (the_inv_into B f (f v)) = 0" for v 840 using fr r ifB[unfolded m2.independent_explicit_module, rule_format, 841 of "f ` {v. r v \<noteq> 0}" "\<lambda>v. r (the_inv_into B f v)"] 842 by auto 843 then have "r v = 0" for v 844 using the_inv_into_f_f[OF f] r by auto 845 then show "(\<Sum>v | r v \<noteq> 0. r v *a v) = 0" by auto 846qed 847 848lemma inj_on_span_iff_independent_image: "m2.independent (f ` B) \<Longrightarrow> inj_on f (m1.span B) \<longleftrightarrow> inj_on f B" 849 using inj_on_span_independent_image[of B] inj_on_subset[OF _ m1.span_superset, of f B] by auto 850 851lemma subspace_linear_preimage: "m2.subspace S \<Longrightarrow> m1.subspace {x. f x \<in> S}" 852 by (simp add: add scale m1.subspace_def m2.subspace_def) 853 854lemma spans_image: "V \<subseteq> m1.span B \<Longrightarrow> f ` V \<subseteq> m2.span (f ` B)" 855 by (metis image_mono span_image) 856 857text \<open>Relation between bases and injectivity/surjectivity of map.\<close> 858 859lemma spanning_surjective_image: 860 assumes us: "UNIV \<subseteq> m1.span S" 861 and sf: "surj f" 862 shows "UNIV \<subseteq> m2.span (f ` S)" 863proof - 864 have "UNIV \<subseteq> f ` UNIV" 865 using sf by (auto simp add: surj_def) 866 also have " \<dots> \<subseteq> m2.span (f ` S)" 867 using spans_image[OF us] . 868 finally show ?thesis . 869qed 870 871lemmas independent_inj_on_image = independent_injective_image 872 873lemma independent_inj_image: 874 "m1.independent S \<Longrightarrow> inj f \<Longrightarrow> m2.independent (f ` S)" 875 using independent_inj_on_image[of S] by (auto simp: subset_inj_on) 876 877end 878 879lemma module_hom_iff: 880 "module_hom s1 s2 f \<longleftrightarrow> 881 module s1 \<and> module s2 \<and> 882 (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (s1 c x) = s2 c (f x))" 883 by (simp add: module_hom_def module_hom_axioms_def) 884 885locale module_pair = m1: module s1 + m2: module s2 886 for s1 :: "'a :: comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b :: ab_group_add" 887 and s2 :: "'a :: comm_ring_1 \<Rightarrow> 'c \<Rightarrow> 'c :: ab_group_add" 888begin 889 890lemma module_hom_zero: "module_hom s1 s2 (\<lambda>x. 0)" 891 by (simp add: module_hom_iff m1.module_axioms m2.module_axioms) 892 893lemma module_hom_add: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 g \<Longrightarrow> module_hom s1 s2 (\<lambda>x. f x + g x)" 894 by (simp add: module_hom_iff module.scale_right_distrib) 895 896lemma module_hom_sub: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 g \<Longrightarrow> module_hom s1 s2 (\<lambda>x. f x - g x)" 897 by (simp add: module_hom_iff module.scale_right_diff_distrib) 898 899lemma module_hom_neg: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 (\<lambda>x. - f x)" 900 by (simp add: module_hom_iff module.scale_minus_right) 901 902lemma module_hom_scale: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 (\<lambda>x. s2 c (f x))" 903 by (simp add: module_hom_iff module.scale_scale module.scale_right_distrib ac_simps) 904 905lemma module_hom_compose_scale: 906 "module_hom s1 s2 (\<lambda>x. s2 (f x) (c))" 907 if "module_hom s1 (*) f" 908proof - 909 interpret mh: module_hom s1 "(*)" f by fact 910 show ?thesis 911 by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib) 912qed 913 914lemma bij_module_hom_imp_inv_module_hom: "module_hom scale1 scale2 f \<Longrightarrow> bij f \<Longrightarrow> 915 module_hom scale2 scale1 (inv f)" 916 by (auto simp: module_hom_iff bij_is_surj bij_is_inj surj_f_inv_f 917 intro!: Hilbert_Choice.inv_f_eq) 918 919lemma module_hom_sum: "(\<And>i. i \<in> I \<Longrightarrow> module_hom s1 s2 (f i)) \<Longrightarrow> (I = {} \<Longrightarrow> module s1 \<and> module s2) \<Longrightarrow> module_hom s1 s2 (\<lambda>x. \<Sum>i\<in>I. f i x)" 920 apply (induction I rule: infinite_finite_induct) 921 apply (auto intro!: module_hom_zero module_hom_add) 922 using m1.module_axioms m2.module_axioms by blast 923 924lemma module_hom_eq_on_span: "f x = g x" 925 if "module_hom s1 s2 f" "module_hom s1 s2 g" 926 and "(\<And>x. x \<in> B \<Longrightarrow> f x = g x)" "x \<in> m1.span B" 927proof - 928 interpret module_hom s1 s2 "\<lambda>x. f x - g x" 929 by (rule module_hom_sub that)+ 930 from eq_0_on_span[OF _ that(4)] that(3) show ?thesis by auto 931qed 932 933end 934 935context module begin 936 937lemma module_hom_scale_self[simp]: 938 "module_hom scale scale (\<lambda>x. scale c x)" 939 using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast 940 941lemma module_hom_scale_left[simp]: 942 "module_hom (*) scale (\<lambda>r. scale r x)" 943 by unfold_locales (auto simp: algebra_simps) 944 945lemma module_hom_id: "module_hom scale scale id" 946 by (simp add: module_hom_iff module_axioms) 947 948lemma module_hom_ident: "module_hom scale scale (\<lambda>x. x)" 949 by (simp add: module_hom_iff module_axioms) 950 951lemma module_hom_uminus: "module_hom scale scale uminus" 952 by (simp add: module_hom_iff module_axioms) 953 954end 955 956lemma module_hom_compose: "module_hom s1 s2 f \<Longrightarrow> module_hom s2 s3 g \<Longrightarrow> module_hom s1 s3 (g o f)" 957 by (auto simp: module_hom_iff) 958 959end 960