PR #4321: feat(algebra/free_algebra): Define a grading

Stream: triage

[Random Issue Bot]

Today I chose PR 4321 for discussion!

feat(algebra/free_algebra): Define a grading
Created by @Eric Wieser (@eric-wieser) on 2020-09-29
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

[Eric Wieser]

For reasons I don't understand, some induction _ using _ tactics in that PR started breaking. Easy to fix by switching to apply, but annoying

[Eric Wieser]

I remember @Kevin Buzzard being a bit opposed to this approach, and not really liking the use of docs#add_monoid_algebra for grading as the type doesn't really encode strict enough requirements.

Since then, I made a bit of progress on making direct_sum viable (docs#direct_sum.ring), but there's no direct_sum.algebra yet.

At the same time, I've noticed that docs#mv_polynomial.sum_homogeneous_component basically uses the same approach I've used in this PR anyway, so maybe add_monoid_algebra is fine as the return type after all.

[Kevin Buzzard]

The thing which struck me as weird was using polynomial to store a list of elements of the ground ring which, to me, had no right to be being treated as a polynomial.

[Eric Wieser]

That's why I used add_monoid_algebra and not polynomial :)

[Kevin Buzzard]

The way a grading should work is that I should be able to grade over an arbitrary add_comm_monoid M (not just nat). An M-grading on A is a map from M to add_subgroup A satisfying some cool axioms which could probably be extremely nicely explained using dfinsupp

[Eric Wieser]

I think a weaker version of what you're describing basically exists today as docs#direct_sum.gcomm_monoid (where ι is your M)

[Eric Wieser]

And the related definition docs#direct_sum.gcomm_monoid.of_add_submonoids

[Eric Wieser]

Of course, the axioms like "the subgroups are disjoint" is missing, but you don't need that axiom to get a sane ring structure.

[Eric Wieser]

My totally unsubstantiated claim would be for the case of the free algebra, the only interesting grading is the one over nat that that PR provides, or one derived from that grading

[Kevin Buzzard]

For a free algebra I can quite imagine that there's only one interesting grading. Looking at the Wikipedia article it starts off with everything nat-graded, remarks that associativity is not needed ( :-) ), then goes on to M-graded things, and then some kind of twisted M-graded things :-/ One now has to make some kind of a decision about what generality to work in. For me, the main thing is that we get to do Proj of a graded ring (which only needs nat grading), and in Stacks they stick to nat gradings, so maybe nat grading is fine for now -- I don't have any killer apps for more general gradings.

[Eric Wieser]

Oh, I've just noticed that "graded modules" on the stacks page index over R i and M i, which seems like it would be rather more of a headache than what I'd planned for with direct_sum.gmonoid etc

[Eric Wieser]

Regarding associativity, I guess I need to add a direct_sum.gmul_one_class to match @Oliver Nash's new mul_one_class and put a non_assoc_semiring instance on direct_sum...

[Julian Külshammer]

If we are talking about gradings in general: I've definitely worked with nat^r-gradings, not only nat-gradings, in my research. I'm not sure, how often gradings by non-commutative groups show up, I think many basic things should go through without assuming it.

[Kevin Buzzard]

The natural example I could think of was that $\R[X_1,X_2,\ldots,X_n]$ was graded by $\N^n$.

[Eric Wieser]

Yes, I think that's what mv_polynomial.sum_homogeneous_component hints at

[Eric Wieser]

That might be a compelling test-case for the current direct_sum API

[Eric Wieser]

That is, to show the direct sum of span (monomial i) gets a ring structure

[Julian Külshammer]

The context where I encountered int^r-gradings was not too exotic either: Let G be a reductive algebraic group over a field of positive characteristic. Let G_r be its r-th Frobenius kernel. Then the category of G_rT-modules (where T is a maximal torus) is equivalent to the category of X(T)-graded G_r-modules where X(T) is the character group of T. Of course this is a little bit outside mathlib's current scope...

[Kevin Buzzard]

I would love to see this sort of stuff in mathlib though. This looks like int^r-gradings?

[Julian Külshammer]

Yes, exactly.

[Damiano Testa]

Also, my favourite computation of the cohomology of projective space uses Z^n-gradings:

https://stacks.math.columbia.edu/tag/01XS

[Damiano Testa]

Maybe, gradings by non-commutative groups sometimes arise implicitly in representation theory: the regular representation is graded by the group itself, though in that case you usually outsource the grading to the choice of basis.

[Kevin Buzzard]

Ok so there are real world examples of int^n gradings

[Eric Wieser]

Although as a reminder that's not really in scope for the PR that started this conversation, which is specifically about grading the free algebra

[Eric Wieser]

But this conversation encouraged me to write the now-merged #6825, whixh added the first part of an N-grading for the multivariate polynomials (docs#mv_polynomial.is_homogeneous.homogeneous_submodule.gcomm_monoid)