# Theory Matrix_Kernel

(*
Author:      René Thiemann
*)
section ‹Matrix Kernel›

text ‹We define the kernel of a matrix $A$ and prove the following properties.

\begin{itemize}
\item The kernel stays invariant when multiplying $A$ with an invertible matrix from the left.
\item The dimension of the kernel stays invariant when
multiplying $A$ with an invertible matrix from the right.
\item The function find-base-vectors returns a basis of the kernel if $A$ is in row-echelon form.
\item The dimension of the kernel of a block-diagonal matrix is the sum of the dimensions of
the kernels of the blocks.
\item There is an executable algorithm which computes the dimension of the kernel of a matrix
(which just invokes Gauss-Jordan and then counts the number of pivot elements).
\end{itemize}
›

theory Matrix_Kernel
imports
VS_Connect
Missing_VectorSpace
Determinant
begin

hide_const real_vector.span
hide_const (open) Real_Vector_Spaces.span
hide_const real_vector.dim
hide_const (open) Real_Vector_Spaces.dim

definition mat_kernel :: "'a :: comm_ring_1 mat ⇒ 'a vec set" where
"mat_kernel A = { v . v ∈ carrier_vec (dim_col A) ∧ A *⇩v v = 0⇩v (dim_row A)}"

lemma mat_kernelI: assumes "A ∈ carrier_mat nr nc" "v ∈ carrier_vec nc" "A *⇩v v = 0⇩v nr"
shows "v ∈ mat_kernel A"
using assms unfolding mat_kernel_def by auto

lemma mat_kernelD: assumes "A ∈ carrier_mat nr nc" "v ∈ mat_kernel A"
shows "v ∈ carrier_vec nc" "A *⇩v v = 0⇩v nr"
using assms unfolding mat_kernel_def by auto

lemma mat_kernel: assumes "A ∈ carrier_mat nr nc"
shows "mat_kernel A = {v. v ∈ carrier_vec nc ∧ A *⇩v v = 0⇩v nr}"
unfolding mat_kernel_def using assms by auto

lemma mat_kernel_carrier:
assumes "A ∈ carrier_mat nr nc" shows "mat_kernel A ⊆ carrier_vec nc"
using assms mat_kernel by auto

lemma mat_kernel_mult_subset: assumes A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat n nr"
shows "mat_kernel A ⊆ mat_kernel (B * A)"
proof -
from A B have BA: "B * A ∈ carrier_mat n nc" by auto
show ?thesis unfolding mat_kernel[OF BA] mat_kernel[OF A] using A B by auto
qed

lemma mat_kernel_smult: assumes A: "A ∈ carrier_mat nr nc"
and v: "v ∈ mat_kernel A"
shows "a ⋅⇩v v ∈  mat_kernel A"
proof -
from mat_kernelD[OF A v] have v: "v ∈ carrier_vec nc"
and z: "A *⇩v v = 0⇩v nr" by auto
from arg_cong[OF z, of "λ v. a ⋅⇩v v"] v
have "a ⋅⇩v (A *⇩v v) = 0⇩v nr" by auto
also have "a ⋅⇩v (A *⇩v v) = A *⇩v (a ⋅⇩v v)" using A v by auto
finally show ?thesis using v A
by (intro mat_kernelI, auto)
qed

lemma mat_kernel_mult_eq: assumes A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nr"
and C: "C ∈ carrier_mat nr nr"
and inv: "C * B = 1⇩m nr"
shows "mat_kernel (B * A) = mat_kernel A"
proof
from B A have BA: "B * A ∈ carrier_mat nr nc" by auto
show "mat_kernel A ⊆ mat_kernel (B * A)" by (rule mat_kernel_mult_subset[OF A B])
{
fix v
assume v: "v ∈ mat_kernel (B * A)"
from mat_kernelD[OF BA this] have v: "v ∈ carrier_vec nc" and z: "B * A *⇩v v = 0⇩v nr" by auto
from arg_cong[OF z, of "λ v. C *⇩v v"]
have "C *⇩v (B * A *⇩v v) = 0⇩v nr" using C v by auto
also have "C *⇩v (B * A *⇩v v) = ((C * B) * A) *⇩v v"
unfolding assoc_mult_mat_vec[symmetric, OF C BA v]
unfolding assoc_mult_mat[OF C B A] by simp
also have "… = A *⇩v v" unfolding inv using A v by auto
finally have "v ∈ mat_kernel A"
by (intro mat_kernelI[OF A v])
}
thus "mat_kernel (B * A) ⊆ mat_kernel A" by auto
qed

locale kernel =
fixes nr :: nat
and nc :: nat
and A :: "'a :: field mat"
assumes A: "A ∈ carrier_mat nr nc"
begin

sublocale NC: vec_space "TYPE('a)" nc .

abbreviation "VK ≡ NC.V⦇carrier := mat_kernel A⦈"

sublocale Ker: vectorspace class_ring VK
rewrites "carrier VK = mat_kernel A"
and [simp]: "add VK = (+)"
and [simp]: "zero VK = 0⇩v nc"
and [simp]: "module.smult VK = (⋅⇩v)"
and "carrier class_ring = UNIV"
and "monoid.mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
and "finprod (class_ring :: 'a ring) = prod"
and "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)"
apply (intro vectorspace.intro)
apply (rule NC.submodule_is_module)
apply (unfold_locales)
by (insert A mult_add_distrib_mat_vec[OF A] mult_mat_vec[OF A] mat_kernel[OF A], auto simp: class_ring_simps)

abbreviation "basis ≡ Ker.basis"
abbreviation "span ≡ Ker.span"
abbreviation "lincomb ≡ Ker.lincomb"
abbreviation "dim ≡ Ker.dim"
abbreviation "lin_dep ≡ Ker.lin_dep"
abbreviation "lin_indpt ≡ Ker.lin_indpt"
abbreviation "gen_set ≡ Ker.gen_set"

lemma finsum_same:
assumes "f : S → mat_kernel A"
shows "finsum VK f S = finsum NC.V f S"
using assms
proof (induct S rule: infinite_finite_induct)
case (insert s S)
hence base: "finite S" "s ∉ S"
and f_VK: "f : S → mat_kernel A" "f s : mat_kernel A" by auto
hence f_NC: "f : S → carrier_vec nc" "f s : carrier_vec nc" using mat_kernel[OF A] by auto
have IH: "finsum VK f S = finsum NC.V f S" using insert f_VK by auto
thus ?case
unfolding NC.M.finsum_insert[OF base f_NC]
unfolding Ker.finsum_insert[OF base f_VK]
by simp
qed auto

lemma lincomb_same:
assumes S_kernel: "S ⊆ mat_kernel A"
shows "lincomb a S = NC.lincomb a S"
unfolding Ker.lincomb_def
unfolding NC.lincomb_def
apply(subst finsum_same)
using S_kernel Ker.smult_closed[unfolded module_vec_simps class_ring_simps] by auto

lemma span_same:
assumes S_kernel: "S ⊆ mat_kernel A"
shows "span S = NC.span S"
proof (rule;rule)
fix v assume L: "v : span S" show "v : NC.span S"
proof -
obtain a U where know: "finite U" "U ⊆ S" "a : U → UNIV" "v = lincomb a U"
using L unfolding Ker.span_def by auto
hence v: "v = NC.lincomb a U" using lincomb_same S_kernel by auto
show ?thesis
unfolding NC.span_def by (rule,intro exI conjI;fact)
qed
next fix v assume R: "v : NC.span S" show "v : span S"
proof -
obtain a U where know: "finite U" "U ⊆ S" "v = NC.lincomb a U"
using R unfolding NC.span_def by auto
hence v: "v = lincomb a U" using lincomb_same S_kernel by auto
show ?thesis unfolding Ker.span_def by (rule, intro exI conjI, insert v know, auto)
qed
qed

