Theory Cayley_Hamilton_Compatible
theory Cayley_Hamilton_Compatible
imports
Rings2
Cayley_Hamilton.Cayley_Hamilton
Gauss_Jordan.Determinants2
begin
subsection ‹Compatibility layer btw @{theory Cayley_Hamilton.Square_Matrix} and @{theory Gauss_Jordan.Determinants2} ›
hide_const (open) Square_Matrix.det
hide_const (open) Square_Matrix.row
hide_const (open) Square_Matrix.col
hide_const (open) Square_Matrix.transpose
hide_const (open) Square_Matrix.cofactor
hide_const (open) Square_Matrix.adjugate
hide_fact (open) det_upperdiagonal
hide_fact (open) row_def
hide_fact (open) col_def
hide_fact (open) transpose_def
lemma det_sq_matrix_eq: "Square_Matrix.det (from_vec A) = det A"
unfolding Square_Matrix.det.rep_eq Determinants.det_def from_vec.rep_eq ..
lemma to_vec_matrix_scalar_mult: "to_vec (x *⇩S A) = x *k to_vec A"
by transfer (simp add: matrix_scalar_mult_def)
lemma to_vec_matrix_matrix_mult: "to_vec (A * B) = to_vec A ** to_vec B"
by transfer (simp add: matrix_matrix_mult_def)
lemma to_vec_diag: "to_vec (diag x) = mat x"
by transfer (simp add: mat_def)
lemma to_vec_one: "to_vec 1 = mat 1"
by transfer (simp add: mat_def)
lemma to_vec_eq_iff: "to_vec M = to_vec N ⟷ M = N"
by transfer (auto simp: vec_eq_iff)
subsection‹Some preliminary lemmas and results›
lemma invertible_iff_is_unit:
fixes A::"'a::{comm_ring_1}^'n^'n"
shows "invertible A ⟷ (det A) dvd 1"
proof
assume inv_A: "invertible A"
obtain B where AB_mat: "A ** B = mat 1" using inv_A unfolding invertible_def by auto
have "1 = det (mat 1::'a^'n^'n)" unfolding det_I ..
also have "... = det (A ** B)" unfolding AB_mat ..
also have "... = det A * det B" unfolding det_mul ..
finally have "1 = det A * det B" by simp
thus "(det A) dvd 1" unfolding dvd_def by auto
next
assume det_unit: "(det A) dvd 1"
from this obtain a where a: "(det A) * a = 1" unfolding dvd_def by auto
let ?A = "to_vec (Square_Matrix.adjugate (from_vec A))"
show "invertible A"
proof (unfold invertible_def, rule exI[of _ "a *k ?A"])
have "from_vec A * (a *⇩S Square_Matrix.adjugate (from_vec A)) = 1"
"(a *⇩S Square_Matrix.adjugate (from_vec A)) * from_vec A = 1"
using a unfolding smult_mult2[symmetric] mult_adjugate_det[of "from_vec A"] smult_diag det_sq_matrix_eq
smult_mult1[symmetric] adjugate_mult_det[of "from_vec A"]
by (simp_all add: ac_simps diag_1)
then show "A ** (a *k ?A) = mat 1 ∧ a *k ?A ** A = mat 1"
unfolding to_vec_eq_iff[symmetric] to_vec_matrix_matrix_mult to_vec_matrix_scalar_mult
to_vec_from_vec to_vec_one by simp
qed
qed
definition "minorM M i j = (χ k l. if k = i ∧ l = j then 1 else if k = i ∨ l = j then 0 else M $ k $ l)"
lemma minorM_eq: "minorM M i j = to_vec (minor (from_vec M) i j)"
unfolding minorM_def by transfer standard
definition cofactor where "cofactor A i j = det (minorM A i j)"
definition cofactorM where "cofactorM A = (χ i j. cofactor A i j)"
lemma cofactorM_eq: "cofactorM = to_vec ∘ Square_Matrix.cofactor ∘ from_vec"
unfolding cofactorM_def cofactor_def[abs_def] det_sq_matrix_eq[symmetric] minorM_eq fun_eq_iff
apply rule
apply transfer'
apply (simp add: fun_eq_iff vec_eq_iff)
apply transfer
apply simp
done
definition mat2matofpoly where "mat2matofpoly A = (χ i j. [: A $ i $ j :])"
definition charpoly where charpoly_def: "charpoly A = det (mat (monom 1 (Suc 0)) - mat2matofpoly A)"
lemma charpoly_eq: "charpoly A = Cayley_Hamilton.charpoly (from_vec A)"
unfolding charpoly_def Cayley_Hamilton.charpoly_def det_sq_matrix_eq[symmetric] X_def C_def
apply (intro arg_cong[where f=Square_Matrix.det])
apply transfer'
apply (simp add: fun_eq_iff mat_def mat2matofpoly_def C_def monom_Suc)
done
definition adjugate where "adjugate A = transpose (cofactorM A)"
lemma adjugate_eq: "adjugate = to_vec ∘ Square_Matrix.adjugate ∘ from_vec"
apply (simp add: adjugate_def Square_Matrix.adjugate_def fun_eq_iff)
apply rule
apply transfer'
apply (simp add: transpose_def cofactorM_eq to_vec.rep_eq
Square_Matrix.cofactor.rep_eq)
done
end