two step resolutions

Stream: condensed mathematics

[Fabian Glöckle]

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]

For LTE itself, we only need the AddCommGroup version.