submodule of free module over PID is free

Stream: Is there code for X?

[Johan Commelin]

Afaik we only know that submodules of finitely-generated free modules are free. But it's true without the finiteness assumption: https://math.stackexchange.com/a/162958

Is the general case already done by chance?

[Riccardo Brasca]

I am pretty sure it's not

[Riccardo Brasca]

I wanted to do it but then I got sucked in flt-regular

[Riccardo Brasca]

But I think all the ingredients are there

[Anne Baanen]

This is essentially the proof we already have for the finite case, but now with transfinite induction, right?

[Johan Commelin]

I guess so

[Johan Commelin]

#xy : we'll need two term projective resolutions of abelian groups at some point in LTE: https://math.stackexchange.com/a/1547055

[Fabian Glöckle]

I'd like to give it a shot starting next week. I'll report here!

[Kevin Buzzard]

Related : @Pierre-Alexandre Bazin is working on structure theorem for f.g. modules over a PID

[Fabian Glöckle]

So, @Anne Baanen there is a sorry-free proof in the lean-liquid repository:
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/pid.lean
But it will require lots of cleanup work before it can go into mathlib, which I will start on after the corollary on 2-step projective resolutions is done.
I'd be glad about some ideas on how to improve the proof :)

[Fabian Glöckle]

Also there are some lemmas regarding other parts of the library which I do not know can be circumvented or could be useful for mathlib in general

[Fabian Glöckle]

It seems to me that particularly the interplay between filtrations / direct limits and supports of linear combinations should be done in greater generality

[Anne Baanen]

Nice work, I'll try and take a look soon!

[Fabian Glöckle]

thank you!

[Kevin Buzzard]

@Fabian Glöckle if you're in the mood then the proof on pages 10 and 11 of Matsumura that a projective module over a local ring is free also goes via transfinite induction :-)