Documentation

Mathlib.CategoryTheory.Localization.HasLocalization

Morphism properties equipped with a localized category

If C : Type u is a category (with [Category.{v} C]), and W : MorphismProperty C, then the constructed localized category W.Localization is in Type u (the objects are essentially the same as that of C), but the morphisms are in Type (max u v). In particular situations, it may happen that there is a localized category for W whose morphisms are in a lower universe like v: it shall be so for the homotopy categories of model categories (TODO), and it should also be so for the derived categories of Grothendieck abelian categories (TODO: but this shall be very technical).

Then, in order to allow the user to provide a localized category with specific universe parameters when it exists, we introduce a typeclass MorphismProperty.HasLocalization.{w} W which contains the data of a localized category D for W with D : Type u and [Category.{w} D]. Then, all definitions which involve "the" localized category for W should contain a [MorphismProperty.HasLocalization.{w} W] assumption for a suitable w. The functor W.Q' : C ⥤ W.Localization' shall be the localization functor for this fixed choice of the localized category. If the statement of a theorem does not involve the localized category, but the proof does, it is no longer necessary to use a HasLocalization assumption, but one may use HasLocalization.standard in the proof instead.

The data of a localized category with a given universe for the morphisms.

Instances
    theorem CategoryTheory.MorphismProperty.HasLocalization.hL {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} [self : W.HasLocalization] :
    CategoryTheory.MorphismProperty.HasLocalization.L.IsLocalization W

    The localized category for W : MorphismProperty C that is fixed by the [HasLocalization W] instance.

    Equations
    Instances For
      Equations
      • W.instCategoryLocalization' = CategoryTheory.MorphismProperty.HasLocalization.hD

      The localization functor C ⥤ W.Localization' that is fixed by the [HasLocalization W] instance.

      Equations
      • W.Q' = CategoryTheory.MorphismProperty.HasLocalization.L
      Instances For
        Equations
        • =