# Matrices of multivariate polynomials #

In this file, we prove results about matrices over an mv_polynomial ring. In particular, we provide `Matrix.mvPolynomialX` which associates every entry of a matrix with a unique variable.

## Tags #

matrix determinant, multivariate polynomial

source
noncomputable def Matrix.mvPolynomialX (m : Type u_1) (n : Type u_2) (R : Type u_3) [CommSemiring R] :
Matrix m n (MvPolynomial (m × n) R)

The matrix with variable `X (i,j)` at location `(i,j)`.

Equations

- Matrix.mvPolynomialX m n R = Matrix.of fun (i : m) (j : n) => MvPolynomial.X (i, j)

Instances For

source
@[simp]
theorem Matrix.mvPolynomialX_apply (m : Type u_1) (n : Type u_2) (R : Type u_3) [CommSemiring R] (i : m) (j : n) :
mvPolynomialX m n R i j = MvPolynomial.X (i, j)
source
theorem Matrix.mvPolynomialX_map_eval₂ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (A : Matrix m n S) :
(mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun (p : m × n) => A p.1 p.2) = A

Any matrix `A` can be expressed as the evaluation of `Matrix.mvPolynomialX`.

This is of particular use when `MvPolynomial (m × n) R` is an integral domain but `S` is not, as if the `MvPolynomial.eval₂` can be pulled to the outside of a goal, it can be solved in under cancellative assumptions.

source
theorem Matrix.mvPolynomialX_mapMatrix_eval {m : Type u_1} {R : Type u_3} [Fintype m] [DecidableEq m] [CommSemiring R] (A : Matrix m m R) :
(MvPolynomial.eval fun (p : m × m) => A p.1 p.2).mapMatrix (mvPolynomialX m m R) = A

A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `RingHom` on the LHS.

source
theorem Matrix.mvPolynomialX_mapMatrix_aeval {m : Type u_1} (R : Type u_3) {S : Type u_4} [Fintype m] [DecidableEq m] [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Matrix m m S) :
(MvPolynomial.aeval fun (p : m × m) => A p.1 p.2).mapMatrix (mvPolynomialX m m R) = A

A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `AlgHom` on the LHS.

source
theorem Matrix.det_mvPolynomialX_ne_zero (m : Type u_1) (R : Type u_3) [DecidableEq m] [Fintype m] [CommRing R] [Nontrivial R] :
(mvPolynomialX m m R).det ≠ 0

In a nontrivial ring, `Matrix.mvPolynomialX m m R` has non-zero determinant.