Algebra isomorphism between matrices of polynomials and polynomials of matrices
Given [comm_ring R] [ring A] [algebra R A]
we show polynomial A ≃ₐ[R] (A ⊗[R] polynomial R).
Combining this with the isomorphism matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) proved earlier
in ring_theory.matrix_algebra, we obtain the algebra isomorphism
def mat_poly_equiv :
matrix n n (polynomial R) ≃ₐ[R] polynomial (matrix n n R)
which is characterized by
coeff (mat_poly_equiv m) k i j = coeff (m i j) k
We will use this algebra isomorphism to prove the Cayley-Hamilton theorem.
(Implementation detail).
The bare function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A, on pure tensors.
Equations
- poly_equiv_tensor.to_fun R A a p = finsupp.sum p (λ (n : ℕ) (r : R), polynomial.monomial n (a * ⇑(algebra_map R A) r))
(Implementation detail).
The function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A,
as a linear map in the second factor.
Equations
- poly_equiv_tensor.to_fun_linear_right R A a = {to_fun := poly_equiv_tensor.to_fun R A a, map_add' := _, map_smul' := _}
(Implementation detail).
The function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A,
as a bilinear function of two arguments.
Equations
- poly_equiv_tensor.to_fun_bilinear R A = {to_fun := poly_equiv_tensor.to_fun_linear_right R A _inst_3, map_add' := _, map_smul' := _}
(Implementation detail).
The function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A,
as a linear map.
Equations
(Implementation detail).
The algebra homomorphism A ⊗[R] polynomial R →ₐ[R] polynomial A.
(Implementation detail.)
The bare function polynomial A → A ⊗[R] polynomial R.
(We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)
Equations
(Implementation detail)
The equivalence, ignoring the algebra structure, (A ⊗[R] polynomial R) ≃ polynomial A.
Equations
- poly_equiv_tensor.equiv R A = {to_fun := ⇑(poly_equiv_tensor.to_fun_alg_hom R A), inv_fun := poly_equiv_tensor.inv_fun R A _inst_3, left_inv := _, right_inv := _}
The R-algebra isomorphism polynomial A ≃ₐ[R] (A ⊗[R] polynomial R).
Equations
- poly_equiv_tensor R A = {to_fun := (poly_equiv_tensor.to_fun_alg_hom R A).to_fun, inv_fun := (poly_equiv_tensor.equiv R A).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm
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
mat_poly_equiv_coeff_apply below.)
Equations
- mat_poly_equiv = ((matrix_equiv_tensor R (polynomial R) n).trans (algebra.tensor_product.comm R (polynomial R) (matrix n n R))).trans (poly_equiv_tensor R (matrix n n R)).symm