Zulip Chat Archive
Stream: triage
Topic: issue #1063: homological algebra
Random Issue Bot (Jan 24 2021 at 14:44):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: feature-request, roadmap
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 18 2021 at 14:20):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: feature-request, roadmap
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Feb 18 2021 at 23:37):
We are wrestling with homological algebra in the condensed mathematics stream. Amelia Livingston has done tensor products of complexes as part of her MSc project, but only for R-modules. Markus Himmel seemed to think that we still needed a lot more machinery before we could do anything for general abelian categories, for example I think he found it hard to show that an object was projective iff it had projective dimension 0 in the general abelian category case.
Random Issue Bot (Mar 06 2021 at 14:20):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: feature-request, roadmap
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Mar 06 2021 at 14:56):
This is being actively worked on in the #condensed mathematics stream and things will slowly but surely get done.
Random Issue Bot (Mar 25 2021 at 14:39):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: feature-request, roadmap
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 14 2022 at 14:14):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: roadmap, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Mar 14 2022 at 22:48):
I ticked off homotopy equivalences, but for exact sequences I think we're at least still waiting for material to arrive from lean-liquid/for_mathlib
. :-)
Random Issue Bot (Mar 24 2022 at 14:13):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: roadmap, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 12 2022 at 14:18):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: roadmap, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 14 2023 at 14:07):
Today I chose issue 1063 for discussion!
homological algebra
Created by @Scott Morrison (@semorrison) on 2019-05-20
Labels: roadmap, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC