Algebra isomorphism between matrices of polynomials and polynomials of matrices

We obtain the algebra isomorphism

def matPolyEquiv : Matrix n n R[X] ≃ₐ[R] (Matrix n n R)[X]

which is characterized by

coeff (matPolyEquiv m) k i j = coeff (m i j) k

We will use this algebra isomorphism to prove the Cayley-Hamilton theorem.

noncomputable def matPolyEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] : Matrix n n (Polynomial R) ≃ₐ[R] Polynomial (Matrix n n R)

The algebra isomorphism stating "matrices of polynomials are the same as polynomials of matrices".

(You probably shouldn't attempt to use this underlying definition --- it's an algebra equivalence, and characterised extensionally by the lemma matPolyEquiv_coeff_apply below.)

@[simp]

theorem matPolyEquiv_symm_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) : matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C

@[simp]

theorem matPolyEquiv_map_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) : matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M

@[simp]

theorem matPolyEquiv_symm_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] : matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun (x : n) => Polynomial.X

@[simp]

theorem matPolyEquiv_diagonal_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] : matPolyEquiv (Matrix.diagonal fun (x : n) => Polynomial.X) = Polynomial.X

theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (k : ℕ) (x : R) : matPolyEquiv (Matrix.single i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.single i j x)

theorem matPolyEquiv_coeff_apply_aux_2 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (p : Polynomial R) (k : ℕ) : (matPolyEquiv (Matrix.single i j p)).coeff k = Matrix.single i j (p.coeff k)

@[simp]

theorem matPolyEquiv_coeff_apply {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (m : Matrix n n (Polynomial R)) (k : ℕ) (i j : n) : (matPolyEquiv m).coeff k i j = (m i j).coeff k

@[simp]

theorem matPolyEquiv_symm_apply_coeff {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial (Matrix n n R)) (i j : n) (k : ℕ) : (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

theorem matPolyEquiv_smul_one {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) : matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p

@[simp]

theorem matPolyEquiv_map_smul {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) (M : Matrix n n (Polynomial R)) : matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M

theorem matPolyEquiv_symm_map_eval {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Polynomial (Matrix n n R)) (r : R) : (matPolyEquiv.symm M).map (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M

theorem matPolyEquiv_eval_eq_map {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n (Polynomial R)) (r : R) : Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = M.map (Polynomial.eval r)

theorem matPolyEquiv_eval {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n (Polynomial R)) (r : R) (i j : n) : Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) i j = Polynomial.eval r (M i j)

theorem support_subset_support_matPolyEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (m : Matrix n n (Polynomial R)) (i j : n) : (m i j).support ⊆ (matPolyEquiv m).support

theorem eval_det {n : Type w} [DecidableEq n] [Fintype n] {R : Type u_3} [CommRing R] (M : Matrix n n (Polynomial R)) (r : R) : Polynomial.eval r M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det

theorem eval_det_add_X_smul {n : Type w} [DecidableEq n] [Fintype n] {R : Type u_3} [CommRing R] (A : Matrix n n (Polynomial R)) (M : Matrix n n R) : Polynomial.eval 0 (A + Polynomial.X • M.map ⇑Polynomial.C).det = Polynomial.eval 0 A.det

noncomputable def RingHom.polyToMatrix {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] {n : Type w} [DecidableEq n] [Fintype n] (f : A →+* Matrix n n R) : Polynomial A →+* Matrix n n (Polynomial R)

Extend a ring hom A → Mₙ(R) to a ring hom A[X] → Mₙ(R[X]).

theorem evalRingHom_mapMatrix_comp_polyToMatrix {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] {S : Type u_3} [CommSemiring S] (f : S →+* Matrix n n R) : (Polynomial.evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (Polynomial.evalRingHom 0)

theorem evalRingHom_mapMatrix_comp_compRingEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type u_4} [Fintype m] [DecidableEq m] : (Polynomial.evalRingHom 0).mapMatrix.comp ↑(Matrix.compRingEquiv m n (Polynomial R)) = (Matrix.compRingEquiv m n R).toRingHom.comp (Polynomial.evalRingHom 0).mapMatrix.mapMatrix