leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Jordan normal form #4971

Open jcommelin opened 3 years ago

jcommelin commented 3 years ago

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

kbuzzard commented 3 years ago

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 commented 9 months ago

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)