Theory Rank_Nullity_Theorem.Dim_Formula
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"
proof (unfold inj_on_def, rule+, rule ccontr)
interpret lf: Vector_Spaces.linear scaleB scaleC f using lf by simp
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
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
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
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)
hence "dependent C" using C_eq x y
by (metis Un_commute Un_upper2 dependent_mono insert_absorb insert_subset)
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 -
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}"
have sub_ker: "subspace {x. f x = 0}" using l.subspace_kernel .
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
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)
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)
have finite_C: "finite C"
using finiteI_independent[OF independent_C] .
have finite_fC: "finite (f ` C)" by (rule finite_imageI [OF finite_C])
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])
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
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 ..
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)"
proof (rule l.vs2.basis_card_eq_dim)
show "range f ⊆ l.vs2.span (f ` W)"
proof (unfold l.vs2.span_finite [OF finite_fW], auto)
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
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
finally show "f v ∈ range (λu. ∑v∈f ` W. scaleC (u v) v)" by auto
qed
show "l.vs2.independent (f ` W)"
using finite_fW
proof (rule l.vs2.independent_if_scalars_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