Theory Rank_Nullity_Theorem.Fundamental_Subspaces

(*  
    Title:      Fundamental_Subspaces.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Maintainer: Jose Divasón <jose.divasonm at unirioja.es>
*)

section‹Fundamental Subspaces›

theory Fundamental_Subspaces
imports 
    Miscellaneous
begin

subsection‹The fundamental subspaces of a matrix›

subsubsection‹Definitions›

definition left_null_space :: "'a::{semiring_1}^'n^'m => ('a^'m) set"
  where "left_null_space A = {x. x v* A = 0}"

definition null_space :: "'a::{semiring_1}^'n^'m => ('a^'n) set"
  where "null_space A = {x. A *v x = 0}"

definition row_space :: "'a::{field}^'n^'m=>('a^'n) set"
  where "row_space A = vec.span (rows A)"

definition col_space :: "'a::{field}^'n^'m=>('a^'m) set"
  where "col_space A = vec.span (columns A)"

subsubsection‹Relationships among them›

lemma left_null_space_eq_null_space_transpose:
  "left_null_space (A::'a::{comm_semiring_1}^'n^'m) = null_space (transpose A)"
  unfolding null_space_def left_null_space_def transpose_vector ..

lemma null_space_eq_left_null_space_transpose:
  "null_space (A::'a::{comm_semiring_1}^'n^'m) = left_null_space (transpose A)"
  using left_null_space_eq_null_space_transpose[of "transpose A"]
  unfolding transpose_transpose ..

lemma row_space_eq_col_space_transpose:
  fixes A::"'a::{field}^'columns^'rows"
  shows "row_space A = col_space (transpose A)"
  unfolding col_space_def row_space_def columns_transpose[of A] ..

lemma col_space_eq_row_space_transpose:
  fixes A::"'a::{field}^'n^'m"
  shows "col_space A = row_space (transpose A)"
  unfolding col_space_def row_space_def unfolding rows_transpose[of A] ..


subsection‹Proving that they are subspaces›

lemma subspace_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (null_space A)"
  by (auto simp: vec.subspace_def null_space_def vec.scale vec.add)

lemma subspace_left_null_space:
  fixes A::"'a::{field}^'n^'m"
  shows "vec.subspace (left_null_space A)"
  unfolding left_null_space_eq_null_space_transpose using subspace_null_space .

lemma subspace_row_space:
  shows "vec.subspace (row_space A)" by (metis row_space_def vec.subspace_span)

lemma subspace_col_space:
  shows "vec.subspace (col_space A)" by (metis col_space_def vec.subspace_span)
  
subsection‹More useful properties and equivalences›

lemma col_space_eq:
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = {y. ∃x. A *v x = y}"
proof (unfold col_space_def vec.span_finite[OF finite_columns], auto)
  fix x
  show "A *v x ∈ range (λu. ∑v∈columns A. u v *s v)" using matrix_vmult_column_sum[of A x] by auto
