# Theory Dim_Span

```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```