Commit 2024-02-13 21:51 12d8bb68

feat(Algebra/Homology): two descriptions of the derived category as a localized category (#9660) In this PR, it is shown that under certain conditions on the complex shape c, the category HomologicalComplexUpToQuasiIso C c of homological complexes up to quasi-isomorphisms, which is a localization of the category of homological complexes, is also a localization of the homotopy category. In particular, in the case of cochain complexes indexed by the integers, this means that the derived category of an abelian category C can be obtained either in a single step by formally inverting the quasi-isomorphisms in the category of cochain complexes, or in two steps by first passing to the homotopy category (which is a quotient category) and then formally inverting the quasi-isomorphisms in the homotopy category.