section ‹Dimension of Spans› text ‹We define the notion of dimension of a span of vectors and prove some natural results about them. The definition is made as a function, so that no interpretation of locales like subspace is required.› theory Dim_Span imports Missing_VS_Connect begin context vec_space begin definition "dim_span W = Max (card ` {V. V ⊆ carrier_vec n ∧ V ⊆ span W ∧ lin_indpt V})" lemma fixes V W :: "'a vec set" shows card_le_dim_span: "V ⊆ carrier_vec n ⟹ V ⊆ span W ⟹ lin_indpt V ⟹ card V ≤ dim_span W" and card_eq_dim_span_imp_same_span: "W ⊆ carrier_vec n ⟹ V ⊆ span W ⟹ lin_indpt V ⟹ card V = dim_span W ⟹ span V = span W" and same_span_imp_card_eq_dim_span: "V ⊆ carrier_vec n ⟹ W ⊆ carrier_vec n ⟹ span V = span W ⟹ lin_indpt V ⟹ card V = dim_span W" and dim_span_cong: "span V = span W ⟹ dim_span V = dim_span W" and ex_basis_span: "V ⊆ carrier_vec n ⟹ ∃ W. W ⊆ carrier_vec n ∧ lin_indpt W ∧ span V = span W ∧ dim_span V = card W" proof - show cong: "⋀ V W. span V = span W ⟹ dim_span V = dim_span W" unfolding dim_span_def by auto { fix W :: "'a vec set" let ?M = "{V. V ⊆ carrier_vec n ∧ V ⊆ span W ∧ lin_indpt V}" have "card ` ?M ⊆ {0 .. n}" proof fix k assume "k ∈ card ` ?M" then obtain V where V: "V ⊆ carrier_vec n ∧ V ⊆ span W ∧ lin_indpt V" and k: "k = card V" by auto from V have "card V ≤ n" using dim_is_n li_le_dim by auto with k show "k ∈ {0 .. n}" by auto qed from finite_subset[OF this] have fin: "finite (card ` ?M)" by auto have "{} ∈ ?M" by (auto simp: span_empty span_zero) from imageI[OF this, of card] have "0 ∈ card ` ?M" by auto hence Mempty: "card ` ?M ≠ {}" by auto from Max_ge[OF fin, folded dim_span_def] show "⋀ V :: 'a vec set. V ⊆ carrier_vec n ⟹ V ⊆ span W ⟹ lin_indpt V ⟹ card V ≤ dim_span W" by auto note this fin Mempty } note part1 = this { fix V W :: "'a vec set" assume W: "W ⊆ carrier_vec n" and VsW: "V ⊆ span W" and linV: "lin_indpt V" and card: "card V = dim_span W" from W VsW have V: "V ⊆ carrier_vec n" using span_mem[OF W] by auto from Max_in[OF part1(2,3), folded dim_span_def, of W] obtain WW where WW: "WW ⊆ carrier_vec n" "WW ⊆ span W" "lin_indpt WW" and id: "dim_span W = card WW" by auto show "span V = span W" proof (rule ccontr) from VsW V W have sub: "span V ⊆ span W" using span_subsetI by metis assume "span V ≠ span W" with sub obtain w where wW: "w ∈ span W" and wsV: "w ∉ span V" by auto from wW W have w: "w ∈ carrier_vec n" by auto from linV V have finV: "finite V" using fin_dim fin_dim_li_fin by blast from wsV span_mem[OF V, of w] have wV: "w ∉ V" by auto let ?X = "insert w V" have "card ?X = Suc (card V)" using wV finV by simp hence gt: "card ?X > dim_span W" unfolding card by simp have linX: "lin_indpt ?X" using lin_dep_iff_in_span[OF V linV w wV] wsV by auto have XW: "?X ⊆ span W" using wW VsW by auto from part1(1)[OF _ XW linX] w V have "card ?X ≤ dim_span W" by auto with gt show False by auto qed } note card_dim_span = this { fix V :: "'a vec set" assume V: "V ⊆ carrier_vec n" from Max_in[OF part1(2,3), folded dim_span_def, of V] obtain W where W: "W ⊆ carrier_vec n" "W ⊆ span V" "lin_indpt W" and idW: "card W = dim_span V" by auto show "∃ W. W ⊆ carrier_vec n ∧ lin_indpt W ∧ span V = span W ∧ dim_span V = card W" proof (intro exI[of _ W] conjI W idW[symmetric]) from card_dim_span[OF V(1) W(2-3) idW] show "span V = span W" by auto qed } { fix V W assume V: "V ⊆ carrier_vec n" and W: "W ⊆ carrier_vec n" and span: "span V = span W" and lin: "lin_indpt V" from Max_in[OF part1(2,3), folded dim_span_def, of W] obtain WW where WW: "WW ⊆ carrier_vec n" "WW ⊆ span W" "lin_indpt WW" and idWW: "card WW = dim_span W" by auto from card_dim_span[OF W WW(2-3) idWW] span have spanWW: "span WW = span V" by auto from span have "V ⊆ span W" using span_mem[OF V] by auto from part1(1)[OF V this lin] have VW: "card V ≤ dim_span W" . have finWW: "finite WW" using WW by (simp add: fin_dim_li_fin) have finV: "finite V" using lin V by (simp add: fin_dim_li_fin) from replacement[OF finWW finV V WW(3) WW(2)[folded span], unfolded idWW] obtain C :: "'a vec set" where le: "int (card C) ≤ int (card V) - int (dim_span W)" by auto from le have "int (dim_span W) + int (card C) ≤ int (card V)" by linarith hence "dim_span W + card C ≤ card V" by linarith with VW show "card V = dim_span W" by auto } qed lemma dim_span_le_n: assumes W: "W ⊆ carrier_vec n" shows "dim_span W ≤ n" proof - from ex_basis_span[OF W] obtain V where V: "V ⊆ carrier_vec n" and lin: "lin_indpt V" and dim: "dim_span W = card V" by auto show ?thesis unfolding dim using lin V using dim_is_n li_le_dim by auto qed lemma dim_span_insert: assumes W: "W ⊆ carrier_vec n" and v: "v ∈ carrier_vec n" and vs: "v ∉ span W" shows "dim_span (insert v W) = Suc (dim_span W)" proof - from ex_basis_span[OF W] obtain V where V: "V ⊆ carrier_vec n" and lin: "lin_indpt V" and span: "span W = span V" and dim: "dim_span W = card V" by auto from V vs[unfolded span] have vV: "v ∉ V" using span_mem[OF V] by blast from lin_dep_iff_in_span[OF V lin v vV] vs span have lin': "lin_indpt (insert v V)" by auto have finV: "finite V" using lin V using fin_dim fin_dim_li_fin by blast have "card (insert v V) = Suc (card V)" using finV vV by auto hence cvV: "card (insert v V) = Suc (dim_span W)" using dim by auto have "span (insert v V) = span (insert v W)" using span V W v by (metis bot_least insert_subset insert_union span_union_is_sum) from same_span_imp_card_eq_dim_span[OF _ _ this lin'] cvV v V W show ?thesis by auto qed end end