Zulip Chat Archive

Stream: PR reviews

Topic: Localization of categories


Joël Riou (May 28 2022 at 10:22):

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 (May 28 2022 at 10:38):

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 (May 28 2022 at 10:54):

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 (May 28 2022 at 10:58):

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 (May 28 2022 at 11:01):

(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 (May 28 2022 at 11:34):

@Joël Riou Cool!

Johan Commelin (May 28 2022 at 11:38):

cc @Reid Barton

Adam Topaz (May 28 2022 at 19:58):

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 (May 28 2022 at 20:48):

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.


Last updated: Dec 20 2023 at 11:08 UTC