Commit 2025-07-23 08:49 134104be

feat(CategoryTheory/Abelian/SerreClass): left Bousfield localizations (#26663) If G : D ⥤ C is an exact functor between abelian categories, with a fully faithful right adjoint F, then G identifies C to the localization of D with respect to the class of morphisms G.kernel.isoModSerre, i.e. D is the localization of C with respect to Serre class G.kernel consisting of the objects in D that are sent to a zero object by G. (We also translate this in terms of a left Bousfield localization.)