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.

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

Equations
Instances For
    source
    @[simp]
    theorem matPolyEquiv_symm_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
    matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C
    source
    @[simp]
    theorem matPolyEquiv_map_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
    matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M
    source
    @[simp]
    theorem matPolyEquiv_symm_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :
    matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun (x : n) => Polynomial.X
    source
    @[simp]
    theorem matPolyEquiv_diagonal_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :
    matPolyEquiv (Matrix.diagonal fun (x : n) => Polynomial.X) = Polynomial.X
    source
    theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (k : ℕ) (x : R) :
    matPolyEquiv (Matrix.single i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.single i j x)
    source
    theorem matPolyEquiv_coeff_apply_aux_2 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (p : Polynomial R) (k : ℕ) :
    (matPolyEquiv (Matrix.single i j p)).coeff k = Matrix.single i j (p.coeff k)
    source
    @[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
    source
    @[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
    source
    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
    source
    @[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)) :
    matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
    source
    theorem matPolyEquiv_symm_map_eval {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Polynomial (Matrix n n R)) (r : R) :
    (matPolyEquiv.symm M).map (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M
    source
    theorem matPolyEquiv_eval_eq_map {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n (Polynomial R)) (r : R) :
    Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = M.map (Polynomial.eval r)
    source
    theorem matPolyEquiv_eval {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n (Polynomial R)) (r : R) (i j : n) :
    Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) i j = Polynomial.eval r (M i j)
    source
    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) :
    (m i j).support ⊆ (matPolyEquiv m).support
    source
    theorem eval_det {n : Type w} [DecidableEq n] [Fintype n] {R : Type u_3} [CommRing R] (M : Matrix n n (Polynomial R)) (r : R) :
    Polynomial.eval r M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det
    source
    theorem eval_det_add_X_smul {n : Type w} [DecidableEq n] [Fintype n] {R : Type u_3} [CommRing R] (A : Matrix n n (Polynomial R)) (M : Matrix n n R) :
    Polynomial.eval 0 (A + Polynomial.X • M.map ⇑Polynomial.C).det = Polynomial.eval 0 A.det
    source
    noncomputable 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) :
    Polynomial A →+* Matrix n n (Polynomial R)

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

    Equations
    Instances For
      source
      theorem evalRingHom_mapMatrix_comp_polyToMatrix {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] {S : Type u_3} [CommSemiring S] (f : S →+* Matrix n n R) :
      (Polynomial.evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (Polynomial.evalRingHom 0)
      source
      theorem evalRingHom_mapMatrix_comp_compRingEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type u_4} [Fintype m] [DecidableEq m] :
      (Polynomial.evalRingHom 0).mapMatrix.comp ↑(Matrix.compRingEquiv m n (Polynomial R)) = (Matrix.compRingEquiv m n R).toRingHom.comp (Polynomial.evalRingHom 0).mapMatrix.mapMatrix