# Zulip Chat Archive

## Stream: triage

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

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

Labels: WIP

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 $\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 (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 `fin n`

Last updated: May 18 2021 at 23:14 UTC