Mathlib.LinearAlgebra.Matrix.Polynomial

Module docstring

{"# Matrices of polynomials and polynomials of matrices

In this file, we prove results about matrices over a polynomial ring. In particular, we give results about the polynomial given by det (t * I + A).

References

\"The trace Cayley-Hamilton theorem\" by Darij Grinberg, Section 5.3

Tags

matrix determinant, polynomial "}

Polynomial.natDegree_det_X_add_C_le theorem

(A B : Matrix n n α) : natDegree (det ((X : α[X]) • A.map C + B.map C : Matrix n n α[X])) ≤ Fintype.card n

Full source

theorem natDegree_det_X_add_C_le (A B : Matrix n n α) :
    natDegree (det ((X : α[X]) • A.map C + B.map C : Matrix n n α[X])) ≤ Fintype.card n := by
  rw [det_apply]
  refine (natDegree_sum_le _ _).trans ?_
  refine Multiset.max_le_of_forall_le _ _ ?_
  simp only [forall_apply_eq_imp_iff, true_and, Function.comp_apply, Multiset.map_map,
    Multiset.mem_map, exists_imp, Finset.mem_univ_val]
  intro g
  calc
    natDegree (sign g • ∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) ≤
        natDegree (∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) := by
      rcases Int.units_eq_one_or (sign g) with sg | sg
      · rw [sg, one_smul]
      · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
    _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C : Matrix n n α[X]) (g i) i) :=
      (natDegree_prod_le (Finset.univ : Finset n) fun i : n =>
        (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)
    _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
    _ ≤ Fintype.card n := by simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
  dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
  compute_degree

Natural Degree Bound for $\det(XA + B)$: $\deg(\det(XA + B)) \leq n$

Informal description

For any square matrices $A$ and $B$ of size $n \times n$ with entries in a semiring $\alpha$, the natural degree of the polynomial $\det(X \cdot A + B)$ is at most $n$, where $X$ is the polynomial variable and $A$ and $B$ are considered as matrices with polynomial entries via the embedding $C: \alpha \to \alpha[X]$. Here, $X \cdot A$ denotes the scalar multiplication of the matrix $A$ by the polynomial variable $X$, and $A.map\ C$ denotes the entrywise application of the constant polynomial embedding $C$ to the matrix $A$.

Polynomial.coeff_det_X_add_C_zero theorem

(A B : Matrix n n α) : coeff (det ((X : α[X]) • A.map C + B.map C)) 0 = det B

Full source

theorem coeff_det_X_add_C_zero (A B : Matrix n n α) :
    coeff (det ((X : α[X]) • A.map C + B.map C)) 0 = det B := by
  rw [det_apply, finset_sum_coeff, det_apply]
  refine Finset.sum_congr rfl ?_
  rintro g -
  convert coeff_smul (R := α) (sign g) _ 0
  rw [coeff_zero_prod]
  refine Finset.prod_congr rfl ?_
  simp

Constant Term of $\det(XA + B)$ is $\det(B)$

Informal description

For any square matrices $A$ and $B$ of size $n \times n$ with entries in a commutative ring $\alpha$, the constant term (coefficient of $X^0$) of the determinant of the matrix polynomial $X \cdot A + B$ equals the determinant of $B$, i.e., \[ \text{coeff}(\det(X \cdot A + B), 0) = \det(B). \]

Polynomial.coeff_det_X_add_C_card theorem

(A B : Matrix n n α) : coeff (det ((X : α[X]) • A.map C + B.map C)) (Fintype.card n) = det A

Full source

theorem coeff_det_X_add_C_card (A B : Matrix n n α) :
    coeff (det ((X : α[X]) • A.map C + B.map C)) (Fintype.card n) = det A := by
  rw [det_apply, det_apply, finset_sum_coeff]
  refine Finset.sum_congr rfl ?_
  simp only [Algebra.id.smul_eq_mul, Finset.mem_univ, RingHom.mapMatrix_apply, forall_true_left,
    map_apply, Pi.smul_apply]
  intro g
  convert coeff_smul (R := α) (sign g) _ _
  rw [← mul_one (Fintype.card n)]
  convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
  · simp [coeff_C]
  · rintro p -
    dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
    compute_degree

Leading coefficient of $\det(tA + B)$ equals $\det(A)$

Informal description

For any square matrices $A$ and $B$ of size $n \times n$ with entries in a semiring $\alpha$, the coefficient of $t^n$ in the polynomial $\det(t \cdot A + B)$ (where $t$ is an indeterminate) equals the determinant of $A$. More precisely, if we consider the polynomial matrix $t \cdot C(A) + C(B)$ (where $C$ maps entries to constant polynomials), then the coefficient of $t^n$ in its determinant is $\det(A)$.

Polynomial.leadingCoeff_det_X_one_add_C theorem

(A : Matrix n n α) : leadingCoeff (det ((X : α[X]) • (1 : Matrix n n α[X]) + A.map C)) = 1

Full source

theorem leadingCoeff_det_X_one_add_C (A : Matrix n n α) :
    leadingCoeff (det ((X : α[X]) • (1 : Matrix n n α[X]) + A.map C)) = 1 := by
  cases subsingleton_or_nontrivial α
  · simp [eq_iff_true_of_subsingleton]
  rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
  simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]
  rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h
  · simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h
    rw [h]
  · -- contradiction. we have a hypothesis that the degree is less than |n|
    -- but we know that coeff _ n = 1
    have H := coeff_eq_zero_of_natDegree_lt h
    rw [coeff_det_X_add_C_card] at H
    simp at H

Leading coefficient of $\det(XI + A)$ is 1

Informal description

For any square matrix $A$ of size $n \times n$ with entries in a semiring $\alpha$, the leading coefficient of the polynomial $\det(X \cdot I + A)$ is equal to $1$, where $I$ is the identity matrix and $X$ is the polynomial variable.