Zulip Chat Archive

Stream: triage

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

view this post on Zulip 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?

view this post on Zulip 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 N\mathbb{N}-grading on a ring RR by giving a map from RR to R[X]R[X] such that the coefficient of XiX^i is the ii 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.

view this post on Zulip Eric Wieser (Dec 28 2020 at 14:48):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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