HepLean Documentation

Mathlib.LinearAlgebra.Matrix.MvPolynomial

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
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) :
    Matrix.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) :
    (Matrix.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 (Matrix.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 (Matrix.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] :
    (Matrix.mvPolynomialX m m R).det ≠ 0

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