Zulip Chat Archive

Stream: condensed mathematics

Topic: acyclics

Johan Commelin (May 02 2022 at 13:40):

Brief notification that I have a pretty thorough skeleton for the fact that you can compute Ext^i(C, B) naively, if C is a complex consisting of Hom(_, B)-acyclic objects.
It's all in for_mathlib/acyclic.lean.

Johan Commelin (May 02 2022 at 13:41):

A more refined version of that argument should be reusable for https://leanprover-community.github.io/liquid/sect0009.html#acyclic-sheaf

Johan Commelin (May 02 2022 at 13:41):

But I haven't made that refinement yet.

Last updated: Dec 20 2023 at 11:08 UTC