Coefficients and determinants of polynomial matrices

Let A be a square matrix with polynomial entries whose j-th column has degree at most e j. Every term of the Leibniz expansion of det A then has degree at most ∑ j, e j, so det A does too, and its coefficient in that degree is the determinant of the scalar matrix of top coefficients (A i j).coeff (e j). This is the standard way to show that a determinant of polynomials is nonzero, by exhibiting a nonsingular matrix of leading coefficients.

Under the same column bounds, reflecting det A at ∑ j, e j, that is, reading it in the reciprocal variable X ^ (∑ j, e j) * det A (1 / X), gives the determinant of the matrix whose j-th column is reflected at e j (Matrix.reflect_det_sum_eq_of_natDegree_le). For instance, when all entries have degree at most one, det (X • Bᵀ + B) is its own reflection at the dimension, being the determinant of the transpose (Matrix.reflect_det_X_smul_transpose_add).

Taking entrywise coefficients commutes with multiplication by constant matrices on either side. In particular, linear coefficients of matrix-valued curves commute with constant conjugation.

Evaluating a polynomial in a matrix commutes with applying a ring homomorphism to the coefficients and to the entries (Matrix.aeval_map), and a rectangular matrix intertwining two square matrices intertwines every polynomial in them (Matrix.aeval_mul_eq_mul_aeval). Natural matrix identities valid at unit parameters extend to all parameters by polynomial specialization (Matrix.identity_of_units).

theorem Matrix.identity_of_units {R : Type u} [CommRing R] {m : Type u_1} {n : Type u_2} (F G : (S : Type u) → [CommRing S] → S → Matrix m n S) (hF : ∀ {S : Type u} [inst : CommRing S] (f : Polynomial R →+* S), (F (Polynomial R) Polynomial.X).map ⇑f = F S (f Polynomial.X)) (hG : ∀ {S : Type u} [inst : CommRing S] (f : Polynomial R →+* S), (G (Polynomial R) Polynomial.X).map ⇑f = G S (f Polynomial.X)) (hunit : ∀ (q : (LaurentPolynomial R)ˣ), F (LaurentPolynomial R) ↑q = G (LaurentPolynomial R) ↑q) (s : R) : F R s = G R s

A matrix identity natural under coefficient homomorphisms holds at every parameter if it holds at every unit of the Laurent polynomial ring. Embed the indeterminate into Laurent polynomials, where it is a unit, then use injectivity and evaluate back in the original ring.

@[simp]

theorem Matrix.aeval_map {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (A : Matrix n n R) (φ : R →+* S) (f : Polynomial R) : (Polynomial.aeval (A.map ⇑φ)) (Polynomial.map φ f) = ((Polynomial.aeval A) f).map ⇑φ

Evaluating a polynomial in a matrix commutes with applying a ring homomorphism to the coefficients of the polynomial and to the entries of the matrix.

theorem Matrix.aeval_mul_eq_mul_aeval {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] {m : Type u_3} [Fintype m] [DecidableEq m] [CommSemiring R] {A : Matrix n n R} {B : Matrix m m R} {V : Matrix n m R} (h : A * V = V * B) (q : Polynomial R) : (Polynomial.aeval A) q * V = V * (Polynomial.aeval B) q

Polynomials preserve intertwiners. If a rectangular matrix V intertwines the square matrices A and B, that is A * V = V * B, then it intertwines every polynomial in them.

@[simp]

theorem Matrix.map_coeff_map_C_mul {n : Type u_1} {R : Type u_2} [Fintype n] [Semiring R] {m : Type u_3} {p : Type u_4} (A : Matrix m n R) (P : Matrix n p (Polynomial R)) (d : ℕ) : ((A.map ⇑Polynomial.C * P).map fun (p : Polynomial R) => p.coeff d) = A * P.map fun (p : Polynomial R) => p.coeff d

Taking an entrywise polynomial coefficient commutes with multiplication on the left by a constant matrix.

@[simp]

theorem Matrix.map_coeff_mul_map_C {n : Type u_1} {R : Type u_2} [Fintype n] [Semiring R] {m : Type u_3} {p : Type u_4} (P : Matrix m n (Polynomial R)) (A : Matrix n p R) (d : ℕ) : ((P * A.map ⇑Polynomial.C).map fun (p : Polynomial R) => p.coeff d) = (P.map fun (p : Polynomial R) => p.coeff d) * A

Taking an entrywise polynomial coefficient commutes with multiplication on the right by a constant matrix.

theorem Matrix.coeff_det_sum_eq_of_natDegree_le {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n (Polynomial R)) (e : n → ℕ) (h : ∀ (i j : n), (A i j).natDegree ≤ e j) : A.det.coeff (∑ j : n, e j) = (of fun (i j : n) => (A i j).coeff (e j)).det

If the j-th column of a polynomial matrix A has degree at most e j, then the coefficient of det A in degree ∑ j, e j is the determinant of the matrix of coefficients of the entries in the degrees e j.

theorem Matrix.natDegree_det_le_of_natDegree_le {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n (Polynomial R)) (e : n → ℕ) (h : ∀ (i j : n), (A i j).natDegree ≤ e j) : A.det.natDegree ≤ ∑ j : n, e j

If the j-th column of a polynomial matrix A has degree at most e j, then det A has degree at most ∑ j, e j.

theorem Matrix.reflect_det_sum_eq_of_natDegree_le {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n (Polynomial R)) (e : n → ℕ) (h : ∀ (i j : n), (A i j).natDegree ≤ e j) : Polynomial.reflect (∑ j : n, e j) A.det = (of fun (i j : n) => Polynomial.reflect (e j) (A i j)).det

If the j-th column of a polynomial matrix A has degree at most e j, then the reflection of det A at ∑ j, e j is the determinant of the matrix whose j-th column is reflected at e j.

theorem Matrix.reflect_det_X_smul_transpose_add {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (S : Matrix n n R) : Polynomial.reflect (Fintype.card n) (Polynomial.X • S.transpose.map ⇑Polynomial.C + S.map ⇑Polynomial.C).det = (Polynomial.X • S.transpose.map ⇑Polynomial.C + S.map ⇑Polynomial.C).det

The polynomial det (X • Sᵀ + S) is its own reflection at the dimension: reflecting each entry X * Sⱼᵢ + Sᵢⱼ at degree one transposes the matrix.