Jordan normal form

[jcommelin]

https://en.wikipedia.org/wiki/Jordan_normal_form

[kbuzzard]

If one first proves the structure theorem for modules over a PID, i.e. if R is a PID and M is a f.g. R-module, then M is isomorphic to prod_{i=1}^n R/(f_i), then this result readily follows. If V is a fdvs over a field k and phi:V->V is k-linear the V becomes a module over k[X] with X acting via phi. V is finite-dimensional hence certainly f.g., so one can apply the theorem. No f_i can be zero for dimension reasons, so one can assume they're all monic. The char poly of X on R/(f) is just f, if f is monic. The eigenvalues of phi are all in k iff each f is a product of linear factors. By CRT one can reduce to the case f=(X-c)^n and now using powers of X-c as a basis one gets the Jordan block.

[LukasMias]

I've been looking into this issue a bit (on mathlib4 however), to get back to speed with the Lean world of 2023 :) @kbuzzard Your proof strategy looks solid to me; if you have any further insights about how to easily tackle this they're certainly appreciated (considering it's been 3 years since you wrote that comment)