mathlib documentation

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) [comm_semiring R] [semiring A] [algebra R A] :
A → polynomial Rpolynomial A

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

Equations
def poly_equiv_tensor.to_fun_linear_right (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] :

(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) [comm_semiring R] [semiring A] [algebra R 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) [comm_semiring R] [semiring A] [algebra R 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) [comm_semiring R] [semiring A] [algebra R A] (p : polynomial R) (k : ) (h : decidable (¬p.coeff k = 0)) (a : A) :
ite (¬p.coeff k = 0) (a * (algebra_map R A) (p.coeff k)) 0 = a * (algebra_map R A) (p.coeff k)

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) :
(a₁ * a₂) * (algebra_map R A) ((p₁ * p₂).coeff k) = ∑ (x : × ) in finset.nat.antidiagonal k, (a₁ * (algebra_map R A) (p₁.coeff x.fst)) * a₂ * (algebra_map R A) (p₂.coeff x.snd)

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) :

def poly_equiv_tensor.to_fun_alg_hom (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R 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) [comm_semiring R] [semiring A] [algebra R A] (a : A) (p : polynomial R) :

def poly_equiv_tensor.inv_fun (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R 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) [comm_semiring R] [semiring A] [algebra R A] {p q : polynomial A} :

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

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) :

def poly_equiv_tensor.equiv (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R 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) [comm_semiring R] [semiring A] [algebra R A] :

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

Equations
@[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) = finsupp.sum p (λ (n : ) (r : R), (polynomial.monomial n) (a * (algebra_map R A) r))

def mat_poly_equiv {R : Type u_1} [comm_semiring R] {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_2 {R : Type u_1} [comm_semiring R] {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} [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 : ) :
((mat_poly_equiv.symm) p i j).coeff k = p.coeff k i j

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