Toward Jordan Normal Form

Stream: maths

[Daniel Packer]

Hi all,
I'm trying to work toward developing results about eigenvalues of matrices in Lean, and it appears that a reasonable short-term goal is to try to develop the concepts of (geometric) eigenvalue multiplicity and the Jordan Normal Form.
That said, it sounds like the community wants to get JNF through the structure theorem for finitely generated modules over a PID, so that it is available for arbitrary fields. So I can also contribute in that direction--let me know if you're already working on that.
I could also leapfrog just to the result for \C by the Schur decomposition as done here: https://www.isa-afp.org/entries/Jordan_Normal_Form.html . Though, I don't know whether I'm just passing the buck there and some part of the Schur decomp relies on the structure theorem. I need to think more about whether that is a reasonable plan.
I'm a beginner to Lean, so any advice about how to approach these goals would be very welcome!

[Patrick Massot]

If you search for module pid you'll see this has been discussed many times, but nobody ever did the work. This is now long overdue so don't hesitate to break the tradition and actually do it!

[Patrick Massot]

I don't really see the point of trying to go the Jordan normal form using a shortcut since we want the module results in mathlib anyway.

[Kevin Buzzard]

@Anne Baanen did Smith Normal Form and I always felt that this was the hard part.

[Patrick Massot]

Oh, I forgot about that.

[Patrick Massot]

So we may be much closer than what I remembered.

[Kevin Buzzard]

Patrick Massot said:

Oh, I forgot about that.

Me too but I soon found out about it again when I clicked your link :-)

[Patrick Massot]

My mistake is I didn't click my link...