Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Mar 22 2021 at 14:21):

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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Mar 22 2021 at 15:49):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Mar 22 2021 at 16:34):

And the related definition docs#direct_sum.gcomm_monoid.of_add_submonoids

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 19:15):

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

view this post on Zulip Eric Wieser (Mar 22 2021 at 19:28):

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

view this post on Zulip Eric Wieser (Mar 22 2021 at 19:30):

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

view this post on Zulip Eric Wieser (Mar 22 2021 at 19:33):

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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Julian Külshammer (Mar 22 2021 at 20:03):

Yes, exactly.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 08:28):

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

view this post on Zulip 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

view this post on Zulip 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