Localization of triangulated categories

Stream: homology

[Joël Riou]

As I had previously suggested, I have now obtained the localization theorem for triangulated categories in Lean/mathlib: if C is a triangulated category and W is a morphism_property C which satisfies certain conditions (left/right calculus of fractions, stability by shift, etc.), the localized category is also triangulated. In particular, if A is a triangulated subcategory of C, one may take for W the class of morphisms whose cone is in A. In order to do this, I had to develop further the localization of categories (e.g. show that the localized category is additive if C is additive and W satisfies some conditions, etc.). One of the results I have obtained is this:

triangulated.subcategory.left_orthogonal_bijective_L_map :
  ∀ {C : Type u_1} [_inst_1 : category C] [_inst_2 : has_zero_object C] [_inst_3 : has_shift C ℤ]
  [_inst_4 : preadditive C] [_inst_5 : ∀ (n : ℤ), (shift_functor C n).additive]
  [_inst_6 : triangulated.pretriangulated C] [_inst_7 : triangulated C]
  (A : triangulated.subcategory C) {D : Type u_3}
  [_inst_8 : category D] (L : C ⥤ D) [_inst_9 : L.is_localization A.W] (X Y : C),
    X ∈ A.left_orthogonal.set → function.bijective (λ (f : X ⟶ Y), L.map f)

If C is the category of complexes (up to homotopy) in an abelian category M, one may apply this to the triangulated subcategory consisting of exact complexes. Homology results in LTE should show that this is indeed a triangulated subcategory and the corresponding class W is the class of quasi-isomorphisms. Then, one may define the derived category of M as a triangulated category, and the lemma above would show that we can compute morphisms in the derived category from a "K-projective" complex into any complex, e.g. compute morphisms from a bounded above complex of projective objects as homotopy classes of morphisms of complexes. This would easily allow to redefine Ext groups as morphisms in the derived category and recover the previous definition in mathlib.

The code, which shall require some polishing... is at https://github.com/joelriou/homotopical_algebra.