Localization of categories

Stream: Is there code for X?

[Jack J Garzella]

Has there been any work done on localization of categories? Perhaps on "localizing classes" in additive categories, which are an ingredient if we want derived categories?

[Johan Commelin]

I think @Adam Topaz might have played a bit with this. But I don't know of any stable code.

[Adam Topaz]

Yeah I tried it out in some old branch...

[Adam Topaz]

One sec I'll find it

[Adam Topaz]

branch#cat_localization

[Adam Topaz]

But it's a general inductive construction which pays no attention to universes, so the universe level of the localization gets very large.

[Jack J Garzella]

What do you think it would take to get this into mathlib? Does it need to be redone with more attention to the universes?

[Adam Topaz]

Perhaps something along the lines of nlab#calculus+of+fractions

[Adam Topaz]

I think the inductive approach is good for theoretical reasons, but something like that nlab link is maybe more useful for actually working with the localization

[Scott Morrison]

Perhaps we want both: the inductive version for daily use, and then the calculus of fractions version when you need to know about universes (perhaps even just hiding this behind the src#category_theory.small_model API).

[Reid Barton]

The calculus of fractions version also bumps the morphism universe to the object universe. You need something like ((co)fibrant) approximations to control the universe level of the morphisms in the localization.

[Jack J Garzella]

Hmm, how important is this universe technicality? Could a "standard treatment" of the calculus of fractions find a place in mathlib?