next
  fix u::"('a, 'n) vec ⇒ 'a"
  let ?g="λy. {i. y=column i A}"
  let ?x="(χ i. if i=(LEAST a. a ∈ ?g (column i A)) then u (column i A) else 0)"
  show "∃x. A *v x = (∑v∈columns A. u v *s v)"
  proof (unfold matrix_mult_sum, rule exI[of _ "?x"], auto)
    have inj: "inj_on ?g (columns A)" unfolding inj_on_def unfolding columns_def by auto
    have union_univ: "⋃(?g`(columns A)) = UNIV" unfolding columns_def by auto               
    have "sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) UNIV 
        = sum (λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) (⋃(?g`(columns A)))"
      unfolding union_univ ..
    also have "... = sum (sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)) (?g`(columns A))" 
      by (rule sum.Union_disjoint[unfolded o_def], auto)
    also have "... = sum ((sum (λi.(if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)) ∘ ?g) 
        (columns A)" by (rule sum.reindex, simp add: inj)
    also have "... = sum (λy. u y *s y) (columns A)"
    proof (rule sum.cong, auto)
      fix x
      assume x_in_cols: "x ∈ columns A"
      obtain b where b: "x=column b A" using x_in_cols unfolding columns_def by blast
      let ?f="(λi. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A)" 
      have sum_rw: "sum ?f ({i. x = column i A} - {LEAST a. x = column a A}) = 0"
        by (rule sum.neutral, auto)
      have "sum ?f {i. x = column i A} = ?f (LEAST a. x = column a A) + sum ?f ({i. x = column i A} - {LEAST a. x = column a A})" 
        apply (rule sum.remove, auto, rule LeastI_ex) 
        using x_in_cols unfolding columns_def by auto
      also have "... = ?f (LEAST a. x = column a A)" unfolding sum_rw by simp
      also have "... = u x *s x"
      proof (auto, rule LeastI2)
        show "x = column b A" using b .
        fix xa
        assume x: "x = column xa A"
        show "u (column xa A) *s column xa A = u x *s x" unfolding x ..
      next
        assume "(LEAST a. x = column a A) ≠ (LEAST a. column (LEAST c. x = column c A) A = column a A)"
        moreover have "(LEAST a. x = column a A) = (LEAST a. column (LEAST c. x = column c A) A = column a A)"
          by (rule Least_equality[symmetric], rule LeastI2, simp_all add: b, rule Least_le, metis (lifting, full_types) LeastI)
        ultimately show "u x = 0" by contradiction
      qed
      finally show " (∑i | x = column i A. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = u x *s x" .
    qed
    finally show "(∑i∈UNIV. (if i = (LEAST a. column i A = column a A) then u (column i A) else 0) *s column i A) = (∑y∈columns A. u y *s y)" .
  qed
qed


corollary col_space_eq':
  fixes A::"'a::{field}^'m::{finite, wellorder}^'n"
  shows "col_space A = range (λx. A *v x)"
  unfolding col_space_eq by auto

lemma row_space_eq:
  fixes A::"'a::{field}^'m^'n::{finite, wellorder}"
  shows "row_space A = {w. ∃y. (transpose A) *v y = w}"
  unfolding row_space_eq_col_space_transpose col_space_eq ..

lemma null_space_eq_ker:
  fixes f::"('a::field^'n) => ('a^'m)"
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
  shows "null_space (matrix f) = {x. f x = 0}" 
  unfolding null_space_def using matrix_works [OF lf] by auto

lemma col_space_eq_range:
  fixes f::"('a::field^'n::{finite, wellorder}) ⇒ ('a^'m)"
  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
  shows "col_space (matrix f) = range f"
  unfolding col_space_eq unfolding matrix_works[OF lf] by blast

lemma null_space_is_preserved:
  fixes A::"'a::{field}^'cols^'rows"
  assumes P: "invertible P"
  shows "null_space (P**A) = null_space A"
  unfolding null_space_def 
  using P matrix_inv_left matrix_left_invertible_ker matrix_vector_mul_assoc matrix_vector_mult_0_right
  by metis

lemma row_space_is_preserved:
  fixes A::"'a::{field}^'cols^'rows::{finite, wellorder}" 
    and P::"'a::{field}^'rows::{finite, wellorder}^'rows::{finite, wellorder}"
  assumes P: "invertible P"
  shows "row_space (P**A) = row_space A"
proof (auto)
  fix w
  assume w: "w ∈ row_space (P**A)"
  from this obtain y where w_By: "w=(transpose (P**A)) *v y" 
    unfolding row_space_eq[of "P ** A" ] by fast
  have "w = (transpose (P**A)) *v y" using w_By .
  also have "... = ((transpose A) ** (transpose P)) *v y" unfolding matrix_transpose_mul ..
  also have "... = (transpose A) *v ((transpose P) *v y)" unfolding matrix_vector_mul_assoc ..
  finally show "w ∈ row_space A" unfolding row_space_eq by blast
next
  fix w
  assume w: "w ∈ row_space A"
  from this obtain y where w_Ay: "w=(transpose A) *v y" unfolding row_space_eq by fast
  have "w = (transpose A) *v y" using w_Ay .
  also have "... = (transpose ((matrix_inv P) ** (P**A))) *v y" 
    by (metis P matrix_inv_left matrix_mul_assoc matrix_mul_lid)
  also have "... = (transpose (P**A) ** (transpose (matrix_inv P))) *v y" 
    unfolding matrix_transpose_mul ..
  also have "... = transpose (P**A) *v (transpose (matrix_inv P) *v y)" 
    unfolding matrix_vector_mul_assoc ..
  finally show "w ∈ row_space (P**A)"  unfolding row_space_eq by blast
qed
end