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