Documentation

TauCeti.LinearAlgebra.Matrix.MvPolynomial

Determinants of matrices of multivariate polynomials #

Let A be a square matrix with entries in MvPolynomial σ R whose l-th column has partial degree at most e l in the variable Xᵢ. Every term of the Leibniz expansion of det A is, up to sign, a product containing exactly one entry from each column, so det A has partial degree at most ∑ l, e l in Xᵢ.

The minors of a matrix Z, and of its powers, are polynomials in the entries of Z: they are the values at Z of the corresponding minors of the generic matrix Matrix.mvPolynomialX.

The generic determinant is a non-zero-divisor over every commutative ring. Translating the generic matrix by the identity and embedding into power series reduces this to its constant coefficient being one.

Order the variables X (i, j) of the generic matrix row by row, by renaming them along toLex to the lexicographically ordered pairs m ×ₗ n, and use the lexicographic monomial order MonomialOrder.lex, for which X (0, 0) is the largest variable, followed by X (0, 1). Every minor on sorted rows r and sorted columns c then has its main diagonal ∏ i, X (r i, c i) as leading term, with coefficient one: in the Leibniz expansion, a permutation other than the identity first differs from the diagonal at some row r j₀, where it uses a column to the right of c j₀, so the diagonal exponent is lexicographically larger. Thus this order is a diagonal term order on the generic matrix. Leading terms of minors are the input to Gröbner and SAGBI bases of determinantal and flag-minor algebras. For finite index types such as Fin p and Fin q, the hypothesis WellFoundedGT (m ×ₗ n) is found by instance search.

Main results #

References #

source
theorem Matrix.degreeOf_det_le_sum {R : Type u_1} {σ : Type u_2} {n : Type u_3} [CommRing R] [Fintype n] [DecidableEq n] (A : Matrix n n (MvPolynomial σ R)) (i : σ) (e : n → ℕ) (hA : ∀ (k l : n), MvPolynomial.degreeOf i (A k l) ≤ e l) :
MvPolynomial.degreeOf i A.det ≤ ∑ l : n, e l

If the l-th column of a matrix A of multivariate polynomials has partial degree at most e l in Xᵢ, then det A has partial degree at most ∑ l, e l in Xᵢ.

source
theorem Matrix.det_mvPolynomialX_mem_nonZeroDivisors {R : Type u_1} {n : Type u_3} [CommRing R] [Fintype n] [DecidableEq n] :
(mvPolynomialX n n R).det ∈ nonZeroDivisors (MvPolynomial (n × n) R)

The generic determinant is a non-zero-divisor over every commutative ring, including the zero ring and matrices of size zero.

source
theorem Matrix.aeval_det_submatrix_mvPolynomialX {R : Type u_1} {S : Type u_2} {m : Type u_3} {n : Type u_4} {l : Type u_5} [CommRing R] [CommRing S] [Algebra R S] [Fintype l] [DecidableEq l] (Z : Matrix m n S) (r : l → m) (c : l → n) :
(MvPolynomial.aeval (Function.uncurry Z)) ((mvPolynomialX m n R).submatrix r c).det = (Z.submatrix r c).det

The minors of a matrix Z are the values at the entries of Z of the corresponding minors of the generic matrix Matrix.mvPolynomialX.

source
theorem Matrix.aeval_det_submatrix_pow_mvPolynomialX {R : Type u_1} {S : Type u_2} {n : Type u_4} {l : Type u_5} [CommRing R] [CommRing S] [Algebra R S] [Fintype l] [DecidableEq l] [Fintype n] [DecidableEq n] (Z : Matrix n n S) (j : ℕ) (r c : l → n) :
(MvPolynomial.aeval (Function.uncurry Z)) ((mvPolynomialX n n R ^ j).submatrix r c).det = ((Z ^ j).submatrix r c).det

The minors of the j-th power of a matrix Z are the values at the entries of Z of the corresponding minors of the j-th power of the generic matrix Matrix.mvPolynomialX.

source
@[simp]
theorem Matrix.degree_rename_toLex_det_submatrix_mvPolynomialX {R : Type u_1} {m : Type u_2} {n : Type u_3} {ι : Type u_4} [CommRing R] [LinearOrder ι] [Fintype ι] [LinearOrder m] [LinearOrder n] [WellFoundedGT (Lex (m × n))] [Nontrivial R] {r : ι → m} {c : ι → n} (hr : StrictMono r) (hc : StrictMono c) :
MonomialOrder.lex.degree ((MvPolynomial.rename ⇑toLex) ((mvPolynomialX m n R).submatrix r c).det) = ∑ i : ι, Finsupp.single (toLex (r i, c i)) 1

For the lexicographic order on the variables X (i, j) ordered row by row, a minor of the generic matrix on sorted rows r and sorted columns c has the main diagonal ∏ i, X (r i, c i) as its leading monomial.

source
@[simp]
theorem Matrix.monic_rename_toLex_det_submatrix_mvPolynomialX {R : Type u_1} {m : Type u_2} {n : Type u_3} {ι : Type u_4} [CommRing R] [LinearOrder ι] [Fintype ι] [LinearOrder m] [LinearOrder n] [WellFoundedGT (Lex (m × n))] {r : ι → m} {c : ι → n} (hr : StrictMono r) (hc : StrictMono c) :
MonomialOrder.lex.Monic ((MvPolynomial.rename ⇑toLex) ((mvPolynomialX m n R).submatrix r c).det)

For the lexicographic order on the variables X (i, j) ordered row by row, a minor of the generic matrix on sorted rows and sorted columns is monic.

source
@[simp]
theorem Matrix.leadingTerm_rename_toLex_det_submatrix_mvPolynomialX {R : Type u_1} {m : Type u_2} {n : Type u_3} {ι : Type u_4} [CommRing R] [LinearOrder ι] [Fintype ι] [LinearOrder m] [LinearOrder n] [WellFoundedGT (Lex (m × n))] {r : ι → m} {c : ι → n} (hr : StrictMono r) (hc : StrictMono c) :
MonomialOrder.lex.leadingTerm ((MvPolynomial.rename ⇑toLex) ((mvPolynomialX m n R).submatrix r c).det) = ∏ i : ι, MvPolynomial.X (toLex (r i, c i))

For the lexicographic order on the variables X (i, j) ordered row by row, the leading term of a minor of the generic matrix on sorted rows r and sorted columns c is the product ∏ i, X (r i, c i) of its diagonal entries.