lemma lindep_same:
assumes S_kernel: "S ⊆ mat_kernel A"
shows "Ker.lin_dep S = NC.lin_dep S"
proof
note [simp] = module_vec_simps class_ring_simps
{ assume L: "Ker.lin_dep S"
then obtain v a U
where finU: "finite U" and US: "U ⊆ S"
and lc: "lincomb a U = 0⇩v nc"
and vU: "v ∈ U"
and av0: "a v ≠ 0"
unfolding Ker.lin_dep_def by auto
have lc': "NC.lincomb a U = 0⇩v nc"
using lc lincomb_same US S_kernel by auto
show "NC.lin_dep S" unfolding NC.lin_dep_def
by (intro exI conjI, insert finU US lc' vU av0, auto)
}
assume R: "NC.lin_dep S"
then obtain v a U
where finU: "finite U" and US: "U ⊆ S"
and lc: "NC.lincomb a U = 0⇩v nc"
and vU: "v : U"
and av0: "a v ≠ 0"
unfolding NC.lin_dep_def by auto
have lc': "lincomb a U = zero VK"
using lc lincomb_same US S_kernel by auto
show "Ker.lin_dep S" unfolding Ker.lin_dep_def
by (intro exI conjI,insert finU US lc' vU av0, auto)
qed

lemma lincomb_index:
assumes i: "i < nc"
and Xk: "X ⊆ mat_kernel A"
shows "lincomb a X $i = sum (λx. a x * x$ i) X"
proof -
have X: "X ⊆ carrier_vec nc" using Xk mat_kernel_def A by auto
show ?thesis
using vec_space.lincomb_index[OF i X]
using lincomb_same[OF Xk] by auto
qed

end

lemma find_base_vectors: assumes ref: "row_echelon_form A"
and A: "A ∈ carrier_mat nr nc" shows
"set (find_base_vectors A) ⊆ mat_kernel A"
"0⇩v nc ∉ set (find_base_vectors A)"
"kernel.basis nc A (set (find_base_vectors A))"
"card (set (find_base_vectors A)) = nc - card { i. i < nr ∧ row A i ≠ 0⇩v nc}"
"length (pivot_positions A) = card { i. i < nr ∧ row A i ≠ 0⇩v nc}"
"kernel.dim nc A = nc - card { i. i < nr ∧ row A i ≠ 0⇩v nc}"
proof -
note non_pivot_base = non_pivot_base[OF ref A]
let ?B = "set (find_base_vectors A)"
let ?pp = "set (pivot_positions A)"
from A have dim: "dim_row A = nr" "dim_col A = nc" by auto
from ref[unfolded row_echelon_form_def] obtain p
where pivot: "pivot_fun A p nc" using dim by auto
note piv = pivot_funD[OF dim(1) pivot]
{
fix v
assume "v ∈ ?B"
from this[unfolded find_base_vectors_def Let_def dim]
obtain c where c: "c < nc" "c ∉ snd  ?pp"
and res: "v = non_pivot_base A (pivot_positions A) c" by auto
from non_pivot_base[OF c, folded res] c
have "v ∈ mat_kernel A" "v ≠ 0⇩v nc"
by (intro mat_kernelI[OF A], auto)
}
thus sub: "?B ⊆ mat_kernel A" and
"0⇩v nc ∉ ?B" by auto
{
fix j j'
assume j: "j < nc" "j ∉ snd  ?pp" and j': "j' < nc" "j' ∉ snd  ?pp" and neq: "j' ≠ j"
from non_pivot_base(2)[OF j] non_pivot_base(4)[OF j' j neq]
have "non_pivot_base A (pivot_positions A) j ≠ non_pivot_base A (pivot_positions A) j'" by auto
}
hence inj: "inj_on (non_pivot_base A (pivot_positions A))
(set [j←[0..<nc] . j ∉ snd  ?pp])" unfolding inj_on_def by auto
note pp = pivot_positions[OF A pivot]
have lc: "length (pivot_positions A) = card (snd  ?pp)"
using distinct_card[OF pp(3)] by auto
show card: "card ?B = nc - card { i. i < nr ∧ row A i ≠ 0⇩v nc}"
"length (pivot_positions A) = card { i. i < nr ∧ row A i ≠ 0⇩v nc}"
unfolding find_base_vectors_def Let_def dim set_map  card_image[OF inj] pp(4)[symmetric]
unfolding pp(1) lc
proof -
have "nc - card (snd  {(i, p i) |i. i < nr ∧ p i ≠ nc})
= card {0 ..< nc} - card (snd  {(i, p i) |i. i < nr ∧ p i ≠ nc})" by auto
also have "… = card ({0 ..< nc} - snd  {(i, p i) |i. i < nr ∧ p i ≠ nc})"
by (rule card_Diff_subset[symmetric], insert piv(1), force+)
also have "{0 ..< nc} - snd  {(i, p i) |i. i < nr ∧ p i ≠ nc} = (set [j←[0..<nc] . j ∉ snd  {(i, p i) |i. i < nr ∧ p i ≠ nc}])"
by auto
finally show "card (set [j←[0..<nc] . j ∉ snd  {(i, p i) |i. i < nr ∧ p i ≠ nc}]) =
nc - card (snd  {(i, p i) |i. i < nr ∧ p i ≠ nc})" by simp
qed auto
interpret kernel nr nc A by (unfold_locales, rule A)
show basis: "basis ?B"
unfolding Ker.basis_def
proof (intro conjI)
show "span ?B = mat_kernel A"
proof
show "span ?B ⊆ mat_kernel A"
using sub by (rule Ker.span_is_subset2)
show "mat_kernel A ⊆ Ker.span ?B"
proof
fix v
assume "v ∈ mat_kernel A"
from mat_kernelD[OF A this]
have v: "v ∈ carrier_vec nc" and Av: "A *⇩v v = 0⇩v nr" by auto
let ?bi = "non_pivot_base A (pivot_positions A)"
let ?ran = "set [j←[0..<nc] . j ∉ snd  ?pp]"
let ?ran' = "set [j←[0..<nc] . j ∈ snd  ?pp]"
have dimv: "dim_vec v = nc" using v by auto
define I where "I = (λ b. SOME i. i ∈ ?ran ∧ ?bi i = b)"
{
fix j
assume j: "j ∈ ?ran"
hence "∃ i. i ∈ ?ran ∧ ?bi i = ?bi j" unfolding find_base_vectors_def Let_def dim by auto
from someI_ex[OF this] have I: "I (?bi j) ∈ ?ran" and id: "?bi (I (?bi j)) = ?bi j" unfolding I_def by blast+
from inj_onD[OF inj id I j] have "I (?bi j) = j" .
} note I = this
define a where "a = (λ b. v $(I b))" from Ker.lincomb_closed[OF sub] have diml: "dim_vec (lincomb a ?B) = nc" unfolding mat_kernel_def using dim lincomb_same by auto have "v = lincomb a ?B" proof (rule eq_vecI; unfold diml dimv) fix j assume j: "j < nc" have "Ker.lincomb a ?B$ j = (∑b∈ ?B. a b * b $j)" by (rule lincomb_index[OF j sub]) also have "… = (∑ i∈ ?ran. v$ i * ?bi i $j)" proof (subst sum.reindex_cong[OF inj]) show "?B = ?bi  ?ran" unfolding find_base_vectors_def Let_def dim by auto fix i assume "i ∈ ?ran" hence "I (?bi i) = i" by (rule I) hence "a (?bi i) = v$ i" unfolding a_def by simp
thus "a (?bi i) * ?bi i $j = v$ i * ?bi i $j" by simp qed auto also have "… = v$ j"
proof (cases "j ∈ ?ran")
case True
hence nmem: "j ∉ snd  set (pivot_positions A)" by auto
note npb = non_pivot_base[OF j nmem]
have "(∑ i∈ ?ran. v $i * (?bi i)$ j) =
v $j * ?bi j$ j + (∑ i∈ ?ran - {j}. v $i * ?bi i$ j)"
by (subst sum.remove[OF _ True], auto)
also have "?bi j $j = 1" using npb by simp also have "(∑ i ∈ ?ran - {j}. v$ i * ?bi i $j) = 0" using insert non_pivot_base(4)[OF _ _ j nmem] by (intro sum.neutral, auto) finally show ?thesis by simp next case False with j have jpp: "j ∈ snd  ?pp" by auto with j pp obtain i where i: "i < nr" and ji: "j = p i" and pi: "p i < nc" by auto from arg_cong[OF Av, of "λ u. u$ i"] i A
have "v $j = v$ j - row A i ∙ v" by auto
also have "row A i ∙ v = (∑ j = 0 ..< nc. A $$(i,j) * v  j)" unfolding scalar_prod_def using v A i by auto also have "… = (∑ j ∈ ?ran. A$$ (i,j) * v $j) + (∑ j ∈ ?ran'. A $$(i,j) * v j)" by (subst sum.union_disjoint[symmetric], auto intro: sum.cong) also have "(∑ j ∈ ?ran'. A$$ (i,j) * v$ j) =
A $$(i,p i) * v  j + (∑ j ∈ ?ran' - {p i}. A$$ (i,j) * v $j)" using jpp by (subst sum.remove, auto simp: ji i pi) also have "A $$(i, p i) = 1" using piv(4)[OF i] pi ji by auto also have "(∑ j ∈ ?ran' - {p i}. A$$ (i,j) * v$ j) = 0"
proof (rule sum.neutral, intro ballI)
fix j'
assume "j' ∈ ?ran' - {p i}"
then obtain i' where i': "i' < nr" and j': "j' = p i'" and pi': "p i' ≠ nc" and neq: "p i' ≠ p i"
unfolding pp by auto
from pi' piv[OF i'] have pi': "p i' < nc" by auto
from pp pi' neq j i' i have "i ≠ i'" by auto
from piv(5)[OF i' pi' i this]
show "A $$(i,j') * v  j' = 0" unfolding j' by simp qed also have "(∑ j ∈ ?ran. A$$ (i,j) * v $j) = - (∑ j ∈ ?ran. v$ j * - A $$(i,j))" unfolding sum_negf[symmetric] by (rule sum.cong, auto) finally have vj: "v  j = (∑ j ∈ ?ran. v  j * - A$$ (i,j))" by simp
show ?thesis unfolding vj j
proof (rule sum.cong[OF refl])
fix j'
assume j': "j' ∈ ?ran"
from jpp j' have jj': "j ≠ j'" by auto
let ?map = "map prod.swap (pivot_positions A)"
from ji i j have "(i,j) ∈ set (pivot_positions A)" unfolding pp by auto
hence mem: "(j,i) ∈ set ?map" by auto
from pp have "distinct (map fst ?map)" unfolding map_map o_def prod.swap_def fst_conv by auto
from map_of_is_SomeI[OF this mem] have "map_of ?map j = Some i" by auto
hence "?bi j' $j = - A $$(i, j')" unfolding non_pivot_base_def Let_def dim using j jj' by auto thus "v j' * ?bi j' j = v j' * - A$$ (i,j')" by simp qed qed finally show "v$ j = lincomb a ?B $j" .. qed auto thus "v ∈ span ?B" unfolding Ker.span_def by auto qed qed show "?B ⊆ mat_kernel A" by (rule sub) { fix a v assume lc: "lincomb a ?B = 0⇩v nc" and vB: "v ∈ ?B" from vB[unfolded find_base_vectors_def Let_def dim] obtain j where j: "j < nc" "j ∉ snd  ?pp" and v: "v = non_pivot_base A (pivot_positions A) j" by auto from arg_cong[OF lc, of "λ v. v$ j"] j
have "0 = lincomb a ?B $j" by auto also have "… = (∑v∈?B. a v * v$ j)"
by (subst lincomb_index[OF j(1) sub], simp)
also have "… = a v * v $j + (∑w∈?B - {v}. a w * w$ j)"
by (subst sum.remove[OF _ vB], auto)
also have "a v * v $j = a v" using non_pivot_base[OF j, folded v] by simp also have "(∑w∈?B - {v}. a w * w$ j) = 0"
proof (rule sum.neutral, intro ballI)
fix w
assume wB: "w ∈ ?B - {v}"
from this[unfolded find_base_vectors_def Let_def dim]
obtain j' where j': "j' < nc" "j' ∉ snd  ?pp" and w: "w = non_pivot_base A (pivot_positions A) j'"
by auto
with wB v have "j' ≠ j" by auto
from non_pivot_base(4)[OF j' j this]
show "a w * w $j = 0" unfolding w by simp qed finally have "a v = 0" by simp } thus "¬ lin_dep ?B" by (intro Ker.finite_lin_indpt2[OF finite_set sub], auto simp: class_field_def) qed show "dim = nc - card { i. i < nr ∧ row A i ≠ 0⇩v nc}" using Ker.dim_basis[OF finite_set basis] card by simp qed definition kernel_dim :: "'a :: field mat ⇒ nat" where [code del]: "kernel_dim A = kernel.dim (dim_col A) A" lemma (in kernel) kernel_dim [simp]: "kernel_dim A = dim" unfolding kernel_dim_def using A by simp lemma kernel_dim_code[code]: "kernel_dim A = dim_col A - length (pivot_positions (gauss_jordan_single A))" proof - define nr where "nr = dim_row A" define nc where "nc = dim_col A" let ?B = "gauss_jordan_single A" have A: "A ∈ carrier_mat nr nc" unfolding nr_def nc_def by auto from gauss_jordan_single[OF A refl] obtain P Q where AB: "?B = P * A" and QP: "Q * P = 1⇩m nr" and P: "P ∈ carrier_mat nr nr" and Q: "Q ∈ carrier_mat nr nr" and B: "?B ∈ carrier_mat nr nc" and row: "row_echelon_form ?B" by auto interpret K: kernel nr nc ?B by (unfold_locales, rule B) from mat_kernel_mult_eq[OF A P Q QP, folded AB] have "kernel_dim A = K.dim" unfolding kernel_dim_def using A by simp also have "… = nc - length (pivot_positions ?B)" using find_base_vectors[OF row B] by auto also have "… = dim_col A - length (pivot_positions ?B)" unfolding nc_def by simp finally show ?thesis . qed lemma kernel_one_mat: fixes A :: "'a :: field mat" and n :: nat defines A: "A ≡ 1⇩m n" shows "kernel.dim n A = 0" "kernel.basis n A {}" proof - have Ac: "A ∈ carrier_mat n n" unfolding A by auto have "pivot_fun A id n" unfolding A by (rule pivot_funI, auto) hence row: "row_echelon_form A" unfolding row_echelon_form_def A by auto have "{i. i < n ∧ row A i ≠ 0⇩v n} = {0 ..< n}" unfolding A by auto hence id: "card {i. i < n ∧ row A i ≠ 0⇩v n} = n" by auto interpret kernel n n A by (unfold_locales, rule Ac) from find_base_vectors[OF row Ac, unfolded id] show "dim = 0" "basis {}" by auto qed lemma kernel_upper_triangular: assumes A: "A ∈ carrier_mat n n" and ut: "upper_triangular A" and 0: "0 ∉ set (diag_mat A)" shows "kernel.dim n A = 0" "kernel.basis n A {}" proof - define ma where "ma = diag_mat A" from det_upper_triangular[OF ut A] have "det A = prod_list (diag_mat A)" . also have "… ≠ 0" using 0 unfolding ma_def[symmetric] by (induct ma, auto) finally have "det A ≠ 0" . from det_non_zero_imp_unit[OF A this, unfolded Units_def, of "()"] obtain B where B: "B ∈ carrier_mat n n" and BA: "B * A = 1⇩m n" and AB: "A * B = 1⇩m n" by (auto simp: ring_mat_def) from mat_kernel_mult_eq[OF A B A AB, unfolded BA] have id: "mat_kernel A = mat_kernel (1⇩m n)" .. show "kernel.dim n A = 0" "kernel.basis n A {}" unfolding id by (rule kernel_one_mat)+ qed lemma kernel_basis_exists: assumes A: "A ∈ carrier_mat nr nc" shows "∃ B. finite B ∧ kernel.basis nc A B" proof - obtain C where gj: "gauss_jordan_single A = C" by auto from gauss_jordan_single[OF A gj] obtain P Q where CPA: "C = P * A" and QP: "Q * P = 1⇩m nr" and P: "P ∈ carrier_mat nr nr" and Q: "Q ∈ carrier_mat nr nr" and C: "C ∈ carrier_mat nr nc" and row: "row_echelon_form C" by auto from find_base_vectors[OF row C] have "∃ B. finite B ∧ kernel.basis nc C B" by blast also have "mat_kernel C = mat_kernel A" unfolding CPA by (rule mat_kernel_mult_eq[OF A P Q QP]) finally show ?thesis . qed lemma mat_kernel_mult_right_gen_set: assumes A: "A ∈ carrier_mat nr nc" and B: "B ∈ carrier_mat nc nc" and C: "C ∈ carrier_mat nc nc" and inv: "B * C = 1⇩m nc" and gen_set: "kernel.gen_set nc (A * B) gen" and gen: "gen ⊆ mat_kernel (A * B)" shows "kernel.gen_set nc A (((*⇩v) B)  gen)" "(*⇩v) B  gen ⊆ mat_kernel A" "card (((*⇩v) B)  gen) = card gen" proof - let ?AB = "A * B" let ?gen = "((*⇩v) B)  gen" from A B have AB: "A * B ∈ carrier_mat nr nc" by auto from B have dimB: "dim_row B = nc" by auto from inv B C have CB: "C * B = 1⇩m nc" by (metis mat_mult_left_right_inverse) interpret AB: kernel nr nc ?AB by (unfold_locales, rule AB) interpret A: kernel nr nc A by (unfold_locales, rule A) { fix w assume "w ∈ ?gen" then obtain v where w: "w = B *⇩v v" and v: "v ∈ gen" by auto from v have "v ∈ mat_kernel ?AB" using gen by auto hence v: "v ∈ carrier_vec nc" and 0: "?AB *⇩v v = 0⇩v nr" unfolding mat_kernel[OF AB] by auto have "?AB *⇩v v = A *⇩v w" unfolding w using v A B by simp with 0 have 0: "A *⇩v w = 0⇩v nr" by auto from w B v have w: "w ∈ carrier_vec nc" by auto from 0 w have "w ∈ mat_kernel A" unfolding mat_kernel[OF A] by auto } thus genn: "?gen ⊆ mat_kernel A" by auto hence one_dir: "A.span ?gen ⊆ mat_kernel A" by fastforce { fix v v' assume v: "v ∈ gen" and v': "v' ∈ gen" and id: "B *⇩v v = B *⇩v v'" from v v' have v: "v ∈ carrier_vec nc" and v': "v' ∈ carrier_vec nc" using gen unfolding mat_kernel[OF AB] by auto from arg_cong[OF id, of "λ v. C *⇩v v"] have "v = v'" using v v' unfolding assoc_mult_mat_vec[symmetric, OF C B v] assoc_mult_mat_vec[symmetric, OF C B v'] CB by auto } note inj = this hence inj_gen: "inj_on ((*⇩v) B) gen" unfolding inj_on_def by auto show "card ?gen = card gen" using inj_gen by (rule card_image) { fix v let ?Cv = "C *⇩v v" assume "v ∈ mat_kernel A" from mat_kernelD[OF A this] have v: "v ∈ carrier_vec nc" and 0: "A *⇩v v = 0⇩v nr" by auto have "?AB *⇩v ?Cv = (A * (B * C)) *⇩v v" using A B C v by (subst assoc_mult_mat_vec[symmetric, OF AB C v], subst assoc_mult_mat[OF A B C], simp) also have "… = 0⇩v nr" unfolding inv using 0 A v by simp finally have 0: "?AB *⇩v ?Cv = 0⇩v nr" and Cv: "?Cv ∈ carrier_vec nc" using C v by auto hence "?Cv ∈ mat_kernel ?AB" unfolding mat_kernel[OF AB] by auto with gen_set have "?Cv ∈ AB.span gen" by auto from this[unfolded AB.Ker.span_def] obtain a gen' where Cv: "?Cv = AB.lincomb a gen'" and sub: "gen' ⊆ gen" and fin: "finite gen'" by auto let ?gen' = "((*⇩v) B)  gen'" from sub gen have gen': "gen' ⊆ mat_kernel ?AB" by auto have lin1: "AB.lincomb a gen' ∈ carrier_vec nc" using AB.Ker.lincomb_closed[OF gen', of a] unfolding mat_kernel[OF AB] by (auto simp: class_field_def) hence dim1: "dim_vec (AB.lincomb a gen') = nc" by auto hence dim1b: "dim_vec (B *⇩v (AB.Ker.lincomb a gen')) = nc" using B by auto from genn sub have genn': "?gen' ⊆ mat_kernel A" by auto from gen sub have gen'nc: "gen' ⊆ carrier_vec nc" unfolding mat_kernel[OF AB] by auto define a' where "a' = (λ b. a (C *⇩v b))" from A.Ker.lincomb_closed[OF genn'] have lin2: "A.Ker.lincomb a' ?gen' ∈ carrier_vec nc" unfolding mat_kernel[OF A] by (auto simp: class_field_def) hence dim2: "dim_vec (A.Ker.lincomb a' ?gen') = nc" by auto have "v = B *⇩v ?Cv" by (unfold assoc_mult_mat_vec[symmetric, OF B C v] inv, insert v, simp) hence "v = B *⇩v AB.Ker.lincomb a gen'" unfolding Cv by simp also have "… = A.Ker.lincomb a' ?gen'" proof (rule eq_vecI; unfold dim1 dim1b dim2) fix i assume i: "i < nc" with dimB have ii: "i < dim_row B" by auto from sub inj have inj: "inj_on ((*⇩v) B) gen'" unfolding inj_on_def by auto { fix v assume "v ∈ gen'" with gen'nc have v: "v ∈ carrier_vec nc" by auto hence "a' (B *⇩v v) = a v" unfolding a'_def assoc_mult_mat_vec[symmetric, OF C B v] CB by auto } note a' = this have "A.Ker.lincomb a' ?gen'$ i = (∑v∈(*⇩v) B  gen'. a' v * v $i)" unfolding A.lincomb_index[OF i genn'] by simp also have "… = (∑v∈gen'. a v * ((B *⇩v v)$ i))"
by (rule sum.reindex_cong[OF inj refl], auto simp: a')
also have "… = (∑v∈gen'. (∑j = 0..< nc. a v * row B i $j * v$ j))"
unfolding mult_mat_vec_def dimB scalar_prod_def index_vec[OF i]
by (rule sum.cong, insert gen'nc, auto simp: sum_distrib_left ac_simps)
also have "… = (∑j = 0 ..< nc. (∑v ∈ gen'. a v * row B i $j * v$ j))"
by (rule sum.swap)
also have "… = (∑j = 0..<nc. row B i $j * (∑v∈gen'. a v * v$ j))"
by (rule sum.cong, auto simp: sum_distrib_left ac_simps)
also have "… = (B *⇩v AB.Ker.lincomb a gen') $i" unfolding index_mult_mat_vec[OF ii] unfolding scalar_prod_def dim1 by (rule sum.cong[OF refl], subst AB.lincomb_index[OF _ gen'], auto) finally show "(B *⇩v AB.Ker.lincomb a gen')$ i = A.Ker.lincomb a' ?gen' $i" .. qed auto finally have "v ∈ A.Ker.span ?gen" using sub fin unfolding A.Ker.span_def by (auto simp: class_field_def intro!: exI[of _ a'] exI[of _ ?gen']) } hence other_dir: "A.Ker.span ?gen ⊇ mat_kernel A" by fastforce from one_dir other_dir show "kernel.gen_set nc A (((*⇩v) B)  gen)" by auto qed lemma mat_kernel_mult_right_basis: assumes A: "A ∈ carrier_mat nr nc" and B: "B ∈ carrier_mat nc nc" and C: "C ∈ carrier_mat nc nc" and inv: "B * C = 1⇩m nc" and fin: "finite gen" and basis: "kernel.basis nc (A * B) gen" shows "kernel.basis nc A (((*⇩v) B)  gen)" "card (((*⇩v) B)  gen) = card gen" proof - let ?AB = "A * B" let ?gen = "((*⇩v) B)  gen" from A B have AB: "?AB ∈ carrier_mat nr nc" by auto from B have dimB: "dim_row B = nc" by auto from inv B C have CB: "C * B = 1⇩m nc" by (metis mat_mult_left_right_inverse) interpret AB: kernel nr nc ?AB by (unfold_locales, rule AB) interpret A: kernel nr nc A by (unfold_locales, rule A) from basis[unfolded AB.Ker.basis_def] have gen_set: "AB.gen_set gen" and genAB: "gen ⊆ mat_kernel ?AB" by auto from mat_kernel_mult_right_gen_set[OF A B C inv gen_set genAB] have gen: "A.gen_set ?gen" and sub: "?gen ⊆ mat_kernel A" and card: "card ?gen = card gen" . from card show "card ?gen = card gen" . from fin have fing: "finite ?gen" by auto from gen have gen: "A.Ker.span ?gen = mat_kernel A" by auto have ABC: "A * B * C = A" using A B C inv by simp from kernel_basis_exists[OF A] obtain bas where finb: "finite bas" and bas: "A.basis bas" by auto from bas have bas': "A.gen_set bas" "bas ⊆ mat_kernel A" unfolding A.Ker.basis_def by auto let ?bas = "(*⇩v) C  bas" from mat_kernel_mult_right_gen_set[OF AB C B CB, unfolded ABC, OF bas'] have bas': "?bas ⊆ mat_kernel ?AB" "AB.Ker.span ?bas = mat_kernel ?AB" "card ?bas = card bas" by auto from finb bas have cardb: "A.dim = card bas" by (rule A.Ker.dim_basis) from fin basis have cardg: "AB.dim = card gen" by (rule AB.Ker.dim_basis) from AB.Ker.gen_ge_dim[OF _ bas'(1-2)] finb bas'(3) cardb cardg have ineq1: "card gen ≤ A.dim" by auto from A.Ker.dim_gen_is_basis[OF fing sub gen, unfolded card, OF this] show "A.basis ?gen" . qed lemma mat_kernel_dim_mult_eq_right: assumes A: "A ∈ carrier_mat nr nc" and B: "B ∈ carrier_mat nc nc" and C: "C ∈ carrier_mat nc nc" and BC: "B * C = 1⇩m nc" shows "kernel.dim nc (A * B) = kernel.dim nc A" proof - let ?AB = "A * B" from A B have AB: "?AB ∈ carrier_mat nr nc" by auto interpret AB: kernel nr nc ?AB by (unfold_locales, rule AB) interpret A: kernel nr nc A by (unfold_locales, rule A) from kernel_basis_exists[OF AB] obtain bas where finb: "finite bas" and bas: "AB.basis bas" by auto let ?bas = "((*⇩v) B)  bas" from mat_kernel_mult_right_basis[OF A B C BC finb bas] finb have bas': "A.basis ?bas" and finb': "finite ?bas" and card: "card ?bas = card bas" by auto show "AB.dim = A.dim" unfolding A.Ker.dim_basis[OF finb' bas'] AB.Ker.dim_basis[OF finb bas] card .. qed locale vardim = fixes f_ty :: "'a :: field itself" begin abbreviation "M == λk. module_vec TYPE('a) k" abbreviation "span == λk. LinearCombinations.module.span class_ring (M k)" abbreviation "lincomb == λk. module.lincomb (M k)" abbreviation "lin_dep == λk. module.lin_dep class_ring (M k)" abbreviation "padr m v == v @⇩v 0⇩v m" definition "unpadr m v == vec (dim_vec v - m) (λi. v$ i)"
abbreviation "padl m v == 0⇩v m @⇩v v"
definition "unpadl m v == vec (dim_vec v - m) (λi. v $(m+i))" lemma unpadr_padr[simp]: "unpadr m (padr m v) = v" unfolding unpadr_def by auto lemma unpadl_padl[simp]: "unpadl m (padl m v) = v" unfolding unpadl_def by auto lemma padr_unpadr[simp]: "v : padr m  U ⟹ padr m (unpadr m v) = v" by auto lemma padl_unpadl[simp]: "v : padl m  U ⟹ padl m (unpadl m v) = v" by auto (* somehow not automatically proven *) lemma padr_image: assumes "U ⊆ carrier_vec n" shows "padr m  U ⊆ carrier_vec (n + m)" proof(rule subsetI) fix v assume "v : padr m  U" then obtain u where "u : U" and vmu: "v = padr m u" by auto hence "u : carrier_vec n" using assms by auto thus "v : carrier_vec (n + m)" unfolding vmu using zero_carrier_vec[of m] append_carrier_vec by metis qed lemma padl_image: assumes "U ⊆ carrier_vec n" shows "padl m  U ⊆ carrier_vec (m + n)" proof(rule subsetI) fix v assume "v : padl m  U" then obtain u where "u : U" and vmu: "v = padl m u" by auto hence "u : carrier_vec n" using assms by auto thus "v : carrier_vec (m + n)" unfolding vmu using zero_carrier_vec[of m] append_carrier_vec by metis qed lemma padr_inj: shows "inj_on (padr m) (carrier_vec n :: 'a vec set)" apply(intro inj_onI) using append_vec_eq by auto lemma padl_inj: shows "inj_on (padl m) (carrier_vec n :: 'a vec set)" apply(intro inj_onI) using append_vec_eq[OF zero_carrier_vec zero_carrier_vec] by auto lemma lincomb_pad: fixes m n a assumes U: "(U :: 'a vec set) ⊆ carrier_vec n" and finU: "finite U" defines "goal pad unpad W == pad m (lincomb n a W) = lincomb (n+m) (a o unpad m) (pad m  W)" shows "goal padr unpadr U" (is ?R) and "goal padl unpadl U" (is "?L") proof - interpret N: vectorspace class_ring "M n" using vec_vs. interpret NM: vectorspace class_ring "M (n+m)" using vec_vs. note [simp] = module_vec_simps class_ring_simps have "?R ∧ ?L" using finU U proof (induct set:finite) case empty thus ?case unfolding goal_def unfolding N.lincomb_def NM.lincomb_def by auto next case (insert u U) hence finU: "finite U" and U: "U ⊆ carrier_vec n" and u[simp]: "u : carrier_vec n" and uU: "u ∉ U" and auU: "a : insert u U → UNIV" and aU: "a : U → UNIV" and au: "a u : UNIV" by auto have IHr: "goal padr unpadr U" and IHl: "goal padl unpadl U" using insert(3) U aU by auto note N_lci = N.lincomb_insert2[unfolded module_vec_simps] note NM_lci = NM.lincomb_insert2[unfolded module_vec_simps] have auu[simp]: "a u ⋅⇩v u : carrier_vec n" using au u by simp have laU[simp]: "lincomb n a U : carrier_vec n" using N.lincomb_closed[unfolded module_vec_simps class_ring_simps, OF U aU]. let ?m0 = "0⇩v m :: 'a vec" have m0: "?m0 : carrier_vec m" by auto have ins: "lincomb n a (insert u U) = a u ⋅⇩v u + lincomb n a U" using N_lci[OF finU U] auU uU u by auto show ?case proof have "padr m (a u ⋅⇩v u + lincomb n a U) = (a u ⋅⇩v u + lincomb n a U) @⇩v (?m0 + ?m0)" by auto also have "... = padr m (a u ⋅⇩v u) + padr m (lincomb n a U)" using append_vec_add[symmetric, OF auu laU] using zero_carrier_vec[of m] by metis also have "padr m (lincomb n a U) = lincomb (n+m) (a o unpadr m) (padr m  U)" using IHr unfolding goal_def. also have "padr m (a u ⋅⇩v u) = a u ⋅⇩v padr m u" by auto also have "... = (a o unpadr m) (padr m u) ⋅⇩v padr m u" by auto also have "... + lincomb (n+m) (a o unpadr m) (padr m  U) = lincomb (n+m) (a o unpadr m) (insert (padr m u) (padr m  U))" apply(subst NM_lci[symmetric]) using finU uU U append_vec_eq[OF u] by auto also have "insert (padr m u) (padr m  U) = padr m  insert u U" by auto finally show "goal padr unpadr (insert u U)" unfolding goal_def ins. have [simp]: "n+m = m+n" by auto have "padl m (a u ⋅⇩v u + lincomb n a U) = (?m0 + ?m0) @⇩v (a u ⋅⇩v u + lincomb n a U)" by auto also have "... = padl m (a u ⋅⇩v u) + padl m (lincomb n a U)" using append_vec_add[symmetric, OF _ _ auu laU] using zero_carrier_vec[of m] by metis also have "padl m (lincomb n a U) = lincomb (n+m) (a o unpadl m) (padl m  U)" using IHl unfolding goal_def. also have "padl m (a u ⋅⇩v u) = a u ⋅⇩v padl m u" by auto also have "... = (a o unpadl m) (padl m u) ⋅⇩v padl m u" by auto also have "... + lincomb (n+m) (a o unpadl m) (padl m  U) = lincomb (n+m) (a o unpadl m) (insert (padl m u) (padl m  U))" apply(subst NM_lci[symmetric]) using finU uU U append_vec_eq[OF m0] by auto also have "insert (padl m u) (padl m  U) = padl m  insert u U" by auto finally show "goal padl unpadl (insert u U)" unfolding goal_def ins. qed qed thus ?R ?L by auto qed lemma span_pad: assumes U: "(U::'a vec set) ⊆ carrier_vec n" defines "goal pad m == pad m  span n U = span (n+m) (pad m  U)" shows "goal padr m" "goal padl m" proof - interpret N: vectorspace class_ring "M n" using vec_vs. interpret NM: vectorspace class_ring "M (n+m)" using vec_vs. { fix pad :: "'a vec ⇒ 'a vec" and unpad :: "'a vec ⇒ 'a vec" assume main: "⋀A a. A ⊆ U ⟹ finite A ⟹ pad (lincomb n a A) = lincomb (n+m) (a o unpad) (pad  A)" assume [simp]: "⋀v. unpad (pad v) = v" assume pU: "pad  U ⊆ carrier_vec (n+m)" have "pad  (span n U) = span (n+m) (pad  U)" proof (intro Set.equalityI subsetI) fix x assume "x : pad  (span n U)" then obtain v where "v : span n U" and xv: "x = pad v" by auto then obtain a A where AU: "A ⊆ U" and finA: "finite A" and a: "a : A → UNIV" and vaA: "v = lincomb n a A" unfolding N.span_def by auto hence A: "A ⊆ carrier_vec n" using U by auto show "x : span (n+m) (pad  U)" unfolding NM.span_def proof (intro CollectI exI conjI) show "x = lincomb (n+m) (a o unpad) (pad  A)" using xv vaA main[OF AU finA] by auto show "pad  A ⊆ pad  U" using AU by auto qed (insert finA, auto simp: class_ring_simps) next fix x assume "x : span (n+m) (pad  U)" then obtain a' A' where A'U: "A' ⊆ pad  U" and finA': "finite A'" and a': "a' : A' → UNIV" and xa'A': "x = lincomb (n+m) a' A'" unfolding NM.span_def by auto then obtain A where finA: "finite A" and AU: "A ⊆ U" and A'A: "A' = pad  A" using finite_subset_image[OF finA' A'U] by auto hence A: "A ⊆ carrier_vec n" using U by auto have A': "A' ⊆ carrier_vec (n+m)" using A'U pU by auto define a where "a = a' o pad" define a'' where "a'' = (a' o pad) o unpad" have a: "a : A → UNIV" by auto have restr: "restrict a' A' = restrict a'' A'" proof(rule restrict_ext) fix u' assume "u' : A'" then obtain u where "u : A" and "u' = pad u" unfolding A'A by auto thus "a' u' = a'' u'" unfolding a''_def a_def by auto qed have "x = lincomb (n+m) a' A'" using xa'A' unfolding A'A. also have "... = lincomb (n+m) a'' A'" apply (subst NM.lincomb_restrict) using finA' A' restr by (auto simp: module_vec_simps class_ring_simps) also have "... = lincomb (n+m) a'' (pad  A)" unfolding A'A.. also have "... = pad (lincomb n a A)" unfolding a''_def using main[OF AU finA] unfolding a_def by auto finally show "x : pad  (span n U)" unfolding N.span_def apply(rule image_eqI, intro CollectI exI conjI) using finA AU by (auto simp: class_ring_simps) qed } note main = this have AUC: "⋀A. A ⊆ U ⟹ A ⊆ carrier_vec n" using U by simp have [simp]: "n+m = m+n" by auto show "goal padr m" unfolding goal_def apply (subst main[OF _ _ padr_image[OF U]]) using lincomb_pad[OF AUC] unpadr_padr by auto show "goal padl m" unfolding goal_def apply (subst main) using lincomb_pad[OF AUC] unpadl_padl padl_image[OF U] by auto qed lemma kernel_padr: assumes aA: "a : mat_kernel (A :: 'a :: field mat)" and A: "A : carrier_mat nr1 nc1" and B: "B : carrier_mat nr1 nc2" and D: "D : carrier_mat nr2 nc2" shows "padr nc2 a : mat_kernel (four_block_mat A B (0⇩m nr2 nc1) D)" (is "_ : mat_kernel ?ABCD") unfolding mat_kernel_def proof (rule, intro conjI) have [simp]: "dim_row A = nr1" "dim_row D = nr2" "dim_row ?ABCD = nr1 + nr2" using A D by auto have a: "a : carrier_vec nc1" using mat_kernel_carrier[OF A] aA by auto show "?ABCD *⇩v padr nc2 a = 0⇩v (dim_row ?ABCD)" (is "?l = ?r") proof fix i assume i: "i < dim_vec ?r" hence "?l$ i = row ?ABCD i ∙ padr nc2 a" by auto
also have "... = 0"
proof (cases "i < nr1")
case True
hence rows: "row A i : carrier_vec nc1" "row B i : carrier_vec nc2"
using A B by auto
have "row ?ABCD i = row A i @⇩v row B i"
using row_four_block_mat(1)[OF A B _ D True] by auto
also have "... ∙ padr nc2 a = row A i ∙ a + row B i ∙ 0⇩v nc2"
using scalar_prod_append[OF rows] a by auto
also have "row A i ∙ a = (A *⇩v a) $i" using True A by auto also have "... = 0" using mat_kernelD[OF A aA] True by auto also have "row B i ∙ 0⇩v nc2 = 0" using True rows by auto finally show ?thesis by simp next case False let ?C = "0⇩m nr2 nc1" let ?i = "i - nr1" have rows: "row ?C ?i : carrier_vec nc1" "row D ?i : carrier_vec nc2" using D i False A by auto have "row ?ABCD i = row ?C ?i @⇩v row D ?i" using row_four_block_mat(2)[OF A B _ D False] i A D by auto also have "... ∙ padr nc2 a = row ?C ?i ∙ a + row D ?i ∙ 0⇩v nc2" using scalar_prod_append[OF rows] a by auto also have "row ?C ?i ∙ a = 0⇩v nc1 ∙ a" using False A i by auto also have "... = 0" using a by auto also have "row D ?i ∙ 0⇩v nc2 = 0" using False rows by auto finally show ?thesis by simp qed finally show "?l$ i = ?r $i" using i by auto qed auto show "padr nc2 a : carrier_vec (dim_col ?ABCD)" using a A D by auto qed lemma kernel_padl: assumes dD: "d ∈ mat_kernel (D :: 'a :: field mat)" and A: "A ∈ carrier_mat nr1 nc1" and C: "C ∈ carrier_mat nr2 nc1" and D: "D ∈ carrier_mat nr2 nc2" shows "padl nc1 d ∈ mat_kernel (four_block_mat A (0⇩m nr1 nc2) C D)" (is "_ ∈ mat_kernel ?ABCD") unfolding mat_kernel_def proof (rule, intro conjI) have [simp]: "dim_row A = nr1" "dim_row D = nr2" "dim_row ?ABCD = nr1 + nr2" using A D by auto have d: "d : carrier_vec nc2" using mat_kernel_carrier[OF D] dD by auto show "?ABCD *⇩v padl nc1 d = 0⇩v (dim_row ?ABCD)" (is "?l = ?r") proof fix i assume i: "i < dim_vec ?r" hence "?l$ i = row ?ABCD i ∙ padl nc1 d" by auto
also have "... = 0"
proof (cases "i < nr1")
case True
let ?B = "0⇩m nr1 nc2"
have rows: "row A i : carrier_vec nc1" "row ?B i : carrier_vec nc2"
using A True by auto
have "row ?ABCD i = row A i @⇩v row ?B i"
using row_four_block_mat(1)[OF A _ C D True] by auto
also have "... ∙ padl nc1 d = row A i ∙ 0⇩v nc1 + row ?B i ∙ d"
using scalar_prod_append[OF rows] d by auto
also have "row A i ∙ 0⇩v nc1 = 0" using A True by auto
also have "row ?B i ∙ d = 0" using True d by auto
finally show ?thesis by simp
next case False
let ?i = "i - nr1"
have rows:
"row C ?i : carrier_vec nc1" "row D ?i : carrier_vec nc2"
using C D i False A by auto
have "row ?ABCD i = row C ?i @⇩v row D ?i"
using row_four_block_mat(2)[OF A _ C D False] i A D by auto
also have "... ∙ padl nc1 d = row C ?i ∙ 0⇩v nc1 + row D ?i ∙ d"
using scalar_prod_append[OF rows] d by auto
also have "row C ?i ∙ 0⇩v nc1 = 0" using False A C i by auto
also have "row D ?i ∙ d = (D *⇩v d) $?i" using D d False i by auto also have "... = 0" using mat_kernelD[OF D dD] using False i by auto finally show ?thesis by simp qed finally show "?l$ i = ?r \$ i" using i by auto
qed auto
show "padl nc1 d : carrier_vec (dim_col ?ABCD)" using d A D by auto
qed

lemma mat_kernel_split:
assumes A: "A ∈ carrier_mat n n"
and D: "D ∈ carrier_mat m m"
and kAD: "k ∈ mat_kernel (four_block_mat A (0⇩m n m) (0⇩m m n) D)"
(is "_ ∈ mat_kernel ?A00D")
shows "vec_first k n ∈ mat_kernel A" (is "?a ∈ _")
and "vec_last k m ∈ mat_kernel D" (is "?d ∈ _")
proof -
have "0⇩v n @⇩v 0⇩v m = 0⇩v (n+m)" by auto
also
have A00D: "?A00D : carrier_mat (n+m) (n+m)" using four_block_carrier_mat[OF A D].
hence k: "k : carrier_vec (n+m)" using kAD mat_kernel_carrier by auto
hence "?a @⇩v ?d = k" by simp
hence "0⇩v (n+m) = ?A00D *⇩v (?a @⇩v ?d)" using mat_kernelD[OF A00D] kAD by auto
also have "... = A *⇩v ?a @⇩v D *⇩v ?d"
using mult_mat_vec_split[OF A D] by auto
finally have "0⇩v n @⇩v 0⇩v m = A *⇩v ?a @⇩v D *⇩v ?d".
hence "0⇩v n = A *⇩v ?a ∧ 0⇩v m = D *⇩v ?d"
apply(subst append_vec_eq[of _ n, symmetric]) using A D by auto
thus "?a : mat_kernel A" "?d : mat_kernel D" unfolding mat_kernel_def using A D by auto
qed

assumes v: "v : carrier_vec n"
shows "padr m v = padl n u ⟷ v = 0⇩v n ∧ u = 0⇩v m"
apply (subst append_vec_eq) using v by auto

assumes A: "A ⊆ carrier_vec n" and A0: "0⇩v n ∉ A" and B: "B ⊆ carrier_vec m"
shows "padr m  A ∩ padl n  B = {}" (is "?A ∩ ?B = _")
proof (intro equals0I)
fix ab assume "ab : ?A ∩ ?B"
then obtain a b
where "ab = padr m a" "ab = padl n b" and dim: "a : A" "b : B" by force
hence "a = 0⇩v n" using dim A B by auto
thus "False" using dim A0 by auto
qed

assumes A: "A ⊆ carrier_vec n" and liA: "~ lin_dep n A"
and B: "B ⊆ carrier_vec m" and liB: "~ lin_dep m B"
shows "~ lin_dep (n+m) (padr m  A ∪ padl n  B)" (is "~ lin_dep _ (?A ∪ ?B)")
proof -
interpret N: vectorspace class_ring "M n" using vec_vs.
interpret M: vectorspace class_ring "M m" using vec_vs.
interpret NM: vectorspace class_ring "M (n+m)" using vec_vs.
note [simp] = module_vec_simps class_ring_simps
have AB: "?A ∪ ?B ⊆ carrier_vec (n+m)"
show ?thesis
unfolding NM.lin_dep_def
unfolding not_ex not_imp[symmetric] not_not
proof(intro allI impI)
fix U f u
assume finU: "finite U"
and UAB: "U ⊆ ?A ∪ ?B"
and f: "f : U → carrier class_ring"
and 0: "lincomb (n+m) f U = 𝟬⇘M (n+m)⇙"
and uU: "u : U"
let ?UA = "U ∩ ?A" and ?UB = "U ∩ ?B"
have "?UA ⊆ ?A" "?UB ⊆ ?B" by auto
then obtain A' B'
where A'A: "A' ⊆ A" and B'B: "B' ⊆ B"
and UAA': "?UA = padr m  A'" and UBB': "?UB = padl n  B'"
unfolding subset_image_iff by auto
hence A': "A' ⊆ carrier_vec n" and B': "B' ⊆ carrier_vec m" using A B by auto
have finA': "finite A'" and finB': "finite B'"
proof -
have "padr m  A' ⊆ U" "padl n  B' ⊆ U" using UAA' UBB' by auto
hence pre: "finite (padr m  A')" "finite (padl n  B')"
using finite_subset[OF _ finU] by auto
show "finite A'"
apply (rule finite_imageD) using subset_inj_on[OF padr_inj A'] pre by auto
show "finite B'"
apply (rule finite_imageD) using subset_inj_on[OF padl_inj B'] pre by auto
qed
have "0⇩v n ∉ A" using N.zero_nin_lin_indpt[OF _ liA] A class_semiring.one_zeroI by auto
hence "?A ∩ ?B = {}" using pad_disjoint A B by auto
hence disj: "?UA ∩ ?UB = {}" by auto
have split: "U = padr m  A' ∪ padl n  B'"
unfolding UAA'[symmetric] UBB'[symmetric] using UAB by auto
show "f u = 𝟬⇘(class_ring::'a ring)⇙"
proof -
let ?a = "f ∘ padr m"
let ?b = "f ∘ padl n"
have lcA': "lincomb n ?a A' : carrier_vec n" using N.lincomb_closed A' by auto
have lcB': "lincomb m ?b B' : carrier_vec m" using M.lincomb_closed B' by auto

have "0⇩v n @⇩v 0⇩v m = 0⇩v (n+m)" by auto
also have "... = lincomb (n+m) f U" using 0 by auto
also have "U = ?UA ∪ ?UB" using UAB by auto
also have "lincomb (n+m) f ... = lincomb (n+m) f ?UA + lincomb (n+m) f ?UB"
apply(subst NM.lincomb_union) using A B finU disj by auto
also have "lincomb (n+m) f ?UA = lincomb (n+m) (restrict f ?UA) ?UA"
apply (subst NM.lincomb_restrict) using A finU by auto
also have "restrict f ?UA = restrict (?a ∘ unpadr m) ?UA"
apply(rule restrict_ext) by auto
also have "lincomb (n+m) ... ?UA = lincomb (n+m) (?a ∘ unpadr m) ?UA"
apply(subst NM.lincomb_restrict) using A finU by auto
also have "?UA = padr m  A'" using UAA'.
also have "lincomb (n+m) (?a ∘ unpadr m) ... =
padr m (lincomb n ?a A')"
also have "lincomb (n+m) f ?UB = lincomb (n+m) (restrict f ?UB) ?UB"
apply (subst NM.lincomb_restrict) using B finU by auto
also have "restrict f ?UB = restrict (?b ∘ unpadl n) ?UB"
apply(rule restrict_ext) by auto
also have "lincomb (n+m) ... ?UB = lincomb (n+m) (?b ∘ unpadl n) ?UB"
apply(subst NM.lincomb_restrict) using B finU by auto
also have "n+m = m+n" by auto
also have "?UB = padl n  B'" using UBB'.
also have "lincomb (m+n) (?b ∘ unpadl n) ... =
padl n (lincomb m ?b B')"
also have "padr m (lincomb n ?a A') + ... =
(lincomb n ?a A' + 0⇩v n) @⇩v (0⇩v m + lincomb m ?b B')"
apply (rule append_vec_add) using lcA' lcB' by auto
also have "... = lincomb n ?a A' @⇩v lincomb m ?b B'" using lcA' lcB' by auto
finally have "0⇩v n @⇩v 0⇩v m = lincomb n ?a A' @⇩v lincomb m ?b B'".
hence "0⇩v n = lincomb n ?a A' ∧ 0⇩v m = lincomb m ?b B'"
apply(subst append_vec_eq[symmetric]) using lcA' lcB' by auto
from conjunct1[OF this] conjunct2[OF this]
have "?a : A' → {0}" "?b : B' → {0}"
using N.not_lindepD[OF liA finA' A'A]
using M.not_lindepD[OF liB finB' B'B] by auto
hence "f : padr m  A' → {0}" "f : padl n  B' → {0}" by auto
hence "f : padr m  A' ∪ padl n  B' → {0}" by auto
hence "f : U → {0}" using split by auto
hence "f u = 0" using uU by auto
thus ?thesis by simp
qed
qed
qed

end

lemma kernel_four_block_0_mat:
assumes Adef: "(A :: 'a::field mat) = four_block_mat B (0⇩m n m) (0⇩m m n) D"
and B: "B ∈ carrier_mat n n"
and D: "D ∈ carrier_mat m m"
shows "kernel.dim (n + m) A = kernel.dim n B + kernel.dim m D"
proof -
have [simp]: "n + m = m + n" by auto
have A: "A ∈ carrier_mat (n+m) (n+m)"
using Adef four_block_carrier_mat[OF B D] by auto
interpret vardim "TYPE('a)".
interpret MN: vectorspace class_ring "M (n+m)" using vec_vs.
interpret KA: kernel "n+m" "n+m" A by (unfold_locales, rule A)
interpret KB: kernel n n B by (unfold_locales, rule B)
interpret KD: kernel m m D by (unfold_locales, rule D)

note [simp] = module_vec_simps

from kernel_basis_exists[OF B]
obtain baseB where fin_bB: "finite baseB" and bB: "KB.basis baseB" by blast
hence bBkB: "baseB ⊆ mat_kernel B" unfolding KB.Ker.basis_def by auto
hence bBc: "baseB ⊆ carrier_vec n" using mat_kernel_carrier[OF B] by auto
have bB0: "0⇩v n ∉ baseB"
using bB unfolding KB.Ker.basis_def
using KB.Ker.vs_zero_lin_dep[OF bBkB] by auto
have bBkA: "padr m  baseB ⊆ mat_kernel A"
proof
fix a assume "a : padr m  baseB"
then obtain b where ab: "a = padr m b" and "b : baseB" by auto
hence "b : mat_kernel B" using bB unfolding KB.Ker.basis_def by auto
hence "padr m b : mat_kernel A"
thus "a : mat_kernel A" using ab by auto
qed
from kernel_basis_exists[OF D]
obtain baseD where fin_bD: "finite baseD" and bD: "KD.basis baseD" by blast
hence bDkD: "baseD ⊆ mat_kernel D" unfolding KD.Ker.basis_def by auto
hence bDc: "baseD ⊆ carrier_vec m" using mat_kernel_carrier[OF D] by auto
have bDkA: "padl n  baseD ⊆ mat_kernel A"
proof
fix a assume "a : padl n  baseD"
then obtain d where ad: "a = padl n d" and "d : baseD" by auto
hence "d : mat_kernel D" using bD unfolding KD.Ker.basis_def by auto
hence "padl n d : mat_kernel A"
thus "a : mat_kernel A" using ad by auto
qed
let ?BD = "(padr m  baseB ∪ padl n  baseD)"
have finBD: "finite ?BD" using fin_bB fin_bD by auto
have "KA.basis  ?BD"
unfolding KA.Ker.basis_def
proof (intro conjI Set.equalityI)
show BDk: "?BD ⊆ mat_kernel A" using bBkA bDkA by auto
also have "mat_kernel A ⊆ carrier_vec (m+n)" using mat_kernel_carrier A by auto
finally have BD: "?BD ⊆ carrier (M (n + m))" by auto
show "mat_kernel A ⊆ KA.Ker.span ?BD"
unfolding KA.span_same[OF BDk]
proof
have BD: "?BD ⊆ carrier_vec (n+m)" (is "_ ⊆ ?R")
proof(rule)
fix v assume "v : ?BD"
moreover
{ assume "v : padr m  baseB"
then obtain b where "b : baseB" and vb: "v = padr m b" by auto
hence "b : carrier_vec n" using bBc by auto
hence "v : ?R" unfolding vb apply(subst append_carrier_vec) by auto
}
moreover
{ assume "v : padl n  baseD"
then obtain d where "d : baseD" and vd: "v = padl n d" by auto
hence "d : carrier_vec m" using bDc by auto
hence "v : ?R" unfolding vd apply(subst append_carrier_vec) by auto
}
ultimately show "v: ?R" by auto
qed
fix a assume a: "a : mat_kernel A"
hence "a : carrier_vec (n+m)" using a mat_kernel_carrier[OF A] by auto
hence "a = vec_first a n @⇩v vec_last a m" (is "_ = ?b @⇩v ?d") by simp
also have "... = padr m ?b + padl n ?d" by auto
finally have 1: "a = padr m ?b + padl n ?d".

have subkernel: "?b : mat_kernel B" "?d : mat_kernel D"
using mat_kernel_split[OF B D] a Adef by auto
hence "?b : span n baseB"
using bB unfolding KB.Ker.basis_def using KB.span_same by auto
hence "padr m ?b : padr m  span n baseB" by auto
also have "padr m  span n baseB = span (n+m) (padr m  baseB)"
also have "... ⊆ span (n+m) ?BD" using MN.span_is_monotone by auto
finally have 2: "padr m ?b : span (n+m) ?BD".
have "?d : span m baseD"
using subkernel bD unfolding KD.Ker.basis_def using KD.span_same by auto
hence "padl n ?d : padl n  span m baseD" by auto
also have "padl n  span m baseD = span (n+m) (padl n  baseD)"
also have "... ⊆ span (n+m) ?BD" using MN.span_is_monotone by auto
finally have 3: "padl n ?d : span (n+m) ?BD".

have "padr m ?b + padl n ?d : span (n+m) ?BD"
using MN.span_add1[OF _ 2 3] BD by auto
thus "a ∈ span (n+m) ?BD" using 1 by auto
qed
show "KA.Ker.span ?BD ⊆ mat_kernel A" using KA.Ker.span_closed[OF BDk] by auto
have li: "~ lin_dep n baseB" "~ lin_dep m baseD"
using bB[unfolded KB.Ker.basis_def]
unfolding KB.lindep_same[OF bBkB]
using bD[unfolded KD.Ker.basis_def]
unfolding KD.lindep_same[OF bDkD] by auto
show "~ KA.Ker.lin_dep ?BD"
unfolding KA.lindep_same[OF BDk]
qed
hence "KA.dim = card ?BD" using KA.Ker.dim_basis[OF finBD] by auto
also have "card ?BD = card (padr m  baseB) + card (padl n  baseD)"
apply(rule card_Un_disjoint)
using pad_disjoint[OF bBc bB0 bDc] fin_bB fin_bD by auto
also have "... = card baseB + card baseD"
using card_image[OF subset_inj_on[OF padl_inj]] bBc bDc by auto
also have "card baseB = KB.dim" using KB.Ker.dim_basis[OF fin_bB] bB by auto
also have "card baseD = KD.dim" using KD.Ker.dim_basis[OF fin_bD] bD by auto
finally show ?thesis.

qed

lemma similar_mat_wit_kernel_dim: assumes A: "A ∈ carrier_mat n n"
and wit: "similar_mat_wit A B P Q"
shows "kernel.dim n A = kernel.dim n B"
proof -
from similar_mat_witD2[OF A wit]
have QP: "Q * P = 1⇩m n" and AB: "A = P * B * Q" and
A: "A ∈ carrier_mat<