(* Title: HOL/Vector_Spaces.thy
Author: Amine Chaieb, University of Cambridge
Author: Jose Divasón <jose.divasonm at unirioja.es>
Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
Author: Johannes Hölzl, VU Amsterdam
Author: Fabian Immler, TUM
*)
section \<open>Vector Spaces\<close>
theory Vector_Spaces
imports Modules
begin
lemma isomorphism_expand:
"f \ g = id \ g \ f = id \ (\x. f (g x) = x) \ (\x. g (f x) = x)"
by (simp add: fun_eq_iff o_def id_def)
lemma left_right_inverse_eq:
assumes fg: "f \ g = id"
and gh: "g \ h = id"
shows "f = h"
proof -
have "f = f \ (g \ h)"
unfolding gh by simp
also have "\ = (f \ g) \ h"
by (simp add: o_assoc)
finally show "f = h"
unfolding fg by simp
qed
lemma ordLeq3_finite_infinite:
assumes A: "finite A" and B: "infinite B" shows "ordLeq3 (card_of A) (card_of B)"
proof -
have \<open>ordLeq3 (card_of A) (card_of B) \<or> ordLeq3 (card_of B) (card_of A)\<close>
by (intro ordLeq_total card_of_Well_order)
moreover have "\ ordLeq3 (card_of B) (card_of A)"
using B A card_of_ordLeq_finite[of B A] by auto
ultimately show ?thesis by auto
qed
locale vector_space =
fixes scale :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*s" 75)
assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
allows us to rewrite in the sublocale.\<close>
"a *s (x + y) = a *s x + a *s y"
"(a + b) *s x = a *s x + b *s x"
"a *s (b *s x) = (a * b) *s x"
"1 *s x = x"
lemma module_iff_vector_space: "module s \ vector_space s"
unfolding module_def vector_space_def ..
locale linear = vs1: vector_space s1 + vs2: vector_space s2 + module_hom s1 s2 f
for s1 :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*a" 75)
and s2 :: "'a::field \ 'c::ab_group_add \ 'c" (infixr "*b" 75)
and f :: "'b \ 'c"
lemma module_hom_iff_linear: "module_hom s1 s2 f \ linear s1 s2 f"
unfolding module_hom_def linear_def module_iff_vector_space by auto
lemmas module_hom_eq_linear = module_hom_iff_linear[abs_def, THEN meta_eq_to_obj_eq]
lemmas linear_iff_module_hom = module_hom_iff_linear[symmetric]
lemmas linear_module_homI = module_hom_iff_linear[THEN iffD1]
and module_hom_linearI = module_hom_iff_linear[THEN iffD2]
context vector_space begin
sublocale module scale rewrites "module_hom = linear"
by unfold_locales (fact vector_space_assms module_hom_eq_linear)+
lemmas\<comment> \<open>from \<open>module\<close>\<close>
linear_id = module_hom_id
and linear_ident = module_hom_ident
and linear_scale_self = module_hom_scale_self
and linear_scale_left = module_hom_scale_left
and linear_uminus = module_hom_uminus
lemma linear_imp_scale:
fixes D::"'a \ 'b"
assumes "linear (*) scale D"
obtains d where "D = (\x. scale x d)"
proof -
interpret linear "(*)" scale D by fact
show ?thesis
by (metis mult.commute mult.left_neutral scale that)
qed
lemma scale_eq_0_iff [simp]: "scale a x = 0 \ a = 0 \ x = 0"
by (metis scale_left_commute right_inverse scale_one scale_scale scale_zero_left)
lemma scale_left_imp_eq:
assumes nonzero: "a \ 0"
and scale: "scale a x = scale a y"
shows "x = y"
proof -
from scale have "scale a (x - y) = 0"
by (simp add: scale_right_diff_distrib)
with nonzero have "x - y = 0" by simp
then show "x = y" by (simp only: right_minus_eq)
qed
lemma scale_right_imp_eq:
assumes nonzero: "x \ 0"
and scale: "scale a x = scale b x"
shows "a = b"
proof -
from scale have "scale (a - b) x = 0"
by (simp add: scale_left_diff_distrib)
with nonzero have "a - b = 0" by simp
then show "a = b" by (simp only: right_minus_eq)
qed
lemma scale_cancel_left [simp]: "scale a x = scale a y \ x = y \ a = 0"
by (auto intro: scale_left_imp_eq)
lemma scale_cancel_right [simp]: "scale a x = scale b x \ a = b \ x = 0"
by (auto intro: scale_right_imp_eq)
lemma injective_scale: "c \ 0 \ inj (\x. scale c x)"
by (simp add: inj_on_def)
lemma dependent_def: "dependent P \ (\a \ P. a \ span (P - {a}))"
unfolding dependent_explicit
proof safe
fix a assume aP: "a \ P" and "a \ span (P - {a})"
then obtain a S u
where aP: "a \ P" and fS: "finite S" and SP: "S \ P" "a \ S" and ua: "(\v\S. u v *s v) = a"
unfolding span_explicit by blast
let ?S = "insert a S"
let ?u = "\y. if y = a then - 1 else u y"
from fS SP have "(\v\?S. ?u v *s v) = 0"
by (simp add: if_distrib[of "\r. r *s a" for a] sum.If_cases field_simps Diff_eq[symmetric] ua)
moreover have "finite ?S" "?S \ P" "a \ ?S" "?u a \ 0"
using fS SP aP by auto
ultimately show "\t u. finite t \ t \ P \ (\v\t. u v *s v) = 0 \ (\v\t. u v \ 0)" by fast
next
fix S u v
assume fS: "finite S" and SP: "S \ P" and vS: "v \ S"
and uv: "u v \ 0" and u: "(\v\S. u v *s v) = 0"
let ?a = v
let ?S = "S - {v}"
let ?u = "\i. (- u i) / u v"
have th0: "?a \ P" "finite ?S" "?S \ P"
using fS SP vS by auto
have "(\v\?S. ?u v *s v) = (\v\S. (- (inverse (u ?a))) *s (u v *s v)) - ?u v *s v"
using fS vS uv by (simp add: sum_diff1 field_simps)
also have "\ = ?a"
unfolding scale_sum_right[symmetric] u using uv by simp
finally have "(\v\?S. ?u v *s v) = ?a" .
with th0 show "\a \ P. a \ span (P - {a})"
unfolding span_explicit by (auto intro!: bexI[where x="?a"] exI[where x="?S"] exI[where x="?u"])
qed
lemma dependent_single[simp]: "dependent {x} \ x = 0"
unfolding dependent_def by auto
lemma in_span_insert:
assumes a: "a \ span (insert b S)"
and na: "a \ span S"
shows "b \ span (insert a S)"
proof -
from span_breakdown[of b "insert b S" a, OF insertI1 a]
obtain k where k: "a - k *s b \ span (S - {b})" by auto
have "k \ 0"
proof
assume "k = 0"
with k span_mono[of "S - {b}" S] have "a \ span S" by auto
with na show False by blast
qed
then have eq: "b = (1/k) *s a - (1/k) *s (a - k *s b)"
by (simp add: algebra_simps)
from k have "(1/k) *s (a - k *s b) \ span (S - {b})"
by (rule span_scale)
also have "... \ span (insert a S)"
by (rule span_mono) auto
finally show ?thesis
using k by (subst eq) (blast intro: span_diff span_scale span_base)
qed
lemma dependent_insertD: assumes a: "a \ span S" and S: "dependent (insert a S)" shows "dependent S"
proof -
have "a \ S" using a by (auto dest: span_base)
obtain b where b: "b = a \ b \ S" "b \ span (insert a S - {b})"
using S unfolding dependent_def by blast
have "b \ a" "b \ S"
using b \<open>a \<notin> S\<close> a by auto
with b have *: "b \ span (insert a (S - {b}))"
by (auto simp: insert_Diff_if)
show "dependent S"
proof cases
assume "b \ span (S - {b})" with \b \ S\ show ?thesis
by (auto simp add: dependent_def)
next
assume "b \ span (S - {b})"
with * have "a \ span (insert b (S - {b}))" by (rule in_span_insert)
with a show ?thesis
using \<open>b \<in> S\<close> by (auto simp: insert_absorb)
qed
qed
lemma independent_insertI: "a \ span S \ independent S \ independent (insert a S)"
by (auto dest: dependent_insertD)
lemma independent_insert:
"independent (insert a S) \ (if a \ S then independent S else independent S \ a \ span S)"
proof -
have "a \ S \ a \ span S \ dependent (insert a S)"
by (auto simp: dependent_def)
then show ?thesis
by (auto intro: dependent_mono simp: independent_insertI)
qed
lemma maximal_independent_subset_extend:
assumes "S \ V" "independent S"
obtains B where "S \ B" "B \ V" "independent B" "V \ span B"
proof -
let ?C = "{B. S \ B \ independent B \ B \ V}"
have "\M\?C. \X\?C. M \ X \ X = M"
proof (rule subset_Zorn)
fix C :: "'b set set" assume "subset.chain ?C C"
then have C: "\c. c \ C \ c \ V" "\c. c \ C \ S \ c" "\c. c \ C \ independent c"
"\c d. c \ C \ d \ C \ c \ d \ d \ c"
unfolding subset.chain_def by blast+
show "\U\?C. \X\C. X \ U"
proof cases
assume "C = {}" with assms show ?thesis
by (auto intro!: exI[of _ S])
next
assume "C \ {}"
with C(2) have "S \ \C"
by auto
moreover have "independent (\C)"
by (intro independent_Union_directed C)
moreover have "\C \ V"
using C by auto
ultimately show ?thesis
by auto
qed
qed
then obtain B where B: "independent B" "B \ V" "S \ B"
and max: "\S. independent S \ S \ V \ B \ S \ S = B"
by auto
moreover
{ assume "\ V \ span B"
then obtain v where "v \ V" "v \ span B"
by auto
with B have "independent (insert v B)" by (auto intro: dependent_insertD)
from max[OF this] \<open>v \<in> V\<close> \<open>B \<subseteq> V\<close>
have "v \ B"
by auto
with \<open>v \<notin> span B\<close> have False
by (auto intro: span_base) }
ultimately show ?thesis
by (meson that)
qed
lemma maximal_independent_subset:
obtains B where "B \ V" "independent B" "V \ span B"
by (metis maximal_independent_subset_extend[of "{}"] empty_subsetI independent_empty)
text \<open>Extends a basis from B to a basis of the entire space.\<close>
definition extend_basis :: "'b set \ 'b set"
where "extend_basis B = (SOME B'. B \ B' \ independent B' \ span B' = UNIV)"
lemma
assumes B: "independent B"
shows extend_basis_superset: "B \ extend_basis B"
and independent_extend_basis: "independent (extend_basis B)"
and span_extend_basis[simp]: "span (extend_basis B) = UNIV"
proof -
define p where "p B' \ B \ B' \ independent B' \ span B' = UNIV" for B'
obtain B' where "p B'"
using maximal_independent_subset_extend[OF subset_UNIV B]
by (metis top.extremum_uniqueI p_def)
then have "p (extend_basis B)"
unfolding extend_basis_def p_def[symmetric] by (rule someI)
then show "B \ extend_basis B" "independent (extend_basis B)" "span (extend_basis B) = UNIV"
by (auto simp: p_def)
qed
lemma in_span_delete:
assumes a: "a \ span S" and na: "a \ span (S - {b})"
shows "b \ span (insert a (S - {b}))"
by (metis Diff_empty Diff_insert0 a in_span_insert insert_Diff na)
lemma span_redundant: "x \ span S \ span (insert x S) = span S"
unfolding span_def by (rule hull_redundant)
lemma span_trans: "x \ span S \ y \ span (insert x S) \ y \ span S"
by (simp only: span_redundant)
lemma span_insert_0[simp]: "span (insert 0 S) = span S"
by (metis span_zero span_redundant)
lemma span_delete_0 [simp]: "span(S - {0}) = span S"
proof
show "span (S - {0}) \ span S"
by (blast intro!: span_mono)
next
have "span S \ span(insert 0 (S - {0}))"
by (blast intro!: span_mono)
also have "... \ span(S - {0})"
using span_insert_0 by blast
finally show "span S \ span (S - {0})" .
qed
lemma span_image_scale:
assumes "finite S" and nz: "\x. x \ S \ c x \ 0"
shows "span ((\x. c x *s x) ` S) = span S"
using assms
proof (induction S arbitrary: c)
case (empty c) show ?case by simp
next
case (insert x F c)
show ?case
proof (intro set_eqI iffI)
fix y
assume "y \ span ((\x. c x *s x) ` insert x F)"
then show "y \ span (insert x F)"
using insert by (force simp: span_breakdown_eq)
next
fix y
assume "y \ span (insert x F)"
then show "y \ span ((\x. c x *s x) ` insert x F)"
using insert
apply (clarsimp simp: span_breakdown_eq)
apply (rule_tac x="k / c x" in exI)
by simp
qed
qed
lemma exchange_lemma:
assumes f: "finite T"
and i: "independent S"
and sp: "S \ span T"
shows "\t'. card t' = card T \ finite t' \ S \ t' \ t' \ S \ T \ S \ span t'"
using f i sp
proof (induct "card (T - S)" arbitrary: S T rule: less_induct)
case less
note ft = \<open>finite T\<close> and S = \<open>independent S\<close> and sp = \<open>S \<subseteq> span T\<close>
let ?P = "\t'. card t' = card T \ finite t' \ S \ t' \ t' \ S \ T \ S \ span t'"
show ?case
proof (cases "S \ T \ T \ S")
case True
then show ?thesis
proof
assume "S \ T" then show ?thesis
by (metis ft Un_commute sp sup_ge1)
next
assume "T \ S" then show ?thesis
by (metis Un_absorb sp spanning_subset_independent[OF _ S sp] ft)
qed
next
case False
then have st: "\ S \ T" "\ T \ S"
by auto
from st(2) obtain b where b: "b \ T" "b \ S"
by blast
from b have "T - {b} - S \ T - S"
by blast
then have cardlt: "card (T - {b} - S) < card (T - S)"
using ft by (auto intro: psubset_card_mono)
from b ft have ct0: "card T \ 0"
by auto
show ?thesis
proof (cases "S \ span (T - {b})")
case True
from ft have ftb: "finite (T - {b})"
by auto
from less(1)[OF cardlt ftb S True]
obtain U where U: "card U = card (T - {b})" "S \ U" "U \ S \ (T - {b})" "S \ span U"
and fu: "finite U" by blast
let ?w = "insert b U"
have th0: "S \ insert b U"
using U by blast
have th1: "insert b U \ S \ T"
using U b by blast
have bu: "b \ U"
using b U by blast
from U(1) ft b have "card U = (card T - 1)"
by auto
then have th2: "card (insert b U) = card T"
using card_insert_disjoint[OF fu bu] ct0 by auto
from U(4) have "S \ span U" .
also have "\ \ span (insert b U)"
by (rule span_mono) blast
finally have th3: "S \ span (insert b U)" .
from th0 th1 th2 th3 fu have th: "?P ?w"
by blast
from th show ?thesis by blast
next
case False
then obtain a where a: "a \ S" "a \ span (T - {b})"
by blast
have ab: "a \ b"
using a b by blast
have at: "a \ T"
using a ab span_base[of a "T- {b}"] by auto
have mlt: "card ((insert a (T - {b})) - S) < card (T - S)"
using cardlt ft a b by auto
have ft': "finite (insert a (T - {b}))"
using ft by auto
have sp': "S \ span (insert a (T - {b}))"
proof
fix x
assume xs: "x \ S"
have T: "T \ insert b (insert a (T - {b}))"
using b by auto
have bs: "b \ span (insert a (T - {b}))"
by (rule in_span_delete) (use a sp in auto)
from xs sp have "x \ span T"
by blast
with span_mono[OF T] have x: "x \ span (insert b (insert a (T - {b})))" ..
from span_trans[OF bs x] show "x \ span (insert a (T - {b}))" .
qed
from less(1)[OF mlt ft' S sp'] obtain U where U:
"card U = card (insert a (T - {b}))"
"finite U" "S \ U" "U \ S \ insert a (T - {b})"
"S \ span U" by blast
from U a b ft at ct0 have "?P U"
by auto
then show ?thesis by blast
qed
qed
qed
lemma independent_span_bound:
assumes f: "finite T"
and i: "independent S"
and sp: "S \ span T"
shows "finite S \ card S \ card T"
by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
lemma independent_explicit_finite_subsets:
"independent A \ (\S \ A. finite S \ (\u. (\v\S. u v *s v) = 0 \ (\v\S. u v = 0)))"
unfolding dependent_explicit [of A] by (simp add: disj_not2)
lemma independent_if_scalars_zero:
assumes fin_A: "finite A"
and sum: "\f x. (\x\A. f x *s x) = 0 \ x \ A \ f x = 0"
shows "independent A"
proof (unfold independent_explicit_finite_subsets, clarify)
fix S v and u :: "'b \ 'a"
assume S: "S \ A" and v: "v \ S"
let ?g = "\x. if x \ S then u x else 0"
have "(\v\A. ?g v *s v) = (\v\S. u v *s v)"
using S fin_A by (auto intro!: sum.mono_neutral_cong_right)
also assume "(\v\S. u v *s v) = 0"
finally have "?g v = 0" using v S sum by force
thus "u v = 0" unfolding if_P[OF v] .
qed
lemma bij_if_span_eq_span_bases:
assumes B: "independent B" and C: "independent C"
and eq: "span B = span C"
shows "\f. bij_betw f B C"
proof cases
assume "finite B \ finite C"
then have "finite B \ finite C \ card C = card B"
using independent_span_bound[of B C] independent_span_bound[of C B] assms
span_superset[of B] span_superset[of C]
by auto
then show ?thesis
by (auto intro!: finite_same_card_bij)
next
assume "\ (finite B \ finite C)"
then have "infinite B" "infinite C" by auto
{ fix B C assume B: "independent B" and C: "independent C" and "infinite B" "infinite C" and eq: "span B = span C"
let ?R = "representation B" and ?R' = "representation C" let ?U = "\c. {v. ?R c v \ 0}"
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)
have in_span_B [simp, intro]: \<open>c \<in> C \<Longrightarrow> c \<in> span B\<close> for c unfolding eq by (rule span_base)
have \<open>B \<subseteq> (\<Union>c\<in>C. ?U c)\<close>
proof
fix b assume \<open>b \<in> B\<close>
have \<open>b \<in> span C\<close>
using \<open>b \<in> B\<close> unfolding eq[symmetric] by (rule span_base)
have \<open>(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) =
(\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close>
by (simp add: scale_sum_right)
also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s v)\<close>
by (auto simp: sum_nonzero_representation_eq B eq span_base representation_ne_zero)
also have \<open>\<dots> = b\<close>
by (rule sum_nonzero_representation_eq[OF C \<open>b \<in> span C\<close>])
finally have "?R b b = ?R (\v | ?R' b v \ 0. \w | ?R v w \ 0. (?R' b v * ?R v w) *s w) b"
by simp
also have "... = (\i\{v. ?R' b v \ 0}. ?R (\w | ?R i w \ 0. (?R' b i * ?R i w) *s w) b)"
by (subst representation_sum[OF B]) (auto intro: span_sum span_scale span_base representation_ne_zero)
also have "... = (\i\{v. ?R' b v \ 0}.
\<Sum>j \<in> {w. ?R i w \<noteq> 0}. ?R ((?R' b i * ?R i j ) *s j ) b)"
by (subst representation_sum[OF B]) (auto simp add: span_sum span_scale span_base representation_ne_zero)
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>
using B \<open>b \<in> B\<close> by (simp add: representation_scale[OF B] span_base representation_ne_zero)
finally have "(\v | ?R' b v \ 0. \w | ?R v w \ 0. ?R' b v * ?R v w * ?R w b) \ 0"
using representation_basis[OF B \<open>b \<in> B\<close>] by auto
then obtain v w where bv: "?R' b v \ 0" and vw: "?R v w \ 0" and "?R' b v * ?R v w * ?R w b \ 0"
by (blast elim: sum.not_neutral_contains_not_neutral)
with representation_basis[OF B, of w] vw[THEN representation_ne_zero]
have \<open>?R' b v \<noteq> 0\<close> \<open>?R v b \<noteq> 0\<close> by (auto split: if_splits)
then show \<open>b \<in> (\<Union>c\<in>C. ?U c)\<close>
by (auto dest: representation_ne_zero)
qed
then have B_eq: \<open>B = (\<Union>c\<in>C. ?U c)\<close>
by (auto intro: span_base representation_ne_zero eq)
have "ordLeq3 (card_of B) (card_of C)"
proof (subst B_eq, rule card_of_UNION_ordLeq_infinite[OF \<open>infinite C\<close>])
show "ordLeq3 (card_of C) (card_of C)"
by (intro ordLeq_refl card_of_Card_order)
show "\c\C. ordLeq3 (card_of {v. ?R c v \ 0}) (card_of C)"
by (intro ballI ordLeq3_finite_infinite \<open>infinite C\<close> finite_representation)
qed }
from this[of B C] this[of C B] B C eq \<open>infinite C\<close> \<open>infinite B\<close>
show ?thesis by (auto simp add: ordIso_iff_ordLeq card_of_ordIso)
qed
definition dim :: "'b set \ nat"
where "dim V = (if \b. independent b \ span b = span V then
card (SOME b. independent b \<and> span b = span V) else 0)"
lemma dim_eq_card:
assumes BV: "span B = span V" and B: "independent B"
shows "dim V = card B"
proof -
define p where "p b \ independent b \ span b = span V" for b
have "p (SOME B. p B)"
using assms by (intro someI[of p B]) (auto simp: p_def)
then have "\f. bij_betw f B (SOME B. p B)"
by (subst (asm) p_def, intro bij_if_span_eq_span_bases[OF B]) (simp_all add: BV)
then have "card B = card (SOME B. p B)"
by (auto intro: bij_betw_same_card)
then show ?thesis
using BV B
by (auto simp add: dim_def p_def)
qed
lemma basis_card_eq_dim: "B \ V \ V \ span B \ independent B \ card B = dim V"
using dim_eq_card[of B V] span_mono[of B V] span_minimal[OF _ subspace_span, of V B] by auto
lemma basis_exists:
obtains B where "B \ V" "independent B" "V \ span B" "card B = dim V"
by (meson basis_card_eq_dim empty_subsetI independent_empty maximal_independent_subset_extend)
lemma dim_eq_card_independent: "independent B \ dim B = card B"
by (rule dim_eq_card[OF refl])
lemma dim_span[simp]: "dim (span S) = dim S"
by (auto simp add: dim_def span_span)
lemma dim_span_eq_card_independent: "independent B \ dim (span B) = card B"
by (simp add: dim_eq_card)
lemma dim_le_card: assumes "V \ span W" "finite W" shows "dim V \ card W"
proof -
obtain A where "independent A" "A \ V" "V \ span A"
using maximal_independent_subset[of V] by force
with assms independent_span_bound[of W A] basis_card_eq_dim[of A V]
show ?thesis by auto
qed
lemma span_eq_dim: "span S = span T \ dim S = dim T"
by (metis dim_span)
corollary dim_le_card':
"finite s \ dim s \ card s"
by (metis basis_exists card_mono)
lemma span_card_ge_dim:
"B \ V \ V \ span B \ finite B \ dim V \ card B"
by (simp add: dim_le_card)
lemma dim_unique:
"B \ V \ V \ span B \ independent B \ card B = n \ dim V = n"
by (metis basis_card_eq_dim)
lemma subspace_sums: "\subspace S; subspace T\ \ subspace {x + y|x y. x \ S \ y \ T}"
apply (simp add: subspace_def)
apply (intro conjI impI allI; clarsimp simp: algebra_simps)
using add.left_neutral apply blast
apply (metis add.assoc)
using scale_right_distrib by blast
end
lemma linear_iff: "linear s1 s2 f \
(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)))"
unfolding linear_def module_hom_iff vector_space_def module_def by auto
context begin
qualified lemma linear_compose: "linear s1 s2 f \ linear s2 s3 g \ linear s1 s3 (g o f)"
unfolding module_hom_iff_linear[symmetric]
by (rule module_hom_compose)
end
locale vector_space_pair = vs1: vector_space s1 + vs2: vector_space s2
for s1 :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*a" 75)
and s2 :: "'a::field \ 'c::ab_group_add \ 'c" (infixr "*b" 75)
begin
context fixes f assumes "linear s1 s2 f" begin
interpretation linear s1 s2 f by fact
lemmas\<comment> \<open>from locale \<open>module_hom\<close>\<close>
linear_0 = zero
and linear_add = add
and linear_scale = scale
and linear_neg = neg
and linear_diff = diff
and linear_sum = sum
and linear_inj_on_iff_eq_0 = inj_on_iff_eq_0
and linear_inj_iff_eq_0 = inj_iff_eq_0
and linear_subspace_image = subspace_image
and linear_subspace_vimage = subspace_vimage
and linear_subspace_kernel = subspace_kernel
and linear_span_image = span_image
and linear_dependent_inj_imageD = dependent_inj_imageD
and linear_eq_0_on_span = eq_0_on_span
and linear_independent_injective_image = independent_injective_image
and linear_inj_on_span_independent_image = inj_on_span_independent_image
and linear_inj_on_span_iff_independent_image = inj_on_span_iff_independent_image
and linear_subspace_linear_preimage = subspace_linear_preimage
and linear_spans_image = spans_image
and linear_spanning_surjective_image = spanning_surjective_image
end
sublocale module_pair
rewrites "module_hom = linear"
by unfold_locales (fact module_hom_eq_linear)
lemmas\<comment> \<open>from locale \<open>module_pair\<close>\<close>
linear_eq_on_span = module_hom_eq_on_span
and linear_compose_scale_right = module_hom_scale
and linear_compose_add = module_hom_add
and linear_zero = module_hom_zero
and linear_compose_sub = module_hom_sub
and linear_compose_neg = module_hom_neg
and linear_compose_scale = module_hom_compose_scale
lemma linear_indep_image_lemma:
assumes lf: "linear s1 s2 f"
and fB: "finite B"
and ifB: "vs2.independent (f ` B)"
and fi: "inj_on f B"
and xsB: "x \ vs1.span B"
and fx: "f x = 0"
shows "x = 0"
using fB ifB fi xsB fx
proof (induction B arbitrary: x rule: finite_induct)
case empty
then show ?case by auto
next
case (insert a b x)
have th0: "f ` b \ f ` (insert a b)"
by (simp add: subset_insertI)
have ifb: "vs2.independent (f ` b)"
using vs2.independent_mono insert.prems(1) th0 by blast
have fib: "inj_on f b"
using insert.prems(2) by blast
from vs1.span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
obtain k where k: "x - k *a a \ vs1.span (b - {a})"
by blast
have "f (x - k *a a) \ vs2.span (f ` b)"
unfolding linear_span_image[OF lf]
using "insert.hyps"(2) k by auto
then have "f x - k *b f a \ vs2.span (f ` b)"
by (simp add: linear_diff linear_scale lf)
then have th: "-k *b f a \ vs2.span (f ` b)"
using insert.prems(4) by simp
have xsb: "x \ vs1.span b"
proof (cases "k = 0")
case True
with k have "x \ vs1.span (b - {a})" by simp
then show ?thesis using vs1.span_mono[of "b - {a}" b]
by blast
next
case False
from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
then have "f a \ vs2.span (f ` b)"
using vs2.dependent_def insert.hyps(2) insert.prems(1) by fastforce
moreover have "f a \ vs2.span (f ` b)"
using False vs2.span_scale[OF th, of "- 1/ k"] by auto
ultimately have False
by blast
then show ?thesis by blast
qed
show "x = 0"
using ifb fib xsb insert.IH insert.prems(4) by blast
qed
lemma linear_eq_on:
assumes l: "linear s1 s2 f" "linear s1 s2 g"
assumes x: "x \ vs1.span B" and eq: "\b. b \ B \ f b = g b"
shows "f x = g x"
proof -
interpret d: linear s1 s2 "\x. f x - g x"
using l by (intro linear_compose_sub) (auto simp: module_hom_iff_linear)
have "f x - g x = 0"
by (rule d.eq_0_on_span[OF _ x]) (auto simp: eq)
then show ?thesis by auto
qed
definition construct :: "'b set \ ('b \ 'c) \ ('b \ 'c)"
where "construct B g v = (\b | vs1.representation (vs1.extend_basis B) v b \ 0.
vs1.representation (vs1.extend_basis B) v b *b (if b \<in> B then g b else 0))"
lemma construct_cong: "(\b. b \ B \ f b = g b) \ construct B f = construct B g"
unfolding construct_def by (rule ext, auto intro!: sum.cong)
lemma linear_construct:
assumes B[simp]: "vs1.independent B"
shows "linear s1 s2 (construct B f)"
unfolding module_hom_iff_linear linear_iff
proof safe
have eB[simp]: "vs1.independent (vs1.extend_basis B)"
using vs1.independent_extend_basis[OF B] .
let ?R = "vs1.representation (vs1.extend_basis B)"
fix c x y
have "construct B f (x + y) =
(\<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))"
by (auto intro!: sum.mono_neutral_cong_left simp: vs1.finite_representation vs1.representation_add construct_def)
also have "\ = construct B f x + construct B f y"
by (auto simp: construct_def vs1.representation_add vs2.scale_left_distrib sum.distrib
intro!: arg_cong2[where f="(+)"] sum.mono_neutral_cong_right vs1.finite_representation)
finally show "construct B f (x + y) = construct B f x + construct B f y" .
show "construct B f (c *a x) = c *b construct B f x"
by (auto simp del: vs2.scale_scale intro!: sum.mono_neutral_cong_left vs1.finite_representation
simp add: construct_def vs2.scale_scale[symmetric] vs1.representation_scale vs2.scale_sum_right)
qed intro_locales
lemma construct_basis:
assumes B[simp]: "vs1.independent B" and b: "b \ B"
shows "construct B f b = f b"
proof -
have *: "vs1.representation (vs1.extend_basis B) b = (\v. if v = b then 1 else 0)"
using vs1.extend_basis_superset[OF B] b
by (intro vs1.representation_basis vs1.independent_extend_basis) auto
then have "{v. vs1.representation (vs1.extend_basis B) b v \ 0} = {b}"
by auto
then show ?thesis
unfolding construct_def by (simp add: * b)
qed
lemma construct_outside:
assumes B: "vs1.independent B" and v: "v \ vs1.span (vs1.extend_basis B - B)"
shows "construct B f v = 0"
unfolding construct_def
proof (clarsimp intro!: sum.neutral simp del: vs2.scale_eq_0_iff)
fix b assume "b \ B"
then have "vs1.representation (vs1.extend_basis B - B) v b = 0"
using vs1.representation_ne_zero[of "vs1.extend_basis B - B" v b] by auto
moreover have "vs1.representation (vs1.extend_basis B) v = vs1.representation (vs1.extend_basis B - B) v"
using vs1.representation_extend[OF vs1.independent_extend_basis[OF B] v] by auto
ultimately show "vs1.representation (vs1.extend_basis B) v b *b f b = 0"
by simp
qed
lemma construct_add:
assumes B[simp]: "vs1.independent B"
shows "construct B (\x. f x + g x) v = construct B f v + construct B g v"
proof (rule linear_eq_on)
show "v \ vs1.span (vs1.extend_basis B)" by simp
show "b \ vs1.extend_basis B \ construct B (\x. f x + g x) b = construct B f b + construct B g b" for b
using construct_outside[OF B vs1.span_base, of b] by (cases "b \ B") (auto simp: construct_basis)
qed (intro linear_compose_add linear_construct B)+
lemma construct_scale:
assumes B[simp]: "vs1.independent B"
shows "construct B (\x. c *b f x) v = c *b construct B f v"
proof (rule linear_eq_on)
show "v \ vs1.span (vs1.extend_basis B)" by simp
show "b \ vs1.extend_basis B \ construct B (\x. c *b f x) b = c *b construct B f b" for b
using construct_outside[OF B vs1.span_base, of b] by (cases "b \ B") (auto simp: construct_basis)
qed (intro linear_construct module_hom_scale B)+
lemma construct_in_span:
assumes B[simp]: "vs1.independent B"
shows "construct B f v \ vs2.span (f ` B)"
proof -
interpret c: linear s1 s2 "construct B f" by (rule linear_construct) fact
let ?R = "vs1.representation B"
have "v \ vs1.span ((vs1.extend_basis B - B) \ B)"
by (auto simp: Un_absorb2 vs1.extend_basis_superset)
then obtain x y where "v = x + y" "x \ vs1.span (vs1.extend_basis B - B)" "y \ vs1.span B"
unfolding vs1.span_Un by auto
moreover have "construct B f (\b | ?R y b \ 0. ?R y b *a b) \ vs2.span (f ` B)"
by (auto simp add: c.sum c.scale construct_basis vs1.representation_ne_zero
intro!: vs2.span_sum vs2.span_scale intro: vs2.span_base )
ultimately show "construct B f v \ vs2.span (f ` B)"
by (auto simp add: c.add construct_outside vs1.sum_nonzero_representation_eq)
qed
lemma linear_compose_sum:
assumes lS: "\a \ S. linear s1 s2 (f a)"
shows "linear s1 s2 (\x. sum (\a. f a x) S)"
proof (cases "finite S")
case True
then show ?thesis
using lS by induct (simp_all add: linear_zero linear_compose_add)
next
case False
then show ?thesis
by (simp add: linear_zero)
qed
lemma in_span_in_range_construct:
"x \ range (construct B f)" if i: "vs1.independent B" and x: "x \ vs2.span (f ` B)"
proof -
interpret linear "(*a)" "(*b)" "construct B f"
using i by (rule linear_construct)
obtain bb :: "('b \ 'c) \ ('b \ 'c) \ 'b set \ 'b" where
"\x0 x1 x2. (\v4. v4 \ x2 \ x1 v4 \ x0 v4) = (bb x0 x1 x2 \ x2 \ x1 (bb x0 x1 x2) \ x0 (bb x0 x1 x2))"
by moura
then have f2: "\B Ba f fa. (B \ Ba \ bb fa f Ba \ Ba \ f (bb fa f Ba) \ fa (bb fa f Ba)) \ f ` B = fa ` Ba"
by (meson image_cong)
have "vs1.span B \ vs1.span (vs1.extend_basis B)"
by (simp add: vs1.extend_basis_superset[OF i] vs1.span_mono)
then show "x \ range (construct B f)"
using f2 x by (metis (no_types) construct_basis[OF i, of _ f]
vs1.span_extend_basis[OF i] subsetD span_image spans_image)
qed
lemma range_construct_eq_span:
"range (construct B f) = vs2.span (f ` B)"
if "vs1.independent B"
by (auto simp: that construct_in_span in_span_in_range_construct)
lemma linear_independent_extend_subspace:
\<comment> \<open>legacy: use \<^term>\<open>construct\<close> instead\<close>
assumes "vs1.independent B"
shows "\g. linear s1 s2 g \ (\x\B. g x = f x) \ range g = vs2.span (f`B)"
by (rule exI[where x="construct B f"])
(auto simp: linear_construct assms construct_basis range_construct_eq_span)
lemma linear_independent_extend:
"vs1.independent B \ \g. linear s1 s2 g \ (\x\B. g x = f x)"
using linear_independent_extend_subspace[of B f] by auto
lemma linear_exists_left_inverse_on:
assumes lf: "linear s1 s2 f"
assumes V: "vs1.subspace V" and f: "inj_on f V"
shows "\g. g ` UNIV \ V \ linear s2 s1 g \ (\v\V. g (f v) = v)"
proof -
interpret linear s1 s2 f by fact
obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
by (metis antisym_conv)
have f: "inj_on f (vs1.span B)"
using f unfolding V_eq .
show ?thesis
proof (intro exI ballI conjI)
interpret p: vector_space_pair s2 s1 by unfold_locales
have fB: "vs2.independent (f ` B)"
using independent_injective_image[OF B f] .
let ?g = "p.construct (f ` B) (the_inv_into B f)"
show "linear (*b) (*a) ?g"
by (rule p.linear_construct[OF fB])
have "?g b \ vs1.span (the_inv_into B f ` f ` B)" for b
by (intro p.construct_in_span fB)
moreover have "the_inv_into B f ` f ` B = B"
by (auto simp: image_comp comp_def the_inv_into_f_f inj_on_subset[OF f vs1.span_superset]
cong: image_cong)
ultimately show "?g ` UNIV \ V"
by (auto simp: V_eq)
have "(?g \ f) v = id v" if "v \ vs1.span B" for v
proof (rule vector_space_pair.linear_eq_on[where x=v])
show "vector_space_pair (*a) (*a)" by unfold_locales
show "linear (*a) (*a) (?g \ f)"
proof (rule Vector_Spaces.linear_compose[of _ "(*b)"])
show "linear (*a) (*b) f"
by unfold_locales
qed fact
show "linear (*a) (*a) id" by (rule vs1.linear_id)
show "v \ vs1.span B" by fact
show "b \ B \ (p.construct (f ` B) (the_inv_into B f) \ f) b = id b" for b
by (simp add: p.construct_basis fB the_inv_into_f_f inj_on_subset[OF f vs1.span_superset])
qed
then show "v \ V \ ?g (f v) = v" for v by (auto simp: comp_def id_def V_eq)
qed
qed
lemma linear_exists_right_inverse_on:
assumes lf: "linear s1 s2 f"
assumes "vs1.subspace V"
shows "\g. g ` UNIV \ V \ linear s2 s1 g \ (\v\f ` V. f (g v) = v)"
proof -
obtain B where V_eq: "V = vs1.span B" and B: "vs1.independent B"
using vs1.maximal_independent_subset[of V] vs1.span_minimal[OF _ \<open>vs1.subspace V\<close>]
by (metis antisym_conv)
obtain C where C: "vs2.independent C" and fB_C: "f ` B \ vs2.span C" "C \ f ` B"
using vs2.maximal_independent_subset[of "f ` B"] by metis
then have "\v\C. \b\B. v = f b" by auto
then obtain g where g: "\v. v \ C \ g v \ B" "\v. v \ C \ f (g v) = v" by metis
show ?thesis
proof (intro exI ballI conjI)
interpret p: vector_space_pair s2 s1 by unfold_locales
let ?g = "p.construct C g"
show "linear (*b) (*a) ?g"
by (rule p.linear_construct[OF C])
have "?g v \ vs1.span (g ` C)" for v
by (rule p.construct_in_span[OF C])
also have "\ \ V" unfolding V_eq using g by (intro vs1.span_mono) auto
finally show "?g ` UNIV \ V" by auto
have "(f \ ?g) v = id v" if v: "v \ f ` V" for v
proof (rule vector_space_pair.linear_eq_on[where x=v])
show "vector_space_pair (*b) (*b)" by unfold_locales
show "linear (*b) (*b) (f \ ?g)"
by (rule Vector_Spaces.linear_compose[of _ "(*a)"]) fact+
show "linear (*b) (*b) id" by (rule vs2.linear_id)
have "vs2.span (f ` B) = vs2.span C"
using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
by auto
then show "v \ vs2.span C"
using v linear_span_image[OF lf, of B] by (simp add: V_eq)
show "(f \ p.construct C g) b = id b" if b: "b \ C" for b
by (auto simp: p.construct_basis g C b)
qed
then show "v \ f ` V \ f (?g v) = v" for v by (auto simp: comp_def id_def)
qed
qed
lemma linear_inj_on_left_inverse:
assumes lf: "linear s1 s2 f"
assumes fi: "inj_on f (vs1.span S)"
shows "\g. range g \ vs1.span S \ linear s2 s1 g \ (\x\vs1.span S. g (f x) = x)"
using linear_exists_left_inverse_on[OF lf vs1.subspace_span fi]
by (auto simp: linear_iff_module_hom)
lemma linear_injective_left_inverse: "linear s1 s2 f \ inj f \ \g. linear s2 s1 g \ g \ f = id"
using linear_inj_on_left_inverse[of f UNIV]
by force
lemma linear_surj_right_inverse:
assumes lf: "linear s1 s2 f"
assumes sf: "vs2.span T \ f`vs1.span S"
shows "\g. range g \ vs1.span S \ linear s2 s1 g \ (\x\vs2.span T. f (g x) = x)"
using linear_exists_right_inverse_on[OF lf vs1.subspace_span, of S] sf
by (force simp: linear_iff_module_hom)
lemma linear_surjective_right_inverse: "linear s1 s2 f \ surj f \ \g. linear s2 s1 g \ f \ g = id"
using linear_surj_right_inverse[of f UNIV UNIV]
by (auto simp: fun_eq_iff)
lemma finite_basis_to_basis_subspace_isomorphism:
assumes s: "vs1.subspace S"
and t: "vs2.subspace T"
and d: "vs1.dim S = vs2.dim T"
and fB: "finite B"
and B: "B \ S" "vs1.independent B" "S \ vs1.span B" "card B = vs1.dim S"
and fC: "finite C"
and C: "C \ T" "vs2.independent C" "T \ vs2.span C" "card C = vs2.dim T"
shows "\f. linear s1 s2 f \ f ` B = C \ f ` S = T \ inj_on f S"
proof -
from B(4) C(4) card_le_inj[of B C] d obtain f where
f: "f ` B \ C" "inj_on f B" using \finite B\ \finite C\ by auto
from linear_independent_extend[OF B(2)] obtain g where
g: "linear s1 s2 g" "\x \ B. g x = f x" by blast
interpret g: linear s1 s2 g by fact
from inj_on_iff_eq_card[OF fB, of f] f(2)
have "card (f ` B) = card B" by simp
with B(4) C(4) have ceq: "card (f ` B) = card C" using d
by simp
have "g ` B = f ` B" using g(2)
by (auto simp add: image_iff)
also have "\ = C" using card_subset_eq[OF fC f(1) ceq] .
finally have gBC: "g ` B = C" .
have gi: "inj_on g B" using f(2) g(2)
by (auto simp add: inj_on_def)
note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
{
fix x y
assume x: "x \ S" and y: "y \ S" and gxy: "g x = g y"
from B(3) x y have x': "x \ vs1.span B" and y': "y \ vs1.span B"
by blast+
from gxy have th0: "g (x - y) = 0"
by (simp add: g.diff)
have th1: "x - y \ vs1.span B" using x' y'
by (metis vs1.span_diff)
have "x = y" using g0[OF th1 th0] by simp
}
then have giS: "inj_on g S" unfolding inj_on_def by blast
from vs1.span_subspace[OF B(1,3) s]
have "g ` S = vs2.span (g ` B)"
by (simp add: g.span_image)
also have "\ = vs2.span C"
unfolding gBC ..
also have "\ = T"
using vs2.span_subspace[OF C(1,3) t] .
finally have gS: "g ` S = T" .
from g(1) gS giS gBC show ?thesis
by blast
qed
end
locale finite_dimensional_vector_space = vector_space +
fixes Basis :: "'b set"
assumes finite_Basis: "finite Basis"
and independent_Basis: "independent Basis"
and span_Basis: "span Basis = UNIV"
begin
definition "dimension = card Basis"
lemma finiteI_independent: "independent B \ finite B"
using independent_span_bound[OF finite_Basis, of B] by (auto simp: span_Basis)
lemma dim_empty [simp]: "dim {} = 0"
by (rule dim_unique[OF order_refl]) (auto simp: dependent_def)
lemma dim_insert:
"dim (insert x S) = (if x \ span S then dim S else dim S + 1)"
proof -
show ?thesis
proof (cases "x \ span S")
case True then show ?thesis
by (metis dim_span span_redundant)
next
case False
obtain B where B: "B \ span S" "independent B" "span S \ span B" "card B = dim (span S)"
using basis_exists [of "span S"] by blast
have "dim (span (insert x S)) = Suc (dim S)"
proof (rule dim_unique)
show "insert x B \ span (insert x S)"
by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI)
show "span (insert x S) \ span (insert x B)"
by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
show "independent (insert x B)"
by (metis B(1-3) independent_insert span_subspace subspace_span False)
show "card (insert x B) = Suc (dim S)"
using B False finiteI_independent by force
qed
then show ?thesis
by (metis False Suc_eq_plus1 dim_span)
qed
qed
lemma dim_singleton [simp]: "dim{x} = (if x = 0 then 0 else 1)"
by (simp add: dim_insert)
proposition choose_subspace_of_subspace:
assumes "n \ dim S"
obtains T where "subspace T" "T \ span S" "dim T = n"
proof -
have "\T. subspace T \ T \ span S \ dim T = n"
using assms
proof (induction n)
case 0 then show ?case by (auto intro!: exI[where x="{0}"] span_zero)
next
case (Suc n)
then obtain T where "subspace T" "T \ span S" "dim T = n"
by force
then show ?case
proof (cases "span S \ span T")
case True
have "span T \ span S"
by (simp add: \<open>T \<subseteq> span S\<close> span_minimal)
then have "dim S = dim T"
by (rule span_eq_dim [OF subset_antisym [OF True]])
then show ?thesis
using Suc.prems \<open>dim T = n\<close> by linarith
next
case False
then obtain y where y: "y \ S" "y \ T"
by (meson span_mono subsetI)
then have "span (insert y T) \ span S"
by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span)
with \<open>dim T = n\<close> \<open>subspace T\<close> y show ?thesis
apply (rule_tac x="span(insert y T)" in exI)
using span_eq_iff by (fastforce simp: dim_insert)
qed
qed
with that show ?thesis by blast
qed
lemma basis_subspace_exists:
assumes "subspace S"
obtains B where "finite B" "B \ S" "independent B" "span B = S" "card B = dim S"
by (metis assms span_subspace basis_exists finiteI_independent)
lemma dim_mono: assumes "V \ span W" shows "dim V \ dim W"
proof -
obtain B where "independent B" "B \ W" "W \ span B"
using maximal_independent_subset[of W] by force
with dim_le_card[of V B] assms independent_span_bound[of Basis B] basis_card_eq_dim[of B W]
span_mono[of B W] span_minimal[OF _ subspace_span, of W B]
show ?thesis
by (auto simp: finite_Basis span_Basis)
qed
lemma dim_subset: "S \ T \ dim S \ dim T"
using dim_mono[of S T] by (auto intro: span_base)
lemma dim_eq_0 [simp]:
"dim S = 0 \ S \ {0}"
by (metis basis_exists card_eq_0_iff dim_span finiteI_independent span_empty subset_empty subset_singletonD)
lemma dim_UNIV[simp]: "dim UNIV = card Basis"
using dim_eq_card[of Basis UNIV] by (simp add: independent_Basis span_Basis)
lemma independent_card_le_dim: assumes "B \ V" and "independent B" shows "card B \ dim V"
by (subst dim_eq_card[symmetric, OF refl \<open>independent B\<close>]) (rule dim_subset[OF \<open>B \<subseteq> V\<close>])
lemma dim_subset_UNIV: "dim S \ dimension"
by (metis dim_subset subset_UNIV dim_UNIV dimension_def)
lemma card_ge_dim_independent:
assumes BV: "B \ V"
and iB: "independent B"
and dVB: "dim V \ card B"
shows "V \ span B"
proof
fix a
assume aV: "a \ V"
{
assume aB: "a \ span B"
then have iaB: "independent (insert a B)"
using iB aV BV by (simp add: independent_insert)
from aV BV have th0: "insert a B \ V"
by blast
from aB have "a \B"
by (auto simp add: span_base)
with independent_card_le_dim[OF th0 iaB] dVB finiteI_independent[OF iB]
have False by auto
}
then show "a \ span B" by blast
qed
lemma card_le_dim_spanning:
assumes BV: "B \ V"
and VB: "V \ span B"
and fB: "finite B"
and dVB: "dim V \ card B"
shows "independent B"
proof -
{
fix a
assume a: "a \ B" "a \ span (B - {a})"
from a fB have c0: "card B \ 0"
by auto
from a fB have cb: "card (B - {a}) = card B - 1"
by auto
{
fix x
assume x: "x \ V"
from a have eq: "insert a (B - {a}) = B"
by blast
from x VB have x': "x \ span B"
by blast
from span_trans[OF a(2), unfolded eq, OF x']
have "x \ span (B - {a})" .
}
then have th1: "V \ span (B - {a})"
by blast
have th2: "finite (B - {a})"
using fB by auto
from dim_le_card[OF th1 th2]
have c: "dim V \ card (B - {a})" .
from c c0 dVB cb have False by simp
}
then show ?thesis
unfolding dependent_def by blast
qed
lemma card_eq_dim: "B \ V \ card B = dim V \ finite B \ independent B \ V \ span B"
by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent)
lemma subspace_dim_equal:
assumes "subspace S"
and "subspace T"
and "S \ T"
and "dim S \ dim T"
shows "S = T"
proof -
obtain B where B: "B \ S" "independent B \ S \ span B" "card B = dim S"
using basis_exists[of S] by metis
then have "span B \ S"
using span_mono[of B S] span_eq_iff[of S] assms by metis
then have "span B = S"
using B by auto
have "dim S = dim T"
using assms dim_subset[of S T] by auto
then have "T \ span B"
using card_eq_dim[of B T] B finiteI_independent assms by auto
then show ?thesis
using assms \<open>span B = S\<close> by auto
qed
corollary dim_eq_span:
shows "\S \ T; dim T \ dim S\ \ span S = span T"
by (simp add: span_mono subspace_dim_equal)
lemma dim_psubset:
"span S \ span T \ dim S < dim T"
by (metis (no_types, hide_lams) dim_span less_le not_le subspace_dim_equal subspace_span)
lemma dim_eq_full:
shows "dim S = dimension \ span S = UNIV"
by (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV
dim_UNIV dim_span dimension_def)
lemma indep_card_eq_dim_span:
assumes "independent B"
shows "finite B \ card B = dim (span B)"
using dim_span_eq_card_independent[OF assms] finiteI_independent[OF assms] by auto
text \<open>More general size bound lemmas.\<close>
lemma independent_bound_general:
"independent S \ finite S \ card S \ dim S"
by (simp add: dim_eq_card_independent finiteI_independent)
lemma independent_explicit:
shows "independent B \ finite B \ (\c. (\v\B. c v *s v) = 0 \ (\v \ B. c v = 0))"
using independent_bound_general
by (fastforce simp: dependent_finite)
proposition dim_sums_Int:
assumes "subspace S" "subspace T"
shows "dim {x + y |x y. x \ S \ y \ T} + dim(S \ T) = dim S + dim T" (is "dim ?ST + _ = _")
proof -
obtain B where B: "B \ S \ T" "S \ T \ span B"
and indB: "independent B"
and cardB: "card B = dim (S \ T)"
using basis_exists by metis
then obtain C D where "B \ C" "C \ S" "independent C" "S \ span C"
and "B \ D" "D \ T" "independent D" "T \ span D"
using maximal_independent_subset_extend
by (metis Int_subset_iff \<open>B \<subseteq> S \<inter> T\<close> indB)
then have "finite B" "finite C" "finite D"
by (simp_all add: finiteI_independent indB independent_bound_general)
have Beq: "B = C \ D"
proof (rule spanning_subset_independent [symmetric])
show "independent (C \ D)"
by (meson \<open>independent C\<close> independent_mono inf.cobounded1)
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)
then have Deq: "D = B \ (D - C)"
by blast
have CUD: "C \ D \ ?ST"
proof (simp, intro conjI)
show "C \ ?ST"
using span_zero span_minimal [OF _ \<open>subspace T\<close>] \<open>C \<subseteq> S\<close> by force
show "D \ ?ST"
using span_zero span_minimal [OF _ \<open>subspace S\<close>] \<open>D \<subseteq> T\<close> by force
qed
have "a v = 0" if 0: "(\v\C. a v *s v) + (\v\D - C. a v *s v) = 0"
and v: "v \ C \ (D-C)" for a v
proof -
have CsS: "\x. x \ C \ a x *s x \ S"
using \<open>C \<subseteq> S\<close> \<open>subspace S\<close> subspace_scale by auto
have eq: "(\v\D - C. a v *s v) = - (\v\C. a v *s v)"
using that add_eq_0_iff by blast
have "(\v\D - C. a v *s v) \ S"
by (simp add: eq CsS \<open>subspace S\<close> subspace_neg subspace_sum)
moreover have "(\v\D - C. a v *s v) \ T"
apply (rule subspace_sum [OF \<open>subspace T\<close>])
by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
ultimately have "(\v \ D-C. a v *s v) \ span B"
using B by blast
then obtain e where e: "(\v\B. e v *s v) = (\v \ D-C. a v *s v)"
using span_finite [OF \<open>finite B\<close>] by force
have "\c v. \(\v\C. c v *s v) = 0; v \ C\ \ c v = 0"
using \<open>finite C\<close> \<open>independent C\<close> independentD by blast
define cc where "cc x = (if x \ B then a x + e x else a x)" for x
have [simp]: "C \ B = B" "D \ B = B" "C \ - B = C-D" "B \ (D - C) = {}"
using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> Beq by blast+
have f2: "(\v\C \ D. e v *s v) = (\v\D - C. a v *s v)"
using Beq e by presburger
have f3: "(\v\C \ D. a v *s v) = (\v\C - D. a v *s v) + (\v\D - C. a v *s v) + (\v\C \ D. a v *s v)"
using \<open>finite C\<close> \<open>finite D\<close> sum.union_diff2 by blast
have f4: "(\v\C \ (D - C). a v *s v) = (\v\C. a v *s v) + (\v\D - C. a v *s v)"
by (meson Diff_disjoint \<open>finite C\<close> \<open>finite D\<close> finite_Diff sum.union_disjoint)
have "(\v\C. cc v *s v) = 0"
using 0 f2 f3 f4
apply (simp add: cc_def Beq \<open>finite C\<close> sum.If_cases algebra_simps sum.distrib
if_distrib if_distribR)
apply (simp add: add.commute add.left_commute diff_eq)
done
then have "\v. v \ C \ cc v = 0"
using independent_explicit \<open>independent C\<close> \<open>finite C\<close> by blast
then have C0: "\v. v \ C - B \ a v = 0"
by (simp add: cc_def Beq) meson
then have [simp]: "(\x\C - B. a x *s x) = 0"
by simp
have "(\x\C. a x *s x) = (\x\B. a x *s x)"
proof -
have "C - D = C - B"
using Beq by blast
then show ?thesis
using Beq \<open>(\<Sum>x\<in>C - B. a x *s x) = 0\<close> f3 f4 by auto
qed
with 0 have Dcc0: "(\v\D. a v *s v) = 0"
by (subst Deq) (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un)
then have D0: "\v. v \ D \ a v = 0"
using independent_explicit \<open>independent D\<close> \<open>finite D\<close> by blast
show ?thesis
using v C0 D0 Beq by blast
qed
then have "independent (C \ (D - C))"
unfolding independent_explicit
using independent_explicit
by (simp add: independent_explicit \<open>finite C\<close> \<open>finite D\<close> sum_Un del: Un_Diff_cancel)
then have indCUD: "independent (C \ D)" by simp
have "dim (S \ T) = card B"
by (rule dim_unique [OF B indB refl])
moreover have "dim S = card C"
by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
moreover have "dim T = card D"
by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
moreover have "dim ?ST = card(C \ D)"
proof -
have *: "\x y. \x \ S; y \ T\ \ x + y \ span (C \ D)"
by (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_mono subsetCE sup.cobounded1 sup.cobounded2)
show ?thesis
by (auto intro: * dim_unique [OF CUD _ indCUD refl])
qed
ultimately show ?thesis
using \<open>B = C \<inter> D\<close> [symmetric]
by (simp add: \<open>independent C\<close> \<open>independent D\<close> card_Un_Int finiteI_independent)
qed
lemma dependent_biggerset_general:
"(finite S \ card S > dim S) \ dependent S"
using independent_bound_general[of S] by (metis linorder_not_le)
lemma subset_le_dim:
"S \ span T \ dim S \ dim T"
by (metis dim_span dim_subset)
lemma linear_inj_imp_surj:
assumes lf: "linear scale scale f"
and fi: "inj f"
shows "surj f"
proof -
interpret lf: linear scale scale f by fact
from basis_exists[of UNIV] obtain B
where B: "B \ UNIV" "independent B" "UNIV \ span B" "card B = dim UNIV"
by blast
from B(4) have d: "dim UNIV = card B"
by simp
have "UNIV \ span (f ` B)"
proof (rule card_ge_dim_independent)
show "independent (f ` B)"
by (simp add: B(2) fi lf.independent_inj_image)
have "card (f ` B) = dim UNIV"
by (metis B(1) card_image d fi inj_on_subset)
then show "dim UNIV \ card (f ` B)"
by simp
qed blast
then show ?thesis
unfolding lf.span_image surj_def
using B(3) by blast
qed
end
locale finite_dimensional_vector_space_pair_1 =
vs1: finite_dimensional_vector_space s1 B1 + vs2: vector_space s2
for s1 :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*a" 75)
and B1 :: "'b set"
and s2 :: "'a::field \ 'c::ab_group_add \ 'c" (infixr "*b" 75)
begin
sublocale vector_space_pair s1 s2 by unfold_locales
lemma dim_image_eq:
assumes lf: "linear s1 s2 f"
and fi: "inj_on f (vs1.span S)"
shows "vs2.dim (f ` S) = vs1.dim S"
proof -
interpret lf: linear by fact
obtain B where B: "B \ S" "vs1.independent B" "S \ vs1.span B" "card B = vs1.dim S"
using vs1.basis_exists[of S] by auto
then have "vs1.span S = vs1.span B"
using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
moreover have "card (f ` B) = card B"
using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
moreover have "(f ` B) \ (f ` S)"
using B by auto
ultimately show ?thesis
by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span)
qed
lemma dim_image_le:
assumes lf: "linear s1 s2 f"
shows "vs2.dim (f ` S) \ vs1.dim (S)"
proof -
from vs1.basis_exists[of S] obtain B where
B: "B \ S" "vs1.independent B" "S \ vs1.span B" "card B = vs1.dim S" by blast
from B have fB: "finite B" "card B = vs1.dim S"
using vs1.independent_bound_general by blast+
have "vs2.dim (f ` S) \ card (f ` B)"
apply (rule vs2.span_card_ge_dim)
using lf B fB
apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff
linear_iff_module_hom)
done
also have "\ \ vs1.dim S"
using card_image_le[OF fB(1)] fB by simp
finally show ?thesis .
qed
end
locale finite_dimensional_vector_space_pair =
vs1: finite_dimensional_vector_space s1 B1 + vs2: finite_dimensional_vector_space s2 B2
for s1 :: "'a::field \ 'b::ab_group_add \ 'b" (infixr "*a" 75)
and B1 :: "'b set"
and s2 :: "'a::field \ 'c::ab_group_add \ 'c" (infixr "*b" 75)
and B2 :: "'c set"
begin
sublocale finite_dimensional_vector_space_pair_1 ..
lemma linear_surjective_imp_injective:
assumes lf: "linear s1 s2 f" and sf: "surj f" and eq: "vs2.dim UNIV = vs1.dim UNIV"
shows "inj f"
proof -
interpret linear s1 s2 f by fact
have *: "card (f ` B1) \ vs2.dim UNIV"
using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf
by (auto simp: vs1.span_Basis vs1.independent_Basis eq
simp del: vs2.dim_UNIV
intro!: card_image_le)
have indep_fB: "vs2.independent (f ` B1)"
using vs1.finite_Basis vs1.dim_eq_card[of B1 UNIV] sf *
by (intro vs2.card_le_dim_spanning[of "f ` B1" UNIV]) (auto simp: span_image vs1.span_Basis )
have "vs2.dim UNIV \ card (f ` B1)"
unfolding eq sf[symmetric] vs2.dim_span_eq_card_independent[symmetric, OF indep_fB]
vs2.dim_span
by (intro vs2.dim_mono) (auto simp: span_image vs1.span_Basis)
with * have "card (f ` B1) = vs2.dim UNIV" by auto
also have "... = card B1"
unfolding eq vs1.dim_UNIV ..
finally have "inj_on f B1"
by (subst inj_on_iff_eq_card[OF vs1.finite_Basis])
then show "inj f"
using inj_on_span_iff_independent_image[OF indep_fB] vs1.span_Basis by auto
qed
lemma linear_injective_imp_surjective:
assumes lf: "linear s1 s2 f" and sf: "inj f" and eq: "vs2.dim UNIV = vs1.dim UNIV"
shows "surj f"
proof -
interpret linear s1 s2 f by fact
have *: False if b: "b \ vs2.span (f ` B1)" for b
proof -
have *: "vs2.independent (f ` B1)"
using vs1.independent_Basis by (intro independent_injective_image inj_on_subset[OF sf]) auto
have **: "vs2.independent (insert b (f ` B1))"
using b * by (rule vs2.independent_insertI)
have "b \ f ` B1" using vs2.span_base[of b "f ` B1"] b by auto
then have "Suc (card B1) = card (insert b (f ` B1))"
using sf[THEN inj_on_subset, of B1] by (subst card.insert_remove) (auto intro: vs1.finite_Basis simp: card_image)
also have "\ = vs2.dim (insert b (f ` B1))"
using vs2.dim_eq_card_independent[OF **] by simp
also have "vs2.dim (insert b (f ` B1)) \ vs2.dim B2"
by (rule vs2.dim_mono) (auto simp: vs2.span_Basis)
also have "\ = card B1"
using vs1.dim_span[of B1] vs2.dim_span[of B2] unfolding vs1.span_Basis vs2.span_Basis eq
vs1.dim_eq_card_independent[OF vs1.independent_Basis] by simp
finally show False by simp
qed
have "f ` UNIV = f ` vs1.span B1" unfolding vs1.span_Basis ..
also have "\ = vs2.span (f ` B1)" unfolding span_image ..
also have "\ = UNIV" using * by blast
finally show ?thesis .
qed
lemma linear_injective_isomorphism:
assumes lf: "linear s1 s2 f"
and fi: "inj f"
and dims: "vs2.dim UNIV = vs1.dim UNIV"
shows "\f'. linear s2 s1 f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)"
unfolding isomorphism_expand[symmetric]
using linear_injective_imp_surjective[OF lf fi dims]
using fi left_right_inverse_eq lf linear_injective_left_inverse linear_surjective_right_inverse by blast
lemma linear_surjective_isomorphism:
assumes lf: "linear s1 s2 f"
and sf: "surj f"
and dims: "vs2.dim UNIV = vs1.dim UNIV"
shows "\f'. linear s2 s1 f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)"
using linear_surjective_imp_injective[OF lf sf dims] sf
linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
dims lf linear_injective_isomorphism by auto
lemma basis_to_basis_subspace_isomorphism:
assumes s: "vs1.subspace S"
and t: "vs2.subspace T"
and d: "vs1.dim S = vs2.dim T"
and B: "B \ S" "vs1.independent B" "S \ vs1.span B" "card B = vs1.dim S"
and C: "C \ T" "vs2.independent C" "T \ vs2.span C" "card C = vs2.dim T"
shows "\f. linear s1 s2 f \ f ` B = C \ f ` S = T \ inj_on f S"
proof -
from B have fB: "finite B"
by (simp add: vs1.finiteI_independent)
from C have fC: "finite C"
by (simp add: vs2.finiteI_independent)
from finite_basis_to_basis_subspace_isomorphism[OF s t d fB B fC C] show ?thesis .
qed
end
context finite_dimensional_vector_space begin
lemma linear_surj_imp_inj:
assumes lf: "linear scale scale f" and sf: "surj f"
shows "inj f"
proof -
interpret finite_dimensional_vector_space_pair scale Basis scale Basis by unfold_locales
let ?U = "UNIV :: 'b set"
from basis_exists[of ?U] obtain B
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.36 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
