Metamath Proof Explorer


Table of Contents - 11.4.4. Ring isomorphism between polynomial matrices and polynomials over matrices

The main result of this section is theorem pmmpric, which shows that the ring of polynomial matrices and the ring of polynomials having matrices as coefficients (called "polynomials over matrices" in the following) are isomorphic:<br> <br><br> Or in a more common notation:<br> corresponds to M(n, R[t]), the ring of n x n polynomial matrices over the ring R.<br> corresponds to M(n, R)[t], the polynomial ring over the ring of n x n matrices with entries in ring R. <br><br> <br><br> with and ( i m j ) ) is an isomorphism between these rings:<br> <br> with (see pm2mpf1o and pm2mprngiso), and<br> <br> p ) <br><br> is the corresponding inverse function:<br> <br> (see mp2pm2mp). <br><br> In this section, the following conventions are mostly used: <ul> <li> is a (unital) ring (see df-ring)</li> <li> is the polynomial algebra over (the ring) (see df-ply1) <ul> <li> is its base set (see df-base)</li> <li> is its variable (see df-vr1)</li> <li> is its scalar multiplication (see df-vsca or lmodvscl)</li> <li> is its exponentiation (see df-mulg) </li> </ul></li> <li> is the algebra of N x N matrices over (the ring) (see df-mat)</li> <li> is the algebra of N x N matrices over (the polynomial ring) . <ul> <li> is its base set</li> <li> is a concrete polynomial matrix</li> </ul></li> <li> is the polynomial algebra over (the matrix ring) . <ul> <li> is its base set</li> <li> is a concrete polynomial with matrix coefficients</li> <li> is its variable</li> <li> is its scalar multiplication</li> <li> is its exponentiation</li></ul></li> </ul>

  1. cpm2mp
  2. df-pm2mp
  3. pm2mpf1lem
  4. pm2mpval
  5. pm2mpfval
  6. pm2mpcl
  7. pm2mpf
  8. pm2mpf1
  9. pm2mpcoe1
  10. idpm2idmp
  11. mptcoe1matfsupp
  12. mply1topmatcllem
  13. mply1topmatval
  14. mply1topmatcl
  15. mp2pm2mplem1
  16. mp2pm2mplem2
  17. mp2pm2mplem3
  18. mp2pm2mplem4
  19. mp2pm2mplem5
  20. mp2pm2mp
  21. pm2mpghmlem2
  22. pm2mpghmlem1
  23. pm2mpfo
  24. pm2mpf1o
  25. pm2mpghm
  26. pm2mpgrpiso
  27. pm2mpmhmlem1
  28. pm2mpmhmlem2
  29. pm2mpmhm
  30. pm2mprhm
  31. pm2mprngiso
  32. pmmpric
  33. monmat2matmon
  34. pm2mp