# Zulip Chat Archive

## 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!

**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 (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:34):

And the related definition docs#direct_sum.gcomm_monoid.of_add_submonoids

#### 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?

#### Julian Külshammer (Mar 22 2021 at 20:03):

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