Quelle Vector_Spaces.thy Sprache: Isabelle

(*  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_representation:
  assumes "independent B" "span B = UNIV"
  shows   "linear scale (*) (\v. representation B v b)"
proof (unfold_locales, goal_cases)
  case (5 x y)
  show ?case
    using assms by (subst representation_add) auto
next
  case (6 r x)
  show ?case
    using assms by (subst representation_scale) auto
qed (simp_all add: algebra_simps)

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 (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, opaque_lifting) 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] inj_on_subset[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)
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.