Zulip Chat Archive

Hello, we have opened a series of PR for filtered ring/algebra/module, the associated graded structure and some basic things about their exactness. Previously there is #20900 merged. The dependencies between the incoming ones are as follow:
4d5e2c0a5c489cc5372c01992c3618c.jpg

Eric Wieser (Mar 16 2025 at 09:06):

A -> B means "A needs B to be merged first" (A depends on B) or "A is the pre-work for B" (B depends on A)?

Nailin Guan (Mar 16 2025 at 10:14):

Yes, sorry that I didn't make it clear.

Eric Wieser (Mar 16 2025 at 10:34):

Which meaning did you intend?

Kevin Buzzard (Mar 16 2025 at 11:01):

aka "where do we start?" (answer: A -> B in the diagram seems to mean "B depends on A")

Nailin Guan (Mar 16 2025 at 12:04):

A->B mean B depend on A, we can start at #22631
#PR reviews > #22631 define associated graded structure for abelian group
There is another PR with no dependency at #22705 consisting of only some relevant lemma

Nailin Guan (Apr 07 2025 at 14:32):

Currently, #22705 is merged.
Can anybody have more look on #22631? Thanks

Nailin Guan (Jul 28 2025 at 18:59):

Newly updated dependency graph:
a5a507aa5dfef8d89dec884afac3343.jpg
There is a conversation in #22631 (the original PR of #26857) about the index of filtration that reference @Kevin Buzzard, do you have any further comments about this?