Searching a finite field for the eigenvalues of a matrix

Over a finite field the eigenvalues of a square matrix can be found by brute force: run through the field and keep the scalars a at which a • 1 - A is singular. This file defines that search, TauCeti.eigenvalueSearch, as a genuine def on decidable data, and proves that it finds exactly the eigenvalues: as a set, eigenvalueSearch A is the spectrum of A (TauCeti.coe_eigenvalueSearch).

Mathlib has the spectrum, the eigenvalues of an endomorphism, and the identification of both with the roots of the characteristic polynomial, but each of those is Set- or Multiset-valued and none of them computes: Polynomial is a Finsupp, spectrum is a Set, and Finset.toList is noncomputable. What is added here is the computable Finset together with the theorem that it agrees with Mathlib's notion, so that a program may use the Finset while its correctness proof uses the whole spectrum API.

This search is the finite-field linear algebra of the Burnside--Dixon--Schneider character-table algorithm, which refines a partition of the class indices by splitting each block along the eigenvalues of a class-multiplication matrix reduced mod p. That is why the matrix is indexed by an arbitrary Fintype rather than by Fin n: there the index type is ConjClasses G. It is also why the eigenvector characterization is recorded on both sides (*ᵥ and ᵥ*): the eigenrows of that algorithm are left eigenvectors.

Main definitions

• TauCeti.eigenvalueSearch: the Finset of eigenvalues of a matrix over a finite field.

Main results

• TauCeti.coe_eigenvalueSearch: the search returns exactly the spectrum.
• TauCeti.mem_eigenvalueSearch_iff_exists_mulVec and TauCeti.mem_eigenvalueSearch_iff_exists_vecMul: membership means a nonzero right, respectively left, eigenvector exists.
• TauCeti.card_eigenvalueSearch_le: at most Fintype.card n scalars are returned.
• TauCeti.decidableMemSpectrum: membership in the spectrum is therefore decidable.

References

This implements the object eigenvalueSearch of Layer 6 of the character theory roadmap and its suggested declarations.

def TauCeti.eigenvalueSearch {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n F) : Finset F

The eigenvalues of A, found by searching the finite field F for the scalars a at which a • 1 - A is singular. By TauCeti.coe_eigenvalueSearch this is the spectrum of A.

A Finset rather than a list: the search has no preferred order on the field, and eigenvalues carry no multiplicity here. The body is exposed because consumers of an executable algorithm evaluate it, and kernel reduction needs the definition.

Equations

• TauCeti.eigenvalueSearch A = {a : F | ((Matrix.scalar n) a - A).det = 0}

@[simp]

theorem TauCeti.mem_eigenvalueSearch {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ ((Matrix.scalar n) a - A).det = 0

The scalars the search keeps are those at which a • 1 - A has vanishing determinant.

theorem TauCeti.notMem_eigenvalueSearch_iff_isUnit {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∉ eigenvalueSearch A ↔ IsUnit ((Matrix.scalar n) a - A)

A scalar the search rejects is one at which a • 1 - A is invertible.

theorem TauCeti.mem_eigenvalueSearch_iff_det_sub_smul_eq_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ (A - a • 1).det = 0

The membership test in the form the algorithm uses it: a is an eigenvalue exactly when A - a • 1 is singular.

theorem TauCeti.mem_eigenvalueSearch_iff_isRoot_charpoly {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ A.charpoly.IsRoot a

The search keeps exactly the roots of the characteristic polynomial.

@[simp]

theorem TauCeti.coe_eigenvalueSearch {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n F) : ↑(eigenvalueSearch A) = spectrum F A

Correctness of the search: it returns exactly the spectrum of A.

theorem TauCeti.mem_eigenvalueSearch_iff_mem_spectrum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ a ∈ spectrum F A

The pointwise form of TauCeti.coe_eigenvalueSearch.

theorem TauCeti.mem_eigenvalueSearch_iff_hasEigenvalue {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ Module.End.HasEigenvalue (Matrix.toLin' A) a

The search finds the eigenvalues of the endomorphism that A defines on n → F.

theorem TauCeti.scalar_sub_mulVec_eq_zero_iff {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [NonUnitalNonAssocRing R] (A : Matrix n n R) (a : R) (v : n → R) : ((Matrix.diagonal fun (x : n) => a) - A).mulVec v = 0 ↔ A.mulVec v = a • v

The scalar-minus-matrix system is the corresponding eigenvector equation.

theorem TauCeti.mem_eigenvalueSearch_iff_exists_mulVec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ ∃ (v : n → F), v ≠ 0 ∧ A.mulVec v = a • v

A scalar is found by the search exactly when it has a nonzero eigenvector.

@[simp]

theorem TauCeti.eigenvalueSearch_transpose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n F) : eigenvalueSearch A.transpose = eigenvalueSearch A

A matrix and its transpose have the same eigenvalues.

theorem TauCeti.mem_eigenvalueSearch_iff_exists_vecMul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n F} {a : F} : a ∈ eigenvalueSearch A ↔ ∃ (v : n → F), v ≠ 0 ∧ Matrix.vecMul v A = a • v

A scalar is found by the search exactly when it has a nonzero left eigenvector: a row vector v with v ᵥ* A = a • v. This is the orientation of the Dixon--Schneider eigenrows.

theorem TauCeti.eigenvalueSearch_eq_toFinset_roots {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n F) : eigenvalueSearch A = A.charpoly.roots.toFinset

The eigenvalues of A are the distinct roots of its characteristic polynomial.

theorem TauCeti.card_eigenvalueSearch_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n F) : (eigenvalueSearch A).card ≤ Fintype.card n

A matrix has at most as many eigenvalues as it has rows.

@[simp]

theorem TauCeti.eigenvalueSearch_diagonal {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (d : n → F) : eigenvalueSearch (Matrix.diagonal d) = Finset.image d Finset.univ

The eigenvalues of a diagonal matrix are its diagonal entries.

theorem TauCeti.eigenvalueSearch_scalar {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (a : F) : eigenvalueSearch ((Matrix.scalar n) a) = {a}

The only eigenvalue of a scalar matrix is the scalar. This is not @[simp]: simp already takes the left-hand side to Finset.image (fun _ => a) Finset.univ, and collapsing that image needs the nonemptiness hypothesis.

@[simp]

theorem TauCeti.eigenvalueSearch_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] : eigenvalueSearch 0 = {0}

The only eigenvalue of the zero matrix is 0.

@[simp]

theorem TauCeti.eigenvalueSearch_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] : eigenvalueSearch 1 = {1}

The only eigenvalue of the identity matrix is 1.

theorem TauCeti.eigenvalueSearch_conjugate {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n F} (hM : IsUnit M) (A : Matrix n n F) : eigenvalueSearch (M * A * M⁻¹) = eigenvalueSearch A

Similar matrices have the same eigenvalues.

@[simp]

theorem TauCeti.eigenvalueSearch_eq_empty_of_isEmpty {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] [IsEmpty n] (A : Matrix n n F) : eigenvalueSearch A = ∅

A matrix with no rows has no eigenvalues: its 0 × 0 determinant is 1.

@[instance_reducible]

instance TauCeti.decidableMemSpectrum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : Type u_2} [Fintype n] [DecidableEq n] (a : F) (A : Matrix n n F) : Decidable (a ∈ spectrum F A)

Membership in the spectrum of a matrix over a finite field is decidable, by running the search.

Equations

• TauCeti.decidableMemSpectrum a A = decidable_of_iff (a ∈ TauCeti.eigenvalueSearch A) ⋯