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.

source
class CategoryTheory.MorphismProperty.HasLocalization {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) :
Type (max (max (u + 1) v) (w + 1))

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

  • D : Type u

    the objects of the localized category.

  • hD : Category.{w, u} (D W)

    the category structure.

  • L : Functor C (D W)

    the localization functor.

  • hL : L.IsLocalization W
Instances
    source
    def CategoryTheory.MorphismProperty.Localization' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.HasLocalization] :
    Type u

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

    Equations
    Instances For
      source
      instance CategoryTheory.MorphismProperty.instCategoryLocalization' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.HasLocalization] :
      Category.{w, u} W.Localization'
      Equations
      source
      def CategoryTheory.MorphismProperty.Q' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.HasLocalization] :
      Functor C W.Localization'

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

      Equations
      Instances For
        source
        instance CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.HasLocalization] :
        W.Q'.IsLocalization W
        source
        def CategoryTheory.MorphismProperty.HasLocalization.standard {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) :
        W.HasLocalization

        The constructed localized category.

        Equations
        Instances For