Graded Modules

Stream: maths

[Thomas Browning]

Mathlib seems to have two definitions of graded rings: docs#direct_sum.gring and docs#graded_ring, but they don't talk to each other as far as I can tell. Is there a reason for having two definitions?

[Yaël Dillies]

cc @Eric Wieser

[Antoine Chambert-Loir]

As far as I understand, docs#direct_sum.gring is about graded rings explicitly defined as the direct sum of their graded components, while docs#graded_ring is rather about a graduation of a given ring, with docs#direct_sum.decompose_ring_equiv showing an equivalence from one to the other.

[Eric Wieser]

One is for internally graded rings, the other for externally graded. The former implies the latter.

[Eric Wieser]

The naming certainly could be improved

[Eric Wieser]

I guess we should probably reference the paper from the docstrings