mathlib3 documentation

ring_theory.polynomial_algebra

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

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

Equations
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] :

(Implementation detail). The function underlying A ⊗[R] R[X] →ₐ[R] A[X], 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) = (finset.nat.antidiagonal k).sum (λ (x : × ), 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) :
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] A[X].

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

(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
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]) ≃ A[X].

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 A[X] ≃ₐ[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 : 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] :

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