breen deligne update

Stream: condensed mathematics

[Johan Commelin]

I've turned the homotopy category into a preadditive category (was a TODO in mathlib, incoming PR soon). I've also defined a "realization functor" for Breen-Deligne data into any abelian category with endofunctor F. Later, we want to specialize to the endofunctor ℤ[_] of condensed abelian groups.

[Johan Commelin]

I pushed more BD stuff. But it's now time for a mathlib bump.