Theory Rank_Nullity_Theorem.Dim_Formula

(*  
    Title:      Dim_Formula.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 "Rank Nullity Theorem of Linear Algebra"

theory Dim_Formula
  imports Fundamental_Subspaces
begin

context vector_space
begin

subsection‹Previous results›

text‹Linear dependency is a monotone property, based on the 
  monotonocity of linear independence:›

lemma dependent_mono:
  assumes d:"dependent A"
  and A_in_B: "A ⊆ B"
  shows  "dependent B"
  using independent_mono [OF _ A_in_B] d by auto

text‹Given a finite independent set, a linear combination of its 
  elements equal to zero is possible only if every coefficient is zero:›

lemma scalars_zero_if_independent:
  assumes fin_A: "finite A"
  and ind: "independent A"
  and sum: "(∑x∈A. scale (f x) x) = 0"
  shows "∀x ∈ A. f x = 0"
  using fin_A ind local.dependent_finite sum by blast

end

context finite_dimensional_vector_space
begin

text‹In an finite dimensional vector space, every independent set is finite, and 
  thus @{thm [display ]scalars_zero_if_independent [no_vars]} holds:›

corollary scalars_zero_if_independent_euclidean:
  assumes ind: "independent A"
    and sum: "(∑x∈A. scale (f x) x) = 0"
  shows "∀x ∈ A. f x = 0"
  using finiteI_independent ind scalars_zero_if_independent sum by blast

end

text‹The following lemma states that every linear form is injective over the 
  elements which define the basis of the range of the linear form. 
  This property is applied later over the elements of an arbitrary 
  basis which are not in the basis of the nullifier or kernel set 
  (\emph{i.e.}, the candidates to be the basis of the range space 
  of the linear form).›

text‹Thanks to this result, it can be concluded that the cardinal 
  of the elements of a basis which do not belong to the kernel 
  of a linear form @{term "f::'a => 'b"} is equal to the cardinal 
  of the set obtained when applying @{term "f::'a => 'b"} to such elements.›

text‹The application of this lemma is not usually found in the pencil and paper 
  proofs of the ``rank nullity theorem'', but will be crucial to know that,
  being @{term "f::'a => 'b"} a linear form from a finite dimensional
  vector space @{term "V"} to a vector space @{term "V'"}, 
  and given a basis @{term "B::'a set"} of @{term "ker f"}, 
  when @{term "B"} is completed up to a basis of @{term "V::'a set"}
  with a set @{term "W::'a set"}, the cardinal of this set is
  equal to the cardinal of its range set:›
  
context vector_space
begin

lemma inj_on_extended:
  assumes lf: "Vector_Spaces.linear scaleB scaleC f"
  and f: "finite C"
  and ind_C: "independent C"
  and C_eq: "C = B ∪ W"
  and disj_set: "B ∩ W = {}"
  and span_B: "{x. f x = 0} ⊆ span B"
  shows "inj_on f W"
  ― ‹The proof is carried out by reductio ad absurdum›
proof (unfold inj_on_def, rule+, rule ccontr)
  interpret lf: Vector_Spaces.linear scaleB scaleC f using lf by simp
  ― ‹Some previous consequences of the premises that are used later:›
  have fin_B: "finite B" using finite_subset [OF _ f] C_eq by simp  
  have ind_B: "independent B" and ind_W: "independent W" 
    using independent_mono[OF ind_C] C_eq by simp_all
  ― ‹The proof starts here; we assume that there exist two different elements›
  ― ‹with the same image:›
  fix x::'b and y::'b
  assume x: "x ∈ W" and y: "y ∈ W" and f_eq: "f x = f y" and x_not_y: "x ≠ y"
  have fin_yB: "finite (insert y B)" using fin_B by simp
  have "f (x - y) = 0" by (metis diff_self f_eq lf.diff)
  hence "x - y ∈ {x. f x = 0}" by simp
  hence "∃g. (∑v∈B. scale (g v) v) = (x - y)" using span_B
    unfolding span_finite [OF fin_B] by force
  then obtain g where sum: "(∑v∈B. scale (g v) v) = (x - y)" by blast
  ― ‹We define one of the elements as a linear combination of the second 
      element and the ones in $B$›
  define h :: "'b ⇒ 'a" where "h a = (if a = y then 1 else g a)" for a
  have "x = y + (∑v∈B. scale (g v) v)" using sum by auto
  also have "... = scale (h y) y  + (∑v∈B. scale (g v) v)" unfolding h_def by simp
  also have "... = scale (h y) y + (∑v∈B. scale (h v) v)"
    apply (unfold add_left_cancel, rule sum.cong) 
    using y h_def empty_iff disj_set by auto   
  also have "... = (∑v∈(insert y B). scale (h v) v)"
    by (rule sum.insert[symmetric], rule fin_B)
       (metis (lifting) IntI disj_set empty_iff y)
  finally have x_in_span_yB: "x ∈ span (insert y B)"
    unfolding span_finite[OF fin_yB] by auto
  ― ‹We have that a subset of elements of $C$ is linearly dependent›
  have dep: "dependent (insert x (insert y B))" 
    by (unfold dependent_def, rule bexI [of _ x])
       (metis Diff_insert_absorb Int_iff disj_set empty_iff insert_iff 
         x x_in_span_yB x_not_y, simp)
  ― ‹Therefore, the set $C$ is also dependent:›
  hence "dependent C" using C_eq x y
    by (metis Un_commute Un_upper2 dependent_mono insert_absorb insert_subset)
  ― ‹This yields the contradiction, since $C$ is independent:›
  thus False using ind_C by contradiction
qed
end

subsection‹The proof›

text‹Now the rank nullity theorem can be proved; given any linear form 
  @{term "f::'a => 'b"}, the sum of the dimensions of its kernel and 
  range subspaces is equal to the dimension of the source vector space.›

text‹The statement of the ``rank nullity theorem for linear algebra'', as 
  well as its proof, follow the ones on~\<^cite>‹"AX97"›. The proof is the 
  traditional one found in the literature. The theorem is also named 
  ``fundamental theorem of linear algebra'' in some texts (for instance,
  in~\<^cite>‹"GO10"›).›

context finite_dimensional_vector_space
begin

theorem rank_nullity_theorem:
  assumes l: "Vector_Spaces.linear scale scaleC f"
  shows "dimension = dim {x. f x = 0} + vector_space.dim scaleC (range f)"
proof -
  ― ‹For convenience we define abbreviations for the universe set, $V$, 
    and the kernel of $f$›
  interpret l: Vector_Spaces.linear scale scaleC f by fact
  define V :: "'b set" where "V = UNIV"
  define ker_f where "ker_f = {x. f x = 0}"
  ― ‹The kernel is a proper subspace:›
  have sub_ker: "subspace {x. f x = 0}" using l.subspace_kernel .
  ― ‹The kernel has its proper basis, $B$:›
  obtain B where B_in_ker: "B ⊆ {x. f x = 0}"
    and independent_B: "independent B"
    and ker_in_span:"{x. f x = 0} ⊆ span B"
    and card_B: "card B = dim {x. f x = 0}" using basis_exists by blast
  ― ‹The space $V$ has a (finite dimensional) basis, $C$:›
  obtain C where B_in_C: "B ⊆ C" and C_in_V: "C ⊆ V" 
    and independent_C: "independent C"
    and span_C: "V = span C"
    unfolding V_def
    by (metis independent_B extend_basis_superset independent_extend_basis span_extend_basis span_superset)
  ― ‹The basis of $V$, $C$, can be decomposed in the disjoint union of the 
      basis of the kernel, $B$, and its complementary set, $C - B$›
  have C_eq: "C = B ∪ (C - B)" by (rule Diff_partition [OF B_in_C, symmetric])
  have eq_fC: "f ` C = f ` B ∪ f ` (C - B)" 
    by (subst C_eq, unfold image_Un, simp) 
  ― ‹The basis $C$, and its image, are finite, since $V$ is finite-dimensional›
  have finite_C: "finite C"
    using finiteI_independent[OF independent_C] .
  have finite_fC: "finite (f ` C)" by (rule finite_imageI [OF finite_C])
  ― ‹The basis $B$ of the kernel of $f$, and its image, are also finite›
  have finite_B: "finite B" by (rule rev_finite_subset [OF finite_C B_in_C])
  have finite_fB: "finite (f ` B)" by (rule finite_imageI[OF finite_B])
  ― ‹The set $C - B$ is also finite›
  have finite_CB: "finite (C - B)" by (rule finite_Diff [OF finite_C, of B])
  have dim_ker_le_dim_V:"dim (ker_f) ≤ dim V" 
    using dim_subset [of ker_f V] unfolding V_def by simp
  ― ‹Here it starts the proof of the theorem: the sets $B$ and 
      $C - B$ must be proven to be bases, respectively, of the kernel 
      of $f$ and its range›
  show ?thesis
  proof -
    have "dimension = dim V" unfolding V_def dim_UNIV dimension_def
      by (metis basis_card_eq_dim dimension_def independent_Basis span_Basis top_greatest)
    also have "dim V = dim C" unfolding span_C dim_span ..
    also have "... = card C"
      using basis_card_eq_dim [of C C, OF _ span_superset independent_C] by simp
    also have "... = card (B ∪ (C - B))" using C_eq by simp
    also have "... = card B + card (C-B)"
      by (rule card_Un_disjoint[OF finite_B finite_CB], fast)
    also have "... = dim ker_f + card (C-B)" unfolding ker_f_def card_B ..
    ― ‹Now it has to be proved that the elements of $C - B$ are a basis of 
      the range of $f$›
    also have "... = dim ker_f + l.vs2.dim (range f)"
    proof (unfold add_left_cancel)
      define W where "W = C - B"
      have finite_W: "finite W" unfolding W_def using finite_CB .
      have finite_fW: "finite (f ` W)" using finite_imageI[OF finite_W] .
      have "card W = card (f ` W)" 
        by (rule card_image [symmetric], rule inj_on_extended[OF l, of C B], rule finite_C)
          (rule independent_C,unfold W_def, subst C_eq, rule refl, simp, rule ker_in_span)
      also have "... = l.vs2.dim (range f)"
        ― ‹The image set of $W$ is independent and its span contains the range 
             of $f$, so it is a basis of the range:›
      proof (rule l.vs2.basis_card_eq_dim)
        ― ‹1. The image set of $W$ generates the range of $f$:›
        show "range f ⊆ l.vs2.span (f ` W)"
        proof (unfold l.vs2.span_finite [OF finite_fW], auto)
          ― ‹Given any element $v$ in $V$, its image can be expressed as a 
            linear combination of elements of the image by $f$ of $C$:›
          fix v :: 'b
          have fV_span: "f ` V ⊆ l.vs2.span  (f ` C)"
            by (simp add: span_C l.span_image)
          have "∃g. (∑x∈f`C. scaleC (g x) x) = f v"
            using fV_span unfolding V_def
            using l.vs2.span_finite[OF finite_fC]
            by (metis (no_types, lifting) V_def rangeE rangeI span_C l.span_image)
          then obtain g where fv: "f v = (∑x∈f ` C. scaleC (g x) x)" by metis
              ― ‹We recall that $C$ is equal to $B$ union $(C - B)$, and $B$ 
            is the basis of the kernel; thus, the image of the elements of 
            $B$ will be equal to zero:›
          have zero_fB: "(∑x∈f ` B. scaleC (g x) x) = 0"
            using B_in_ker by (auto intro!: sum.neutral)
          have zero_inter: "(∑x∈(f ` B ∩ f ` W). scaleC (g x) x) = 0"
            using B_in_ker by (auto intro!: sum.neutral)
          have "f v = (∑x∈f ` C. scaleC (g x) x)" using fv .
          also have "... = (∑x∈(f ` B ∪ f ` W).  scaleC (g x) x)" 
            using eq_fC W_def by simp
          also have "... = 
              (∑x∈f ` B. scaleC (g x) x) + (∑x∈f ` W. scaleC (g x) x) 
                - (∑x∈(f ` B ∩ f ` W). scaleC (g x) x)" 
            using sum_Un [OF finite_fB finite_fW] by simp
          also have "... = (∑x∈f ` W. scaleC (g x) x)" 
            unfolding zero_fB zero_inter by simp
              ― ‹We have proved that the image set of $W$ is a generating set 
              of the range of $f$›
          finally show "f v ∈ range (λu. ∑v∈f ` W. scaleC (u v) v)" by auto
        qed
          ― ‹2. The image set of $W$ is linearly independent:›
        show "l.vs2.independent (f ` W)"
          using finite_fW
        proof (rule l.vs2.independent_if_scalars_zero)
          ― ‹Every linear combination (given by $g x$) of the elements of 
           the image set of $W$ equal to zero, requires every coefficient to 
           be zero:›
          fix g :: "'c => 'a" and w :: 'c
          assume sum: "(∑x∈f ` W. scaleC (g x) x) = 0" and w: "w ∈ f ` W"
          have "0 = (∑x∈f ` W. scaleC (g x) x)" using sum by simp
          also have "... = sum ((λx. scaleC (g x) x) ∘ f) W"
            by (rule sum.reindex, rule inj_on_extended[OF l, of C B])
              (unfold W_def, rule finite_C, rule independent_C, rule C_eq, simp, 
                rule ker_in_span)
          also have "... = (∑x∈W. scaleC ((g ∘ f) x) (f x))" unfolding o_def ..
          also have "... = f (∑x∈W. scale ((g ∘ f) x) x)"
            unfolding l.sum[symmetric] l.scale[symmetric] by simp
          finally have f_sum_zero:"f (∑x∈W. scale ((g ∘ f) x) x) = 0" by (rule sym)
          hence "(∑x∈W. scale ((g ∘ f) x) x) ∈ ker_f" unfolding ker_f_def by simp
          hence "∃h. (∑v∈B. scale (h v) v) = (∑x∈W. scale ((g ∘ f) x) x)"
            using span_finite[OF finite_B] using ker_in_span
            unfolding ker_f_def by force
          then obtain h where 
            sum_h: "(∑v∈B. scale (h v) v) = (∑x∈W. scale ((g ∘ f) x) x)" by blast
          define t where "t a = (if a ∈ B then h a else - ((g ∘ f) a))" for a
          have "0 = (∑v∈B. scale (h v) v) + - (∑x∈W. scale ((g ∘ f) x) x)" 
            using sum_h by simp
          also have "... =  (∑v∈B. scale (h v) v) + (∑x∈W. - (scale ((g ∘ f) x) x))" 
            unfolding sum_negf ..
          also have "... = (∑v∈B. scale (t v) v) + (∑x∈W. -(scale((g ∘ f) x) x))" 
            unfolding add_right_cancel unfolding t_def by simp
          also have "... =  (∑v∈B. scale (t v) v) + (∑x∈W. scale (t x) x)"
            by (unfold add_left_cancel t_def W_def, rule sum.cong) simp+
          also have "... = (∑v∈B ∪ W. scale (t v) v)"
            by (rule sum.union_inter_neutral [symmetric], rule finite_B, rule finite_W) 
              (simp add: W_def)
          finally have "(∑v∈B ∪ W. scale (t v) v) = 0" by simp
          hence coef_zero: "∀x∈B ∪ W. t x = 0"
            using C_eq scalars_zero_if_independent [OF finite_C independent_C]
            unfolding W_def by simp
          obtain y where w_fy: "w = f y " and y_in_W: "y ∈ W" using w by fast
          have "- g w = t y" 
            unfolding t_def w_fy using y_in_W unfolding W_def by simp
          also have "... = 0" using coef_zero y_in_W unfolding W_def by simp
          finally show "g w = 0" by simp
        qed
      qed auto
      finally show "card (C - B) = l.vs2.dim (range f)" unfolding W_def .
    qed
    finally show ?thesis unfolding V_def ker_f_def unfolding dim_UNIV .
  qed
qed

end

subsection‹The rank nullity theorem for matrices›

text‹The proof of the theorem for matrices
  is direct, as a consequence of the ``rank nullity theorem''.›

lemma rank_nullity_theorem_matrices:
  fixes A::"'a::{field}^'cols::{finite, wellorder}^'rows"
  shows "ncols A = vec.dim (null_space A) + vec.dim (col_space A)"
  using vec.rank_nullity_theorem[OF matrix_vector_mul_linear_gen, of A]
  apply (subst (2 3) matrix_of_matrix_vector_mul [of A, symmetric])
  unfolding null_space_eq_ker[OF matrix_vector_mul_linear_gen]
  unfolding col_space_eq_range [OF matrix_vector_mul_linear_gen]
  unfolding vec.dimension_def ncols_def card_cart_basis
  by simp

end