Common Eigenvalue Field Degree
Abstract
A common nonzero eigenvector over an extension field bounds the degree of the field generated by an arbitrary family of eigenvalues.
Let F and L be fields with an F-algebra structure on L, let J be finite and I arbitrary, and let M_i be J-by-J matrices over F. Suppose a single nonzero vector x in L^J satisfies M_i^L x=eigenvalue_i*x for every i. Scalar extension here means entrywise algebraMap F L; the matrices need not commute, be semisimple or admit a common eigenbasis. The extension L/F need not be finite or algebraic.
Theorem 1.1 (The entire eigenvalue field has degree at most the matrix size).
Lean statement: D5/S1/Eigenstructure/CommonEigenvalueFieldDegree.common_eigenvalue_field_degree
Proof. Machine-checked in Lean as D5/S1/Eigenstructure/CommonEigenvalueFieldDegree.common_eigenvalue_field_degree (✓ std3). ∎
Source. Repository-derived.
Commentary.
The actual intermediate field adjoin F (range eigenvalues) is finite-dimensional over F and has finrank at most card J. The family I may be infinite or empty. If J is empty, the nonzero-vector hypothesis is impossible. Zero and repeated eigenvalues are allowed; the proof never divides by an eigenvalue.
Normalize one nonzero coordinate of x to 1. The whole F-algebra A generated by the matrices preserves its L-line, by algebra-adjoin induction. Reading that coordinate gives an F-algebra character chi:A->L. Let W be the image of A under the selected-row linear map. Row evaluation restricts to a surjection W->chi(A), so the character image is finite-dimensional of dimension at most dim W<=card J, rather than the weaker full-matrix bound card J squared.
The image is a finite-dimensional commutative domain inside the actual field L. Mathlib’s finite-domain-to-field theorem converts it to an intermediate field with the same carrier. Every supplied eigenvalue lies in that field, and intermediate-field inclusion transfers finite-dimensionality and the degree bound to the entire eigenvalue-generated field. No finite-generator hypothesis is imposed on I.
This theorem bounds the eigenvalue field, not the field generated by the normalized coordinates. For example, rational scalar matrices with vector (1,cube-root(2)) have rational eigenvalues even though their two coordinates generate a cubic field. The actual Hecke coefficient-field consumer proves a separate equality between its coordinate field and its eigenvalue field before applying this theorem.
The new mathematical connections are the generated-algebra action character and its factorization through a single row. Finite-dimensional images, subspace and surjection dimension bounds, finite domains being fields and intermediate-field monotonicity are reused directly from pinned Mathlib. This is a general algebraic supplier; no literature originality or official competition acceptance is claimed.