jordan normal form

Stream: maths

[Johan Commelin]

Afaik we don't have the jordan normal form of a matrix. It would be good to have this at some point. We have the basics on eigenvalues/vectors/spaces, so this should be within reach. See #4971

[Kevin Buzzard]

I have always felt like the canonical way to do this would be to prove the structure theorem for f.g. modules over a PID and deduce it from that. Amelia started on this but has now been distracted by other things. Ashvni will need a more general structure theorem which applies to modules such as $\mathbb{Z}_p[[T]]$ but she also has other things on her plate right now.

[Johan Commelin]

It would be good to get the ball rolling on this, and I don't really care how we do it. Structure theorem for fg modules over a PID sounds good to me. We want that anyways.

[Kevin Buzzard]

Maybe it's best to focus on structure theorem for PID modules rather than to wait for some fancy Noetherian local ring generalisation involving pseudo-null modules etc.

[Simon Andreys]

Hi everyone ! I'm new to lean (just finished the tutorials files), and I'm interested in trying to formalize this structure theorem; I remember reading its proof in Serge Lang's "undergraduate algebra" and being amazed at how it allowed both to construct Jordan normal forms and to describe the structure of finite commutative groups. I probably ridiculously underestimate how long and complicated it will be, since I still don't know the ring_theory and algebra/module part of matlib, but I shall give it a try.

[Johan Commelin]

@Simon Andreys Cool, that would be great! One bit of advice: ask lots of questions here.

[Simon Andreys]

Ok thanks ! I will try to do that.

[Riccardo Brasca]

That would be a great result! Maybe the best strategy is start by proving the classification of modules over PID?

[Riccardo Brasca]

or even euclidean domains, that should simplify some proofs

[Johan Commelin]

I think that's exactly what @Simon Andreys was referring to

[Filippo A. E. Nuccio]

This is actually something @Anne Baanen, @Ashvni Narayanan and myself will need to implement in connection with Dedekind domains. I think it is better to coordinate the efforts!

[Riccardo Brasca]

I meant to prove it non only for abelian groups

[Riccardo Brasca]

@Filippo A. E. Nuccio are you able to prove the classification over Dedekind domains?! Already stating the result seems hard!

[Filippo A. E. Nuccio]

Oh, certainly not! This is something we discussed yesterday and I think nobody has worked on this yet! If @Simon Andreys wants to go in this direction, I believe it is great!

[Anne Baanen]

So AFAICT, the specific statement we'll need is that submodules of finitely generated free R-modules are again f.g. free R-modules

[Filippo A. E. Nuccio]

I simply meant to say that we're also thinking about proving something along those lines, so it would be fruitful to discuss this together...

[Anne Baanen]

And the proof of the structure theorem uses that as an ingredient, right?

[Simon Andreys]

Okay ! I was planning to do only PID, I didn't even know about the generalization to Dedekind domains. Anyway my goal is mostly to learn more lean in a productive way, I probably won't be very efficient. For now my plan is :
1) first write proofs that a vector space with a linear map L can be seen as a module on the ring of polynomials (with the action P.v -> P(L).v ) . This gives me a nice example to work with and will get me started on the module/ring parts of mathlib.
2) Constructions of R/(p) for a prime ideal (p), if it does not exist, for a PID R.
3) The actual structure theorem on PID.
4) specialization to the case of vector spaces with endomorphism, and statement of the Jordan-Dunford/Chevalley theorem

[Riccardo Brasca]

@Simon Andreys The exact same statement is false for Dedekind domain, the torsion-free part is not necessarily free, but it can be characterized using protective modules.

[Simon Andreys]

@Riccardo Brasca I'm just reading it on wikipedia. The only part which is used to prove the Jordan normal form is the structure of the torsion module, maybe we can start by just considering this part of the structure theorem and clear the rest later.

[Riccardo Brasca]

Yes, torsion modules are enough for Jordan.

[Simon Andreys]

@Anne Baanen I think I will concentrate on the torsion part of the theorem for now, so it will probably not include any argument on free modules

[Eric Wieser]

Kevin Buzzard said:

I have always felt like the canonical way to do this would be to prove the structure theorem for f.g. modules over a PID and deduce it from that.

For anyone else finding this thread; we now have docs#module.equiv_free_prod_direct_sum which is presumably the theorem in question.