submodules of a graded module

Stream: maths

[Kevin Buzzard]

My student @FMLJohn just asked me the following question, which has stumped me. He has a graded ring $A=\oplus_i A_i$ and a graded $A$-module $M=\oplus_i M_i$ (all sums over Nat). Note that $A$ might be a polynomial ring, it's not literally equal to the direct sum, it's internally graded, and the same is true for $M$. Here's how one might set this up:

variable {A : Type } [CommRing A]
variable (𝒜 : ℕ → Submodule ℤ A) [GradedRing 𝒜]
variable {M : Type } [AddCommGroup M] [Module A M]
variable (ℳ : ℕ → Submodule ℤ M) [SetLike.GradedSmul 𝒜 ℳ] [DirectSum.Decomposition ℳ]

Note that $A_0$ is a subring of $A$. He can put things like "$M_i$ is an $A_0$-module$$" into the typeclass inference system, but he can't put things like "$\oplus_iM_i$ is an $A$-module" in, because the typeclass inference system can't see 𝒜 . A #mwe of a failure:

import Mathlib

variable {A : Type } [CommRing A]
variable (𝒜 : ℕ → Submodule ℤ A) [GradedRing 𝒜]
variable {M : Type } [AddCommGroup M] [Module A M]
variable (ℳ : ℕ → Submodule ℤ M) [SetLike.GradedSmul 𝒜 ℳ] [DirectSum.Decomposition ℳ]

instance : Module A (⨁ (i : ℕ), ℳ i) := GradedModule.isModule 𝒜 ℳ

The (expected) error is cannot find synthesization order...all remaining arguments have metavariables

Does this mean that there should be some typeclass HasGrading A which carries 𝒜 around? John would like to make things like $\oplus_{i\geq t}M_i$ into an $A$-module, for example. This comes up in the theory of Hilbert-Poincar\'e series.

[Eric Wieser]

Can you make do by replacing A with the direct sum of its pieces?

[Eric Wieser]

The problem with HasGrading is that I think it's rare to have a canonical grading

[Kevin Buzzard]

I suspect that we can. Is this really what we have to do though? It's going to get really messy when we have an A-module and a $\oplus_i A_i$-module and want to consider, say their tensor product. I should say that I don't think that this will happen for the current application though.

[Antoine Chambert-Loir]

In our work with Maria Ines, we had the impression that some basic work on graded stuff is still missing. For example, quotients of submodules, or 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 ).

[Kevin Buzzard]

In alg geom it's pretty common to have the rings indexed by $\N$ and the modules by $\Z$.

[Eric Wieser]

The (non-categorical) graded stuff is still fairly young in mathlib; @Jujian Zhang and I put a few things in, but I haven't seen much other work on it yet.

[Eric Wieser]

Sounds like for your use case Kevin, the grades should combine with +ᵥ instead of +

[Eric Wieser]

(which would be an easy refactor!)

[Eric Wieser]

Done in #7573

[Antoine Chambert-Loir]

Great!

[Eric Wieser]

There's a long tail here though; I don't think we have the fact that Nat acts additively on Int

[Eric Wieser]

And we certainly don't have the fact that Nat acts additively on any docs#AddMonoidWIthOne

[Eric Wieser]

(tangentially, there are some simple results about graded rings in #7574/ #7575/ #7577 that would be nice to have)

[Antoine Chambert-Loir]

The point is that not only should one haveNat acting on Int, but also Nat ^ n acting on Int ^ n, or, but that would be more natural Macting on N for any M : SubAddMonoid N where AddMonoid N.

[Damiano Testa]

Something like that already exists: docs#AddSubmonoid.addAction.

[Damiano Testa]

However, Nat is not a submonoid of Int. :upside_down:

[Antoine Chambert-Loir]

yes, and of course it is not…

[Eric Wieser]

Antoine Chambert-Loir said:

but also Nat ^ n acting on Int ^ n

This strategy is dangerous; how does Nat ^ n act on (Nat ^ n) ^ n?

[Eric Wieser]

(we have the action you ask for already, it's docs#Pi.vadd'; but it's also diamond-inducing)

[Antoine Chambert-Loir]

I observe that mathlib's tendency is to have all actions as implicit instances. I don't think that this is how mathematicians work.

[Eric Wieser]

I think arguably the actions that mathematicians wouldn't write implicitly (such as Pi.vadd'?) shouldn't be instances

[Eric Wieser]

But presumably you agree that a mathematical would write rv for the multiplicative action of r : R on v : R ^ n with the action implicit?

[Antoine Chambert-Loir]

Yes, s·he would, but only within a restricted amount of time would this notation be fixed to some definition, while a mathlib instance is like a Bourbaki definition: it's once and for all, bis ins Ewigkeit.

[Yaël Dillies]

Eric Wieser said:

There's a long tail here though; I don't think we have the fact that Nat acts additively on Int

I added that a year ago

[Antoine Chambert-Loir]

The work of @Sebastien Gouezel on the change of variable formula (more precisely on Suslin's theorem) shows that it is possible to handle a series of instances (in his case, many topological space structures on the same type), but it becomes complicated to do so when other instances depend on them. Actions are one thing, but there are also assumptions that they commute together, etc.

[Eric Wieser]

Yaël Dillies said:

I added that a year ago

@loogle Nat, Int, VAdd

[loogle]

:shrug: nothing found

[Antoine Chambert-Loir]

it's v0 of the @yael engine, which only says “it exists because I wrote it”.
when zulip has the v1, it will give the precise location.

[Eric Wieser]

V0 also occasionally has this bug where they refer to an unmerged Lean 3 PR

[Eric Wieser]

Eric Wieser said:

Done in #7573

The conversation here has gotten side-tracked a little; it would be great if someone could give this a reivew!