Documentation

Mathlib.CategoryTheory.Localization.LocallySmall

Locally small localizations #

In this file, given W : MorphismProperty C and a universe w, we show that there exists a term in HasLocalization.{w} W if and only if there exists (or for all) localization functors L : C ⥤ D for W, the category D is locally w-small.

source
@[instance_reducible]
noncomputable def CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₁} [Category.{v₂, u₁} D] [LocallySmall.{w, v₂, u₁} D] (L : Functor C D) [L.IsLocalization W] :
W.HasLocalization

If L : C ⥤ D is a localization functor for a class of morphisms W : MorphismProperty C, and D is locally w-small, we may obtain a HasLocalization.{w} W instance by shrinking the morphisms in D. (This version assumes that the types of objects of the categories C and D are in the same universe.)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall' {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] :
    W.HasLocalization

    If L : C ⥤ D is a localization functor for a class of morphisms W : MorphismProperty C, and D is locally w-small, we may obtain a HasLocalization.{w} W instance. This should be used only in the unlikely situation where the types of objects of C and D are in different universes. Otherwise, use hasLocalizationOfLocallySmall.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.MorphismProperty.locallySmall_of_hasLocalization {C : Type u₁} [Category.{v₁, u₁} C] (W : MorphismProperty C) {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [L.IsLocalization W] [W.HasLocalization] :
      LocallySmall.{w, v₂, u₂} D

      If a class of morphisms W : MorphismProperty C satisfies HasLocalization.{w} W, then any localized category for W (i.e. any target of a localization functor L : C ⥤ D for W) is locally w-small.