[Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID #13524

pbazin · 2022-04-19T17:23:09Z

A finitely generated torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.
(TODO : This part should be generalisable to a Dedekind domain, see https://en.wikipedia.org/wiki/Dedekind_domain#Finitely_generated_modules_over_a_Dedekind_domain . Part of the proof is already generalised).

More generally, a finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of some
R ⧸ R ∙ (p i ^ e i).
(TODO : prove this decomposition is unique.)
(TODO : deduce the structure theorem for finite(ly generated) abelian groups).

Ruben-VandeVelde · 2022-04-22T14:32:22Z

Does this belong in https://github.com/leanprover-community/mathlib/blob/master/docs/overview.yaml?

pbazin · 2022-04-25T08:14:52Z

I added it

pbazin · 2022-04-25T12:19:23Z

hmm... what's up ?

semorrison · 2022-05-07T00:31:45Z

I'm guessing you'd like a review of this? Sorry, I just saw this has been sitting here unlabelled for a while. (This means people won't see it on the #queue.)

pbazin · 2022-05-09T07:52:57Z

Indeed, I forgot to add the "awaiting-review" label after the dependent issue was merged

pbazin · 2022-05-11T13:48:44Z

actually, it seems the part on torsion modules can be generalised for a Dedekind domain (https://en.wikipedia.org/wiki/Dedekind_domain#Finitely_generated_modules_over_a_Dedekind_domain). I'm working on it

src/algebra/module/pid.lean

jcommelin · 2022-05-12T08:38:01Z

Could you please edit the first message in this PR to reflect the current state? Because that message will end up as the commit message once the PR is merged. So if you have done some TODO, please rewrite the message (instead of just stiking out the TODO).

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

pbazin · 2022-05-12T12:18:44Z

Done @jcommelin

pbazin · 2022-05-16T14:41:15Z

(for generalisation to a Dedekind domain, I'll need the results on #14176)

riccardobrasca

I know it's annoying, but I suggest you open another PR with the modifications to algebra/module/torsion.lean (including those I suggested to move there), and make this one depending on the new one. In general the review process is much faster on smaller PR.

In any case this looks really good, thanks!

src/algebra/module/pid.lean

…es (#14573) An intermediate PR for various lemmas about torsion modules needed at #13524

mathlib-dependent-issues-bot · 2022-06-09T15:41:03Z

This PR/issue depends on:

~~[Merged by Bors] - feat(algebra/module/torsion): torsion ideal, decomposition lemma #13414~~
~~[Merged by Bors] - feat(alegbra/homology/short_exact/abelian.lean): Right split exact sequences + case of modules #14376~~
~~[Merged by Bors] - feat(algebra/module/torsion.lean): various lemmas about torsion modules #14573~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca

I think it's almost ready to go!

src/algebra/module/dedekind_domain.lean

riccardobrasca · 2022-06-10T12:56:48Z

Just one last thing... can you deduce the result for abelian groups? I mean, without mentioning Z-modules. If it more than a couple of lines let's keep it for another PR.

pbazin · 2022-06-13T10:53:42Z

Just one last thing... can you deduce the result for abelian groups? I mean, without mentioning Z-modules. If it more than a couple of lines let's keep it for another PR.

It turns out there's some messy stuff going on when trying to change the ℤ ⧸ ℤ · _ into zmod in the direct sum, that makes it more than just a couple of lines. So better keep it for another PR

riccardobrasca · 2022-06-13T14:34:31Z

Just one last thing... can you deduce the result for abelian groups? I mean, without mentioning Z-modules. If it more than a couple of lines let's keep it for another PR.

It turns out there's some messy stuff going on when trying to change the ℤ ⧸ ℤ · _ into zmod in the direct sum, that makes it more than just a couple of lines. So better keep it for another PR

OK, no problem. Can you just add a TODO? And thanks for your work!

bors d+

bors · 2022-06-13T14:34:33Z

✌️ pbazin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

pbazin · 2022-06-13T18:52:10Z

bors r+

…n modules over a PID (#13524) A finitely generated torsion module over a PID is isomorphic to a direct sum of some `R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers. (TODO : This part should be generalisable to a Dedekind domain, see https://en.wikipedia.org/wiki/Dedekind_domain#Finitely_generated_modules_over_a_Dedekind_domain . Part of the proof is already generalised). More generally, a finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of some `R ⧸ R ∙ (p i ^ e i)`. (TODO : prove this decomposition is unique.) (TODO : deduce the structure theorem for finite(ly generated) abelian groups). - [x] depends on: #13414 - [x] depends on: #14376 - [x] depends on: #14573 Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>

bors · 2022-06-13T21:43:02Z

Pull request successfully merged into master.

Build succeeded:

pbazin added 9 commits April 12, 2022 16:18

initial commit

7a8009d

style

eaa7694

torsion_is_internal docstring

5b90fef

Merge branch 'master' into pid_fg_module_classification

6a153ec

initial commit

89afa03

some lint

9085427

move

2c6b2da

lint + move

4c126f7

doc + move

2212b25

leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 19, 2022

j-loreaux changed the title ~~feat(algebra/module/pid.lean): Classification of finitely generated torsion modules over a PID~~ feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID Apr 20, 2022

General case (no torsion hypothesis)

beb3c9e

pbazin changed the title ~~feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID~~ feat(algebra/module/pid): Classification of finitely generated modules over a PID Apr 22, 2022

doc

6307e82

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 4, 2022

leanprover-community deleted a comment from leanprover-community-bot-assistant May 4, 2022

pbazin and others added 2 commits May 5, 2022 11:17

Merge branch 'master' into pid_fg_module_classification

f180699

fix after merge

3f09386

semorrison added the awaiting-review The author would like community review of the PR label May 7, 2022

riccardobrasca reviewed May 11, 2022

View reviewed changes

src/algebra/module/pid.lean Outdated Show resolved Hide resolved

src/algebra/module/pid.lean Outdated Show resolved Hide resolved

grammar

90ffa2b

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

unduplicate is_domain

44f8b59

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 30, 2022

pbazin added 3 commits May 31, 2022 11:50

Merge branch 'master' into pid_fg_module_classification

34ac32a

is_internal post-merge fix

7298bbe

fix

9b0ec5c

riccardobrasca reviewed Jun 3, 2022

View reviewed changes

pbazin mentioned this pull request Jun 6, 2022

[Merged by Bors] - feat(algebra/module/torsion.lean): various lemmas about torsion modules #14573

Closed

mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 6, 2022

bors bot pushed a commit that referenced this pull request Jun 9, 2022

feat(algebra/module/torsion.lean): various lemmas about torsion modul…

c2bb59e

…es (#14573) An intermediate PR for various lemmas about torsion modules needed at #13524

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 9, 2022

pbazin added 2 commits June 9, 2022 18:49

temporary commit to compile

0505912

Merge branch 'master' into pid_fg_module_classification

72bddd0

riccardobrasca reviewed Jun 10, 2022

View reviewed changes

src/algebra/module/dedekind_domain.lean Outdated Show resolved Hide resolved

src/algebra/module/dedekind_domain.lean Outdated Show resolved Hide resolved

pbazin added 3 commits June 10, 2022 11:45

namespace

ea2ce48

doc

829cc97

doc

e0cd558

riccardobrasca changed the title ~~feat(algebra/module/pid): Classification of finitely generated modules over a PID~~ feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID Jun 11, 2022

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jun 13, 2022

bors bot changed the title ~~feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID~~ [Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID Jun 13, 2022

bors bot closed this Jun 13, 2022

bors bot deleted the pid_fg_module_classification branch June 13, 2022 21:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID #13524

[Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID #13524

pbazin commented Apr 19, 2022 •

edited by alexjbest

Loading

Ruben-VandeVelde commented Apr 22, 2022

pbazin commented Apr 25, 2022

pbazin commented Apr 25, 2022

semorrison commented May 7, 2022

pbazin commented May 9, 2022

pbazin commented May 11, 2022

jcommelin commented May 12, 2022

pbazin commented May 12, 2022

pbazin commented May 16, 2022

riccardobrasca left a comment

mathlib-dependent-issues-bot commented Jun 9, 2022

riccardobrasca left a comment •

edited

Loading

riccardobrasca commented Jun 10, 2022

pbazin commented Jun 13, 2022

riccardobrasca commented Jun 13, 2022

bors bot commented Jun 13, 2022

pbazin commented Jun 13, 2022

bors bot commented Jun 13, 2022

[Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID #13524

[Merged by Bors] - feat(algebra/module/pid): Classification of finitely generated torsion modules over a PID #13524

Conversation

pbazin commented Apr 19, 2022 • edited by alexjbest Loading

Ruben-VandeVelde commented Apr 22, 2022

pbazin commented Apr 25, 2022

pbazin commented Apr 25, 2022

semorrison commented May 7, 2022

pbazin commented May 9, 2022

pbazin commented May 11, 2022

jcommelin commented May 12, 2022

pbazin commented May 12, 2022

pbazin commented May 16, 2022

riccardobrasca left a comment

Choose a reason for hiding this comment

mathlib-dependent-issues-bot commented Jun 9, 2022

riccardobrasca left a comment • edited Loading

Choose a reason for hiding this comment

riccardobrasca commented Jun 10, 2022

pbazin commented Jun 13, 2022

riccardobrasca commented Jun 13, 2022

bors bot commented Jun 13, 2022

pbazin commented Jun 13, 2022

bors bot commented Jun 13, 2022

pbazin commented Apr 19, 2022 •

edited by alexjbest

Loading

riccardobrasca left a comment •

edited

Loading