Documentation

Mathlib.RingTheory.PolynomialAlgebra

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.

@[simp]
theorem PolyEquivTensor.toFunBilinear_apply_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (b : A) (a : Polynomial R) :
((PolyEquivTensor.toFunBilinear R A) b) a = b (Polynomial.aeval Polynomial.X) a

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a bilinear function of two arguments.

Equations
Instances For
    theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :
    ((PolyEquivTensor.toFunBilinear R A) a) p = Polynomial.sum p fun (n : ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

    (Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], as a linear map.

    Equations
    Instances For
      theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (k : ) (h : Decidable ¬Polynomial.coeff p k = 0) (a : A) :
      (if ¬Polynomial.coeff p k = 0 then a * (algebraMap R A) (Polynomial.coeff p k) else 0) = a * (algebraMap R A) (Polynomial.coeff p k)
      theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (k : ) (a₁ : A) (a₂ : A) (p₁ : Polynomial R) (p₂ : Polynomial R) :
      a₁ * a₂ * (algebraMap R A) (Polynomial.coeff (p₁ * p₂) k) = Finset.sum (Finset.antidiagonal k) fun (x : × ) => a₁ * (algebraMap R A) (Polynomial.coeff p₁ x.1) * (a₂ * (algebraMap R A) (Polynomial.coeff p₂ x.2))
      theorem PolyEquivTensor.toFunLinear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a₁ : A) (a₂ : A) (p₁ : Polynomial R) (p₂ : Polynomial R) :
      (PolyEquivTensor.toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (PolyEquivTensor.toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (PolyEquivTensor.toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

      (Implementation detail). The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X].

      Equations
      Instances For
        @[simp]
        theorem PolyEquivTensor.toFunAlgHom_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :
        (PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = Polynomial.sum p fun (n : ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)
        def PolyEquivTensor.invFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) :

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

        Equations
        Instances For
          theorem PolyEquivTensor.invFun_monomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (n : ) (a : A) :
          PolyEquivTensor.invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n

          (Implementation detail)

          The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X].

          Equations
          Instances For

            The R-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X]).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem polyEquivTensor_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) :
              (polyEquivTensor R A) p = Polynomial.eval₂ (Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
              @[simp]
              theorem polyEquivTensor_symm_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :
              (AlgEquiv.symm (polyEquivTensor R A)) (a ⊗ₜ[R] p) = Polynomial.sum p fun (n : ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)
              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
              • One or more equations did not get rendered due to their size.
              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) :
                (AlgEquiv.symm matPolyEquiv) (Polynomial.C M) = Matrix.map M Polynomial.C
                @[simp]
                theorem matPolyEquiv_map_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
                matPolyEquiv (Matrix.map M Polynomial.C) = Polynomial.C M
                @[simp]
                theorem matPolyEquiv_symm_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :
                (AlgEquiv.symm matPolyEquiv) Polynomial.X = Matrix.diagonal fun (x : n) => Polynomial.X
                @[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
                theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i : n) (j : n) (k : ) (x : R) :
                theorem matPolyEquiv_coeff_apply_aux_2 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i : n) (j : n) (p : Polynomial R) (k : ) :
                @[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 : n) (j : n) :
                Polynomial.coeff (matPolyEquiv m) k i j = Polynomial.coeff (m i j) 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 : n) (j : n) (k : ) :
                Polynomial.coeff ((AlgEquiv.symm matPolyEquiv) p i j) k = Polynomial.coeff p k i j
                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
                @[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
                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 : n) (j : n) :
                Polynomial.support (m i j) Polynomial.support (matPolyEquiv m)