Zulip Chat Archive

Stream: condensed mathematics

Topic: two step resolutions


Fabian Glöckle (Mar 02 2022 at 11:37):

I just pushed the two step projective resolutions for AddCommGroup and Module over PIDs. First, I thought to use the resolution for Z and the forgetful functor to AddCommGroup, but this makes working with the terms very clumsy.
So now there are two separate sets of definitions and theorems which are unrelated and basically copied over from each other. I hope this makes working with them better because there will be good defeqs. And let's hope no one needs to comparison morphism too soon :)

And feel free to suggest other names, two_step_resolution and two_step_resolution_ab were just the first ones that came to my mind.

Johan Commelin (Mar 02 2022 at 13:22):

For LTE itself, we only need the AddCommGroup version.


Last updated: Dec 20 2023 at 11:08 UTC