# Documentation

Mathlib.RingTheory.PolynomialAlgebra

# 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 : ) :
↑(↑() b) 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.

Instances For
theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (a : A) (p : ) :
↑(↑() a) p = Polynomial.sum p fun n 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.

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) = ↑(↑() a) p
theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] (p : ) (k : ) (h : Decidable ¬ = 0) (a : A) :
(if ¬ = 0 then a * ↑() () else 0) = a * ↑() ()
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₂ * ↑() (Polynomial.coeff (p₁ * p₂) k) = Finset.sum () fun x => a₁ * ↑() (Polynomial.coeff p₁ x.fst) * (a₂ * ↑() (Polynomial.coeff p₂ x.snd))
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].

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) = Polynomial.sum p fun n 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.)

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) :
PolyEquivTensor.invFun R 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 ()) :
PolyEquivTensor.invFun R A (↑() x) = 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].

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

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 : ) :
↑() (a ⊗ₜ[R] p) = Polynomial.sum p fun n 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.)

Instances For
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 : ) :
Polynomial.coeff (matPolyEquiv ()) k =
@[simp]
theorem matPolyEquiv_coeff_apply {R : Type u_1} [] {n : Type w} [] [] (m : Matrix n n ()) (k : ) (i : n) (j : n) :
Polynomial.coeff (Matrix n n R) Matrix.semiring (matPolyEquiv m) k i j = Polynomial.coeff (m i j) 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 : ) :
Polynomial.coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = Polynomial.coeff (Matrix n n R) Matrix.semiring p 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
theorem support_subset_support_matPolyEquiv {R : Type u_1} [] {n : Type w} [] [] (m : Matrix n n ()) (i : n) (j : n) :
Polynomial.support (m i j) Polynomial.support (matPolyEquiv m)