Zulip Chat Archive

Stream: Is there code for X?

Topic: Quotient of homogeneous ideals

Bernhard Reinke (Sep 17 2025 at 16:15):

Suppose I have a graded algebra A and a homogeneous ideal I. I can form the quotient A ⧸ I as an algebra. I didn't find the code in mathlib to obtain the quotient as a graded algebra, is this already there?

Kenny Lau (Sep 17 2025 at 16:28):

it's one of those old PR's that still haven't been merged (there are actually two)

Kenny Lau (Sep 17 2025 at 16:29):

#27307 (continuing #22279) by @Wang Jingting

Kenny Lau (Sep 17 2025 at 16:32):

the second PR is #9820 by @Jujian Zhang

Last updated: Dec 20 2025 at 21:32 UTC