Matrices of multivariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

matrix determinant, multivariate polynomial

source

noncomputable def matrix.mv_polynomial_X (m : Type u_1) (n : Type u_2) (R : Type u_3) [comm_semiring R] :

matrix m n (mv_polynomial (m × n) R)

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

Equations

matrix.mv_polynomial_X m n R = ⇑matrix.of (λ (i : m) (j : n), mv_polynomial.X (i, j))

source

@[simp]

theorem matrix.mv_polynomial_X_apply (m : Type u_1) (n : Type u_2) (R : Type u_3) [comm_semiring R] (i : m) (j : n) :

matrix.mv_polynomial_X m n R i j = mv_polynomial.X (i, j)

source

theorem matrix.mv_polynomial_X_map_eval₂ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [comm_semiring R] [comm_semiring S] (f : R →+* S) (A : matrix m n S) :

(matrix.mv_polynomial_X m n R).map (mv_polynomial.eval₂ f (λ (p : m × n), A p.fst p.snd)) = A

Any matrix A can be expressed as the evaluation of matrix.mv_polynomial_X.

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

source

theorem matrix.mv_polynomial_X_map_matrix_eval {m : Type u_1} {R : Type u_3} [fintype m] [decidable_eq m] [comm_semiring R] (A : matrix m m R) :

⇑((mv_polynomial.eval (λ (p : m × m), A p.fst p.snd)).map_matrix) (matrix.mv_polynomial_X m m R) = A

A variant of matrix.mv_polynomial_X_map_eval₂ with a bundled ring_hom on the LHS.

source

theorem matrix.mv_polynomial_X_map_matrix_aeval {m : Type u_1} (R : Type u_3) {S : Type u_4} [fintype m] [decidable_eq m] [comm_semiring R] [comm_semiring S] [algebra R S] (A : matrix m m S) :

⇑((mv_polynomial.aeval (λ (p : m × m), A p.fst p.snd)).map_matrix) (matrix.mv_polynomial_X m m R) = A

A variant of matrix.mv_polynomial_X_map_eval₂ with a bundled alg_hom on the LHS.

source

theorem matrix.det_mv_polynomial_X_ne_zero (m : Type u_1) (R : Type u_3) [decidable_eq m] [fintype m] [comm_ring R] [nontrivial R] :

(matrix.mv_polynomial_X m m R).det ≠ 0

In a nontrivial ring, matrix.mv_polynomial_X m m R has non-zero determinant.