Stream: triage

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

Random Issue Bot (Mar 22 2021 at 14:21):

Today I chose PR 4321 for discussion!

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 (Mar 22 2021 at 14:48):

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 (Mar 22 2021 at 14:52):

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 (Mar 22 2021 at 15:20):

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 (Mar 22 2021 at 15:49):

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

Kevin Buzzard (Mar 22 2021 at 16:06):

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 (Mar 22 2021 at 16:34):

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 (Mar 22 2021 at 16:35):

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 (Mar 22 2021 at 16:37):

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 (Mar 22 2021 at 18:40):

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 (Mar 22 2021 at 18:58):

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 (Mar 22 2021 at 19:08):

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 (Mar 22 2021 at 19:10):

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 (Mar 22 2021 at 19:15):

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

Eric Wieser (Mar 22 2021 at 19:28):

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

Eric Wieser (Mar 22 2021 at 19:30):

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

Eric Wieser (Mar 22 2021 at 19:33):

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

Julian Külshammer (Mar 22 2021 at 19:43):

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 (Mar 22 2021 at 20:02):

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

Yes, exactly.

Damiano Testa (Mar 23 2021 at 07:09):

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

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

Damiano Testa (Mar 23 2021 at 07:10):

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 (Mar 23 2021 at 08:28):

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

Eric Wieser (Mar 23 2021 at 08:37):

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 (Mar 23 2021 at 08:38):

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)

Last updated: May 09 2021 at 16:20 UTC