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
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
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
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
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
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 was graded by .
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
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
T is a maximal torus) is equivalent to the category of
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):
Damiano Testa (Mar 23 2021 at 07:09):
Also, my favourite computation of the cohomology of projective space uses Z^n-gradings:
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