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.
(Implementation detail).
The function underlying A ⊗[R] R[X] →ₐ[R] A[X]
,
as a bilinear function of two arguments.
Instances For
(Implementation detail).
The function underlying A ⊗[R] R[X] →ₐ[R] A[X]
,
as a linear map.
Instances For
(Implementation detail).
The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X]
.
Instances For
(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
(Implementation detail)
The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X]
.
Instances For
The R
-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X])
.
Instances For
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.)