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] 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] 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.

noncomputable 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] R[X] →ₐ[R] polynomial A, 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) (ᾰ : R[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 : R[X]) :
((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] :

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] polynomial A, 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 : R[X]) :
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 : R[X]) (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₂ : R[X]) :
(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₂ : R[X]) :
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] :

(Implementation detail). The algebra homomorphism A ⊗[R] R[X] →ₐ[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 : R[X]) :
(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 : A[X]) :
A R[X]

(Implementation detail.)

The bare function polynomial A → 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 : A[X]} :
theorem poly_equiv_tensor.left_inv (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] (x : A R[X]) :
theorem poly_equiv_tensor.right_inv (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] (x : A[X]) :
noncomputable 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] R[X]) ≃ polynomial A.

Equations
noncomputable 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] R[X]).

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 : R[X]) :
((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] :

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 : R[X]) (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 R[X]) (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 : (matrix n n R)[X]) (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 : R[X]) :
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 R[X]) (i j : n) :