Theory Rank_Nullity

section ‹The rank--nullity theorem›

theory Rank_Nullity
  imports Steinitz Module_Homomorphism
begin

text ‹As in the module-homomorphism theory, suppress HOL arithmetic syntax while binding the
  scalar-ring operations in the locale header.›
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax

text ‹A linear map is a module homomorphism between vector spaces over the same scalar field.›

locale linear_map =
  source: Vector_Space R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" +
  target: Vector_Space R "(+)" "(⋅)" 𝟬 𝟭 "(⊕⇩2)" "𝟬⇩2" M' "(⊙⇩2)" +
  hom: module_homomorphism
    R "(+)" "(⋅)" 𝟬 𝟭
    M "(⊕)" "𝟬⇩M" "(⊙)"
    M' "(⊕⇩2)" "𝟬⇩2" "(⊙⇩2)" η
  for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70)
    and zero (‹𝟬›) and unit (‹𝟭›)
    and M and madd (infixl ‹⊕› 65) and mzero (‹𝟬⇩M›)
    and scale (infixr ‹⊙› 75)
    and M' and madd' (infixl ‹⊕⇩2› 65) and mzero' (‹𝟬⇩2›)
    and scale' (infixr ‹⊙⇩2› 75) and η
begin

text ‹The kernel and image inherit vector-space structures from the source and target.›

sublocale kernel: vector_subspace
  R "(+)" "(⋅)" "𝟬" "𝟭" "(⊕)" "𝟬⇩M" M "(⊙)" hom.Ker
proof
  show "source.mod.submodule hom.Ker" by (rule hom.Ker_submodule)
qed

sublocale image: vector_subspace
  R "(+)" "(⋅)" "𝟬" "𝟭" "(⊕⇩2)" "𝟬⇩2" M' "(⊙⇩2)" "η ` M"
proof
  show "target.mod.submodule (η ` M)" by (rule hom.image_submodule)
qed

text ‹Reindex a target linear combination over the images of a finite set.  Injectivity is
  exactly what makes the transported coefficient function unambiguous.›

lemma image_lincomb_reindex:
  assumes finD: "finite D" and DM: "D ⊆ M" and inj: "inj_on η D"
    and c: "⋀v. v ∈ D ⟹ c v ∈ R"
  defines "d ≡ λy. c (inv_into D η y)"
  shows "image.sub.lincomb d (η ` D) =
    target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
