English
For Noetherian R-modules, the top generalized eigenspace equals the generalized eigenspace at the index maxUnifEigenspaceIndex f μ.
Русский
Для Нётеровых модулей вершина обобщённых собственных пространств равна обобщённому собственному пространству при индексе maxUnifEigenspaceIndex f μ.
LaTeX
$$genEigenspace f μ ⊤ = f.genEigenspace μ (maxUnifEigenspaceIndex f μ)$$
Lean4
/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`. -/
theorem genEigenspace_top_eq_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M) (μ : R) :
genEigenspace f μ ⊤ = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) :=
by
have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <| (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
convert this using 1
simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe, Function.comp_def]
rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]
congr 1
aesop
