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
def
PolyEquivTensor.toFunBilinear
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
A →ₗ[A] Polynomial R →ₗ[R] Polynomial A
(Implementation detail).
The function underlying A ⊗[R] R[X] →ₐ[R] A[X],
as a bilinear function of two arguments.
Equations
- PolyEquivTensor.toFunBilinear R A = LinearMap.toSpanSingleton A (Polynomial R →ₗ[R] Polynomial A) (Polynomial.aeval Polynomial.X).toLinearMap
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 = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)
def
PolyEquivTensor.toFunLinear
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
TensorProduct R A (Polynomial R) →ₗ[R] Polynomial A
(Implementation detail).
The function underlying A ⊗[R] R[X] →ₐ[R] A[X],
as a linear map.
Equations
@[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)
:
(PolyEquivTensor.toFunLinear R A) (a ⊗ₜ[R] p) = ((PolyEquivTensor.toFunBilinear R A) a) p
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 ¬p.coeff k = 0)
(a : A)
:
(if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff 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) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff 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₂)
theorem
PolyEquivTensor.toFunLinear_one_tmul_one
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
(PolyEquivTensor.toFunLinear R A) (1 ⊗ₜ[R] 1) = 1
def
PolyEquivTensor.toFunAlgHom
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
TensorProduct R A (Polynomial R) →ₐ[R] Polynomial A
(Implementation detail).
The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X].
@[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) = p.sum 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)
:
TensorProduct R A (Polynomial R)
(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
- PolyEquivTensor.invFun R A p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
@[simp]
theorem
PolyEquivTensor.invFun_add
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
{p : Polynomial A}
{q : Polynomial A}
:
PolyEquivTensor.invFun R A (p + q) = PolyEquivTensor.invFun R A p + PolyEquivTensor.invFun R A q
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
theorem
PolyEquivTensor.left_inv
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : TensorProduct R A (Polynomial R))
:
PolyEquivTensor.invFun R A ((PolyEquivTensor.toFunAlgHom R A) x) = x
theorem
PolyEquivTensor.right_inv
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : Polynomial A)
:
(PolyEquivTensor.toFunAlgHom R A) (PolyEquivTensor.invFun R A x) = x
def
PolyEquivTensor.equiv
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
TensorProduct R A (Polynomial R) ≃ Polynomial A
(Implementation detail)
The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X].
Equations
- PolyEquivTensor.equiv R A = { toFun := ⇑(PolyEquivTensor.toFunAlgHom R A), invFun := PolyEquivTensor.invFun R A, left_inv := ⋯, right_inv := ⋯ }
def
polyEquivTensor
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Polynomial A ≃ₐ[R] TensorProduct R A (Polynomial R)
The R-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X]).
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
(polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum 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]
:
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
- matPolyEquiv = ((matrixEquivTensor R (Polynomial R) n).trans (Algebra.TensorProduct.comm R (Polynomial R) (Matrix n n R))).trans (polyEquivTensor R (Matrix n n R)).symm
@[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
@[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
@[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
@[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)
:
matPolyEquiv (Matrix.stdBasisMatrix i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.stdBasisMatrix i j x)
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 : ℕ)
:
(matPolyEquiv (Matrix.stdBasisMatrix i j p)).coeff k = Matrix.stdBasisMatrix i j (p.coeff 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)
:
(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 : n)
(j : n)
(k : ℕ)
:
(matPolyEquiv.symm p i j).coeff k = p.coeff 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)
:
(m i j).support ⊆ (matPolyEquiv m).support