Localization of categories

Stream: PR reviews

[Joël Riou]

In PR #14422, I construct the localized category, obtained by formally inverting a class of arrows W in a category C. The universal property of the localization if also obtained.

[Kevin Buzzard]

Don't they have the homotopy category associated to a category of complexes in LTE? Was this not defined as a localisation?

[Joël Riou]

I believe that what is in mathlib (and LTE) is the homotopy category K(A) of a (pre)additive category: it is a quotient category. The derived category D(A) is obtained from the category of complexes C(A) by formally inverting quasi-isomorphisms.

[Joël Riou]

In general, in a model category, what we call the "homotopy category" is obtained by formally inverting weak equivalences. It turns out to be equivalent to the quotient category of cofibrant and fibrant objects up to homotopy. (This is basically the fundamental lemma of homotopical algebra, which I have fully implemented in Lean recently.)
(For example, one may describe the "D^-" derived category of some abelian categories as the homotopy category of bounded below complexes of projective objects.)

[Joël Riou]

(In general, the homotopy category K(A) is not equivalent to the derived category D(A) because they may be quasi-isomorphisms which are not homotopy equivalences.)

[Johan Commelin]

@Joël Riou Cool!

[Johan Commelin]

cc @Reid Barton

[Adam Topaz]

Great! I can finally delete branch#cat_localization ;)
BTW, does this PR also introduce a characteristic predicate for the localization? I think that would be a fairly important construction to have!

[Joël Riou]

Adam Topaz said:

BTW, does this PR also introduce a characteristic predicate for the localization? I think that would be a fairly important construction to have!

Thanks! Of course, the predicate(s) will be in a separate PR as I did not want to make this one too long.