Decomposition theorem for graded modules over a PID

Stream: Is there code for X?

[VayusElytra]

Hi, has the decomposition theorem for graded modules over a PID been implemented into mathlib? Here is the wikipedia reference of the theorem I am talking about. I could only find a couple of files that deal with graded modules at all, so I assume it is still to do.

[Ruben Van de Velde]

I see nothing specific about graded modules in that article. Am I missing something?

[VayusElytra]

I think this wikipedia article is the correct thing to ask about. The literature I am following along is a little ambiguous; one paper refers to a "fundamental theorem for finitely generated modules over a graded principal ideal domains" (that it does not state), another as "the structure theorem for finitely-generated graded modules over a principal ideal domain" - changing which object is graded. To complicate the matter further, this same source includes a reference to Hungerford's Algebra, P.225, Theorem 6.12, which is a decomposition theorem for modules over PIDs... that features no talk of graded objects at all.

I think for now, let's ignore grading and talk about the decomposition theorem from this Wikipedia article. If it isn't implemented into mathlib yet, then surely any potentially more complex results with an additional grading hypothesis won't be either. My apologies for the confusion.

[Kevin Buzzard]

We have the structure theorem for fg modules over a PID and I don't know what statement we're talking about when it comes to adding a grading

[VayusElytra]

Thank you!
As for the grading: this passage from "Topology for Computing" by Zomorodian clears up the confusion:
image.png