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]
:
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
@[simp]
theorem
matPolyEquiv_symm_C
{R : Type u_1}
[CommSemiring R]
{n : Type w}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
@[simp]
theorem
matPolyEquiv_map_C
{R : Type u_1}
[CommSemiring R]
{n : Type w}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
@[simp]
theorem
matPolyEquiv_symm_X
{R : Type u_1}
[CommSemiring R]
{n : Type w}
[DecidableEq n]
[Fintype n]
:
@[simp]
theorem
matPolyEquiv_diagonal_X
{R : Type u_1}
[CommSemiring R]
{n : Type w}
[DecidableEq n]
[Fintype n]
:
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.stdBasisMatrix i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.stdBasisMatrix 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 : ℕ)
:
@[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)
:
@[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 : ℕ)
:
theorem
matPolyEquiv_smul_one
{R : Type u_1}
[CommSemiring R]
{n : Type w}
[DecidableEq n]
[Fintype n]
(p : Polynomial R)
:
@[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))
:
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)
:
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)
:
Extend a ring hom A → Mₙ(R)
to a ring hom A[X] → Mₙ(R[X])
.
Equations
Instances For
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)
:
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