Documentation

Mathlib.RingTheory.MatrixPolynomialAlgebra

Algebra isomorphism between matrices of polynomials and polynomials of matrices #

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.

noncomputable def matPolyEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :

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

Equations
Instances For
    @[simp]
    theorem matPolyEquiv_symm_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
    @[simp]
    theorem matPolyEquiv_map_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
    @[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 j : n) :
    (matPolyEquiv m).coeff k i j = (m i j).coeff 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 j : n) (k : ) :
    (matPolyEquiv.symm p i j).coeff k = p.coeff k i j
    @[simp]
    theorem matPolyEquiv_map_smul {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) (M : Matrix n n (Polynomial R)) :
    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 j : n) :
    def RingHom.polyToMatrix {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] {n : Type w} [DecidableEq n] [Fintype n] (f : A →+* Matrix n n R) :

    Extend a ring hom A → Mₙ(R) to a ring hom A[X] → Mₙ(R[X]).

    Equations
    Instances For