# Zulip Chat Archive

## Stream: homology

### Topic: Localization of triangulated categories

#### Joël Riou (Oct 07 2022 at 13:30):

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.

Last updated: Aug 03 2023 at 10:10 UTC