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.

class CategoryTheory.MorphismProperty.HasLocalization {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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 : CategoryTheory.Category.{w, u} (CategoryTheory.MorphismProperty.HasLocalization.D W)

  the category structure.

• L : CategoryTheory.Functor C (CategoryTheory.MorphismProperty.HasLocalization.D W)

  the localization functor.

• hL : CategoryTheory.MorphismProperty.HasLocalization.L.IsLocalization W

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

def CategoryTheory.MorphismProperty.Localization' {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasLocalization] : Type u

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

Equations

• W.Localization' = CategoryTheory.MorphismProperty.HasLocalization.D W

instance CategoryTheory.MorphismProperty.instCategoryLocalization' {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasLocalization] : CategoryTheory.Category.{w, u} W.Localization'

Equations

• W.instCategoryLocalization' = CategoryTheory.MorphismProperty.HasLocalization.hD

def CategoryTheory.MorphismProperty.Q' {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasLocalization] : CategoryTheory.Functor C W.Localization'

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

Equations

• W.Q' = CategoryTheory.MorphismProperty.HasLocalization.L

instance CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q' {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasLocalization] : W.Q'.IsLocalization W

Equations

• ⋯ = ⋯

def CategoryTheory.MorphismProperty.HasLocalization.standard {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) : W.HasLocalization

The constructed localized category.

Equations

• CategoryTheory.MorphismProperty.HasLocalization.standard W = CategoryTheory.MorphismProperty.HasLocalization.mk W.Q