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.

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

• W.hasLocalizationOfLocallySmall L = CategoryTheory.MorphismProperty.HasLocalization.mk (L.comp (CategoryTheory.ShrinkHoms.equivalence D).functor)

@[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.

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 = let_fun this := ⋯; let L' := { obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => L.map f, map_id := ⋯, map_comp := ⋯ }; let_fun this_1 := ⋯; let_fun this_2 := ⋯; let_fun this_3 := ⋯; let e := (inducedFunctor L.obj).asEquivalence; let e' := L'.associator e.functor e.inverse ≪≫ isoWhiskerLeft L' e.unitIso.symm ≪≫ L'.rightUnitor; let_fun this_4 := ⋯; W.hasLocalizationOfLocallySmall L'

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.