# mathlibdocumentation

ring_theory.polynomial_algebra

# Algebra isomorphism between matrices of polynomials and polynomials of matrices

Given [comm_ring R] [ring A] [algebra R A] we show polynomial A ≃ₐ[R] (A ⊗[R] polynomial R). 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 (polynomial R) ≃ₐ[R] polynomial (matrix n n R)


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.

def poly_equiv_tensor.to_fun (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
A →

(Implementation detail). The bare function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A, on pure tensors.

Equations
• p = (λ (n : ) (r : R), (a * A) r))
def poly_equiv_tensor.to_fun_linear_right (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
A → →ₗ[R]

(Implementation detail). The function underlying A ⊗[R] polynomial R →ₐ[R] polynomial A, as a linear map in the second factor.

Equations
def poly_equiv_tensor.to_fun_bilinear (R : Type u_1) (A : Type u_2) [semiring A] [ A] :

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

Equations
def poly_equiv_tensor.to_fun_linear (R : Type u_1) (A : Type u_2) [semiring A] [ A] :

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

Equations
theorem poly_equiv_tensor.to_fun_linear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [semiring A] [ A] (p : polynomial R) (k : ) (h : decidable (¬p.coeff k = 0)) (a : A) :
ite (¬p.coeff k = 0) (a * A) (p.coeff k)) 0 = a * A) (p.coeff k)

theorem poly_equiv_tensor.to_fun_linear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [semiring A] [ A] (k : ) (a₁ a₂ : A) (p₁ p₂ : polynomial R) :
(a₁ * a₂) * A) ((p₁ * p₂).coeff k) = ∑ (x : × ) in , (a₁ * A) (p₁.coeff x.fst)) * a₂ * A) (p₂.coeff x.snd)

theorem poly_equiv_tensor.to_fun_linear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [semiring A] [ A] (a₁ a₂ : A) (p₁ p₂ : polynomial R) :
((a₁ * a₂) ⊗ₜ[R] p₁ * p₂) = (a₁ ⊗ₜ[R] p₁)) * (a₂ ⊗ₜ[R] p₂)

theorem poly_equiv_tensor.to_fun_linear_algebra_map_tmul_one (R : Type u_1) (A : Type u_2) [semiring A] [ A] (r : R) :
( A) r ⊗ₜ[R] 1) = (polynomial A)) r

def poly_equiv_tensor.to_fun_alg_hom (R : Type u_1) (A : Type u_2) [semiring A] [ A] :

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

Equations
@[simp]
theorem poly_equiv_tensor.to_fun_alg_hom_apply_tmul (R : Type u_1) (A : Type u_2) [semiring A] [ A] (a : A) (p : polynomial R) :
(a ⊗ₜ[R] p) = (λ (n : ) (r : R), (a * A) r))

def poly_equiv_tensor.inv_fun (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
A

(Implementation detail.)

The bare function polynomial A → A ⊗[R] polynomial R. (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) [semiring A] [ A] {p q : polynomial A} :
(p + q) =

theorem poly_equiv_tensor.inv_fun_monomial (R : Type u_1) (A : Type u_2) [semiring A] [ A] (n : ) (a : A) :
( a) =

theorem poly_equiv_tensor.left_inv (R : Type u_1) (A : Type u_2) [semiring A] [ A] (x : A ) :
= x

theorem poly_equiv_tensor.right_inv (R : Type u_1) (A : Type u_2) [semiring A] [ A] (x : polynomial A) :
= x

def poly_equiv_tensor.equiv (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
A

(Implementation detail)

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

Equations
def poly_equiv_tensor (R : Type u_1) (A : Type u_2) [semiring A] [ A] :

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

Equations
@[simp]
theorem poly_equiv_tensor_apply (R : Type u_1) (A : Type u_2) [semiring A] [ A] (p : polynomial A) :

@[simp]
theorem poly_equiv_tensor_symm_apply_tmul (R : Type u_1) (A : Type u_2) [semiring A] [ A] (a : A) (p : polynomial R) :
A).symm) (a ⊗ₜ[R] p) = (λ (n : ) (r : R), (a * A) r))

def mat_poly_equiv {R : Type u_1} {n : Type w} [decidable_eq 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 mat_poly_equiv_coeff_apply below.)

Equations
theorem mat_poly_equiv_coeff_apply_aux_1 {R : Type u_1} {n : Type w} [decidable_eq n] [fintype n] (i j : n) (k : ) (x : R) :

theorem mat_poly_equiv_coeff_apply_aux_2 {R : Type u_1} {n : Type w} [decidable_eq n] [fintype n] (i j : n) (p : polynomial R) (k : ) :

@[simp]
theorem mat_poly_equiv_coeff_apply {R : Type u_1} {n : Type w} [decidable_eq n] [fintype n] (m : n (polynomial R)) (k : ) (i j : n) :
.coeff k i j = (m i j).coeff k

@[simp]
theorem mat_poly_equiv_symm_apply_coeff {R : Type u_1} {n : Type w} [decidable_eq n] [fintype n] (p : polynomial (matrix n n R)) (i j : n) (k : ) :
((mat_poly_equiv.symm) p i j).coeff k = p.coeff k i j

theorem mat_poly_equiv_smul_one {R : Type u_1} {n : Type w} [decidable_eq n] [fintype n] (p : polynomial R) :