PR #4812: feat(algebra/graded_algebra): Define a dependen...

Stream: triage

[Random Issue Bot]

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
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

@Reid Barton how do you think this should be set up? #4321 seems to be some attempt to define a $\mathbb{N}$-grading on a ring $R$ by giving a map from $R$ to $R[X]$ such that the coefficient of $X^i$ is the $i$ 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]

I plan to come back to these, but an indeed not actively working on them

[Eric Wieser]

Somehow #4321 started failing CI, complaining about something that used to be a valid induction principle not being one any more

[Eric Wieser]

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]

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 fin n