Mathlib.LinearAlgebra.Matrix.MvPolynomial

Module docstring

{"# 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 "}

Matrix.mvPolynomialX definition

[CommSemiring R] : Matrix m n (MvPolynomial (m × n) R)

Full source

/-- The matrix with variable `X (i,j)` at location `(i,j)`. -/
noncomputable def mvPolynomialX [CommSemiring R] : Matrix m n (MvPolynomial (m × n) R) :=
  of fun i j => MvPolynomial.X (i, j)

Matrix of independent variables in multivariate polynomial ring

Informal description

For a commutative semiring $R$ and index types $m$ and $n$, the matrix $\text{mvPolynomialX}$ is defined as the $m \times n$ matrix whose $(i,j)$-th entry is the variable $X_{(i,j)}$ in the multivariate polynomial ring over $R$ with variables indexed by $m \times n$.

Matrix.mvPolynomialX_apply theorem

[CommSemiring R] (i j) : mvPolynomialX m n R i j = MvPolynomial.X (i, j)

Full source

@[simp]
theorem mvPolynomialX_apply [CommSemiring R] (i j) :
    mvPolynomialX m n R i j = MvPolynomial.X (i, j) :=
  rfl

Matrix Entry as Variable: $(\text{mvPolynomialX})_{i,j} = X_{(i,j)}$

Informal description

For any commutative semiring $R$ and indices $i \in m$, $j \in n$, the $(i,j)$-th entry of the matrix $\text{mvPolynomialX}_{m \times n}(R)$ is equal to the variable $X_{(i,j)}$ in the multivariate polynomial ring over $R$ with variables indexed by $m \times n$. That is, $(\text{mvPolynomialX}_{m \times n}(R))_{i,j} = X_{(i,j)}$.

Matrix.mvPolynomialX_map_eval₂ theorem

 [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

Full source

/-- 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. -/
theorem mvPolynomialX_map_eval₂ [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 :=
  ext fun i j => MvPolynomial.eval₂_X _ (fun p : m × n => A p.1 p.2) (i, j)

Evaluation of Matrix of Variables Yields Original Matrix

Informal description

Let $R$ and $S$ be commutative semirings, and let $f: R \to S$ be a ring homomorphism. For any matrix $A \in \text{Matrix}_{m \times n}(S)$, the evaluation of the matrix $\text{mvPolynomialX}_{m \times n}(R)$ (whose entries are independent variables $X_{(i,j)}$) under the map $\text{MvPolynomial.eval}_2(f, \lambda p, A_{p_1 p_2})$ yields the original matrix $A$. In other words, applying the evaluation map $\text{MvPolynomial.eval}_2$ with coefficients mapped via $f$ and variables replaced by corresponding entries of $A$ to the matrix $\text{mvPolynomialX}_{m \times n}(R)$ results in $A$ itself.

Matrix.mvPolynomialX_mapMatrix_eval theorem

 [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

Full source

/-- A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `RingHom` on the LHS. -/
theorem mvPolynomialX_mapMatrix_eval [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 :=
  mvPolynomialX_map_eval₂ _ A

Evaluation of Variable Matrix Yields Original Matrix

Informal description

For a finite type $m$ with decidable equality and a commutative semiring $R$, let $A$ be an $m \times m$ matrix over $R$. Then applying the evaluation map $\text{MvPolynomial.eval}$ (which substitutes each variable $X_{(i,j)}$ with the corresponding entry $A_{i,j}$) to the matrix $\text{mvPolynomialX}_{m \times m}(R)$ (whose entries are the variables $X_{(i,j)}$) yields the original matrix $A$. In other words, $(\text{MvPolynomial.eval} (\lambda p, A_{p_1 p_2}))(\text{mvPolynomialX}_{m \times m}(R)) = A$.

Matrix.mvPolynomialX_mapMatrix_aeval theorem

 [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

Full source

/-- A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `AlgHom` on the LHS. -/
theorem mvPolynomialX_mapMatrix_aeval [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 :=
  mvPolynomialX_map_eval₂ _ A

Algebraic Evaluation of Variable Matrix Yields Original Matrix

Informal description

Let $m$ be a finite type with decidable equality, and let $R$ and $S$ be commutative semirings with an algebra structure $R \to S$. For any matrix $A \in \text{Matrix}_{m \times m}(S)$, applying the algebra evaluation map $\text{MvPolynomial.aeval}$ (which substitutes each variable $X_{(i,j)}$ with the corresponding entry $A_{i,j}$) to the matrix $\text{mvPolynomialX}_{m \times m}(R)$ (whose entries are the variables $X_{(i,j)}$) yields the original matrix $A$. In other words, $(\text{MvPolynomial.aeval} (\lambda p, A_{p_1 p_2}))(\text{mvPolynomialX}_{m \times m}(R)) = A$.

Matrix.det_mvPolynomialX_ne_zero theorem

[DecidableEq m] [Fintype m] [CommRing R] [Nontrivial R] : det (mvPolynomialX m m R) ≠ 0

Full source

/-- In a nontrivial ring, `Matrix.mvPolynomialX m m R` has non-zero determinant. -/
theorem det_mvPolynomialX_ne_zero [DecidableEq m] [Fintype m] [CommRing R] [Nontrivial R] :
    detdet (mvPolynomialX m m R) ≠ 0 := by
  intro h_det
  have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
  rw [det_one, ← RingHom.map_det, h_det, RingHom.map_zero] at this
  exact zero_ne_one this

Nonvanishing Determinant of the Matrix of Independent Variables: $\det(\text{mvPolynomialX}_{m \times m}(R)) \neq 0$

Informal description

For a finite type $m$ with decidable equality and a nontrivial commutative ring $R$, the determinant of the matrix $\text{mvPolynomialX}_{m \times m}(R)$ (whose $(i,j)$-th entry is the variable $X_{(i,j)}$ in the multivariate polynomial ring over $R$) is nonzero, i.e., \[ \det(\text{mvPolynomialX}_{m \times m}(R)) \neq 0. \]