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 => ↑(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
      @[simp]
      theorem PolyEquivTensor.toFunLinear_tmul_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :
      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.Nat.antidiagonal k) fun x => a₁ * ↑(algebraMap R A) (Polynomial.coeff p₁ x.fst) * (a₂ * ↑(algebraMap R A) (Polynomial.coeff p₂ x.snd))
      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
      • One or more equations did not get rendered due to their size.
      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 => ↑(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
          • One or more equations did not get rendered due to their size.
          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 => ↑(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
                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 (Matrix n n R) Matrix.semiring (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 (Matrix n n R) Matrix.semiring 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
                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)