Rational eigenspaces after scalar extension

For a matrix over a commutative algebra Q over a field k, rationalEigenspace consists of vectors over k that become eigenvectors after scalar extension to Q. If a matrix is diagonalized over k, these eigenspaces span the vector space over k.

Main declarations

• Matrix.rationalEigenspace: the subspace of rational eigenvectors.
• Matrix.mem_rationalEigenspace: its membership criterion after scalar extension.
• Matrix.iSup_rationalEigenspace_eq_top: spanning under rational diagonalization.

def Matrix.rationalEigenspace {k : Type u_1} {Q : Type u_2} [Field k] [CommRing Q] [Algebra k Q] {n : Type u_3} [Fintype n] (M : Matrix n n Q) (s : Q) : Submodule k (n → k)

The k-subspace of rational vectors which the matrix M over Q scales by s.

Equations

• M.rationalEigenspace s = (↑k (M.mulVecLin - s • LinearMap.id) ∘ₗ (Algebra.linearMap k Q).compLeft n).ker

@[simp]

theorem Matrix.mem_rationalEigenspace {k : Type u_1} {Q : Type u_2} [Field k] [CommRing Q] [Algebra k Q] {n : Type u_3} [Fintype n] {M : Matrix n n Q} {s : Q} {v : n → k} : v ∈ M.rationalEigenspace s ↔ M.mulVec (⇑(algebraMap k Q) ∘ v) = s • ⇑(algebraMap k Q) ∘ v

Membership in a rational eigenspace is the eigenvector equation after scalar extension.

theorem Matrix.iSup_rationalEigenspace_eq_top {k : Type u_1} {Q : Type u_2} [Field k] [CommRing Q] [Algebra k Q] {n : Type u_3} {ι : Type u_4} [Fintype n] [DecidableEq n] {M : Matrix n n Q} {P₀ : Matrix n n k} (hP₀ : IsUnit P₀) (e : ι → Q) {t : n → ι} (h : M * P₀.map ⇑(algebraMap k Q) = P₀.map ⇑(algebraMap k Q) * diagonal fun (i : n) => e (t i)) : ⨆ (s : ι), M.rationalEigenspace (e s) = ⊤

If P₀ diagonalizes M with eigenvalues in the image of e, the corresponding rational eigenspaces span because they contain the columns of P₀.