Algebra isomorphism between matrices of polynomials and polynomials of matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Given [comm_ring 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 ring_theory.matrix_algebra, we obtain the algebra isomorphism
def mat_poly_equiv :
matrix n n R[X] ≃ₐ[R] (matrix n n R)[X]
which is characterized by
coeff (mat_poly_equiv m) k i j = coeff (m i j) k
We will use this algebra isomorphism to prove the Cayley-Hamilton theorem.
noncomputable
def
poly_equiv_tensor.to_fun_bilinear
(R : Type u_1)
(A : Type u_2)
[comm_semiring 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
@[simp]
theorem
poly_equiv_tensor.to_fun_bilinear_apply_apply
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(b : A)
(ᾰ : polynomial R) :
⇑(⇑(poly_equiv_tensor.to_fun_bilinear R A) b) ᾰ = b • ⇑(polynomial.aeval polynomial.X) ᾰ
theorem
poly_equiv_tensor.to_fun_bilinear_apply_eq_sum
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(a : A)
(p : polynomial R) :
⇑(⇑(poly_equiv_tensor.to_fun_bilinear R A) a) p = p.sum (λ (n : ℕ) (r : R), ⇑(polynomial.monomial n) (a * ⇑(algebra_map R A) r))
noncomputable
def
poly_equiv_tensor.to_fun_linear
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A] :
tensor_product 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
poly_equiv_tensor.to_fun_linear_tmul_apply
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(a : A)
(p : polynomial R) :
⇑(poly_equiv_tensor.to_fun_linear R A) (a ⊗ₜ[R] p) = ⇑(⇑(poly_equiv_tensor.to_fun_bilinear R A) a) p
theorem
poly_equiv_tensor.to_fun_linear_mul_tmul_mul_aux_1
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(p : polynomial R)
(k : ℕ)
(h : decidable (¬p.coeff k = 0))
(a : A) :
theorem
poly_equiv_tensor.to_fun_linear_mul_tmul_mul_aux_2
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(k : ℕ)
(a₁ a₂ : A)
(p₁ p₂ : polynomial R) :
theorem
poly_equiv_tensor.to_fun_linear_mul_tmul_mul
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(a₁ a₂ : A)
(p₁ p₂ : polynomial R) :
theorem
poly_equiv_tensor.to_fun_linear_algebra_map_tmul_one
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(poly_equiv_tensor.to_fun_linear R A) (⇑(algebra_map R A) r ⊗ₜ[R] 1) = ⇑(algebra_map R (polynomial A)) r
noncomputable
def
poly_equiv_tensor.to_fun_alg_hom
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A] :
tensor_product R A (polynomial R) →ₐ[R] polynomial A
(Implementation detail).
The algebra homomorphism A ⊗[R] R[X] →ₐ[R] A[X].
@[simp]
theorem
poly_equiv_tensor.to_fun_alg_hom_apply_tmul
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(a : A)
(p : polynomial R) :
⇑(poly_equiv_tensor.to_fun_alg_hom R A) (a ⊗ₜ[R] p) = p.sum (λ (n : ℕ) (r : R), ⇑(polynomial.monomial n) (a * ⇑(algebra_map R A) r))
noncomputable
def
poly_equiv_tensor.inv_fun
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(p : polynomial A) :
tensor_product 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
@[simp]
theorem
poly_equiv_tensor.inv_fun_add
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
{p q : polynomial A} :
poly_equiv_tensor.inv_fun R A (p + q) = poly_equiv_tensor.inv_fun R A p + poly_equiv_tensor.inv_fun R A q
theorem
poly_equiv_tensor.inv_fun_monomial
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(n : ℕ)
(a : A) :
poly_equiv_tensor.inv_fun R A (⇑(polynomial.monomial n) a) = ⇑algebra.tensor_product.include_left a * 1 ⊗ₜ[R] polynomial.X ^ n
theorem
poly_equiv_tensor.left_inv
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(x : tensor_product R A (polynomial R)) :
poly_equiv_tensor.inv_fun R A (⇑(poly_equiv_tensor.to_fun_alg_hom R A) x) = x
theorem
poly_equiv_tensor.right_inv
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(x : polynomial A) :
⇑(poly_equiv_tensor.to_fun_alg_hom R A) (poly_equiv_tensor.inv_fun R A x) = x
noncomputable
def
poly_equiv_tensor.equiv
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A] :
tensor_product R A (polynomial R) ≃ polynomial A
(Implementation detail)
The equivalence, ignoring the algebra structure, (A ⊗[R] R[X]) ≃ A[X].
Equations
- poly_equiv_tensor.equiv R A = {to_fun := ⇑(poly_equiv_tensor.to_fun_alg_hom R A), inv_fun := poly_equiv_tensor.inv_fun R A _inst_3, left_inv := _, right_inv := _}
noncomputable
def
poly_equiv_tensor
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A] :
polynomial A ≃ₐ[R] tensor_product R A (polynomial R)
The R-algebra isomorphism A[X] ≃ₐ[R] (A ⊗[R] R[X]).
Equations
- poly_equiv_tensor R A = {to_fun := (poly_equiv_tensor.to_fun_alg_hom R A).to_fun, inv_fun := (poly_equiv_tensor.equiv R A).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm
@[simp]
theorem
poly_equiv_tensor_apply
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(p : polynomial A) :
@[simp]
theorem
poly_equiv_tensor_symm_apply_tmul
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[semiring A]
[algebra R A]
(a : A)
(p : polynomial R) :
⇑((poly_equiv_tensor R A).symm) (a ⊗ₜ[R] p) = p.sum (λ (n : ℕ) (r : R), ⇑(polynomial.monomial n) (a * ⇑(algebra_map R A) r))
noncomputable
def
mat_poly_equiv
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq 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
mat_poly_equiv_coeff_apply below.)
Equations
- mat_poly_equiv = ((matrix_equiv_tensor R (polynomial R) n).trans (algebra.tensor_product.comm R (polynomial R) (matrix n n R))).trans (poly_equiv_tensor R (matrix n n R)).symm
theorem
mat_poly_equiv_coeff_apply_aux_1
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(i j : n)
(k : ℕ)
(x : R) :
⇑mat_poly_equiv (matrix.std_basis_matrix i j (⇑(polynomial.monomial k) x)) = ⇑(polynomial.monomial k) (matrix.std_basis_matrix i j x)
theorem
mat_poly_equiv_coeff_apply_aux_2
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(i j : n)
(p : polynomial R)
(k : ℕ) :
(⇑mat_poly_equiv (matrix.std_basis_matrix i j p)).coeff k = matrix.std_basis_matrix i j (p.coeff k)
@[simp]
theorem
mat_poly_equiv_coeff_apply
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(m : matrix n n (polynomial R))
(k : ℕ)
(i j : n) :
(⇑mat_poly_equiv m).coeff k i j = (m i j).coeff k
@[simp]
theorem
mat_poly_equiv_symm_apply_coeff
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(p : polynomial (matrix n n R))
(i j : n)
(k : ℕ) :
theorem
mat_poly_equiv_smul_one
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(p : polynomial R) :
⇑mat_poly_equiv (p • 1) = polynomial.map (algebra_map R (matrix n n R)) p
theorem
support_subset_support_mat_poly_equiv
{R : Type u_1}
[comm_semiring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(m : matrix n n (polynomial R))
(i j : n) :
(m i j).support ⊆ (⇑mat_poly_equiv m).support