Documentation

TauCeti.LinearAlgebra.Matrix.Charpoly.Reverse

The reversed characteristic polynomial det (1 - X A) of a square matrix #

For a square matrix A over a commutative ring, Mathlib's Matrix.charpolyRev A is the determinant det (1 - X A). It is the finite-dimensional case of the Fredholm determinant. In the intended nonarchimedean setting, under suitable analytic hypotheses this extends to compact operators on infinite-dimensional Banach spaces as a power series with constant coefficient 1. This file develops the finite-dimensional algebra of det (1 - X A) that such a theory reduces to.

In dimension n = Fintype.card ι, det (1 - X A) is the reflection X ^ n · χ_A(1 / X) of the characteristic polynomial at degree n (Matrix.charpolyRev_eq_reflect). The reflection is taken at n rather than at the actual degree, which is smaller when A is singular: for A = diag(a, 0) one gets 1 - a X in dimension two, and the zero eigenvalue is remembered only by the dimension.

Main results #

References #

source
theorem Matrix.charpolyRev_eq_reflect {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
A.charpolyRev = Polynomial.reflect (Fintype.card ι) A.charpoly

det (1 - X A) is the reflection, at the dimension Fintype.card ι, of the characteristic polynomial of A. The reflection is at the dimension, not at the degree of det (1 - X A).

source
theorem Matrix.natDegree_charpolyRev_le {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
A.charpolyRev.natDegree ≤ Fintype.card ι

The degree of det (1 - X A) is at most the dimension.

source
theorem Matrix.coeff_charpolyRev {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) (k : ℕ) :
A.charpolyRev.coeff k = (-1) ^ k * ∑ s ∈ Finset.powersetCard k Finset.univ, (A.submatrix Subtype.val Subtype.val).det

Principal-minor expansion. The k-th coefficient of det (1 - X A) is (-1) ^ k times the sum of the k × k principal minors of A.

source
@[simp]
theorem Matrix.coeff_charpolyRev_zero {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
A.charpolyRev.coeff 0 = 1

The constant coefficient of det (1 - X A) is 1.

source
theorem Matrix.coeff_charpolyRev_card {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
A.charpolyRev.coeff (Fintype.card ι) = (-1) ^ Fintype.card ι * A.det

The coefficient of det (1 - X A) in degree Fintype.card ι is (-1) ^ Fintype.card ι times the determinant of A.

source
@[simp]
theorem Matrix.eval_one_charpolyRev {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
Polynomial.eval 1 A.charpolyRev = (1 - A).det

Evaluating det (1 - X A) at X = 1 gives det (1 - A).

source
theorem Matrix.coeff_adjugate_one_sub_X_smul_apply {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) (m : ℕ) (i j : ι) :
((1 - Polynomial.X • A.map ⇑Polynomial.C).adjugate i j).coeff m = (∑ k ∈ Finset.range (m + 1), A.charpolyRev.coeff k • A ^ (m - k)) i j

The Fredholm resolvent of a matrix. The m-th coefficient of the adjugate of 1 - X A is ∑ k ∈ range (m + 1), c k • A ^ (m - k), where c k is the k-th coefficient of det (1 - X A).

source
theorem Matrix.coeff_charpolyRev_eq_zero {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) {k : ℕ} (hk : Fintype.card ι < k) :
A.charpolyRev.coeff k = 0

The coefficients of det (1 - X A) above the dimension vanish.

source
theorem Matrix.charpolyRev_map {ι : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] [CommRing S] (A : Matrix ι ι R) (f : R →+* S) :
(A.map ⇑f).charpolyRev = Polynomial.map f A.charpolyRev

det (1 - X A) commutes with ring homomorphisms of the coefficients.

source
@[simp]
theorem Matrix.charpolyRev_transpose {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) :
A.transpose.charpolyRev = A.charpolyRev

det (1 - X A) is unchanged by transposition.

source
theorem Matrix.charpolyRev_reindex {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommRing R] (e : ι ≃ κ) (A : Matrix ι ι R) :
((reindex e e) A).charpolyRev = A.charpolyRev

det (1 - X A) is unchanged by relabelling the rows and columns simultaneously.

source
theorem Matrix.charpolyRev_eq_charpolyRev_iff {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommRing R] {A : Matrix ι ι R} {B : Matrix κ κ R} (h : Fintype.card ι = Fintype.card κ) :
A.charpolyRev = B.charpolyRev ↔ A.charpoly = B.charpoly

For square matrices of the same size, det (1 - X A) = det (1 - X B) if and only if A and B have the same characteristic polynomial.

source
@[simp]
theorem Matrix.charpolyRev_isEmpty {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [IsEmpty ι] (A : Matrix ι ι R) :
A.charpolyRev = 1

det (1 - X A) of an empty matrix is 1.

source
@[simp]
theorem Matrix.charpolyRev_zero {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] :
charpolyRev 0 = 1

det (1 - X · 0) is 1 in every dimension.

source
theorem Matrix.charpolyRev_diagonal {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (d : ι → R) :
(diagonal d).charpolyRev = ∏ i : ι, (1 - Polynomial.C (d i) * Polynomial.X)

det (1 - X A) of a diagonal matrix is the product of the linear factors 1 - d i X.

source
theorem Matrix.charpolyRev_mul_comm {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommRing R] (A : Matrix ι κ R) (B : Matrix κ ι R) :
(A * B).charpolyRev = (B * A).charpolyRev

Cyclicity. det (1 - X A B) = det (1 - X B A) for rectangular matrices A and B of transposed shapes.

source
@[simp]
theorem Matrix.charpolyRev_fromBlocks_zero₂₁ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommRing R] (A : Matrix ι ι R) (B : Matrix ι κ R) (D : Matrix κ κ R) :
(fromBlocks A B 0 D).charpolyRev = A.charpolyRev * D.charpolyRev

Block-triangular multiplicativity. det (1 - X A) of a block upper-triangular matrix is the product over its diagonal blocks.

source
@[simp]
theorem Matrix.charpolyRev_fromBlocks_zero₁₂ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [CommRing R] (A : Matrix ι ι R) (C' : Matrix κ ι R) (D : Matrix κ κ R) :
(fromBlocks A 0 C' D).charpolyRev = A.charpolyRev * D.charpolyRev

det (1 - X A) of a block lower-triangular matrix is the product over its diagonal blocks.

source
@[simp]
theorem Matrix.charpolyRev_blockDiagonal' {R : Type u_3} [CommRing R] {o : Type u_5} {m : o → Type u_6} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m i)] [(i : o) → DecidableEq (m i)] (A : (i : o) → Matrix (m i) (m i) R) :
(blockDiagonal' A).charpolyRev = ∏ i : o, (A i).charpolyRev

det (1 - X A) of a finite dependent block-diagonal matrix is the product of the reversed characteristic polynomials of its blocks. Empty blocks contribute the factor 1.

source
@[simp]
theorem Matrix.charpolyRev_submatrix_blockDiagonal' {R : Type u_3} [CommRing R] {o : Type u_5} {m : o → Type u_6} [Fintype o] [DecidableEq o] [(i : o) → DecidableEq (m i)] (A : (i : o) → Matrix (m i) (m i) R) (S : Finset ((i : o) × m i)) :
((blockDiagonal' A).submatrix Subtype.val Subtype.val).charpolyRev = ∏ i : o, ((A i).submatrix Subtype.val Subtype.val).charpolyRev

A finite compression of a dependent block-diagonal matrix factors over the compressed blocks. The block at i is restricted to the coordinates of the compression lying over i.

source
@[simp]
theorem Matrix.charpolyRev_submatrix_fromBlocks_zero₂₁ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [DecidableEq ι] [DecidableEq κ] [CommRing R] (A : Matrix ι ι R) (B : Matrix ι κ R) (D : Matrix κ κ R) (s : Finset ι) (t : Finset κ) :
((fromBlocks A B 0 D).submatrix Subtype.val Subtype.val).charpolyRev = (A.submatrix Subtype.val Subtype.val).charpolyRev * (D.submatrix Subtype.val Subtype.val).charpolyRev

Compressing an upper block-triangular matrix to a disjoint sum of finite coordinate sets gives the product of the reversed characteristic polynomials of its diagonal compressions.

source
theorem Matrix.BlockTriangular.charpolyRev {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] {α : Type u_5} [LinearOrder α] {b : ι → α} {A : Matrix ι ι R} (h : A.BlockTriangular b) :
A.charpolyRev = ∏ a ∈ Finset.image b Finset.univ, (A.toSquareBlock b a).charpolyRev

det (1 - X A) of a block-triangular matrix is the product of det (1 - X A_a) over its diagonal blocks A_a.

source
theorem Matrix.charpolyRev_of_isUpperTriangular {ι : Type u_1} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [LinearOrder ι] {A : Matrix ι ι R} (h : A.IsUpperTriangular) :
A.charpolyRev = ∏ i : ι, (1 - Polynomial.C (A i i) * Polynomial.X)

det (1 - X A) of an upper-triangular matrix is the product of the factors 1 - A i i X.

source
theorem Module.Basis.reverse_charpoly_of_apply {κ : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype κ] [CommRing R] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (hf : ∀ (i : κ), f (b i) = a i • b i) :
f.charpoly.reverse = ∏ i : κ, (1 - Polynomial.C (a i) * Polynomial.X)

det(1 - X f) of an endomorphism diagonal in a finite basis is the product of the linear factors 1 - aᵢ X over its eigenvalues aᵢ.