Topic: jordan normal form
Johan Commelin (Nov 11 2020 at 09:32):
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 (Nov 11 2020 at 09:34):
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 but she also has other things on her plate right now.
Johan Commelin (Nov 11 2020 at 09:39):
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 (Nov 11 2020 at 09:41):
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 (Nov 20 2020 at 14:20):
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 (Nov 20 2020 at 14:21):
@Simon Andreys Cool, that would be great! One bit of advice: ask lots of questions here.
Simon Andreys (Nov 20 2020 at 14:22):
Ok thanks ! I will try to do that.
Riccardo Brasca (Nov 20 2020 at 14:49):
That would be a great result! Maybe the best strategy is start by proving the classification of modules over PID?
Riccardo Brasca (Nov 20 2020 at 14:49):
or even euclidean domains, that should simplify some proofs
Johan Commelin (Nov 20 2020 at 14:50):
I think that's exactly what @Simon Andreys was referring to
Filippo A. E. Nuccio (Nov 20 2020 at 14:51):
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 (Nov 20 2020 at 14:59):
I meant to prove it non only for abelian groups
Riccardo Brasca (Nov 20 2020 at 15:00):
@Filippo A. E. Nuccio are you able to prove the classification over Dedekind domains?! Already stating the result seems hard!
Filippo A. E. Nuccio (Nov 20 2020 at 15:01):
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 (Nov 20 2020 at 15:02):
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 (Nov 20 2020 at 15:02):
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 (Nov 20 2020 at 15:03):
And the proof of the structure theorem uses that as an ingredient, right?
Simon Andreys (Nov 20 2020 at 15:07):
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 (Nov 20 2020 at 15:10):
@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 (Nov 20 2020 at 15:12):
@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 (Nov 20 2020 at 15:23):
Yes, torsion modules are enough for Jordan.
Simon Andreys (Nov 20 2020 at 15:54):
@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
Last updated: May 14 2021 at 19:21 UTC