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) [CommSemiring R] [Semiring A] [Algebra R A] (b : A) (a : Polynomial R) : ↑(↑(PolyEquivTensor.toFunBilinear R A) b) a = b • ↑(Polynomial.aeval Polynomial.X) a

def PolyEquivTensor.toFunBilinear (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : A →ₗ[A] Polynomial R →ₗ[R] Polynomial A

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

theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ↑(↑(PolyEquivTensor.toFunBilinear R A) a) p = Polynomial.sum p fun n r => ↑(Polynomial.monomial n) (a * ↑(algebraMap R A) r)

def PolyEquivTensor.toFunLinear (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) →ₗ[R] Polynomial A

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

@[simp]

theorem PolyEquivTensor.toFunLinear_tmul_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ↑(PolyEquivTensor.toFunLinear R A) (a ⊗ₜ[R] p) = ↑(↑(PolyEquivTensor.toFunBilinear R A) a) p

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (k : ℕ) (h : Decidable ¬Polynomial.coeff p k = 0) (a : A) : (if ¬Polynomial.coeff p k = 0 then a * ↑(algebraMap R A) (Polynomial.coeff p k) else 0) = a * ↑(algebraMap R A) (Polynomial.coeff p k)

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (k : ℕ) (a₁ : A) (a₂ : A) (p₁ : Polynomial R) (p₂ : Polynomial R) : a₁ * a₂ * ↑(algebraMap R A) (Polynomial.coeff (p₁ * p₂) k) = Finset.sum (Finset.Nat.antidiagonal k) fun x => a₁ * ↑(algebraMap R A) (Polynomial.coeff p₁ x.fst) * (a₂ * ↑(algebraMap R A) (Polynomial.coeff p₂ x.snd))

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a₁ : A) (a₂ : A) (p₁ : Polynomial R) (p₂ : Polynomial R) : ↑(PolyEquivTensor.toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = ↑(PolyEquivTensor.toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * ↑(PolyEquivTensor.toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

theorem PolyEquivTensor.toFunLinear_one_tmul_one (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : ↑(PolyEquivTensor.toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

def PolyEquivTensor.toFunAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) →ₐ[R] Polynomial A

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

@[simp]

theorem PolyEquivTensor.toFunAlgHom_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ↑(PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = Polynomial.sum p fun n r => ↑(Polynomial.monomial n) (a * ↑(algebraMap R A) r)

def PolyEquivTensor.invFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) : TensorProduct R A (Polynomial R)

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

@[simp]

theorem PolyEquivTensor.invFun_add (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial A} {q : Polynomial A} : PolyEquivTensor.invFun R A (p + q) = PolyEquivTensor.invFun R A p + PolyEquivTensor.invFun R A q

theorem PolyEquivTensor.invFun_monomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) (a : A) : PolyEquivTensor.invFun R A (↑(Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n

theorem PolyEquivTensor.left_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : TensorProduct R A (Polynomial R)) : PolyEquivTensor.invFun R A (↑(PolyEquivTensor.toFunAlgHom R A) x) = x

theorem PolyEquivTensor.right_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : Polynomial A) : ↑(PolyEquivTensor.toFunAlgHom R A) (PolyEquivTensor.invFun R A x) = x

def PolyEquivTensor.equiv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A (Polynomial R) ≃ Polynomial A

(Implementation detail)

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

def polyEquivTensor (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Polynomial A ≃ₐ[R] TensorProduct R A (Polynomial R)

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

@[simp]

theorem polyEquivTensor_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) : ↑(polyEquivTensor R A) 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) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ↑(AlgEquiv.symm (polyEquivTensor R A)) (a ⊗ₜ[R] p) = Polynomial.sum p fun n r => ↑(Polynomial.monomial n) (a * ↑(algebraMap R A) r)

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

theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i : n) (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 : n) (j : n) (p : Polynomial R) (k : ℕ) : Polynomial.coeff (↑matPolyEquiv (Matrix.stdBasisMatrix i j p)) k = Matrix.stdBasisMatrix i j (Polynomial.coeff p 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 : 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} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (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} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) : ↑matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p

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 : n) (j : n) : Polynomial.support (m i j) ⊆ Polynomial.support (↑matPolyEquiv m)