# 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.

source
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.)

Equations

- matPolyEquiv = ((matrixEquivTensor n R (Polynomial R)).trans (Algebra.TensorProduct.comm R (Polynomial R) (Matrix n n R))).trans (polyEquivTensor R (Matrix n n R)).symm

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
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)
source
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)
source
@[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
source
@[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
source
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
source
@[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
source
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
source
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)
source
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)
source
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
source
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
source
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
source
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])`.

Equations

- f.polyToMatrix = matPolyEquiv.symm.toRingEquiv.toRingHom.comp (Polynomial.mapRingHom f)

Instances For

source
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)
source
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