## Stream: maths

### Topic: F.g. modules over PIDs

#### Alexey S. Vasilev (May 04 2021 at 12:37):

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 (May 04 2021 at 12:38):

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 (May 04 2021 at 12:40):

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

#### Kevin Buzzard (May 04 2021 at 12:41):

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 (May 04 2021 at 12:44):

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 (May 04 2021 at 12:45):

And yes , there are shortcuts for abelian groups.

#### Patrick Massot (May 04 2021 at 12:46):

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

#### Patrick Massot (May 04 2021 at 12:46):

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

#### Alexey S. Vasilev (May 04 2021 at 13:06):

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 (May 04 2021 at 13:12):

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

#### David Wärn (May 04 2021 at 13:13):

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 (May 04 2021 at 13:14):

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

#### Kevin Buzzard (May 04 2021 at 13:15):

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

Last updated: Jun 17 2021 at 16:20 UTC