F.g. modules over PIDs

Stream: maths

[Alexey S. Vasilev]

There is a group of students at my university studying Lean, with the final goal being some contribution to mathlib. Our supervisor offered to prove the structure theorem for finitely generated abelian groups (or even the structure theorem for f.g. modules over PIDs).
We found out that the first half was already proved by @Anne Baanen. This also looks relevant.

Were there any other results in this direction? Maybe someone works on the second part of the theorem right now?

[Kevin Buzzard]

Right now we have f.g. + torsion-free implies free (for modules over a PID) but we don't have the full theorem. (oh sorry, you already spotted this!). @Patrick Massot are you planning on proving the structure theorem for f.g. modules over a PID?

[Johan Commelin]

I think the only part that is missing is the "nasty" part that classifies f.g. torsion modules.

[Kevin Buzzard]

I've seen a proof which involves a lot of manipulation of matrices :-/ That won't be much fun to do formally. Is the structure theorem for finite abelian groups any easier?

[Patrick Massot]

Yes, the remaining part is classification of f.g. torsion modules, even in the abelian group case. Yes the classical proof involves a lot of matrix manipulations, but it's not the only possible proof. The matrix proof can probably give you a computable classification, but this is not what we usually care about in mathlib.

[Patrick Massot]

And yes , there are shortcuts for abelian groups.

[Patrick Massot]

For abelian groups it is easy to setup an induction process using the group exponent.

[Patrick Massot]

And I don't plan to work on this at all. I did #7341 because it was potentially useful for LTE and low hanging.

[Patrick Massot]

Alexey, who is your advisor? What is your university?

[Alexey S. Vasilev]

My university is Novosibirsk State University, Russia, and the advisor is Evgeny Vdovin. He does not specialize in formalizing mathematics, and in fact our Lean group is quite new. Perhaps the theorem we chose is too complicated (for example, we thought that the matrix proof is the easiest to formalize). We will be glad to hear any advice or suggestions.

[Johan Commelin]

Typically, the more abstract the easier it is to formalize. Explicitly manipulating matrices can quickly become quite dirty.

[David Wärn]

Am I right in saying we also don't have the infinitary version of Dedekind's theorem "submodule of free module over PID is free"? I don't think this one should be too hard using well-ordering principle

[Johan Commelin]

Right, I don't think that's in mathlib

[Kevin Buzzard]

That might be a more accessible challenge for beginners (if you know the maths, that is)

[Kevin Buzzard]

@Pierre-Alexandre Bazin is currently thinking about this. Did anything come of @Alexey S. Vasilev 's project?

[Antoine Chambert-Loir]

What about projective modules over local rings ?

[Kevin Buzzard]

That would be another good project. The proof in Matsumura uses transfinite induction! I once noted to Conrad that it was the only time I'd ever seen ordinals used in "regular math" and he pointed out that he knew a proof which didn't use transfinite induction.

[Reid Barton]

I may have commented this to you before but I think as a rule, arguments with Zorn's lemma tend to be more transparent with transfinite induction (e.g. every vector space has a basis: well-order the elements of the vector space arbitrarily and keep whatever vectors are not in the span of the preceding ones).

[Reid Barton]

It's just Gaussian elimination that takes a bit longer.

[Pierre-Alexandre Bazin]

I'm glad to announce the structure theorem for f.g. modules over a PID is now proved in mathlib ! (#13524)

[Oliver Nash]

docs#module.equiv_free_prod_direct_sum

[Kevin Buzzard]

It's been a long time coming. Thank you very much @Pierre-Alexandre Bazin for making it happen!

[Riccardo Brasca]

We still need a little bit of glue to get the statement for finite abelian groups, but nothing special I think.

Are we ready for Jordan normal form?

[Pierre-Alexandre Bazin]

For Jordan normal form I'll at least need the stuff at #14666 + defining what a Jordan block is (I don't think we have it) and show it's multiplication by Xin R[X] ⧸ ((X - a) ^ n) (with the right basis) so that's still quite some work remaining

[Patrick Massot]

It's great that we got this! However isn't a bit exaggerated to call that "the structure theorem for f.g. modules over a PID " if you don't have uniqueness? I thought uniqueness is the tricky part.

[Eric Wieser]

What would a statement of uniqueness look like there?

[Patrick Massot]

https://en.wikipedia.org/wiki/Structure_theorem_for_finitely_generated_modules_over_a_principal_ideal_domain#Invariant_factor_decomposition

[Eric Wieser]

Oh, I guess you mean uniqueness of p and e up to permutation of ι?

[Kevin Buzzard]

I don't think uniqueness is too hard; you tensor up to the field of fractions to get uniqueness of rank, and you look at P^i-torsion to get uniqueness of the powers of P. I agree it might be fiddly to do uniqueness in Lean, but existence is hard even on paper.

[Patrick Massot]

Maybe I'm misremembering what is really harder in the general case than in the abelian group case.

[Eric Wieser]

I had a go at extracting some constructions from the existentials in #14734, in case that's helpful for showing uniqueness

[Pierre-Alexandre Bazin]

Indeed, uniqueness is missing. By the way, I just opened #14736 for the case of abelian groups