# Algebra isomorphism between matrices of polynomials and polynomials of matrices #

Given [CommRing R] [Ring A] [Algebra R A] we show A[X] ≃ₐ[R] (A ⊗[R] R[X]). Combining this with the isomorphism Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R) proved earlier in RingTheory.MatrixAlgebra, 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.

@[simp]
theorem PolyEquivTensor.toFunBilinear_apply_apply (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (b : A) (a : ) :
() a = b (Polynomial.aeval Polynomial.X) a
def PolyEquivTensor.toFunBilinear (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a bilinear function of two arguments.

Equations
Instances For
theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a : A) (p : ) :
() p = p.sum fun (n : ) (r : R) => (a * () r)
def PolyEquivTensor.toFunLinear (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a linear map.

Equations
Instances For
@[simp]
theorem PolyEquivTensor.toFunLinear_tmul_apply (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a : A) (p : ) :
(a ⊗ₜ[R] p) = () p
theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (p : ) (k : ) (h : Decidable ¬p.coeff k = 0) (a : A) :
(if ¬p.coeff k = 0 then a * () (p.coeff k) else 0) = a * () (p.coeff k)
theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (k : ) (a₁ : A) (a₂ : A) (p₁ : ) (p₂ : ) :
a₁ * a₂ * () ((p₁ * p₂).coeff k) = .sum fun (x : ) => a₁ * () (p₁.coeff x.1) * (a₂ * () (p₂.coeff x.2))
theorem PolyEquivTensor.toFunLinear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a₁ : A) (a₂ : A) (p₁ : ) (p₂ : ) :
((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (a₁ ⊗ₜ[R] p₁) * (a₂ ⊗ₜ[R] p₂)
theorem PolyEquivTensor.toFunLinear_one_tmul_one (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :
(1 ⊗ₜ[R] 1) = 1
def PolyEquivTensor.toFunAlgHom (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

(Implementation detail). The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X].

Equations
Instances For
@[simp]
theorem PolyEquivTensor.toFunAlgHom_apply_tmul (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a : A) (p : ) :
(a ⊗ₜ[R] p) = p.sum fun (n : ) (r : R) => (a * () r)
def PolyEquivTensor.invFun (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (p : ) :

(Implementation detail.)

The bare function A[X] → A ⊗[R] R[X]. (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)

Equations
Instances For
@[simp]
theorem PolyEquivTensor.invFun_add (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] {p : } {q : } :
theorem PolyEquivTensor.invFun_monomial (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (n : ) (a : A) :
= a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n
theorem PolyEquivTensor.left_inv (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (x : TensorProduct R A ()) :
= x
theorem PolyEquivTensor.right_inv (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (x : ) :
() = x
def PolyEquivTensor.equiv (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

(Implementation detail)

The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X].

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
def polyEquivTensor (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

The R-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X]).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem polyEquivTensor_apply (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (p : ) :
() p = Polynomial.eval₂ (Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
@[simp]
theorem polyEquivTensor_symm_apply_tmul (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a : A) (p : ) :
().symm (a ⊗ₜ[R] p) = p.sum fun (n : ) (r : R) => (a * () r)
noncomputable def matPolyEquiv {R : Type u_1} [] {n : Type w} [] [] :

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
Instances For
@[simp]
theorem matPolyEquiv_symm_C {R : Type u_1} [] {n : Type w} [] [] (M : Matrix n n R) :
matPolyEquiv.symm (Polynomial.C M) = M.map Polynomial.C
@[simp]
theorem matPolyEquiv_map_C {R : Type u_1} [] {n : Type w} [] [] (M : Matrix n n R) :
matPolyEquiv (M.map Polynomial.C) = Polynomial.C M
@[simp]
theorem matPolyEquiv_symm_X {R : Type u_1} [] {n : Type w} [] [] :
matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun (x : n) => Polynomial.X
@[simp]
theorem matPolyEquiv_diagonal_X {R : Type u_1} [] {n : Type w} [] [] :
matPolyEquiv (Matrix.diagonal fun (x : n) => Polynomial.X) = Polynomial.X
theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [] {n : Type w} [] [] (i : n) (j : n) (k : ) (x : R) :
matPolyEquiv (Matrix.stdBasisMatrix i j ( x)) = ()
theorem matPolyEquiv_coeff_apply_aux_2 {R : Type u_1} [] {n : Type w} [] [] (i : n) (j : n) (p : ) (k : ) :
(matPolyEquiv ()).coeff k = Matrix.stdBasisMatrix i j (p.coeff k)
@[simp]
theorem matPolyEquiv_coeff_apply {R : Type u_1} [] {n : Type w} [] [] (m : Matrix n n ()) (k : ) (i : n) (j : n) :
(matPolyEquiv m).coeff k i j = (m i j).coeff k
@[simp]
theorem matPolyEquiv_symm_apply_coeff {R : Type u_1} [] {n : Type w} [] [] (p : Polynomial (Matrix n n R)) (i : n) (j : n) (k : ) :
(matPolyEquiv.symm p i j).coeff k = p.coeff k i j
theorem matPolyEquiv_smul_one {R : Type u_1} [] {n : Type w} [] [] (p : ) :
matPolyEquiv (p 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
@[simp]
theorem matPolyEquiv_map_smul {R : Type u_1} [] {n : Type w} [] [] (p : ) (M : Matrix n n ()) :
matPolyEquiv (p M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
theorem support_subset_support_matPolyEquiv {R : Type u_1} [] {n : Type w} [] [] (m : Matrix n n ()) (i : n) (j : n) :
(m i j).support (matPolyEquiv m).support