proof -
  have imageD: "η ` D ⊆ η ` M" using DM by blast
  have dR: "⋀y. y ∈ η ` D ⟹ d y ∈ R"
    using inj c by (auto simp: d_def inv_into_f_f)
  have terms: "(λy. d y ⊙⇩2 y) ∈ η ` D → M'"
    using imageD dR by (auto intro!: target.scale_closed)
  have "image.sub.lincomb d (η ` D) = target.lincomb d (η ` D)"
    by (rule image.sub_lincomb_eq) (use finD imageD dR in auto)
  also have "… = target.vadd.fincomp (λy. d y ⊙⇩2 y) (η ` D)"
    by (simp add: target.lincomb_def)
  also have "… = target.vadd.fincomp (λv. d (η v) ⊙⇩2 η v) D"
    by (rule target.vadd.fincomp_reindex[OF terms inj])
  also have "… = target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
    by (rule target.vadd.fincomp_cong')
       (use DM inj c in ‹auto simp: d_def inv_into_f_f intro!: target.scale_closed hom.hom_closed›)
  finally show ?thesis .
qed

text ‹Once a kernel basis has been extended to a source basis, the map is injective on the
  complementary basis vectors.  Equality of two images puts their difference in the kernel; the
  kernel basis would then express either vector in the span of the remaining source basis.›

lemma injective_on_basis_complement:
  assumes A: "kernel.sub.basis A" and C: "source.basis C" and AC: "A ⊆ C"
  shows "inj_on η (C ∖ A)"
proof (rule inj_onI)
  fix x y
  assume x: "x ∈ C ∖ A" and y: "y ∈ C ∖ A" and eq: "η x = η y"
  have CM: "C ⊆ M" using C by (simp add: source.basis_def)
  have xM: "x ∈ M" and yM: "y ∈ M" using x y CM by auto
  define z where "z = x ⊕ source.vadd.inverse y"
  have zM: "z ∈ M" using xM yM by (simp add: z_def)
  have "η z = η x ⊕⇩2 η (source.vadd.inverse y)"
    using xM yM by (simp add: z_def hom.hom_add)
  also have "… = η x ⊕⇩2 target.vadd.inverse (η y)"
    using yM by (simp add: hom.hom_neg)
  also have "… = 𝟬⇩2" using eq xM yM by (simp add: hom.hom_closed)
  finally have zKer: "z ∈ hom.Ker" using zM by (rule hom.Ker_memI)
  have AKer: "A ⊆ hom.Ker" using A by (simp add: kernel.sub.basis_def)
  have z_sub_span: "z ∈ kernel.sub.span A"
    using kernel.sub.basis_spanning[OF A] zKer by (rule kernel.sub.spanning_span_all)
  have z_span: "z ∈ source.span A"
    using z_sub_span kernel.sub_span_eq[OF AKer] by simp
  show "x = y"
  proof (rule ccontr)
    assume xy: "x ≠ y"
    have AM: "A ⊆ M" using AKer hom.Ker_subset by blast
    have insM: "insert y A ⊆ M" using yM AM by simp
    have z_ins: "z ∈ source.span (insert y A)"
      using z_span source.span_mono[of A "insert y A"] by blast
    have y_ins: "y ∈ source.span (insert y A)" by (rule source.span_incl[OF insM]) simp
    have "z ⊕ y ∈ source.span (insert y A)"
      by (rule source.span_vadd[OF insM z_ins y_ins])
    moreover have "z ⊕ y = x" using xM yM by (simp add: z_def source.vadd.associative)
    ultimately have "x ∈ source.span (insert y A)" by simp
    moreover have "insert y A ⊆ C ∖ {x}" using AC x y xy by auto
    ultimately have "x ∈ source.span (C ∖ {x})" using source.span_mono by blast
    moreover have "source.lin_indep C" using C by (rule source.basis_lin_indep)
    ultimately show False using x by (simp add: source.lin_indep_not_in_span)
  qed
qed

text ‹Split a linear combination over a basis into a chosen subset and its complement.›

lemma source_lincomb_diff:
  assumes finC: "finite C" and CM: "C ⊆ M" and AC: "A ⊆ C"
    and c: "⋀v. v ∈ C ⟹ c v ∈ R"
  shows "source.lincomb c C =
    source.lincomb c A ⊕ source.lincomb c (C ∖ A)"
proof -
  have finA: "finite A" and finD: "finite (C ∖ A)" using finC AC by (auto intro: finite_subset)
  have C_eq: "C = A ∪ (C ∖ A)" using AC by auto
  have A_terms: "(λv. c v ⊙ v) ∈ A → M"
    using AC CM c by (auto intro!: source.scale_closed)
  have D_terms: "(λv. c v ⊙ v) ∈ C ∖ A → M"
    using CM c by (auto intro!: source.scale_closed)
  have "source.lincomb c C = source.lincomb c (A ∪ (C ∖ A))"
    by (rule arg_cong[OF C_eq])
  also have "… = source.lincomb c A ⊕ source.lincomb c (C ∖ A)"
    unfolding source.lincomb_def
    by (rule source.vadd.fincomp_Un_disjoint[OF finA finD])
       (use A_terms D_terms in auto)
  finally show ?thesis .
qed

text ‹The images of the complementary basis vectors form a basis of the image.›

lemma image_basis_complement:
  assumes A: "kernel.sub.basis A" and C: "source.basis C" and AC: "A ⊆ C"
  defines "D ≡ C ∖ A"
  shows "image.sub.basis (η ` D)"
proof -
  have finC: "finite C" and CM: "C ⊆ M" using C by (auto simp: source.basis_def)
  have finD: "finite D" and DM: "D ⊆ M" using finC CM by (auto simp: D_def)
  have finA: "finite A" by (rule finite_subset[OF AC finC])
  have DC: "D ⊆ C" by (simp add: D_def)
  have AKer: "A ⊆ hom.Ker" using A by (simp add: kernel.sub.basis_def)
  have AM: "A ⊆ M" using AKer hom.Ker_subset by blast
  have injD: "inj_on η D"
    using injective_on_basis_complement[OF A C AC] by (simp add: D_def)
  have imageDM: "η ` D ⊆ η ` M" using DM by blast
  have fin_imageD: "finite (η ` D)" using finD by simp
  show ?thesis
  proof (rule image.sub.basisI)
    show "image.sub.spanning (η ` D)"
      unfolding image.sub.spanning_iff_mod_spanning[OF fin_imageD imageDM]
    proof (rule image.sub.mod.spanningI[OF imageDM])
      fix z assume "z ∈ η ` M"
      then obtain x where xM: "x ∈ M" and z: "z = η x" by blast
      obtain c where c: "c ∈ C →⇩E R" "x = source.lincomb c C"
        using source.basis_spanning[OF C] xM unfolding source.spanning_def by blast
      have cR: "⋀v. v ∈ C ⟹ c v ∈ R" using c(1) by auto
      have cA: "⋀v. v ∈ A ⟹ c v ∈ R" using AC cR by blast
      have cD: "⋀v. v ∈ D ⟹ c v ∈ R" using cR by (simp add: D_def)
      have split: "source.lincomb c C = source.lincomb c A ⊕ source.lincomb c D"
        using source_lincomb_diff[OF finC CM AC cR] by (simp add: D_def)
      have subA_closed: "kernel.sub.lincomb c A ∈ hom.Ker"
        by (rule kernel.sub.lincomb_closed[OF AKer cA])
      have ambientA: "source.lincomb c A = kernel.sub.lincomb c A"
        by (rule kernel.sub_lincomb_eq[OF finA AKer cA, symmetric])
      have linA_Ker: "source.lincomb c A ∈ hom.Ker" using subA_closed ambientA by simp
      have linA_M: "source.lincomb c A ∈ M" using AM cA by (rule source.lincomb_closed)
      have linD_M: "source.lincomb c D ∈ M" using DM cD by (rule source.lincomb_closed)
      have map_split: "η x = η (source.lincomb c D)"
      proof -
        have "η x = η (source.lincomb c A ⊕ source.lincomb c D)" using c(2) split by simp
        also have "… = η (source.lincomb c A) ⊕⇩2 η (source.lincomb c D)"
          by (rule hom.hom_add[OF linA_M linD_M])
        also have "η (source.lincomb c A) = 𝟬⇩2" using linA_Ker by (rule hom.Ker_image)
        also have "𝟬⇩2 ⊕⇩2 η (source.lincomb c D) = η (source.lincomb c D)"
          using linD_M by (simp add: hom.hom_closed)
        finally show ?thesis .
      qed
      define d where "d = (λy. c (inv_into D η y))"
      have dR: "⋀y. y ∈ η ` D ⟹ d y ∈ R"
        using injD cD by (auto simp: d_def inv_into_f_f)
      have image_sum: "image.sub.lincomb d (η ` D) =
          target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
      proof -
        have "image.sub.lincomb (λy. c (inv_into D η y)) (η ` D) =
            target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
          by (rule image_lincomb_reindex[OF finD DM injD cD])
        then show ?thesis by (simp add: d_def)
      qed
      have map_sum: "η (source.lincomb c D) =
          target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
        by (rule hom.hom_lincomb[OF finD DM cD])
      have z_eq: "z = image.sub.lincomb d (η ` D)"
        using z map_split map_sum image_sum by simp
      show "z ∈ image.sub.span (η ` D)"
      proof (rule image.sub.mod.spanI[where c=d and A="η ` D"])
        show "finite (η ` D)" by (rule fin_imageD)
        show "η ` D ⊆ η ` D" by simp
        show "image.sub.mod.coeffs_on d (η ` D)"
          using dR by (rule image.sub.mod.coeffs_onI)
        show "z = image.sub.lincomb d (η ` D)" by (rule z_eq)
      qed
    qed
  next
    show "image.sub.lin_indep (η ` D)"
      unfolding image.sub.lin_indep_def
    proof (intro conjI ballI impI fin_imageD imageDM)
      fix d y
      assume d: "d ∈ η ` D →⇩E R"
        and zero: "image.sub.lincomb d (η ` D) = 𝟬⇩2" and y: "y ∈ η ` D"
      define c where "c = (λv. d (η v))"
      have cR: "⋀v. v ∈ D ⟹ c v ∈ R" using d by (auto simp: c_def)
      define e where "e = (λz. c (inv_into D η z))"
      have ed: "⋀z. z ∈ η ` D ⟹ e z = d z"
        using injD by (auto simp: e_def c_def inv_into_f_f)
      have image_eq: "image.sub.lincomb e (η ` D) = image.sub.lincomb d (η ` D)"
      proof (rule image.sub.lincomb_cong)
        show "η ` D ⊆ η ` M" by (rule imageDM)
        show "⋀z. z ∈ η ` D ⟹ d z ∈ R" using d by auto
        show "⋀z. z ∈ η ` D ⟹ e z = d z" by (rule ed)
      qed
      have image_sum: "image.sub.lincomb e (η ` D) =
          target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
      proof -
        have "image.sub.lincomb (λz. c (inv_into D η z)) (η ` D) =
            target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
          by (rule image_lincomb_reindex[OF finD DM injD cR])
        then show ?thesis by (simp add: e_def)
      qed
      have map_zero: "η (source.lincomb c D) = 𝟬⇩2"
      proof -
        have "η (source.lincomb c D) =
            target.vadd.fincomp (λv. c v ⊙⇩2 η v) D"
          by (rule hom.hom_lincomb[OF finD DM cR])
        also have "… = image.sub.lincomb e (η ` D)" using image_sum by simp
        also have "… = image.sub.lincomb d (η ` D)" by (rule image_eq)
        also have "… = 𝟬⇩2" by (rule zero)
        finally show ?thesis .
      qed
      have linD_M: "source.lincomb c D ∈ M" using DM cR by (rule source.lincomb_closed)
      have linD_Ker: "source.lincomb c D ∈ hom.Ker" by (rule hom.Ker_memI[OF map_zero linD_M])
      obtain a where a: "a ∈ A →⇩E R"
        "source.lincomb c D = kernel.sub.lincomb a A"
        using kernel.sub.basis_spanning[OF A] linD_Ker
        unfolding kernel.sub.spanning_def by blast
      have aR: "⋀v. v ∈ A ⟹ a v ∈ R" using a(1) by auto
      have sourceA: "kernel.sub.lincomb a A = source.lincomb a A"
        by (rule kernel.sub_lincomb_eq[OF finA AKer aR])
      have eq_comb: "source.lincomb c D = source.lincomb a A" using a(2) sourceA by simp
      have source_ind: "source.mod.lin_indep C"
        using source.basis_lin_indep[OF C] source.lin_indep_iff_mod_lin_indep[OF finC CM] by simp
      have c_coeff: "source.mod.coeffs_on c D" using cR by (rule source.mod.coeffs_onI)
      have a_coeff: "source.mod.coeffs_on a A" using aR by (rule source.mod.coeffs_onI)
      obtain v where v: "v ∈ D" "y = η v" using y by blast
      have coord_eq: "(if v ∈ D then c v else 𝟬) = (if v ∈ A then a v else 𝟬)"
        by (rule source.mod.lin_indep_lincomb_unique_gen
            [OF source_ind finD DC finA AC c_coeff a_coeff eq_comb])
      have "c v = 𝟬" using coord_eq v by (simp add: D_def)
      then show "d y = 𝟬" using v by (simp add: c_def)
    qed
  qed
qed

text ‹Rank--nullity follows by extending a basis of the kernel to a basis of the
  source.  The complementary vectors map bijectively to a basis of the image.›

theorem rank_nullity:
  assumes B: "source.basis B"
  shows "plus kernel.sub.dimension image.sub.dimension = source.dimension"
proof -
  obtain A where A: "kernel.sub.basis A"
    using kernel.subspace_basis_exists[OF B] by blast
  have AKer: "A ⊆ hom.Ker" using A by (simp add: kernel.sub.basis_def)
  have source_ind: "source.lin_indep A"
    using kernel.sub.basis_lin_indep[OF A] kernel.sub_lin_indep_iff[OF AKer] by simp
  obtain C where AC: "A ⊆ C" and C: "source.basis C"
    using source.basis_extension[OF source_ind B] by blast
  have image_basis: "image.sub.basis (η ` (C ∖ A))"
    by (rule image_basis_complement[OF A C AC])
  have finC: "finite C" using C by (simp add: source.basis_def)
  have inj: "inj_on η (C ∖ A)"
    by (rule injective_on_basis_complement[OF A C AC])
  have image_card: "card (η ` (C ∖ A)) = card (C ∖ A)"
    by (rule card_image[OF inj])
  have card_split: "plus (card A) (card (C ∖ A)) = card C"
  proof -
    have finA: "finite A" by (rule finite_subset[OF AC finC])
    have finD: "finite (C ∖ A)" using finC by simp
    have "card (A ∪ (C ∖ A)) = plus (card A) (card (C ∖ A))"
      by (rule card_Un_disjoint[OF finA finD]) simp
    moreover have "A ∪ (C ∖ A) = C" using AC by auto
    ultimately show ?thesis by simp
  qed
  have "kernel.sub.dimension = card A"
    by (rule kernel.sub.dimension_eq_any_field[OF A])
  moreover have "image.sub.dimension = card (C ∖ A)"
    using image.sub.dimension_eq_any_field[OF image_basis] image_card by simp
  moreover have "source.dimension = card C"
    by (rule source.dimension_eq_any_field[OF C])
  ultimately show ?thesis using card_split by simp
qed

text ‹A bijective linear map preserves dimension.  Its kernel is the trivial subspace, so the
  image of any source basis is a basis of the entire target.›

theorem dimension_eq_of_bij_betw:
  assumes B: "source.basis B" and bij: "bij_betw η M M'"
  shows "source.dimension = target.dimension"
proof -
  have injM: "inj_on η M" and imageM: "η ` M = M'"
    using bij by (auto simp: bij_betw_def)
  have ker: "hom.Ker = {𝟬⇩M}"
    using injM hom.injective_iff_kernel_trivial by simp
  have empty_basis: "kernel.sub.basis {}"
    by (rule kernel.sub.basis_empty_trivial[OF ker])
  have image_basis: "image.sub.basis (η ` B)"
    using image_basis_complement[OF empty_basis B] by simp
  have target_basis: "target.basis (η ` B)" using image_basis imageM by simp
  have BM: "B ⊆ M" using B by (simp add: source.basis_def)
  have injB: "inj_on η B" using injM BM by (rule inj_on_subset)
  have card_image: "card (η ` B) = card B" by (rule card_image[OF injB])
  show ?thesis
    using source.dimension_eq_any_field[OF B]
      target.dimension_eq_any_field[OF target_basis] card_image by simp
qed

subsection ‹Finite-dimensional consequences›

text ‹Rank--nullity immediately bounds both the kernel and the image by the source
  dimension.  These named forms avoid making clients repeat arithmetic reasoning about the
  decomposition.›

corollary kernel_dimension_le:
  assumes B: "source.basis B"
  shows "kernel.sub.dimension ≤ source.dimension"
  using rank_nullity[OF B] by presburger

corollary image_dimension_le:
  assumes B: "source.basis B"
  shows "image.sub.dimension ≤ source.dimension"
  using rank_nullity[OF B] by presburger

text ‹An injective map has trivial kernel, so rank--nullity identifies the source dimension
  with the image dimension.›

theorem image_dimension_eq_of_injective:
  assumes B: "source.basis B" and inj: "inj_on η M"
  shows "image.sub.dimension = source.dimension"
proof -
  have ker: "hom.Ker = {𝟬⇩M}"
    using inj hom.injective_iff_kernel_trivial by simp
  have ker_dim: "kernel.sub.dimension = 0"
    using kernel.subspace_dimension_eq_zero_iff[OF B] ker by simp
  show ?thesis using rank_nullity[OF B] ker_dim by simp
qed

text ‹Comparing the image of an injective map with the finite-dimensional target gives
  the expected dimension inequality.›

theorem source_dimension_le_of_injective:
  assumes B: "source.basis B" and C: "target.basis C" and inj: "inj_on η M"
  shows "source.dimension ≤ target.dimension"
proof -
  have image_eq: "image.sub.dimension = source.dimension"
    by (rule image_dimension_eq_of_injective[OF B inj])
  have "image.sub.dimension ≤ target.dimension"
    by (rule image.subspace_dimension_le[OF C])
  then show ?thesis using image_eq by simp
qed

text ‹A surjective map has the whole target as its image, so the image bound from
  rank--nullity compares the target dimension directly with the source dimension.›

theorem target_dimension_le_of_surjective:
  assumes B: "source.basis B" and surj: "η ` M = M'"
  shows "target.dimension ≤ source.dimension"
proof -
  have dim_image: "image.sub.dimension = target.dimension" using surj by simp
  show ?thesis using image_dimension_le[OF B] dim_image by simp
qed

text ‹For finite-dimensional spaces of equal dimension, a linear map is injective exactly
  when it is surjective.  Injectivity gives an image of full target dimension; conversely,
  surjectivity and rank--nullity force the kernel to have dimension zero.›

theorem injective_iff_surjective:
  assumes B: "source.basis B" and C: "target.basis C"
    and dim: "source.dimension = target.dimension"
  shows "inj_on η M ⟷ η ` M = M'"
proof
  assume inj: "inj_on η M"
  have image_source: "image.sub.dimension = source.dimension"
    by (rule image_dimension_eq_of_injective[OF B inj])
  have image_target: "image.sub.dimension = target.dimension"
    using image_source dim by simp
  show "η ` M = M'"
    using image.subspace_eq_ambient_iff_dimension_eq[OF C] image_target by blast
next
  assume surj: "η ` M = M'"
  have image_target: "image.sub.dimension = target.dimension" using surj by simp
  have image_source: "image.sub.dimension = source.dimension"
    using image_target dim by simp
  have ker_dim: "kernel.sub.dimension = 0"
    using rank_nullity[OF B] image_source by presburger
  have ker: "hom.Ker = {𝟬⇩M}"
    using kernel.subspace_dimension_eq_zero_iff[OF B] ker_dim by blast
  show "inj_on η M"
    using hom.injective_iff_kernel_trivial ker by simp
qed

end

notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax

end