Theory DL_Rank_Submatrix
section ‹Rank and Submatrices›
theory DL_Rank_Submatrix
imports DL_Rank DL_Submatrix Matrix
begin
lemma row_submatrix_UNIV:
assumes "i < card {i. i < dim_row A ∧ i ∈ I}"
shows "row (submatrix A I UNIV) i = row A (pick I i)"
proof (rule eq_vecI)
show dim_eq:"dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))"
unfolding carrier_vecD[OF row_carrier] dim_submatrix by auto
fix j assume "j < dim_vec (row A (pick I i))"
then have "j < dim_col (submatrix A I UNIV)" "j < dim_col A" "j < card {j. j < dim_col A ∧ j ∈ UNIV}" using dim_eq by auto
show "row (submatrix A I UNIV) i $ j = row A (pick I i) $ j"
unfolding row_def index_vec[OF ‹j < dim_col (submatrix A I UNIV)›] index_vec[OF ‹j < dim_col A›]
using submatrix_index[OF assms ‹j < card {j. j < dim_col A ∧ j ∈ UNIV}›] using pick_UNIV by auto
qed
lemma distinct_cols_submatrix_UNIV:
assumes "distinct (cols (submatrix A I UNIV))"
shows "distinct (cols A)"
using assms proof (rule contrapos_pp)
assume "¬ distinct (cols A)"
then obtain i j where "i < dim_col A" "j < dim_col A" "(cols A)!i = (cols A)!j" "i≠j"
using distinct_conv_nth cols_length by metis
have "i < dim_col (submatrix A I UNIV)" "j < dim_col (submatrix A I UNIV)"
unfolding dim_submatrix using ‹i < dim_col A› ‹j < dim_col A›by simp_all
then have "i < length (cols (submatrix A I UNIV))" "j < length (cols (submatrix A I UNIV))"
unfolding cols_length by simp_all
have "(cols (submatrix A I UNIV))!i = (cols (submatrix A I UNIV))!j"
proof (rule eq_vecI)
show "dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)"
by (simp add: ‹i < dim_col (submatrix A I UNIV)› ‹j < dim_col (submatrix A I UNIV)›)
fix k assume "k < dim_vec (cols (submatrix A I UNIV) ! j)"
then have "k < dim_row (submatrix A I UNIV)"
using ‹j < length (cols (submatrix A I UNIV))› by auto
then have "k < card {j. j < dim_row A ∧ j ∈ I}" using dim_submatrix(1) by metis
have i_transfer:"cols (submatrix A I UNIV) ! i $ k = (cols A) ! i $ (pick I k)"
unfolding cols_nth[OF ‹i < dim_col (submatrix A I UNIV)›] col_def index_vec[OF ‹k < dim_row (submatrix A I UNIV)›]
unfolding submatrix_index[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}› ‹i < dim_col (submatrix A I UNIV)›[unfolded dim_submatrix]]
unfolding pick_UNIV cols_nth[OF ‹i < dim_col A›] col_def index_vec[OF pick_le[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}›]]
by metis
have j_transfer:"cols (submatrix A I UNIV) ! j $ k = (cols A) ! j $ (pick I k)"
unfolding cols_nth[OF ‹j < dim_col (submatrix A I UNIV)›] col_def index_vec[OF ‹k < dim_row (submatrix A I UNIV)›]
unfolding submatrix_index[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}› ‹j < dim_col (submatrix A I UNIV)›[unfolded dim_submatrix]]
unfolding pick_UNIV cols_nth[OF ‹j < dim_col A›] col_def index_vec[OF pick_le[OF ‹k < card {j. j < dim_row A ∧ j ∈ I}›]]
by metis
show "cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k"
using ‹cols A ! i = cols A ! j› i_transfer j_transfer by auto
qed
then show "¬ distinct (cols (submatrix A I UNIV))" unfolding distinct_conv_nth
using ‹i < length (cols (submatrix A I UNIV))› ‹j < length (cols (submatrix A I UNIV))› ‹i ≠ j› by blast
qed
lemma cols_submatrix_subset: "set (cols (submatrix A UNIV J)) ⊆ set (cols A)"
proof
fix c assume "c ∈ set (cols (submatrix A UNIV J))"
then obtain j where "j < length (cols (submatrix A UNIV J))" "cols (submatrix A UNIV J) ! j = c"
by (meson in_set_conv_nth)
then have "j < dim_col (submatrix A UNIV J)" by simp
then have "j < card {j. j < dim_col A ∧ j ∈ J}" by (simp add: dim_submatrix(2))
have "cols (submatrix A UNIV J) ! j = cols A ! (pick J j)"
unfolding cols_nth[OF ‹j < dim_col (submatrix A UNIV J)›] cols_nth[OF pick_le[OF ‹j < card {j. j < dim_col A ∧ j ∈ J}›]]
proof (rule eq_vecI)
show "dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))" unfolding dim_col dim_submatrix by auto
fix i assume "i < dim_vec (col A (pick J j))"
then have "i < dim_row A" by simp
then have "i < dim_row (submatrix A UNIV J)" using ‹dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))› by auto
show "col (submatrix A UNIV J) j $ i = col A (pick J j) $ i"
unfolding col_def index_vec[OF ‹i < dim_row (submatrix A UNIV J)›] index_vec[OF ‹i < dim_row A›]
using submatrix_index by (metis (no_types, lifting) ‹dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))›
‹i < dim_vec (col A (pick J j))› ‹j < dim_col (submatrix A UNIV J)› dim_col dim_submatrix(1) dim_submatrix(2) pick_UNIV)
qed
then show "c ∈ set (cols A)"
using ‹cols (submatrix A UNIV J) ! j = c›
using pick_le[OF ‹j < card {j. j < dim_col A ∧ j ∈ J}›] by (metis cols_length nth_mem)
qed
lemma (in vec_space) lin_dep_submatrix_UNIV:
assumes "A ∈ carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols (submatrix A I UNIV))"
shows "LinearCombinations.module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n ∧ i ∈ I})) (set (cols (submatrix A I UNIV)))"
(is "LinearCombinations.module.lin_dep class_ring ?M (set ?S')")
proof -
obtain v where 2:"v ∈ carrier_vec nc" and 3:"v ≠ 0⇩v nc" and "A *⇩v v = 0⇩v n"
using vec_space.lin_depE[OF assms(1) assms(2) distinct_cols_submatrix_UNIV[OF assms(3)]] by auto
have 1: "submatrix A I UNIV ∈ carrier_mat (card {i. i < n ∧ i ∈ I}) nc"
apply (rule carrier_matI) unfolding dim_submatrix using ‹A ∈ carrier_mat n nc› by auto
have 4:"submatrix A I UNIV *⇩v v = 0⇩v (card {i. i < n ∧ i ∈ I})"
proof (rule eq_vecI)
show dim_eq:"dim_vec (submatrix A I UNIV *⇩v v) = dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))" using "1" by auto
fix i assume "i < dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))"
then have i_le:"i < card {i. i < n ∧ i ∈ I}" by auto
have "(submatrix A I UNIV *⇩v v) $ i = row (submatrix A I UNIV) i ∙ v" using dim_eq i_le by auto
also have "... = row A (pick I i) ∙ v" using row_submatrix_UNIV
by (metis (no_types, lifting) dim_eq dim_mult_mat_vec dim_submatrix(1) ‹i < dim_vec (0⇩v (card {i. i < n ∧ i ∈ I}))›)
also have "... = 0"
using ‹A *⇩v v = 0⇩v n› i_le[THEN pick_le] by (metis assms(1) index_mult_mat_vec carrier_matD(1) index_zero_vec(1))
also have "... = 0⇩v (card {i. i < n ∧ i ∈ I}) $ i" by (simp add: i_le)
finally show "(submatrix A I UNIV *⇩v v) $ i = 0⇩v (card {i. i < n ∧ i ∈ I}) $ i" by metis
qed
show ?thesis using vec_space.lin_depI[OF 1 2 3 4] using assms(3) by auto
qed
lemma (in vec_space) rank_gt_minor:
assumes "A ∈ carrier_mat n nc"
assumes "det (submatrix A I J) ≠ 0"
shows "card {j. j < nc ∧ j ∈ J} ≤ rank A"
proof -
have square:"dim_row (submatrix A I J) = dim_col (submatrix A I J)"
using det_def ‹det (submatrix A I J) ≠ 0› by metis
then have full_rank:"vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)"
using vec_space.low_rank_det_zero assms(2) carrier_matI by auto
then have distinct:"distinct (cols (submatrix A I J))"
using vec_space.non_distinct_low_rank square less_irrefl carrier_matI by metis
then have indpt:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))"
using vec_space.full_rank_lin_indpt[OF _ full_rank distinct] square by fastforce
have distinct2: "distinct (cols (submatrix (submatrix A UNIV J) I UNIV))" using submatrix_split distinct by metis
have indpt2:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (card {i. i < n ∧ i ∈ I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))"
using submatrix_split dim_submatrix(1) indpt by (metis (full_types) assms(1) carrier_matD(1))
have "submatrix A UNIV J ∈ carrier_mat n (dim_col (submatrix A UNIV J))"
apply (rule carrier_matI) unfolding dim_submatrix(1) using ‹A ∈ carrier_mat n nc› carrier_matD by simp_all
have "lin_indpt (set (cols (submatrix A UNIV J)))"
using indpt2 vec_space.lin_dep_submatrix_UNIV[OF ‹submatrix A UNIV J ∈ carrier_mat n (dim_col (submatrix A UNIV J))› _ distinct2] by blast
have distinct3:"distinct (cols (submatrix A UNIV J))" by (metis distinct distinct_cols_submatrix_UNIV submatrix_split)
show ?thesis using
rank_ge_card_indpt[OF ‹A ∈ carrier_mat n nc› cols_submatrix_subset ‹lin_indpt (set (cols (submatrix A UNIV J)))›,
unfolded distinct_card[OF distinct3, unfolded cols_length dim_submatrix], unfolded carrier_matD(2)[OF ‹A ∈ carrier_mat n nc›]]
by blast
qed
end