Eigenspaces of diagonal operators over reduced rings

For a diagonal linear operator over a reduced ring, coordinatewise generalized eigenvector conditions already imply the corresponding eigenvector conditions. The theorem below identifies the maximal generalized eigenspace with the eigenspace, so a diagonalized action can be studied through its ordinary eigenvectors.

The main theorem extends Mathlib's Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, whose domain hypothesis is weakened here to the reduced-ring hypothesis needed by the coordinatewise nilpotence argument.

theorem TauCeti.maxGenEigenspace_toLin_diagonal_eq_eigenspace_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] {ι : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (d : ι → R) (b : Module.Basis ι R M) (μ : R) : Module.End.maxGenEigenspace ((Matrix.toLin b b) (Matrix.diagonal d)) μ = Module.End.eigenspace ((Matrix.toLin b b) (Matrix.diagonal d)) μ

A generalized eigenspace of a diagonal operator over a reduced ring is its eigenspace.

Coordinatewise, a generalized eigenvector satisfies (d j - μ) ^ k * x j = 0; reducedness is exactly what removes the nilpotent factor.