HepLean Documentation

Mathlib.RingTheory.PolynomialAlgebra

Algebra isomorphism between matrices of polynomials and polynomials of matrices #

Given [CommRing 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 RingTheory.MatrixAlgebra, we obtain the algebra isomorphism

def matPolyEquiv :
    Matrix n n R[X] ≃ₐ[R] (Matrix n n R)[X]

which is characterized by

coeff (matPolyEquiv m) k i j = coeff (m i j) k

We will use this algebra isomorphism to prove the Cayley-Hamilton theorem.

def PolyEquivTensor.toFunBilinear (R : Type u_1) (A : Type u_2) [CommSemiring 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

PolyEquivTensor.toFunBilinear R A = LinearMap.toSpanSingleton A (Polynomial R →ₗ[R] Polynomial A) (Polynomial.aeval Polynomial.X).toLinearMap

Instances For

@[simp]

theorem PolyEquivTensor.toFunBilinear_apply_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (b : A) (a : Polynomial R) :

((PolyEquivTensor.toFunBilinear R A) b) a = b • (Polynomial.aeval Polynomial.X) a

theorem PolyEquivTensor.toFunBilinear_apply_eq_sum (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :

((PolyEquivTensor.toFunBilinear R A) a) p = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

def PolyEquivTensor.toFunLinear (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :

TensorProduct R A (Polynomial R) →ₗ[R] Polynomial A

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

Equations

PolyEquivTensor.toFunLinear R A = TensorProduct.lift (↑R (PolyEquivTensor.toFunBilinear R A))

Instances For

@[simp]

theorem PolyEquivTensor.toFunLinear_tmul_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :

(PolyEquivTensor.toFunLinear R A) (a ⊗ₜ[R] p) = ((PolyEquivTensor.toFunBilinear R A) a) p

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (k : ℕ) (h : Decidable ¬p.coeff k = 0) (a : A) :

(if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (k : ℕ) (a₁ a₂ : A) (p₁ p₂ : Polynomial R) :

a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))

theorem PolyEquivTensor.toFunLinear_mul_tmul_mul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a₁ a₂ : A) (p₁ p₂ : Polynomial R) :

(PolyEquivTensor.toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (PolyEquivTensor.toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (PolyEquivTensor.toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

theorem PolyEquivTensor.toFunLinear_one_tmul_one (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :

(PolyEquivTensor.toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

def PolyEquivTensor.toFunAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :

TensorProduct R A (Polynomial R) →ₐ[R] Polynomial A

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

Equations

PolyEquivTensor.toFunAlgHom R A = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (PolyEquivTensor.toFunLinear R A) ⋯ ⋯

Instances For

@[simp]

theorem PolyEquivTensor.toFunAlgHom_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :

(PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

def PolyEquivTensor.invFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) :

TensorProduct 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

PolyEquivTensor.invFun R A p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p

Instances For

@[simp]

theorem PolyEquivTensor.invFun_add (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial A} :

PolyEquivTensor.invFun R A (p + q) = PolyEquivTensor.invFun R A p + PolyEquivTensor.invFun R A q

theorem PolyEquivTensor.invFun_monomial (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) (a : A) :

PolyEquivTensor.invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n

theorem PolyEquivTensor.left_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : TensorProduct R A (Polynomial R)) :

PolyEquivTensor.invFun R A ((PolyEquivTensor.toFunAlgHom R A) x) = x

theorem PolyEquivTensor.right_inv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (x : Polynomial A) :

(PolyEquivTensor.toFunAlgHom R A) (PolyEquivTensor.invFun R A x) = x

def PolyEquivTensor.equiv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :

TensorProduct R A (Polynomial R) ≃ Polynomial A

(Implementation detail)

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

Equations

PolyEquivTensor.equiv R A = { toFun := ⇑(PolyEquivTensor.toFunAlgHom R A), invFun := PolyEquivTensor.invFun R A, left_inv := ⋯, right_inv := ⋯ }

Instances For

def polyEquivTensor (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :

Polynomial A ≃ₐ[R] TensorProduct R A (Polynomial R)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem polyEquivTensor_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial A) :

(polyEquivTensor R A) p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p

@[simp]

theorem polyEquivTensor_symm_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) :

(polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun (n : ℕ) (r : R) => (Polynomial.monomial n) (a * (algebraMap R A) r)

noncomputable def matPolyEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq 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 matPolyEquiv_coeff_apply below.)

Equations

matPolyEquiv = ((matrixEquivTensor R (Polynomial R) n).trans (Algebra.TensorProduct.comm R (Polynomial R) (Matrix n n R))).trans (polyEquivTensor R (Matrix n n R)).symm

Instances For

@[simp]

theorem matPolyEquiv_symm_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :

matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C

@[simp]

theorem matPolyEquiv_map_C {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :

matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M

@[simp]

theorem matPolyEquiv_symm_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :

matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun (x : n) => Polynomial.X

@[simp]

theorem matPolyEquiv_diagonal_X {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] :

matPolyEquiv (Matrix.diagonal fun (x : n) => Polynomial.X) = Polynomial.X

theorem matPolyEquiv_coeff_apply_aux_1 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (k : ℕ) (x : R) :

matPolyEquiv (Matrix.stdBasisMatrix i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.stdBasisMatrix i j x)

theorem matPolyEquiv_coeff_apply_aux_2 {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (p : Polynomial R) (k : ℕ) :

(matPolyEquiv (Matrix.stdBasisMatrix i j p)).coeff k = Matrix.stdBasisMatrix i j (p.coeff k)

@[simp]

theorem matPolyEquiv_coeff_apply {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (m : Matrix n n (Polynomial R)) (k : ℕ) (i j : n) :

(matPolyEquiv m).coeff k i j = (m i j).coeff k

@[simp]

theorem matPolyEquiv_symm_apply_coeff {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial (Matrix n n R)) (i j : n) (k : ℕ) :

(matPolyEquiv.symm p i j).coeff k = p.coeff k i j

theorem matPolyEquiv_smul_one {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) :

matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p

@[simp]

theorem matPolyEquiv_map_smul {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) (M : Matrix n n (Polynomial R)) :

matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M

theorem support_subset_support_matPolyEquiv {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (m : Matrix n n (Polynomial R)) (i j : n) :

(m i j).support ⊆ (matPolyEquiv m).support