Random Issue Bot (Dec 28 2020 at 14:28):
Today I chose PR 4812 for discussion!
feat(algebra/graded_algebra): Define a dependent version of add_monoid_algebra
Created by @Eric Wieser (@eric-wieser) on 2020-10-28
Is this PR still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Dec 28 2020 at 14:44):
@Reid Barton how do you think this should be set up? #4321 seems to be some attempt to define a -grading on a ring by giving a map from to such that the coefficient of is the th piece; this one has a definition of grading which assumes some underlying multiplication for some "universe" where the graded pieces live (they're add_subgroups of a ring). I'm not sure @Eric Wieser is working on either PR right now, and @Amelia Livingston has defined gradings on tensor algebras and exterior algebras by hand.
Eric Wieser (Dec 28 2020 at 14:48):
I plan to come back to these, but an indeed not actively working on them
Eric Wieser (Dec 28 2020 at 14:49):
Somehow #4321 started failing CI, complaining about something that used to be a valid induction principle not being one any more
Eric Wieser (Dec 28 2020 at 14:51):
But I'm using stuff from #4321 in my own work to grade clifford algebras (and have grading of tensor and exterior algebras by the same approach, not yet PR'd)
Eric Wieser (Dec 28 2020 at 14:54):
The titular PR here had some good feedback from Kenny on zulip about bundling linear maps that I found more difficult to use than intended. However, I expect I'll come back to this when I find myself needing to define a multiplication over direct sums of alternating maps indexed by
Last updated: May 18 2021 at 23:14 UTC