Theory Jordan_Normal_Form.DL_Rank
section ‹Matrix Rank›
theory DL_Rank
imports VS_Connect DL_Missing_List
Determinant
Missing_VectorSpace
begin
lemma (in vectorspace) full_dim_span:
assumes "S ⊆ carrier V"
and "finite S"
and "vectorspace.dim K (span_vs S) = card S"
shows "lin_indpt S"
proof -
have "vectorspace K (span_vs S)"
using field.field_axioms vectorspace_def submodule_is_module[OF span_is_submodule[OF assms(1)]] by metis
have "S ⊆ carrier (span_vs S)" by (simp add: assms(1) in_own_span)
have "LinearCombinations.module.span K (vs (span S)) S = carrier (vs (span S))"
using module.span_li_not_depend[OF _ span_is_submodule[OF assms(1)]]
by (simp add: assms(1) in_own_span)
have "vectorspace.basis K (vs (span S)) S"
using vectorspace.dim_gen_is_basis[OF ‹vectorspace K (span_vs S)› ‹finite S› ‹S ⊆ carrier (span_vs S)›
‹LinearCombinations.module.span K (vs (span S)) S = carrier (vs (span S))›] ‹vectorspace.dim K (span_vs S) = card S›
by simp
then have "LinearCombinations.module.lin_indpt K (vs (span S)) S"
using vectorspace.basis_def[OF ‹vectorspace K (span_vs S)›] by blast
then show ?thesis using module.span_li_not_depend[OF _ span_is_submodule[OF assms(1)]]
by (simp add: assms(1) in_own_span)
qed
lemma (in vectorspace) dim_span:
assumes "S ⊆ carrier V"
and "finite S"
and "maximal U (λT. T ⊆ S ∧ lin_indpt T)"
shows "vectorspace.dim K (span_vs S) = card U"
proof -
have "lin_indpt U" "U ⊆ S" by (metis assms(3) maximal_def)+
then have "U ⊆ span S" using in_own_span[OF assms(1)] by blast
then have lin_indpt: "LinearCombinations.module.lin_indpt K (span_vs S) U"
using module.span_li_not_depend(2)[OF ‹U ⊆ span S›] ‹lin_indpt U› assms(1) span_is_submodule by blast
have "span U = span S"
proof (rule ccontr)
assume "span U ≠ span S"
have "span U ⊆ span S" using span_is_monotone ‹U⊆S› by metis
then have "¬ S ⊆ span U" by (meson ‹U ⊆ S› ‹span U ≠ span S› assms(1) span_is_submodule
span_is_subset subset_antisym subset_trans)
then obtain s where "s∈S" "s ∉ span U" by blast
then have "lin_indpt (U∪{s})" using lindep_span
by (meson ‹U ⊆ S› ‹lin_indpt U› assms(1) lin_dep_iff_in_span rev_subsetD span_mem subset_trans)
have "s∉U" using ‹U ⊆ S› ‹s ∉ span U› assms(1) span_mem by auto
then have "(U∪{s}) ⊆ S ∧ lin_indpt (U∪{s})" using ‹U ⊆ S› ‹lin_indpt (U ∪ {s})› ‹s ∈ S› by auto
then have "¬maximal U (λT. T ⊆ S ∧ lin_indpt T)"
unfolding maximal_def using Un_subset_iff ‹s ∉ U› insert_subset order_refl by auto
then show False using assms by metis
qed
then have span:"LinearCombinations.module.span K (vs (span S)) U = span S"
using module.span_li_not_depend[OF ‹U ⊆ span S›]
by (simp add: LinearCombinations.module.span_is_submodule assms(1) module_axioms)
have "vectorspace K (vs (span S))"
using field.field_axioms vectorspace_def submodule_is_module[OF span_is_submodule[OF assms(1)]] by metis
then have "vectorspace.basis K (vs (span S)) U" using vectorspace.basis_def[OF ‹vectorspace K (vs (span S))›]
by (simp add: span ‹U ⊆ span S› lin_indpt)
then show ?thesis
using ‹U ⊆ S› ‹vectorspace K (vs (span S))› assms(2) infinite_super vectorspace.dim_basis by blast
qed
definition (in vec_space) rank ::"'a mat ⇒ nat"
where "rank A = vectorspace.dim class_ring (span_vs (set (cols A)))"
lemma (in vec_space) rank_card_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
shows "rank A = card S"
proof -
have "set (cols A) ⊆ carrier_vec n" using cols_dim assms(1) by blast
have "finite (set (cols A))" by blast
show ?thesis using dim_span[OF ‹set (cols A) ⊆ carrier_vec n› ‹finite (set (cols A))› assms(2)]
unfolding rank_def by blast
qed
lemma maximal_exists_superset:
assumes "finite S"
assumes maxc: "⋀A. P A ⟹ A ⊆ S" and "P B"
shows "∃A. finite A ∧ maximal A P ∧ B ⊆ A"
proof -
have "finite (S-B)" using assms(1) assms(3) infinite_super maxc by blast
then show ?thesis using ‹P B›
proof (induction "S-B" arbitrary:B rule: finite_psubset_induct)
case (psubset B)
then show ?case
proof (cases "maximal B P")
case True
then show ?thesis using order_refl psubset.hyps by (metis assms(1) maxc psubset.prems rev_finite_subset)
next
case False
then obtain B' where "B ⊂ B'" "P B'" using maximal_def psubset.prems by (metis dual_order.order_iff_strict)
then have "B' ⊆ S" "B ⊆ S" using maxc ‹P B› by auto
then have "S - B' ⊂ S - B" using ‹B ⊂ B'› by blast
then show ?thesis using psubset(2)[OF ‹S - B' ⊂ S - B› ‹P B'›] using ‹B ⊂ B'› by fast
qed
qed
qed
lemma (in vec_space) rank_ge_card_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "U ⊆ set (cols A)"
assumes "lin_indpt U"
shows "rank A ≥ card U"
proof -
obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)" "U⊆S" "finite S"
using maximal_exists_superset[of "set (cols A)" "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" U]
using List.finite_set assms(2) assms(3) maximal_exists_superset by blast
then show ?thesis
unfolding rank_card_indpt[OF ‹A ∈ carrier_mat n nc› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
using card_mono by blast
qed
lemma (in vec_space) lin_indpt_full_rank:
assumes "A ∈ carrier_mat n nc"
assumes "distinct (cols A)"
assumes "lin_indpt (set (cols A))"
shows "rank A = nc"
proof -
have "maximal (set (cols A)) (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
by (simp add: assms(3) maximal_def subset_antisym)
then have "rank A = card (set (cols A))" using assms(1) vec_space.rank_card_indpt by blast
then show ?thesis using assms(1) assms(2) distinct_card by fastforce
qed
lemma (in vec_space) rank_le_nc:
assumes "A ∈ carrier_mat n nc"
shows "rank A ≤ nc"
proof -
obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
using maximal_exists[of "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" "card (set (cols A))" "{}"]
by (meson List.finite_set card_mono empty_iff empty_subsetI finite_lin_indpt2 rev_finite_subset)
then have "card S ≤ card (set (cols A))" by (simp add: card_mono maximal_def)
then have "card S ≤ nc"
using assms(1) cols_length card_length carrier_matD(2) by (metis dual_order.trans)
then show ?thesis
using rank_card_indpt[OF ‹A ∈ carrier_mat n nc› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
by simp
qed
lemma (in vec_space) full_rank_lin_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "rank A = nc"
assumes "distinct (cols A)"
shows "lin_indpt (set (cols A))"
proof -
have 1:"set (cols A) ⊆ carrier_vec n" using assms(1) cols_dim by blast
have 2:"finite (set (cols A))" by simp
have "card (set (cols A)) = nc"
using assms(1) assms(3) distinct_card by fastforce
have 3:"vectorspace.dim class_ring (span_vs (set (cols A))) = card (set (cols A))"
using ‹rank A = nc›[unfolded rank_def]
using assms(1) assms(3) distinct_card by fastforce
show ?thesis using full_dim_span[OF 1 2 3] .
qed
lemma (in vec_space) mat_mult_eq_lincomb:
assumes "A ∈ carrier_mat n nc"
assumes "distinct (cols A)"
shows "A *⇩v (vec nc (λi. a (col A i))) = lincomb a (set (cols A))"
proof (rule eq_vecI)
have "finite (set (cols A))" using assms(1) by simp
then show "dim_vec (A *⇩v (vec nc (λi. a (col A i)))) = dim_vec (lincomb a (set (cols A)))"
using assms cols_dim vec_space.lincomb_dim by (metis dim_mult_mat_vec carrier_matD(1))
fix i assume "i < dim_vec (lincomb a (set (cols A)))"
then have "i < n" using ‹dim_vec (A *⇩v (vec nc (λi. a (col A i)))) = dim_vec (lincomb a (set (cols A)))› assms by auto
have "set (cols A) ⊆ carrier_vec n" using cols_dim ‹A ∈ carrier_mat n nc› carrier_matD(1) by blast
have "bij_betw (nth (cols A)) {..<length (cols A)} (set (cols A))"
unfolding bij_betw_def by (rule conjI, simp add: inj_on_nth ‹distinct (cols A)›;
metis subset_antisym in_set_conv_nth lessThan_iff rev_image_eqI subsetI
image_subsetI lessThan_iff nth_mem)
then have " (∑x∈set (cols A). a x * x $ i) =
(∑j∈{..<length (cols A)}. a (cols A ! j) * (cols A ! j) $ i)"
using bij_betw_imp_surj_on bij_betw_imp_inj_on by (metis (no_types, lifting) sum.reindex_cong)
also have "... = (∑j∈{..<length (cols A)}. a (col A j) * (cols A ! j) $ i)"
using assms(1) assms(2) find_first_unique[OF ‹distinct (cols A)›] ‹i < n› by auto
also have "... = (∑j∈{..<length (cols A)}. (cols A ! j) $ i * a (col A j))" by (metis mult_commute_abs)
also have "... = (∑j∈{..<length (cols A)}. row A i $ j * a (col A j))" using ‹i < n› assms(1) assms(2) by auto
finally show "(A *⇩v (vec nc (λi. a (col A i)))) $ i = lincomb a (set (cols A)) $ i"
unfolding lincomb_index[OF ‹i < n› ‹set (cols A) ⊆ carrier_vec n›]
unfolding mult_mat_vec_def scalar_prod_def
using ‹i < n› assms(1) atLeast0LessThan lessThan_def carrier_matD(1) index_vec sum.cong by auto
qed
lemma (in vec_space) lincomb_eq_mat_mult:
assumes "A ∈ carrier_mat n nc"
assumes "v ∈ carrier_vec nc"
assumes "distinct (cols A)"
shows "lincomb (λa. v $ find_first a (cols A)) (set (cols A)) = (A *⇩v v)"
proof -
have "⋀i. i < nc ⟹ find_first (col A i) (cols A) = i"
using assms(1) assms(3) find_first_unique by fastforce
then have "vec nc (λi. v $ find_first (col A i) (cols A)) = v"
using assms(2) by auto
then show ?thesis
using mat_mult_eq_lincomb[where a = "(λa. v $ find_first a (cols A))", OF assms(1) assms(3)] by auto
qed
lemma (in vec_space) lin_depI:
assumes "A ∈ carrier_mat n nc"
assumes "v ∈ carrier_vec nc" "v ≠ 0⇩v nc" "A *⇩v v = 0⇩v n"
assumes "distinct (cols A)"
shows "lin_dep (set (cols A))"
proof -
have 1: "finite (set (cols A))" by simp
have 2: "set (cols A) ⊆ set (cols A)" by auto
have 3: "(λa. v $ find_first a (cols A)) ∈ set (cols A) → UNIV" by simp
obtain i where "v $ i ≠ 0" "i < nc"
using ‹v ≠ 0⇩v nc›
by (metis assms(2) dim_vec carrier_vecD vec_eq_iff zero_vec_def index_zero_vec(1))
then have "i < dim_col A" using assms(1) by blast
have 4:"col A i ∈ set (cols A)"
using cols_nth[OF ‹i < dim_col A›] ‹i < dim_col A› in_set_conv_nth by fastforce
have 5:"v $ find_first (col A i) (cols A) ≠ 0"
using find_first_unique[OF ‹distinct (cols A)›] cols_nth[OF ‹i < dim_col A›] ‹i < nc› ‹v $ i ≠ 0›
assms(1) by auto
have 6:"lincomb (λa. v $ find_first a (cols A)) (set (cols A)) = 0⇩v n"
using assms(1) assms(2) assms(4) assms(5) lincomb_eq_mat_mult by auto
show ?thesis using lin_dep_crit[OF 1 2 _ 4 5 6] by metis
qed
lemma (in vec_space) lin_depE:
assumes "A ∈ carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols A)"
obtains v where "v ∈ carrier_vec nc" "v ≠ 0⇩v nc" "A *⇩v v = 0⇩v n"
proof -
have "finite (set (cols A))" by simp
obtain a w where "a ∈ set (cols A) → UNIV" "lincomb a (set (cols A)) = 0⇩v n" "w ∈ set (cols A)" "a w ≠ 0"
using finite_lin_dep[OF ‹finite (set (cols A))› ‹lin_dep (set (cols A))›]
using assms(1) cols_dim carrier_matD(1) by blast
define v where "v = vec nc (λi. a (col A i))"
have 1:"v ∈ carrier_vec nc" by (simp add: v_def)
have 2:"v ≠ 0⇩v nc"
proof -
obtain i where "w = col A i" "i < length (cols A)"
by (metis ‹w ∈ set (cols A)› cols_length cols_nth in_set_conv_nth)
have "v $ i ≠ 0"
unfolding v_def
using ‹a w ≠ 0›[unfolded ‹w = col A i›] index_vec[OF ‹i < length (cols A)›]
assms(1) cols_length carrier_matD(2) by (metis (no_types) ‹A ∈ carrier_mat n nc›
‹⋀f. vec (length (cols A)) f $ i = f i› ‹a (col A i) ≠ 0› cols_length carrier_matD(2))
then show ?thesis using ‹i < length (cols A)› assms(1) by auto
qed
have 3:"A *⇩v v = 0⇩v n" unfolding v_def
using ‹lincomb a (set (cols A)) = 0⇩v n› mat_mult_eq_lincomb[OF ‹A ∈ carrier_mat n nc› ‹distinct (cols A)›] by auto
show thesis using 1 2 3 by (simp add: that)
qed
lemma (in vec_space) non_distinct_low_rank:
assumes "A ∈ carrier_mat n n"
and "¬ distinct (cols A)"
shows "rank A < n"
proof -
obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
using maximal_exists[of "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" "card (set (cols A))" "{}"]
by (meson List.finite_set card_mono empty_iff empty_subsetI finite_lin_indpt2 rev_finite_subset)
then have "card S ≤ card (set (cols A))" by (simp add: card_mono maximal_def)
then have "card S < n"
using assms(1) cols_length card_length ‹¬ distinct (cols A)› card_distinct carrier_matD(2) nat_less_le
by (metis dual_order.antisym dual_order.trans)
then show ?thesis
using rank_card_indpt[OF ‹A ∈ carrier_mat n n› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
by simp
qed
text ‹The theorem "det non-zero $\longleftrightarrow$ full rank" is practically proven in det\_0\_iff\_vec\_prod\_zero\_field,
but without an actual definition of the rank.›
lemma (in vec_space) det_zero_low_rank:
assumes "A ∈ carrier_mat n n"
and "det A = 0"
shows "rank A < n"
proof (rule ccontr)
assume "¬ rank A < n"
then have "rank A = n" using rank_le_nc assms le_neq_implies_less by blast
obtain v where "v ∈ carrier_vec n" "v ≠ 0⇩v n" "A *⇩v v = 0⇩v n"
using det_0_iff_vec_prod_zero_field[OF assms(1)] assms(2) by blast
then show False
proof (cases "distinct (cols A)")
case True
then have "lin_indpt (set (cols A))" using full_rank_lin_indpt using ‹rank A = n› assms(1) by auto
then show False using lin_depI[OF assms(1) ‹v ∈ carrier_vec n› ‹v ≠ 0⇩v n› ‹A *⇩v v = 0⇩v n›] True by blast
next
case False
then show False using non_distinct_low_rank ‹rank A = n› ‹¬ rank A < n› assms(1) by blast
qed
qed
lemma det_identical_cols:
assumes A: "A ∈ carrier_mat n n"
and ij: "i ≠ j"
and i: "i < n" and j: "j < n"
and r: "col A i = col A j"
shows "det A = 0"
using det_identical_rows det_transpose
by (metis A i ij j carrier_matD(2) transpose_carrier_mat r row_transpose)
lemma (in vec_space) low_rank_det_zero:
assumes "A ∈ carrier_mat n n"
and "det A ≠ 0"
shows "rank A = n"
proof -
have "distinct (cols A)"
proof (rule ccontr)
assume "¬ distinct (cols A)"
then obtain i j where "i≠j" "(cols A) ! i = (cols A) ! j" "i<length (cols A)" "j<length (cols A)"
using distinct_conv_nth by blast
then have "col A i = col A j" "i<n" "j<n" using assms(1) by auto
then have "det A = 0" using det_identical_cols using ‹i ≠ j› assms(1) by blast
then show False using ‹det A ≠ 0› by auto
qed
have "⋀v. v ∈ carrier_vec n ⟹ v ≠ 0⇩v n ⟹ A *⇩v v ≠ 0⇩v n"
using det_0_iff_vec_prod_zero_field[OF assms(1)] assms(2) by auto
then have "lin_indpt (set (cols A))" using lin_depE[OF assms(1) _ ‹distinct (cols A)›] by auto
then show ?thesis using lin_indpt_full_rank[OF assms(1) ‹distinct (cols A)›] by metis
qed
lemma (in vec_space) det_rank_iff:
assumes "A ∈ carrier_mat n n"
shows "det A ≠ 0 ⟷ rank A = n"
using assms det_zero_low_rank low_rank_det_zero by force
section "Subadditivity of rank"
text ‹Subadditivity is the property of rank, that rank (A + B) <= rank A + rank B.›
lemma (in Module.module) lincomb_add:
assumes "finite (b1 ∪ b2)"
assumes "b1 ∪ b2 ⊆ carrier M"
assumes "x1 = lincomb a1 b1" "a1∈ (b1→carrier R)"
assumes "x2 = lincomb a2 b2" "a2∈ (b2→carrier R)"
assumes "x = x1 ⊕⇘M⇙ x2"
shows "lincomb (λv. (λv. if v ∈ b1 then a1 v else 𝟬) v ⊕ (λv. if v ∈ b2 then a2 v else 𝟬) v) (b1 ∪ b2) = x"
proof -
have "finite (b1 ∪ (b2-b1))" "finite (b2 ∪ (b1-b2))"
"b1 ∪ (b2 - b1) ⊆ carrier M" "b2 ∪ (b1-b2) ⊆ carrier M"
"b1 ∩ (b2 - b1) = {}" "b2 ∩ (b1 - b2) = {}"
"(λb. 𝟬⇘R⇙) ∈ b2 - b1 → carrier R" "(λb. 𝟬⇘R⇙) ∈ b1 - b2 → carrier R"
using ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier M› ‹a2∈ (b2→carrier R)› by auto
have "lincomb (λb. 𝟬⇘R⇙) (b2 - b1) = 𝟬⇘M⇙" "lincomb (λb. 𝟬⇘R⇙) (b1 - b2) = 𝟬⇘M⇙"
unfolding lincomb_def using M.finsum_all0 assms(2) lmult_0 subset_iff
by (metis (no_types, lifting) Un_Diff_cancel2 inf_sup_aci(5) le_sup_iff)+
then have "x1 = lincomb (λv. if v ∈ b1 then a1 v else 𝟬) (b1 ∪ b2)"
"x2 = lincomb (λv. if v ∈ b2 then a2 v else 𝟬) (b1 ∪ b2)"
using lincomb_union2[OF ‹finite (b1 ∪ (b2-b1))› ‹b1 ∪ (b2 - b1) ⊆ carrier M› ‹b1 ∩ (b2 - b1) = {}› ‹a1∈ (b1→carrier R)› ‹(λb. 𝟬⇘R⇙) ∈ b2 - b1 → carrier R›]
lincomb_union2[OF ‹finite (b2 ∪ (b1-b2))› ‹b2 ∪ (b1-b2) ⊆ carrier M› ‹b2 ∩ (b1 - b2) = {}› ‹a2∈ (b2→carrier R)› ‹(λb. 𝟬⇘R⇙) ∈ b1 - b2 → carrier R›]
using assms(2) assms(3) assms(4) assms(5) assms(6) by (simp_all add:Un_commute)
have "(λv. if v ∈ b1 then a1 v else 𝟬) ∈ (b1 ∪ b2) → carrier R"
"(λv. if v ∈ b2 then a2 v else 𝟬) ∈ (b1 ∪ b2) → carrier R" using assms(4) assms(6) by auto
show "lincomb (λv. (λv. if v ∈ b1 then a1 v else 𝟬) v ⊕ (λv. if v ∈ b2 then a2 v else 𝟬) v) (b1 ∪ b2) = x"
using lincomb_sum[OF ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier M›
‹(λv. if v ∈ b1 then a1 v else 𝟬) ∈ (b1 ∪ b2) → carrier R› ‹(λv. if v ∈ b2 then a2 v else 𝟬) ∈ (b1 ∪ b2) → carrier R›]
‹x1 = lincomb (λv. if v ∈ b1 then a1 v else 𝟬) (b1 ∪ b2)› ‹x2 = lincomb (λv. if v ∈ b2 then a2 v else 𝟬) (b1 ∪ b2)› assms(7) by blast
qed
lemma (in vectorspace) dim_subadditive:
assumes "subspace K W1 V"
and "vectorspace.fin_dim K (vs W1)"
assumes "subspace K W2 V"
and "vectorspace.fin_dim K (vs W2)"
shows "vectorspace.dim K (vs (subspace_sum W1 W2)) ≤ vectorspace.dim K (vs W1) + vectorspace.dim K (vs W2)"
proof -
have "vectorspace K (vs W1)" "vectorspace K (vs W2)" "submodule K W1 V" "submodule K W2 V"
by (simp add: ‹subspace K W1 V› ‹subspace K W2 V› subspace_is_vs)+
obtain b1 b2 where "vectorspace.basis K (vs W1) b1" "vectorspace.basis K (vs W2) b2" "finite b1" "finite b2"
using vectorspace.finite_basis_exists[OF ‹vectorspace K (vs W1)› ‹vectorspace.fin_dim K (vs W1)›]
using vectorspace.finite_basis_exists[OF ‹vectorspace K (vs W2)› ‹vectorspace.fin_dim K (vs W2)›]
by blast
then have "LinearCombinations.module.gen_set K (vs W1) b1" "LinearCombinations.module.gen_set K (vs W2) b2"
using ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)› vectorspace.basis_def by blast+
then have "span b1 = W1" "span b2 = W2"
using module.span_li_not_depend(1) ‹submodule K W1 V› ‹submodule K W2 V›
‹vectorspace K (vs W1)› ‹vectorspace.basis K (vs W1) b1› ‹vectorspace K (vs W2)›
‹vectorspace.basis K (vs W2) b2› vectorspace.basis_def by force+
have "W1 ⊆ carrier V" "W2 ⊆ carrier V" using ‹subspace K W1 V› ‹subspace K W2 V› subspace_def submodule_def by metis+
have "b1 ⊆ carrier V"
using ‹vectorspace.basis K (vs W1) b1› ‹vectorspace K (vs W1)› vectorspace.basis_def
‹W1 ⊆ carrier V› by fastforce
have "b2 ⊆ carrier V"
using ‹vectorspace.basis K (vs W2) b2› ‹vectorspace K (vs W2)› vectorspace.basis_def
‹W2 ⊆ carrier V› by fastforce
have "finite (b1 ∪ b2)" "b1 ∪ b2 ⊆ carrier V"
by (simp_all add: ‹finite b1› ‹finite b2› ‹b2 ⊆ carrier V› ‹b1 ⊆ carrier V›)
have "subspace_sum W1 W2 ⊆ span (b1∪b2)"
proof (rule subsetI)
fix x assume "x ∈ subspace_sum W1 W2"
obtain x1 x2 where "x1 ∈ W1" "x2 ∈ W2" "x = x1 ⊕⇘V⇙ x2"
using imageE[OF ‹x ∈ subspace_sum W1 W2›[unfolded submodule_sum_def]]
by (metis (no_types, lifting) BNF_Def.Collect_case_prodD split_def)
obtain a1 where "x1 = lincomb a1 b1" "a1∈ (b1→carrier K)"
using ‹span b1 = W1› finite_span[OF ‹finite b1› ‹b1 ⊆ carrier V›] ‹x1 ∈ W1› by auto
obtain a2 where "x2 = lincomb a2 b2" "a2∈ (b2→carrier K)"
using ‹span b2 = W2› finite_span[OF ‹finite b2› ‹b2 ⊆ carrier V›] ‹x2 ∈ W2› by auto
obtain a where "x = lincomb a (b1 ∪ b2)" using lincomb_add[OF ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier V›
‹x1 = lincomb a1 b1› ‹a1∈ (b1→carrier K)› ‹x2 = lincomb a2 b2› ‹a2∈ (b2→carrier K)› ‹x = x1 ⊕⇘V⇙ x2›] by blast
then show "x ∈ span (b1 ∪ b2)" using finite_span[OF ‹finite (b1 ∪ b2)› ‹(b1 ∪ b2) ⊆ carrier V›]
using ‹b1 ⊆ carrier V› ‹b2 ⊆ carrier V› ‹span b1 = W1› ‹span b2 = W2› ‹x ∈ subspace_sum W1 W2› span_union_is_sum by auto
qed
have "b1 ⊆ W1" "b2 ⊆ W2"
using ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)› ‹vectorspace.basis K (vs W1) b1›
‹vectorspace.basis K (vs W2) b2› vectorspace.basis_def local.carrier_vs_is_self by blast+
then have "b1∪b2 ⊆ subspace_sum W1 W2" using ‹submodule K W1 V› ‹submodule K W2 V› in_sum
by (metis assms(1) assms(3) dual_order.trans sup_least vectorspace.vsum_comm vectorspace_axioms)
have "subspace_sum W1 W2 = LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
proof (rule subset_antisym)
have "submodule K (subspace_sum W1 W2) V" by (simp add: ‹submodule K W1 V› ‹submodule K W2 V› sum_is_submodule)
show "subspace_sum W1 W2 ⊆ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
using module.span_li_not_depend(1)[OF ‹b1∪b2 ⊆ subspace_sum W1 W2› ‹submodule K (subspace_sum W1 W2) V›]
by (simp add: ‹subspace_sum W1 W2 ⊆ span (b1 ∪ b2)›)
show "subspace_sum W1 W2 ⊇ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
using ‹b1∪b2 ⊆ subspace_sum W1 W2› by (metis (full_types) LinearCombinations.module.span_is_subset2
LinearCombinations.module.submodule_is_module ‹submodule K (subspace_sum W1 W2) V› local.carrier_vs_is_self submodule_def)
qed
have "vectorspace K (vs (subspace_sum W1 W2))" using assms(1) assms(3) subspace_def sum_is_subspace vectorspace.subspace_is_vs by blast
then have "vectorspace.dim K (vs (subspace_sum W1 W2)) ≤ card (b1 ∪ b2)"
using vectorspace.gen_ge_dim[OF ‹vectorspace K (vs (subspace_sum W1 W2))› ‹finite (b1 ∪ b2)›]
‹b1 ∪ b2 ⊆ subspace_sum W1 W2›
‹subspace_sum W1 W2 = LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2)›
local.carrier_vs_is_self by blast
also have "... ≤ card b1 + card b2" by (simp add: card_Un_le)
also have "... = vectorspace.dim K (vs W1) + vectorspace.dim K (vs W2)"
by (metis ‹finite b1› ‹finite b2› ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)›
‹vectorspace.basis K (vs W1) b1› ‹vectorspace.basis K (vs W2) b2› vectorspace.dim_basis)
finally show ?thesis by auto
qed
lemma (in Module.module) nested_submodules:
assumes "submodule R W M"
assumes "submodule R X M"
assumes "X ⊆ W"
shows "submodule R X (md W)"
unfolding submodule_def
using ‹X ⊆ W› submodule_is_module[OF ‹submodule R W M›] using ‹submodule R X M›[unfolded submodule_def] by auto
lemma (in vectorspace) nested_subspaces:
assumes "subspace K W V"
assumes "subspace K X V"
assumes "X ⊆ W"
shows "subspace K X (vs W)"
using assms nested_submodules subspace_def subspace_is_vs by blast
lemma (in vectorspace) subspace_dim:
assumes "subspace K X V" "fin_dim" "vectorspace.fin_dim K (vs X)"
shows "vectorspace.dim K (vs X) ≤ dim"
proof -
have "vectorspace K (vs X)" using assms(1) subspace_is_vs by auto
then obtain b where "vectorspace.basis K (vs X) b" using vectorspace.finite_basis_exists
using assms(3) by blast
then have "b ⊆ carrier V" "LinearCombinations.module.lin_indpt K (vs X) b"
using vectorspace.basis_def[OF ‹vectorspace K (vs X)›] ‹subspace K X V›[unfolded subspace_def submodule_def] by auto
then have "lin_indpt b"
by (metis LinearCombinations.module.span_li_not_depend(2) ‹vectorspace K (vs X)› ‹vectorspace.basis K (vs X) b›
assms(1) is_module local.carrier_vs_is_self submodule_def vectorspace.basis_def)
show ?thesis using li_le_dim(2)[OF ‹fin_dim› ‹b ⊆ carrier V› ‹lin_indpt b›]
using ‹b ⊆ carrier V› ‹lin_indpt b› ‹vectorspace K (vs X)› ‹vectorspace.basis K (vs X) b› assms(2)
fin_dim_li_fin vectorspace.dim_basis by fastforce
qed
lemma (in vectorspace) fin_dim_subspace_sum:
assumes "subspace K W1 V"
assumes "subspace K W2 V"
assumes "vectorspace.fin_dim K (vs W1)" "vectorspace.fin_dim K (vs W2)"
shows "vectorspace.fin_dim K (vs (subspace_sum W1 W2))"
proof -
obtain b1 where "finite b1" "b1 ⊆ W1" "LinearCombinations.module.gen_set K (vs W1) b1"
using assms vectorspace.fin_dim_def subspace_is_vs by force
obtain b2 where "finite b2" "b2 ⊆ W2" "LinearCombinations.module.gen_set K (vs W2) b2"
using assms vectorspace.fin_dim_def subspace_is_vs by force
have 1:"finite (b1 ∪ b2)" by (simp add: ‹finite b1› ‹finite b2›)
have 2:"b1 ∪ b2 ⊆ subspace_sum W1 W2"
by (metis (no_types, lifting) ‹b1 ⊆ W1› ‹b2 ⊆ W2› assms(1) assms(2)
le_sup_iff subset_Un_eq vectorspace.in_sum_vs vectorspace.vsum_comm vectorspace_axioms)
have 3:"LinearCombinations.module.gen_set K (vs (subspace_sum W1 W2)) (b1 ∪ b2)"
proof (rule subset_antisym)
have 0:"LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2) = span (b1 ∪ b2)"
using span_li_not_depend(1)[OF ‹b1 ∪ b2 ⊆ subspace_sum W1 W2›] sum_is_subspace[OF assms(1) assms(2)] by auto
then show "LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2) ⊆ carrier (vs (subspace_sum W1 W2))"
using ‹b1 ∪ b2 ⊆ subspace_sum W1 W2› span_is_subset sum_is_subspace[OF assms(1) assms(2)] by auto
show "carrier (vs (subspace_sum W1 W2)) ⊆ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2)"
unfolding 0
proof
fix x assume assumption:"x ∈ carrier (vs (subspace_sum W1 W2))"
then have "x∈subspace_sum W1 W2" by auto
then obtain x1 x2 where "x = x1 ⊕⇘V⇙ x2" "x1∈W1" "x2∈W2"
using imageE[OF ‹x ∈ subspace_sum W1 W2›[unfolded submodule_sum_def]]
by (metis (no_types, lifting) BNF_Def.Collect_case_prodD split_def)
have "x1∈span b1" "x2∈span b2"
using ‹LinearCombinations.module.span K (vs W1) b1 = carrier (vs W1)› ‹b1 ⊆ W1› ‹x1 ∈ W1›
‹LinearCombinations.module.span K (vs W2) b2 = carrier (vs W2)› ‹b2 ⊆ W2› ‹x2 ∈ W2›
assms(1) assms(2) span_li_not_depend(1) by auto
then have "x1∈span (b1 ∪ b2)" "x2∈span (b1 ∪ b2)" by (meson le_sup_iff subsetD span_is_monotone subsetI)+
then show "x ∈ span (b1 ∪ b2)" unfolding ‹x = x1 ⊕⇘V⇙ x2›
by (meson ‹b1 ∪ b2 ⊆ subspace_sum W1 W2› assms(1) assms(2) is_module submodule.subset
subset_trans sum_is_submodule vectorspace.span_add1 vectorspace_axioms)
qed
qed
show ?thesis using 1 2 3 vectorspace.fin_dim_def
by (metis assms(1) assms(2) local.carrier_vs_is_self subspace_def sum_is_subspace vectorspace.subspace_is_vs)
qed
lemma (in vec_space) rank_subadditive:
assumes "A ∈ carrier_mat n nc"
assumes "B ∈ carrier_mat n nc"
shows "rank (A + B) ≤ rank A + rank B"
proof -
define W1 where "W1 = span (set (cols A))"
define W2 where "W2 = span (set (cols B))"
have "set (cols (A + B)) ⊆ subspace_sum W1 W2"
proof
fix x assume "x ∈ set (cols (A + B))"
obtain i where "x = col (A + B) i" "i < length (cols (A + B))"
using ‹x ∈ set (cols (A + B))› nth_find_first cols_nth find_first_le by (metis cols_length)
then have "x = col A i + col B i" using ‹i < length (cols (A + B))› assms(1) assms(2) by auto
have "col A i ∈ span (set (cols A))" "col B i ∈ span (set (cols B))"
using ‹i < length (cols (A + B))› assms(1) assms(2) in_set_conv_nth
by (metis cols_dim cols_length cols_nth carrier_matD(1) carrier_matD(2) index_add_mat(3) span_mem)+
then show "x ∈ subspace_sum W1 W2"
unfolding W1_def W2_def ‹x = col A i + col B i› submodule_sum_def by blast
qed
have "subspace class_ring (subspace_sum W1 W2) V"
by (metis W1_def W2_def assms(1) assms(2) cols_dim carrier_matD(1) span_is_submodule subspace_def sum_is_submodule vec_vs)
then have "span (set (cols (A + B))) ⊆ subspace_sum W1 W2"
by (simp add: ‹set (cols (A + B)) ⊆ subspace_sum W1 W2› span_is_subset)
have "subspace class_ring (span (set (cols (A + B)))) V" by (metis assms(2) cols_dim add_carrier_mat carrier_matD(1) span_is_subspace)
have subspace:"subspace class_ring (span (set (cols (A + B)))) (vs (subspace_sum W1 W2))"
using nested_subspaces[OF ‹subspace class_ring (subspace_sum W1 W2) V› ‹subspace class_ring (span (set (cols (A + B)))) V›
‹span (set (cols (A + B))) ⊆ subspace_sum W1 W2›] .
have "vectorspace.fin_dim class_ring (vs W1)" "vectorspace.fin_dim class_ring (vs W2)"
"subspace class_ring W1 V" "subspace class_ring W2 V"
using span_is_subspace W1_def W2_def assms(1) assms(2) cols_dim carrier_matD fin_dim_span_cols by auto
then have fin_dim: "vectorspace.fin_dim class_ring (vs (subspace_sum W1 W2))" using fin_dim_subspace_sum by auto
have "vectorspace.fin_dim class_ring (span_vs (set (cols (A + B))))" using assms(2) add_carrier_mat vec_space.fin_dim_span_cols by blast
then have "rank (A + B) ≤ vectorspace.dim class_ring (vs (subspace_sum W1 W2))" unfolding rank_def
using vectorspace.subspace_dim[OF subspace_is_vs[OF ‹subspace class_ring (subspace_sum W1 W2) V›] subspace fin_dim] by auto
also have "vectorspace.dim class_ring (vs (subspace_sum W1 W2)) ≤ rank A + rank B" unfolding rank_def
using W1_def W2_def ‹subspace class_ring W1 V› ‹subspace class_ring W2 V› ‹vectorspace.fin_dim class_ring (vs W1)›
‹vectorspace.fin_dim class_ring (vs W2)› subspace_def vectorspace.dim_subadditive by blast
finally show ?thesis by auto
qed
lemma (in vec_space) span_zero: "span {zero V} = {zero V}"
by (metis (no_types, lifting) empty_subsetI in_own_span span_is_submodule span_is_subset
span_is_subset2 subset_antisym vectorspace.span_empty vectorspace_axioms)
lemma (in vec_space) dim_zero_vs: "vectorspace.dim class_ring (span_vs {}) = 0"
proof -
have "vectorspace class_ring (span_vs {})" using field.field_axioms span_is_submodule submodule_is_module vectorspace_def by auto
have "{} ⊆ carrier_vec n ∧ lin_indpt {}"
by (metis (no_types) empty_subsetI fin_dim finite_basis_exists subset_li_is_li vec_vs vectorspace.basis_def)
then have "vectorspace.basis class_ring (span_vs {}) {}" using vectorspace.basis_def
by (simp add: ‹vectorspace class_ring (vs (span {}))› span_is_submodule span_li_not_depend(1) span_li_not_depend(2) vectorspace.basis_def)
then show ?thesis using ‹vectorspace class_ring (vs (span {}))› vectorspace.dim_basis by fastforce
qed
lemma (in vec_space) rank_0I: "rank (0⇩m n nc) = 0"
proof -
have "set (cols (0⇩m n nc)) ⊆ {0⇩v n}"
by (metis col_zero cols_length cols_nth in_set_conv_nth insertCI index_zero_mat(3) subsetI)
have "set (cols (0⇩m n nc::'a mat)) = {} ∨ set (cols (0⇩m n nc)) = {0⇩v n::'a vec}"
by (meson ‹set (cols (0⇩m n nc)) ⊆ {0⇩v n}› subset_singletonD)
then have "span (set (cols (0⇩m n nc))) = {0⇩v n}"
by (metis (no_types) span_empty span_zero vectorspace.span_empty vectorspace_axioms)
then show ?thesis unfolding rank_def ‹span (set (cols (0⇩m n nc))) = {0⇩v n}›
using span_empty dim_zero_vs by simp
qed
lemma (in vec_space) rank_le_1_product_entries:
fixes f g::"nat ⇒ 'a"
assumes "A ∈ carrier_mat n nc"
assumes "⋀r c. r<dim_row A ⟹ c<dim_col A ⟹ A $$ (r,c) = f r * g c"
shows "rank A ≤ 1"
proof -
have "set (cols A) ⊆ span {vec n f}"
proof
fix v assume "v ∈ set (cols A)"
then obtain c where "c < dim_col A" "v = col A c" by (metis cols_length cols_nth in_set_conv_nth)
have "g c ⋅⇩v vec n f = v"
proof (rule eq_vecI)
show "dim_vec (g c ⋅⇩v Matrix.vec n f) = dim_vec v" using ‹v = col A c› assms(1) by auto
fix r assume "r < dim_vec v"
then have "r < dim_vec (Matrix.vec n f)" using ‹dim_vec (g c ⋅⇩v Matrix.vec n f) = dim_vec v› by auto
then have "r < n" "r < dim_row A"using index_smult_vec(2) ‹A ∈ carrier_mat n nc› by auto
show "(g c ⋅⇩v Matrix.vec n f) $ r = v $ r"
unfolding ‹v = col A c› col_def index_smult_vec(1)[OF ‹r < dim_vec (Matrix.vec n f)›]
index_vec[OF ‹r < n›] index_vec[OF ‹r < dim_row A›] by (simp add: ‹c < dim_col A› ‹r < dim_row A› assms(2))
qed
then show "v ∈ span {vec n f}" using submodule.smult_closed[OF span_is_submodule]
using UNIV_I empty_subsetI insert_subset span_self dim_vec module_vec_simps(4) by auto
qed
have "vectorspace class_ring (vs (span {Matrix.vec n f}))" using span_is_subspace[THEN subspace_is_vs, of "{vec n f}"] by auto
have "submodule class_ring (span {Matrix.vec n f}) V" by (simp add: span_is_submodule)
have "subspace class_ring(span (set (cols A))) (vs (span {Matrix.vec n f}))"
using vectorspace.span_is_subspace[OF ‹vectorspace class_ring (vs (span {Matrix.vec n f}))›, of "set (cols A)", unfolded
span_li_not_depend(1)[OF ‹set (cols A) ⊆ span {vec n f}› ‹submodule class_ring (span {Matrix.vec n f}) V›]]
‹set (cols A) ⊆ span {vec n f}› by auto
have fin_dim:"vectorspace.fin_dim class_ring (vs (span {Matrix.vec n f}))"
"vectorspace.fin_dim class_ring (vs (span {Matrix.vec n f})⦇carrier := span (set (cols A))⦈)"
using fin_dim_span fin_dim_span_cols ‹A ∈ carrier_mat n nc› by auto
have "vectorspace.dim class_ring (vs (span {Matrix.vec n f})) ≤ 1"
using vectorspace.dim_le1I[OF ‹vectorspace class_ring (vs (span {Matrix.vec n f}))›]
span_mem span_li_not_depend(1)[OF _ ‹submodule class_ring (span {Matrix.vec n f}) V›] by simp
then show ?thesis unfolding rank_def using "vectorspace.subspace_dim"[OF
‹vectorspace class_ring (vs (span {Matrix.vec n f}))› ‹subspace class_ring (span (set (cols A))) (vs (span {Matrix.vec n f}))›
fin_dim(1) fin_dim(2)] by simp
qed
end