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
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
    @[irreducible]
    noncomputable def CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall' {C : Type u_1} [Category.{u_2, u_1} C] (W : MorphismProperty C) {D : Type u_3} [Category.{u_4, u_3} D] [LocallySmall.{u_5, u_4, u_3} 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.hasLocalizationOfLocallySmall'_def {C : Type u_1} [Category.{u_2, u_1} C] (W : MorphismProperty C) {D : Type u_3} [Category.{u_4, u_3} D] [LocallySmall.{u_5, u_4, u_3} D] (L : Functor C D) [L.IsLocalization W] :
      W.hasLocalizationOfLocallySmall' L = have this := ⋯; let L' := { obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => L.map f, map_id := ⋯, map_comp := ⋯ }; have this_1 := ⋯; have this_2 := ⋯; have this_3 := ⋯; have e := (inducedFunctor L.obj).asEquivalence; have e' := L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor; have this_4 := ⋯; W.hasLocalizationOfLocallySmall L'
      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.