Commit 2023-10-19 13:16 d3c0421b

feat(Algebra/Module/GradedModule): generalize + to +ᵥ in indicies (#7573) The action is now of signature A i → M j → M (i +ᵥ j) instead of A i → M j → M (i + j). These are defeq when i and j are of the same type. This allow the grading type of the ring and module to be different, as long as one acts additively on the other, as requested on Zulip: @AntoineChambert-Loir said:

In our work with Maria Ines, we had the impression that some basic work on graded stuff is still missing. For example, [...] graduations which are not indexed by the same thing on the ring and on the module (some action of one on the other would be required, of course ) @kbuzzard said: In alg geom it's pretty common to have the rings indexed by $ℕ$ and the modules by $ℤ$. Mathlib is rather short on instances for additive actions, but with suitable instances this will allow the ring to be ℕ-graded and the module to be ℤ-graded.